Skip to content

Commit 3c7bab8

Browse files
Rename class to smt2_symbol_exprt
This reflects the inheritance from exprt and will avoid collision with a type that will be introduced for smt2 ASTs.
1 parent d9a5113 commit 3c7bab8

File tree

2 files changed

+8
-7
lines changed

2 files changed

+8
-7
lines changed

src/solvers/smt2/smt2_conv.cpp

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1893,7 +1893,8 @@ void smt2_convt::convert_expr(const exprt &expr)
18931893
// width must be multiple of bytes
18941894
DATA_INVARIANT(
18951895
width % bits_per_byte == 0,
1896-
"bit width indicated by type of bswap expression should be a multiple "
1896+
"bit width indicated by type of bswap expression should "
1897+
"be a multiple "
18971898
"of the number of bits per byte");
18981899

18991900
const std::size_t bytes = width / bits_per_byte;
@@ -4461,8 +4462,8 @@ void smt2_convt::find_symbols(const exprt &expr)
44614462

44624463
exprt tmp1=expr;
44634464
for(std::size_t i = 0; i < tmp1.operands().size(); i++)
4464-
tmp1.operands()[i]=
4465-
smt2_symbolt("op"+std::to_string(i), tmp1.operands()[i].type());
4465+
tmp1.operands()[i] = smt2_symbol_exprt(
4466+
"op" + std::to_string(i), tmp1.operands()[i].type());
44664467

44674468
exprt tmp2=float_bv(tmp1);
44684469
tmp2=letify(tmp2);

src/solvers/smt2/smt2_conv.h

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -154,10 +154,10 @@ class smt2_convt : public stack_decision_proceduret
154154
std::string floatbv_suffix(const exprt &) const;
155155
std::set<irep_idt> bvfp_set; // already converted
156156

157-
class smt2_symbolt : public nullary_exprt
157+
class smt2_symbol_exprt : public nullary_exprt
158158
{
159159
public:
160-
smt2_symbolt(const irep_idt &_identifier, const typet &_type)
160+
smt2_symbol_exprt(const irep_idt &_identifier, const typet &_type)
161161
: nullary_exprt(ID_smt2_symbol, _type)
162162
{ set(ID_identifier, _identifier); }
163163

@@ -167,10 +167,10 @@ class smt2_convt : public stack_decision_proceduret
167167
}
168168
};
169169

170-
const smt2_symbolt &to_smt2_symbol(const exprt &expr)
170+
const smt2_symbol_exprt &to_smt2_symbol(const exprt &expr)
171171
{
172172
assert(expr.id()==ID_smt2_symbol && !expr.has_operands());
173-
return static_cast<const smt2_symbolt&>(expr);
173+
return static_cast<const smt2_symbol_exprt &>(expr);
174174
}
175175

176176
// flattens any non-bitvector type into a bitvector,

0 commit comments

Comments
 (0)