SMT2 backend: use check-sat-assuming, when available

Instead of assing the assumptions as (hard) constraints, use the SMT-LIB
command check-sat-assuming, which has been designed for this particular
use-case.

Author: kroening

src/solvers/smt2/smt2_conv.cpp

@@ -54,9 +54,10 @@ smt2_convt::smt2_convt(
   solvert _solver,
   std::ostream &_out)
   : use_FPA_theory(false),
+    use_array_of_bool(false),
     use_as_const(false),
+    use_check_sat_assuming(false),
     use_datatypes(false),
-    use_array_of_bool(false),
     use_lambda_for_array(false),
     emit_set_logic(true),
     ns(_ns),
@@ -81,8 +82,9 @@ smt2_convt::smt2_convt(
     break;
 
   case solvert::CPROVER_SMT2:
-    use_as_const = true;
     use_array_of_bool = true;
+    use_as_const = true;
+    use_check_sat_assuming = true;
     emit_set_logic = false;
     break;
 
@@ -100,8 +102,9 @@ smt2_convt::smt2_convt(
     break;
 
   case solvert::Z3:
-    use_as_const = true;
     use_array_of_bool = true;
+    use_as_const = true;
+    use_check_sat_assuming = true;
     use_lambda_for_array = true;
     emit_set_logic = false;
     use_datatypes = true;
@@ -173,26 +176,36 @@ void smt2_convt::write_footer(std::ostream &os)
 {
   os << "\n";
 
-  // add the assumptions, if any
-  if(!assumptions.empty())
-  {
-    os << "; assumptions\n";
+  // fix up the object sizes
+  for(const auto &object : object_sizes)
+    define_object_size(object.second, object.first);
 
+  if(use_check_sat_assuming && !assumptions.empty())
+  {
+    os << "(check-sat-assuming (";
     for(const auto &assumption : assumptions)
-    {
-      os << "(assert ";
       convert_literal(to_literal_expr(assumption).get_literal());
-      os << ")"
-         << "\n";
-    }
+    os << "))\n";
   }
+  else
+  {
+    // add the assumptions, if any
+    if(!assumptions.empty())
+    {
+      os << "; assumptions\n";
 
-  // fix up the object sizes
-  for(const auto &object : object_sizes)
-    define_object_size(object.second, object.first);
+      for(const auto &assumption : assumptions)
+      {
+        os << "(assert ";
+        convert_literal(to_literal_expr(assumption).get_literal());
+        os << ")"
+           << "\n";
+      }
+    }
+
+    os << "(check-sat)\n";
+  }
 
-  os << "(check-sat)"
-     << "\n";
   os << "\n";
 
   if(solver!=solvert::BOOLECTOR)

src/solvers/smt2/smt2_conv.h

@@ -59,9 +59,10 @@ class smt2_convt : public stack_decision_proceduret
   ~smt2_convt() override = default;
 
   bool use_FPA_theory;
+  bool use_array_of_bool;
   bool use_as_const;
+  bool use_check_sat_assuming;
   bool use_datatypes;
-  bool use_array_of_bool;
   bool use_lambda_for_array;
   bool emit_set_logic;