SMT2: simplify interface

This relieves the user of the dec_solve(assumption) interface from the need
to obtain a handle for the assumption.

The typing of the assumptions member is strengthened; instead of maintaining
the invariant that the expression stored is a literal_exprt, the vector now
stores literals directly.

src/solvers/smt2/smt2_conv.cpp

@@ -214,7 +214,7 @@ void smt2_convt::write_footer()
   {
     out << "(check-sat-assuming (";
     for(const auto &assumption : assumptions)
-      convert_literal(to_literal_expr(assumption).get_literal());
+      convert_literal(assumption);
     out << "))\n";
   }
   else
@@ -227,7 +227,7 @@ void smt2_convt::write_footer()
       for(const auto &assumption : assumptions)
       {
         out << "(assert ";
-        convert_literal(to_literal_expr(assumption).get_literal());
+        convert_literal(assumption);
         out << ")"
             << "\n";
       }
@@ -323,7 +323,7 @@ decision_proceduret::resultt smt2_convt::dec_solve(const exprt &assumption)
     write_footer();
   else
   {
-    assumptions.push_back(literal_exprt(convert(assumption)));
+    assumptions.push_back(convert(assumption));
     write_footer();
     assumptions.pop_back();
   }
@@ -987,7 +987,9 @@ void smt2_convt::push(const std::vector<exprt> &_assumptions)
 {
   INVARIANT(assumptions.empty(), "nested contexts are not supported");
 
-  assumptions = _assumptions;
+  assumptions.reserve(_assumptions.size());
+  for(auto &assumption : _assumptions)
+    assumptions.push_back(convert(assumption));
 }
 
 void smt2_convt::pop()

src/solvers/smt2/smt2_conv.h

@@ -101,7 +101,7 @@ class smt2_convt : public stack_decision_proceduret
     unordered_map<irep_idt, std::function<void(const exprt &)>, irep_id_hash>;
   converterst converters;
 
-  std::vector<exprt> assumptions;
+  std::vector<literalt> assumptions;
   boolbv_widtht boolbv_width;
 
   std::size_t number_of_solver_calls = 0;

src/solvers/smt2/smt2_dec.cpp

@@ -13,6 +13,8 @@ Author: Daniel Kroening, [email protected]
 #include <util/run.h>
 #include <util/tempfile.h>
 
+#include <solvers/prop/literal_expr.h>
+
 #include "smt2irep.h"
 
 std::string smt2_dect::decision_procedure_text() const
@@ -44,10 +46,20 @@ decision_proceduret::resultt smt2_dect::dec_solve(const exprt &assumption)
   const auto write_problem_to_file = [&](std::ofstream problem_out) {
     cached_output << stringstream.str();
     stringstream.str(std::string{});
-    write_footer();
+
+    if(assumption.is_nil())
+      write_footer();
+    else
+    {
+      assumptions.push_back(convert(assumption));
+      write_footer();
+      assumptions.pop_back();
+    }
+
     problem_out << cached_output.str() << stringstream.str();
     stringstream.str(std::string{});
   };
+
   write_problem_to_file(std::ofstream(
     temp_file_problem(), std::ios_base::out | std::ios_base::trunc));