From 09718c32ae26935b01fca87d8d7e61919be90b85 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Tue, 19 Dec 2023 02:23:55 -0800
Subject: [PATCH] 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 | 10 ++++++----
 src/solvers/smt2/smt2_conv.h   |  2 +-
 src/solvers/smt2/smt2_dec.cpp  | 14 +++++++++++++-
 3 files changed, 20 insertions(+), 6 deletions(-)

diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index 5b7ab53c4ea5..a925580e80e5 100644
--- 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
index 9f83687f8be9..8d1353262743 100644
--- a/src/solvers/smt2/smt2_conv.h
+++ b/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;
diff --git a/src/solvers/smt2/smt2_dec.cpp b/src/solvers/smt2/smt2_dec.cpp
index 55528f80ce77..89532a41e877 100644
--- a/src/solvers/smt2/smt2_dec.cpp
+++ b/src/solvers/smt2/smt2_dec.cpp
@@ -13,6 +13,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #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));