new decision_proceduret API

This changes the API offered by decision_proceduret to solving under
assumptions.  Solving under assumptions has been popularised by MiniSat, and
is a state-less alternative to context stacks.

This change mimics the transition from check-sat to check-sat-assuming that
SMT-LIB is undergoing.

Author: kroening

src/solvers/decision_procedure.cpp

@@ -11,13 +11,21 @@ Author: Daniel Kroening, [email protected]
 
 #include "decision_procedure.h"
 
+#include <util/std_expr.h>
+
 decision_proceduret::~decision_proceduret()
 {
 }
 
 decision_proceduret::resultt decision_proceduret::operator()()
 {
-  return dec_solve();
+  return dec_solve(nil_exprt());
+}
+
+decision_proceduret::resultt
+decision_proceduret::operator()(const exprt &assumption)
+{
+  return dec_solve(assumption);
 }
 
 void decision_proceduret::set_to_true(const exprt &expr)

src/solvers/decision_procedure.h

@@ -17,18 +17,19 @@ Author: Daniel Kroening, [email protected]
 
 class exprt;
 
+/// An interface for a decision procedure for satisfiability problems.
 class decision_proceduret
 {
 public:
   /// For a Boolean expression \p expr, add the constraint 'expr' if \p value
   /// is `true`, otherwise add 'not expr'
-  virtual void set_to(const exprt &expr, bool value) = 0;
+  virtual void set_to(const exprt &, bool value) = 0;
 
   /// For a Boolean expression \p expr, add the constraint 'expr'
-  void set_to_true(const exprt &expr);
+  void set_to_true(const exprt &);
 
   /// For a Boolean expression \p expr, add the constraint 'not expr'
-  void set_to_false(const exprt &expr);
+  void set_to_false(const exprt &);
 
   /// Generate a handle, which is an expression that
   /// has the same value as the argument in any model
@@ -37,7 +38,7 @@ class decision_proceduret
   /// \ref set_to.
   /// The returned expression may be the expression itself or a more compact
   /// but solver-specific representation.
-  virtual exprt handle(const exprt &expr) = 0;
+  virtual exprt handle(const exprt &) = 0;
 
   /// Result of running the decision procedure
   enum class resultt
@@ -48,12 +49,18 @@ class decision_proceduret
   };
 
   /// Run the decision procedure to solve the problem
+  /// This corresponds to SMT-LIB's check-sat.
   resultt operator()();
 
+  /// Run the decision procedure to solve the problem under
+  /// the given assumption.
+  /// This corresponds to SMT-LIB's check-sat-assuming.
+  resultt operator()(const exprt &assumption);
+
   /// Return \p expr with variables replaced by values from satisfying
   /// assignment if available.
   /// Return `nil` if not available
-  virtual exprt get(const exprt &expr) const = 0;
+  virtual exprt get(const exprt &) const = 0;
 
   /// Print satisfying assignment to \p out
   virtual void print_assignment(std::ostream &out) const = 0;
@@ -67,8 +74,8 @@ class decision_proceduret
   virtual ~decision_proceduret();
 
 protected:
-  /// Run the decision procedure to solve the problem
-  virtual resultt dec_solve() = 0;
+  /// Implementation of the decision procedure.
+  virtual resultt dec_solve(const exprt &assumption) = 0;
 };
 
 /// Add Boolean constraint \p src to decision procedure \p dest

src/solvers/prop/prop_conv_solver.cpp

@@ -439,7 +439,8 @@ void prop_conv_solvert::finish_eager_conversion()
 {
 }
 
