Clean up smt2_conv

src/solvers/smt2/smt2_conv.cpp

@@ -42,6 +42,70 @@ Author: Daniel Kroening, [email protected]
 // General todos
 #define SMT2_TODO(S) PRECONDITION_WITH_DIAGNOSTICS(false, "TODO: " S)
 
+smt2_convt::smt2_convt(
+  const namespacet &_ns,
+  const std::string &_benchmark,
+  const std::string &_notes,
+  const std::string &_logic,
+  solvert _solver,
+  std::ostream &_out)
+  : use_FPA_theory(false),
+    use_datatypes(false),
+    use_array_of_bool(false),
+    emit_set_logic(true),
+    ns(_ns),
+    out(_out),
+    benchmark(_benchmark),
+    notes(_notes),
+    logic(_logic),
+    solver(_solver),
+    boolbv_width(_ns),
+    pointer_logic(_ns),
+    no_boolean_variables(0)
+{
+  // We set some defaults differently
+  // for some solvers.
+
+  switch(solver)
+  {
+  case solvert::GENERIC:
+    break;
+
+  case solvert::BOOLECTOR:
+    break;
+
+  case solvert::CPROVER_SMT2:
+    use_array_of_bool = true;
+    emit_set_logic = false;
+    break;
+
+  case solvert::CVC3:
+    break;
+
+  case solvert::CVC4:
+    break;
+
+  case solvert::MATHSAT:
+    break;
+
+  case solvert::YICES:
+    break;
+
+  case solvert::Z3:
+    use_array_of_bool = true;
+    emit_set_logic = false;
+    use_datatypes = true;
+    break;
+  }
+
+  write_header();
+}
+
+std::string smt2_convt::decision_procedure_text() const
+{
+  return "SMT2";
+}
+
 void smt2_convt::print_assignment(std::ostream &os) const
 {
   // Boolean stuff

src/solvers/smt2/smt2_conv.h

@@ -31,7 +31,7 @@ class constant_exprt;
 class index_exprt;
 class member_exprt;
 
-class smt2_convt:public prop_convt
+class smt2_convt : public stack_decision_proceduret
 {
 public:
   enum class solvert
@@ -52,77 +52,20 @@ class smt2_convt:public prop_convt
     const std::string &_notes,
     const std::string &_logic,
     solvert _solver,
-    std::ostream &_out)
-    : use_FPA_theory(false),
-      use_datatypes(false),
-      use_array_of_bool(false),
-      emit_set_logic(true),
-      ns(_ns),
-      out(_out),
-      benchmark(_benchmark),
-      notes(_notes),
-      logic(_logic),
-      solver(_solver),
-      boolbv_width(_ns),
-      pointer_logic(_ns),
-      no_boolean_variables(0)
-  {
-    // We set some defaults differently
-    // for some solvers.
-
-    switch(solver)
-    {
-    case solvert::GENERIC:
-      break;
-
-    case solvert::BOOLECTOR:
-      break;
-
-    case solvert::CPROVER_SMT2:
-      use_array_of_bool = true;
-      emit_set_logic = false;
-      break;
-
-    case solvert::CVC3:
-      break;
-
-    case solvert::CVC4:
-      break;
-
-    case solvert::MATHSAT:
-      break;
-
-    case solvert::YICES:
-      break;
-
-    case solvert::Z3:
-      use_array_of_bool=true;
-      emit_set_logic=false;
-      use_datatypes=true;
-      break;
-    }
-
-    write_header();
-  }
+    std::ostream &_out);
 
   ~smt2_convt() override = default;
-  resultt dec_solve() override;
 
   bool use_FPA_theory;
   bool use_datatypes;
   bool use_array_of_bool;
   bool emit_set_logic;
 
   exprt handle(const exprt &expr) override;
-  literalt convert(const exprt &expr) override;
   void set_to(const exprt &expr, bool value) override;
   exprt get(const exprt &expr) const override;
-  std::string decision_procedure_text() const override
-  {
-    return "SMT2";
-  }
+  std::string decision_procedure_text() const override;
   void print_assignment(std::ostream &out) const override;
-  tvt l_get(literalt l) const override;
 
   /// Unimplemented
   void push() override;
@@ -133,10 +76,6 @@ class smt2_convt:public prop_convt
   /// Currently, only implements a single stack element (no nested contexts)
   void pop() override;
 
-  void convert_expr(const exprt &);
-  void convert_type(const typet &);
-  void convert_literal(const literalt);
-
   std::size_t get_number_of_solver_calls() const override;
 
 protected:
@@ -150,6 +89,8 @@ class smt2_convt:public prop_convt
 
   std::size_t number_of_solver_calls = 0;
 
+  resultt dec_solve() override;
+
   void write_header();
   void write_footer(std::ostream &);
 
@@ -183,6 +124,13 @@ class smt2_convt:public prop_convt
 
   std::string convert_identifier(const irep_idt &identifier);
 
+  void convert_expr(const exprt &);
+  void convert_type(const typet &);
+  void convert_literal(const literalt);
+
+  literalt convert(const exprt &expr);
+  tvt l_get(literalt l) const;
+
   // auxiliary methods
   exprt prepare_for_convert_expr(const exprt &expr);
   exprt lower_byte_operators(const exprt &expr);