Merge pull request #4581 from peterschrammel/stack-decision-procedure

stack_decision_proceduret for solving under assumptions/contexts

Author: peterschrammel

src/goto-checker/goto_symex_fault_localizer.cpp

@@ -11,13 +11,11 @@ Author: Peter Schrammel
 
 #include "goto_symex_fault_localizer.h"
 
-#include <solvers/prop/prop_conv.h>
-
 goto_symex_fault_localizert::goto_symex_fault_localizert(
   const optionst &options,
   ui_message_handlert &ui_message_handler,
   const symex_target_equationt &equation,
-  prop_convt &solver)
+  stack_decision_proceduret &solver)
   : options(options),
     ui_message_handler(ui_message_handler),
     equation(equation),
@@ -58,7 +56,7 @@ const SSA_stept &goto_symex_fault_localizert::collect_guards(
       step.assignment_type == symex_targett::assignment_typet::STATE &&
       !step.ignore)
     {
-      literalt l = solver.convert(step.guard_handle);
+      exprt l = solver.handle(step.guard_handle);
       if(!l.is_constant())
       {
         auto emplace_result = fault_location.scores.emplace(step.source.pc, 0);
@@ -79,21 +77,21 @@ bool goto_symex_fault_localizert::check(
   const localization_points_valuet &value)
 {
   PRECONDITION(value.size() == localization_points.size());
-  bvt assumptions;
+  std::vector<exprt> assumptions;
   localization_points_valuet::const_iterator v_it = value.begin();
   for(const auto &l : localization_points)
   {
     if(v_it->is_true())
       assumptions.push_back(l.first);
     else if(v_it->is_false())
-      assumptions.push_back(!l.first);
+      assumptions.push_back(solver.handle(not_exprt(l.first)));
     ++v_it;
   }
 
   // lock the failed assertion
-  assumptions.push_back(!solver.convert(failed_step.cond_handle));
+  assumptions.push_back(solver.handle(not_exprt(failed_step.cond_handle)));
 
-  solver.set_assumptions(assumptions);
+  solver.push(assumptions);
 
   return solver() != decision_proceduret::resultt::D_SATISFIABLE;
 }
@@ -104,11 +102,11 @@ void goto_symex_fault_localizert::update_scores(
   for(auto &l : localization_points)
   {
     auto &score = l.second->second;
-    if(solver.l_get(l.first).is_true())
+    if(solver.get(l.first).is_true())
     {
       score++;
     }
-    else if(solver.l_get(l.first).is_false() && score > 0)
+    else if(solver.get(l.first).is_false() && score > 0)
     {
       score--;
     }
@@ -135,6 +133,5 @@ void goto_symex_fault_localizert::localize_linear(
   }
 
   // clear assumptions
-  bvt assumptions;
-  solver.set_assumptions(assumptions);
+  solver.pop();
 }

src/goto-checker/goto_symex_fault_localizer.h

@@ -18,7 +18,7 @@ Author: Peter Schrammel
 
 #include <goto-symex/symex_target_equation.h>
 
-#include <solvers/prop/prop_conv.h>
+#include <solvers/stack_decision_procedure.h>
 
 #include "fault_localization_provider.h"
 
@@ -29,18 +29,18 @@ class goto_symex_fault_localizert
     const optionst &options,
     ui_message_handlert &ui_message_handler,
     const symex_target_equationt &equation,
-    prop_convt &solver);
+    stack_decision_proceduret &solver);
 
   fault_location_infot operator()(const irep_idt &failed_property_id);
 
 protected:
   const optionst &options;
   ui_message_handlert &ui_message_handler;
   const symex_target_equationt &equation;
-  prop_convt &solver;
+  stack_decision_proceduret &solver;
 
   /// A localization point is a goto instruction that is potentially at fault
-  typedef std::map<literalt, fault_location_infot::score_mapt::iterator>
+  typedef std::map<exprt, fault_location_infot::score_mapt::iterator>
     localization_pointst;
 
   /// Collects the guards as \p localization_points up to \p failed_property_id

src/goto-checker/goto_symex_property_decider.h

@@ -37,10 +37,6 @@ class goto_symex_property_decidert
   /// Convert the instances of a property into a goal variable
   void convert_goals();
 
-  /// Prevent the solver to optimize-away the goal variables
-  /// (necessary for incremental solving)
-  void freeze_goal_variables();
-
   /// Add disjunction of negated selected properties to the equation
   void add_constraint_from_goals(
     std::function<bool(const irep_idt &property_id)> select_property);

src/solvers/prop/prop_conv.cpp

@@ -7,14 +7,3 @@ Author: Daniel Kroening, [email protected]
 \*******************************************************************/
 
 #include "prop_conv.h"
-
-#include "literal_expr.h"
-
-#include <util/std_expr.h>
-
-#include <algorithm>
-
-void prop_convt::set_assumptions(const bvt &)
-{
-  UNREACHABLE;
-}

src/solvers/prop/prop_conv.h

@@ -10,32 +10,25 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_SOLVERS_PROP_PROP_CONV_H
 #define CPROVER_SOLVERS_PROP_PROP_CONV_H
 
-#include <solvers/decision_procedure.h>
-
-#include "literal.h"
+#include <solvers/stack_decision_procedure.h>
 
+class literalt;
 class tvt;
 
 // API that provides a "handle" in the form of a literalt
 // for expressions.
 
-class prop_convt:public decision_proceduret
+class prop_convt : public stack_decision_proceduret
 {
 public:
   virtual ~prop_convt() { }
 
-  using decision_proceduret::operator();
-
   /// Convert a Boolean expression and return the corresponding literal
   virtual literalt convert(const exprt &expr) = 0;
 
   /// Return value of literal \p l from satisfying assignment.
   /// Return tvt::UNKNOWN if not available
   virtual tvt l_get(literalt l) const = 0;
-
-  // incremental solving
-  virtual void set_assumptions(const bvt &_assumptions);
-  virtual bool has_set_assumptions() const { return false; }
 };
 
 #endif // CPROVER_SOLVERS_PROP_PROP_CONV_H

src/solvers/prop/prop_conv_solver.cpp

@@ -365,7 +365,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::add_constraints_to_prop(const exprt &expr, bool value)
 {
   PRECONDITION(expr.type().id() == ID_bool);
 
@@ -380,7 +380,7 @@ void prop_conv_solvert::set_to(const exprt &expr, bool value)
     {
       if(expr.operands().size() == 1)
       {
-        set_to(expr.op0(), !value);
+        add_constraints_to_prop(expr.op0(), !value);
         return;
       }
     }
@@ -393,7 +393,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);
+            add_constraints_to_prop(*it, true);
 
           return;
         }
