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())
+  if(assumption.is_nil())
+    push();
+  else
+    push({literal_exprt(convert(assumption))});
+
+  auto prop_result = prop.prop_solve();
+
+  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.