Implement context-based solver on top of prop_conv_solvert

Also allows using raw assumptions within contexts
(as required by minimization and refinement algorithms).

Author: peterschrammel

src/solvers/prop/prop_conv_solver.cpp

@@ -331,7 +331,7 @@ bool prop_conv_solvert::set_equality_to_true(const equal_exprt &expr)
   return true;
 }
 
-void prop_conv_solvert::set_to(const exprt &expr, bool value)
+void prop_conv_solvert::do_set_to(const exprt &expr, bool value)
 {
   PRECONDITION(expr.type().id() == ID_bool);
 
@@ -346,7 +346,7 @@ void prop_conv_solvert::set_to(const exprt &expr, bool value)
     {
       if(expr.operands().size() == 1)
       {
-        set_to(expr.op0(), !value);
+        do_set_to(expr.op0(), !value);
         return;
       }
     }
@@ -359,7 +359,7 @@ void prop_conv_solvert::set_to(const exprt &expr, bool value)
         if(expr.id() == ID_and)
         {
           forall_operands(it, expr)
-            set_to_true(*it);
+            do_set_to(*it, true);
 
           return;
         }
@@ -403,14 +403,14 @@ void prop_conv_solvert::set_to(const exprt &expr, bool value)
         {
           const implies_exprt &implies_expr = to_implies_expr(expr);
 
-          set_to_true(implies_expr.op0());
-          set_to_false(implies_expr.op1());
+          do_set_to(implies_expr.op0(), true);
+          do_set_to(implies_expr.op1(), false);
           return;
         }
         else if(expr.id() == ID_or) // !(a || b)  ==  (!a && !b)
         {
           forall_operands(it, expr)
-            set_to_false(*it);
+            do_set_to(*it, false);
           return;
         }
       }
@@ -493,3 +493,51 @@ std::size_t prop_conv_solvert::get_number_of_solver_calls() const
 {
   return prop.get_number_of_solver_calls();
 }
+
+const char *prop_conv_solvert::context_prefix = "prop_conv::context$";
+
+void prop_conv_solvert::set_to(const exprt &expr, bool value)
+{
+  if(context_literals.empty())
+  {
+    // We are in the root context.
+    do_set_to(expr, value);
+  }
+  else
+  {
+    // We have a child context. We add context_literal ==> expr to the formula.
+    do_set_to(or_exprt(literal_exprt(!context_literals.back()), expr), value);
+  }
+}
+
+void prop_conv_solvert::set_assumptions(const bvt &assumptions)
+{
+  bvt combined_assumptions;
+  combined_assumptions.reserve(context_literals.size() + assumptions.size());
+  combined_assumptions.insert(
+    combined_assumptions.end(),
+    context_literals.begin(),
+    context_literals.end());
+  combined_assumptions.insert(
+    combined_assumptions.end(), assumptions.begin(), assumptions.end());
+  prop.set_assumptions(combined_assumptions);
+}
+
+void prop_conv_solvert::push_context()
+{
+  // We create a new context literal.
+  literalt context_literal = prop_conv_solvert::convert(symbol_exprt(
+    context_prefix + std::to_string(context_literal_counter++), bool_typet()));
+
+  context_literals.push_back(context_literal);
+  prop.set_assumptions(context_literals);
+}
+
+void prop_conv_solvert::pop_context()
+{
+  PRECONDITION(!context_literals.empty());
+
+  // We remove the last context literal from the stack.
+  context_literals.pop_back();
+  prop.set_assumptions(context_literals);
+}

src/solvers/prop/prop_conv_solver.h

@@ -16,14 +16,14 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/message.h>
 #include <util/std_expr.h>
 
-#include "decision_procedure_assumptions.h"
+#include "decision_procedure_contexts.h"
 #include "literal.h"
 #include "literal_expr.h"
 #include "prop.h"
 #include "solver_conflicts.h"
 #include "solver_resource_limits.h"
 
-class prop_conv_solvert : public decision_procedure_assumptionst,
+class prop_conv_solvert : public decision_procedure_contextst,
                           public solver_conflictst,
                           public solver_resource_limitst
 {
@@ -36,7 +36,6 @@ class prop_conv_solvert : public decision_procedure_assumptionst,
   virtual ~prop_conv_solvert() = default;
 
   // overloading from decision_proceduret
-  void set_to(const exprt &expr, bool value) override;
   decision_proceduret::resultt dec_solve() override;
   void print_assignment(std::ostream &out) const override;
   std::string decision_procedure_text() const override
@@ -55,10 +54,7 @@ class prop_conv_solvert : public decision_procedure_assumptionst,
   {
     prop.set_frozen(a);
   }
-  void set_assumptions(const bvt &_assumptions) override
-  {
-    prop.set_assumptions(_assumptions);
-  }
+
   void set_all_frozen() override
   {
     freeze_all = true;
@@ -69,6 +65,26 @@ class prop_conv_solvert : public decision_procedure_assumptionst,
     return prop.is_in_conflict(l);
   }
 
+  /// For a Boolean expression \p expr, add the constraint
+  /// 'current_context => expr' if \p value is `true`,
+  /// otherwise add 'current_context => not expr'
+  void set_to(const exprt &expr, bool value) override;
+
+  /// Set \p assumptions within current context.
+  /// These assumptions can be removed by passing empty \p assumptions.
+  /// These assumptions will also be dropped in the course of any context
+  /// operation (`push_context` or `pop_context`).
+  void set_assumptions(const bvt &assumptions) override;
+
+  /// Push a new context on the stack
+  /// This context becomes a child context nested in the current context.
+  void push_context() override;
+
+  /// Pop the current context
+  void pop_context() override;
+
+  static const char *context_prefix;
+
   // get literal for expression, if available
   bool literal(const symbol_exprt &expr, literalt &literal) const;
 
@@ -123,10 +139,18 @@ class prop_conv_solvert : public decision_procedure_assumptionst,
 
   virtual void ignoring(const exprt &expr);
 
-  // deliberately protected now to protect lower-level API
+  /// Actually adds the constraints to `prop`
+  void do_set_to(const exprt &expr, bool value);
+
   propt &prop;
 
   messaget log;
+
+  /// Context literals used as assumptions
+  bvt context_literals;
+
+  /// Unique context literal names
+  std::size_t context_literal_counter = 0;
 };
 
 #endif // CPROVER_SOLVERS_PROP_PROP_CONV_SOLVER_H