@@ -437,14 +437,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());
+          add_constraints_to_prop(implies_expr.op0(), true);
+          add_constraints_to_prop(implies_expr.op1(), false);
           return;
         }
         else if(expr.id() == ID_or) // !(a || b)  ==  (!a && !b)
         {
           forall_operands(it, expr)
-            set_to_false(*it);
+            add_constraints_to_prop(*it, false);
           return;
         }
       }
@@ -525,3 +525,52 @@ 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(assumption_stack.empty())
+  {
+    // We are in the root context.
+    add_constraints_to_prop(expr, value);
+  }
+  else
+  {
+    // We have a child context. We add context_literal ==> expr to the formula.
+    add_constraints_to_prop(
+      or_exprt(literal_exprt(!assumption_stack.back()), expr), value);
+  }
+}
+
+void prop_conv_solvert::push(const std::vector<exprt> &assumptions)
+{
+  // We push the given assumptions as a single context onto the stack.
+  assumption_stack.reserve(assumption_stack.size() + assumptions.size());
+  for(const auto &assumption : assumptions)
+    assumption_stack.push_back(to_literal_expr(assumption).get_literal());
+  context_size_stack.push_back(assumptions.size());
+
+  prop.set_assumptions(assumption_stack);
+}
+
+void prop_conv_solvert::push()
+{
+  // We create a new context literal.
+  literalt context_literal = convert(symbol_exprt(
+    context_prefix + std::to_string(context_literal_counter++), bool_typet()));
+
+  assumption_stack.push_back(context_literal);
+  context_size_stack.push_back(1);
+
+  prop.set_assumptions(assumption_stack);
+}
+
+void prop_conv_solvert::pop()
+{
+  // We remove the context from the stack.
+  assumption_stack.resize(assumption_stack.size() - context_size_stack.back());
+  context_size_stack.pop_back();
+
+  prop.set_assumptions(assumption_stack);
+}