-decision_proceduret::resultt prop_conv_solvert::dec_solve()
+decision_proceduret::resultt
+prop_conv_solvert::dec_solve(const exprt &assumption)
 {
   // post-processing isn't incremental yet
   if(!post_processing_done)
@@ -459,7 +460,16 @@ decision_proceduret::resultt prop_conv_solvert::dec_solve()
 
   log.statistics() << "Solving with " << prop.solver_text() << messaget::eom;
 
-  switch(prop.prop_solve(assumption_stack))
+  if(assumption.is_nil())
+    push();
+  else
+    push({literal_exprt(convert(assumption))});
+
+  auto prop_result = prop.prop_solve(assumption_stack);
+
+  pop();
+
+  switch(prop_result)
   {
   case propt::resultt::P_SATISFIABLE:
     return resultt::D_SATISFIABLE;

src/solvers/prop/prop_conv_solver.h

@@ -40,7 +40,7 @@ class prop_conv_solvert : public conflict_providert,
   virtual void finish_eager_conversion();
 
   // overloading from decision_proceduret
-  decision_proceduret::resultt dec_solve() override;
+  decision_proceduret::resultt dec_solve(const exprt &) override;
   void print_assignment(std::ostream &out) const override;
   std::string decision_procedure_text() const override;
   exprt get(const exprt &expr) const override;

src/solvers/refinement/bv_refinement.h

@@ -39,7 +39,7 @@ class bv_refinementt:public bv_pointerst
 
   explicit bv_refinementt(const infot &info);
 
-  decision_proceduret::resultt dec_solve() override;
+  decision_proceduret::resultt dec_solve(const exprt &) override;
 
   std::string decision_procedure_text() const override
   {

src/solvers/refinement/bv_refinement_loop.cpp

@@ -21,7 +21,7 @@ bv_refinementt::bv_refinementt(const infot &info)
   PRECONDITION(prop.has_is_in_conflict());
 }
 
-decision_proceduret::resultt bv_refinementt::dec_solve()
+decision_proceduret::resultt bv_refinementt::dec_solve(const exprt &assumption)
 {
   // do the usual post-processing
   log.status() << "BV-Refinement: post-processing" << messaget::eom;

src/solvers/smt2/smt2_conv.cpp

@@ -317,9 +317,17 @@ void smt2_convt::define_object_size(
   }
 }
 
-decision_proceduret::resultt smt2_convt::dec_solve()
+decision_proceduret::resultt smt2_convt::dec_solve(const exprt &assumption)
 {
-  write_footer();
+  if(assumption.is_nil())
+    write_footer();
+  else
+  {
+    assumptions.push_back(literal_exprt(convert(assumption)));
+    write_footer();
+    assumptions.pop_back();
+  }
+
   out.flush();
   return decision_proceduret::resultt::D_ERROR;
 }

src/solvers/smt2/smt2_conv.h

@@ -106,7 +106,7 @@ class smt2_convt : public stack_decision_proceduret
 
   std::size_t number_of_solver_calls = 0;
 
-  resultt dec_solve() override;
+  resultt dec_solve(const exprt &) override;
 
   void write_header();
   /// Writes the end of the SMT file to the `smt_convt::out` stream. These parts

src/solvers/smt2/smt2_dec.cpp

@@ -33,7 +33,7 @@ std::string smt2_dect::decision_procedure_text() const
   // clang-format on
 }
 
-decision_proceduret::resultt smt2_dect::dec_solve()
+decision_proceduret::resultt smt2_dect::dec_solve(const exprt &assumption)
 {
   ++number_of_solver_calls;
 

src/solvers/smt2/smt2_dec.h

@@ -39,11 +39,11 @@ class smt2_dect : protected smt2_stringstreamt, public smt2_convt
   {
   }
 
-  resultt dec_solve() override;
   std::string decision_procedure_text() const override;
 
 protected:
   message_handlert &message_handler;
+  resultt dec_solve(const exprt &) override;
 
   /// Everything except the footer is cached, so that output files can be
   /// rewritten with varying footers.

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -690,7 +690,8 @@ exprt smt2_incremental_decision_proceduret::lower(exprt expression) const
   return lowered;
 }
 
-decision_proceduret::resultt smt2_incremental_decision_proceduret::dec_solve()
+decision_proceduret::resultt
+smt2_incremental_decision_proceduret::dec_solve(const exprt &assumption)
 {
   ++number_of_solver_calls;
   define_object_properties();

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h

@@ -64,7 +64,7 @@ class smt2_incremental_decision_proceduret final
 
 protected:
   // Implementation of protected decision_proceduret member function.
-  resultt dec_solve() override;
+  resultt dec_solve(const exprt &) override;
   /// \brief Defines a function of array sort and asserts the element values
   /// from `array_exprt` or `array_of_exprt`.
   /// \details

src/solvers/strings/string_refinement.cpp

@@ -603,7 +603,8 @@ output_equations(std::ostream &output, const std::vector<exprt> &equations)
 /// \return `resultt::D_SATISFIABLE` if the constraints are satisfiable,
 ///   `resultt::D_UNSATISFIABLE` if they are unsatisfiable,
 ///   `resultt::D_ERROR` if the limit of iteration was reached.
-decision_proceduret::resultt string_refinementt::dec_solve()
+decision_proceduret::resultt
+string_refinementt::dec_solve(const exprt &assumption)
 {
 #ifdef DEBUG
   log.debug() << "dec_solve: Initial set of equations" << messaget::eom;
@@ -781,7 +782,8 @@ decision_proceduret::resultt string_refinementt::dec_solve()
   // Initial try without index set
   const auto get = [this](const exprt &expr) { return this->get(expr); };
   dependencies.clean_cache();
-  const decision_proceduret::resultt initial_result = supert::dec_solve();
+  const decision_proceduret::resultt initial_result =
+    supert::dec_solve(nil_exprt());
   if(initial_result == resultt::D_SATISFIABLE)
   {
     bool satisfied;
@@ -822,7 +824,8 @@ decision_proceduret::resultt string_refinementt::dec_solve()
   while((loop_bound_--) > 0)
   {
     dependencies.clean_cache();
-    const decision_proceduret::resultt refined_result = supert::dec_solve();
+    const decision_proceduret::resultt refined_result =
+      supert::dec_solve(nil_exprt());
 
     if(refined_result == resultt::D_SATISFIABLE)
     {

src/solvers/strings/string_refinement.h

@@ -84,7 +84,9 @@ class string_refinementt final : public bv_refinementt
 
   exprt get(const exprt &expr) const override;
   void set_to(const exprt &expr, bool value) override;
-  decision_proceduret::resultt dec_solve() override;
+
+protected:
+  decision_proceduret::resultt dec_solve(const exprt &) override;
 
 private:
   // Base class

unit/Makefile

@@ -96,6 +96,7 @@ SRC += analyses/ai/ai.cpp \
        path_strategies.cpp \
        pointer-analysis/value_set.cpp \
        solvers/bdd/miniBDD/miniBDD.cpp \
+       solvers/flattening/boolbv.cpp \
        solvers/floatbv/float_utils.cpp \
        solvers/prop/bdd_expr.cpp \
        solvers/sat/external_sat.cpp \

unit/solvers/flattening/boolbv.cpp

@@ -0,0 +1,50 @@
+/*******************************************************************\
+
+Module: Unit tests for boolbvt
+
+Author: Daniel Kroening
+
+\*******************************************************************/
+
+/// \file
+/// Unit tests for boolbvt
+
+#include <util/arith_tools.h>
+#include <util/bitvector_types.h>
+#include <util/cout_message.h>
+#include <util/namespace.h>
+#include <util/std_expr.h>
+#include <util/symbol_table.h>
+
+#include <solvers/flattening/boolbv.h>
+#include <solvers/sat/satcheck.h>
+#include <testing-utils/use_catch.h>
+
+SCENARIO("boolbvt", "[core][solvers][flattening][boolbvt]")
+{
+  console_message_handlert message_handler;
+  message_handler.set_verbosity(0);
+
+  GIVEN("A satisfiable bit-vector formula f")
+  {
+    satcheckt satcheck(message_handler);
+    symbol_tablet symbol_table;
+    namespacet ns(symbol_table);
+    boolbvt boolbv(ns, satcheck, message_handler);
+
+    unsignedbv_typet u32(32);
+    boolbv << equal_exprt(symbol_exprt("x", u32), from_integer(10, u32));
+
+    THEN("is indeed satisfiable")
+    {
+      REQUIRE(boolbv() == decision_proceduret::resultt::D_SATISFIABLE);
+    }
+    THEN("is unsatisfiable under an inconsistent assumption")
+    {
+      auto assumption =
+        equal_exprt(symbol_exprt("x", u32), from_integer(11, u32));
+      REQUIRE(
+        boolbv(assumption) == decision_proceduret::resultt::D_UNSATISFIABLE);
+    }
+  }
+}

unit/solvers/flattening/module_dependencies.txt

@@ -0,0 +1,3 @@
+solvers/sat
+testing-utils
+util

unit/solvers/strings/string_refinement/string_refinement.cpp

@@ -100,7 +100,7 @@ SCENARIO("string refinement", "[core][solvers][strings][string_refinement]")
       solver.set_to(
         equal_exprt{return_length, from_integer(15, int_type)}, true);
 
-      auto result = solver.dec_solve();
+      auto result = solver();
       THEN("The formula is satisfiable")
       {
         REQUIRE(result == decision_proceduret::resultt::D_SATISFIABLE);
@@ -136,7 +136,7 @@ SCENARIO("string refinement", "[core][solvers][strings][string_refinement]")
         "The formula is satisfiable and the model of the array should have"
         "length 10 and end with 'b'")
       {
-        auto result = solver.dec_solve();
+        auto result = solver();
         REQUIRE(result == decision_proceduret::resultt::D_SATISFIABLE);
         const exprt array_model = solver.get(array1);
         REQUIRE(can_cast_expr<array_exprt>(array_model));
@@ -183,7 +183,7 @@ SCENARIO("string refinement", "[core][solvers][strings][string_refinement]")
         "The model for array1 has length 10 and contains 'c' at "
         " position 3 and b at position 9")
       {
-        auto result = solver.dec_solve();
+        auto result = solver();
         REQUIRE(result == decision_proceduret::resultt::D_SATISFIABLE);
         const exprt array_model = solver.get(array1);
         REQUIRE(can_cast_expr<array_exprt>(array_model));
@@ -230,7 +230,7 @@ SCENARIO("string refinement", "[core][solvers][strings][string_refinement]")
         true);
       THEN("The model for array1 has length 10 and contains 'c' at position 9")
       {
-        auto result = solver.dec_solve();
+        auto result = solver();
         REQUIRE(result == decision_proceduret::resultt::D_SATISFIABLE);
         const exprt array_model = solver.get(array1);
         REQUIRE(can_cast_expr<array_exprt>(array_model));