Merge pull request #8123 from diffblue/smt2-assumptions

SMT2: simplify interface
diffblue · Feb 7, 2024 · 547b1a8 · 547b1a8
2 parents 3dcf5f9 + d656764
commit 547b1a8
Show file tree

Hide file tree

Showing 3 changed files with 16 additions and 5 deletions.
diff --git a/src/solvers/smt2/smt2_conv.cpp b/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()

diff --git a/src/solvers/smt2/smt2_conv.h b/src/solvers/smt2/smt2_conv.h
@@ -102,7 +102,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;

diff --git a/src/solvers/smt2/smt2_dec.cpp b/src/solvers/smt2/smt2_dec.cpp
@@ -42,12 +42,21 @@ decision_proceduret::resultt smt2_dect::dec_solve(const exprt &assumption)
     temp_file_stderr("smt2_dec_stderr_", "");
 
   const auto write_problem_to_file = [&](std::ofstream problem_out) {
+    if(assumption.is_not_nil())
+      assumptions.push_back(convert(assumption));
+
     cached_output << stringstream.str();
     stringstream.str(std::string{});
+
     write_footer();
+
+    if(assumption.is_not_nil())
+      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));