src/solvers/prop/prop_conv_solver.h

@@ -37,7 +37,6 @@ class prop_conv_solvert : public conflict_providert,
   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
@@ -50,14 +49,6 @@ class prop_conv_solvert : public conflict_providert,
   {
     return prop.l_get(a);
   }
-  void set_assumptions(const bvt &_assumptions) override
-  {
-    prop.set_assumptions(_assumptions);
-  }
-  bool has_set_assumptions() const override
-  {
-    return prop.has_set_assumptions();
-  }
 
   exprt handle(const exprt &expr) override;
 
@@ -68,6 +59,18 @@ class prop_conv_solvert : public conflict_providert,
   literalt convert(const exprt &expr) override;
   bool is_in_conflict(const exprt &expr) const override;
 
+  /// 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;
+
+  void push() override;
+
+  /// Push \p assumptions in form of `literal_exprt`
+  void push(const std::vector<exprt> &assumptions) override;
+
+  void pop() override;
+
   // get literal for expression, if available
   bool literal(const symbol_exprt &expr, literalt &literal) const;
 
@@ -124,10 +127,26 @@ class prop_conv_solvert : public conflict_providert,
 
   virtual void ignoring(const exprt &expr);
 
-  // deliberately protected now to protect lower-level API
   propt &prop;
 
   messaget log;
+
+  static const char *context_prefix;
+
+  /// Assumptions on the stack
+  bvt assumption_stack;
+
+  /// To generate unique literal names for contexts
+  std::size_t context_literal_counter = 0;
+
+  /// `assumption_stack` is segmented in contexts;
+  /// Number of assumptions in each context on the stack
+  std::vector<size_t> context_size_stack;
+
+private:
+  /// Helper method used by `set_to` for adding the constraints to `prop`.
+  /// This method is private because it must not be used by derived classes.
+  void add_constraints_to_prop(const exprt &expr, bool value);
 };
 
 #endif // CPROVER_SOLVERS_PROP_PROP_CONV_SOLVER_H

src/solvers/prop/prop_minimize.cpp

@@ -95,9 +95,6 @@ literalt prop_minimizet::constraint()
 /// Try to cover all objectives
 void prop_minimizet::operator()()
 {
-  // we need to use assumptions
-  PRECONDITION(prop_conv.has_set_assumptions());
-
   _iterations = 0;
   _number_satisfied = 0;
   _value = 0;
@@ -120,9 +117,7 @@ void prop_minimizet::operator()()
       {
         _iterations++;
 
-        bvt assumptions;
-        assumptions.push_back(c);
-        prop_conv.set_assumptions(assumptions);
+        prop_conv.push({literal_exprt{c}});
         dec_result = prop_conv();
 
         switch(dec_result)
@@ -150,8 +145,7 @@ void prop_minimizet::operator()()
     // We don't have a satisfying assignment to work with.
     // Run solver again to get one.
 
-    bvt assumptions; // no assumptions
-    prop_conv.set_assumptions(assumptions);
+    prop_conv.pop();
     (void)prop_conv();
   }
 }

src/solvers/prop/prop_minimize.h

@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/message.h>
 
+#include "literal.h"
 #include "prop_conv.h"
 
 /// Computes a satisfying assignment of minimal cost according to a const