Skip to content

Commit de2202a

Browse files
Make smt2_convt inherit from stack_decision_proceduret directly
1 parent cb2f5ea commit de2202a

File tree

1 file changed

+4
-3
lines changed

1 file changed

+4
-3
lines changed

src/solvers/smt2/smt2_conv.h

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,7 @@ class constant_exprt;
3131
class index_exprt;
3232
class member_exprt;
3333

34-
class smt2_convt:public prop_convt
34+
class smt2_convt : public stack_decision_proceduret
3535
{
3636
public:
3737
enum class solvert
@@ -114,15 +114,13 @@ class smt2_convt:public prop_convt
114114
bool emit_set_logic;
115115

116116
exprt handle(const exprt &expr) override;
117-
literalt convert(const exprt &expr) override;
118117
void set_to(const exprt &expr, bool value) override;
119118
exprt get(const exprt &expr) const override;
120119
std::string decision_procedure_text() const override
121120
{
122121
return "SMT2";
123122
}
124123
void print_assignment(std::ostream &out) const override;
125-
tvt l_get(literalt l) const override;
126124

127125
/// Unimplemented
128126
void push() override;
@@ -183,6 +181,9 @@ class smt2_convt:public prop_convt
183181

184182
std::string convert_identifier(const irep_idt &identifier);
185183

184+
literalt convert(const exprt &expr);
185+
tvt l_get(literalt l) const;
186+
186187
// auxiliary methods
187188
exprt prepare_for_convert_expr(const exprt &expr);
188189
exprt lower_byte_operators(const exprt &expr);

0 commit comments

Comments
 (0)