Split out decision procedure with solving under assumptions

peterschrammel · peterschrammel · commit 1d07a1c714cd · 2019-03-28T17:27:41.000Z
Makes it explicit which algorithms actually require this feature.
diff --git a/src/goto-checker/bmc_util.cpp b/src/goto-checker/bmc_util.cpp
@@ -368,13 +368,14 @@ std::chrono::duration<double> prepare_property_decider(
 {
   auto solver_start = std::chrono::steady_clock::now();
 
+  decision_proceduret &decision_procedure =
+    property_decider.get_solver().decision_procedure();
   messaget log(ui_message_handler);
   log.status() << "Passing problem to "
-               << property_decider.get_solver().decision_procedure_text()
-               << messaget::eom;
+               << decision_procedure.decision_procedure_text() << messaget::eom;
 
   convert_symex_target_equation(
-    equation, property_decider.get_solver(), ui_message_handler);
+    equation, decision_procedure, ui_message_handler);
   property_decider.update_properties_goals_from_symex_target_equation(
     properties);
   property_decider.convert_goals();
@@ -394,9 +395,10 @@ void run_property_decider(
 {
   auto solver_start = std::chrono::steady_clock::now();
 
+  const decision_proceduret &decision_procedure =
+    property_decider.get_solver().decision_procedure();
   messaget log(ui_message_handler);
-  log.status() << "Running "
-               << property_decider.get_solver().decision_procedure_text()
+  log.status() << "Running " << decision_procedure.decision_procedure_text()
                << messaget::eom;
 
   property_decider.add_constraint_from_goals(
diff --git a/src/goto-checker/goto_symex_fault_localizer.cpp b/src/goto-checker/goto_symex_fault_localizer.cpp
@@ -15,7 +15,7 @@ goto_symex_fault_localizert::goto_symex_fault_localizert(
   const optionst &options,
   ui_message_handlert &ui_message_handler,
   const symex_target_equationt &equation,
-  decision_procedure_incrementalt &solver)
+  decision_procedure_assumptionst &solver)
   : options(options),
     ui_message_handler(ui_message_handler),
     equation(equation),
diff --git a/src/goto-checker/goto_symex_fault_localizer.h b/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/decision_procedure_incremental.h>
+#include <solvers/prop/decision_procedure_assumptions.h>
 
 #include "fault_localization_provider.h"
 
@@ -29,15 +29,15 @@ class goto_symex_fault_localizert
     const optionst &options,
     ui_message_handlert &ui_message_handler,
     const symex_target_equationt &equation,
-    decision_procedure_incrementalt &solver);
+    decision_procedure_assumptionst &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;
-  decision_procedure_incrementalt &solver;
+  decision_procedure_assumptionst &solver;
 
   /// A localization point is a goto instruction that is potentially at fault
   typedef std::map<literalt, fault_location_infot::score_mapt::iterator>
diff --git a/src/goto-checker/goto_symex_property_decider.cpp b/src/goto-checker/goto_symex_property_decider.cpp
@@ -11,6 +11,8 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include "goto_symex_property_decider.h"
 
+#include <solvers/prop/literal_expr.h>
+
 goto_symex_property_decidert::goto_symex_property_decidert(
   const optionst &options,
   ui_message_handlert &ui_message_handler,
@@ -108,10 +110,9 @@ decision_proceduret::resultt goto_symex_property_decidert::solve()
   return (*decision_procedure)();
 }
 
-decision_procedure_incrementalt &
-goto_symex_property_decidert::get_solver() const
+const solver_factoryt::solvert &goto_symex_property_decidert::get_solver() const
 {
-  return *decision_procedure;
+  return *solver;
 }
 
 symex_target_equationt &goto_symex_property_decidert::get_equation() const
diff --git a/src/goto-checker/goto_symex_property_decider.h b/src/goto-checker/goto_symex_property_decider.h
@@ -49,7 +49,7 @@ class goto_symex_property_decidert
   decision_proceduret::resultt solve();
 
   /// Returns the solver instance
-  decision_procedure_incrementalt &get_solver() const;
+  const solver_factoryt::solvert &get_solver() const;
 
   /// Return the equation associated with this instance
   symex_target_equationt &get_equation() const;
diff --git a/src/goto-checker/multi_path_symex_checker.cpp b/src/goto-checker/multi_path_symex_checker.cpp
@@ -73,7 +73,8 @@ multi_path_symex_checkert::prepare_property_decider(propertiest &properties)
     properties, equation, property_decider, ui_message_handler);
 
   if(options.get_bool_option("localize-faults"))
-    freeze_guards(equation, property_decider.get_solver());
+    freeze_guards(
+      equation, property_decider.get_solver().decision_procedure_incremental());
 
   return solver_runtime;
 }
@@ -93,7 +94,7 @@ goto_tracet multi_path_symex_checkert::build_full_trace() const
   build_goto_trace(
     equation,
     equation.SSA_steps.end(),
-    property_decider.get_solver(),
+    property_decider.get_solver().decision_procedure(),
     ns,
     goto_trace);
 
@@ -106,11 +107,17 @@ goto_tracet multi_path_symex_checkert::build_shortest_trace() const
   {
     // NOLINTNEXTLINE(whitespace/braces)
     counterexample_beautificationt{ui_message_handler}(
-      dynamic_cast<boolbvt &>(property_decider.get_solver()), equation);
+      dynamic_cast<boolbvt &>(
+        property_decider.get_solver().decision_procedure()),
+      equation);
   }
 
   goto_tracet goto_trace;
-  build_goto_trace(equation, property_decider.get_solver(), ns, goto_trace);
+  build_goto_trace(
+    equation,
+    property_decider.get_solver().decision_procedure(),
+    ns,
+    goto_trace);
 
   return goto_trace;
 }
@@ -122,7 +129,7 @@ multi_path_symex_checkert::build_trace(const irep_idt &property_id) const
   build_goto_trace(
     equation,
     ssa_step_matches_failing_property(property_id),
-    property_decider.get_solver(),
+    property_decider.get_solver().decision_procedure(),
     ns,
     goto_trace);
 
@@ -149,7 +156,10 @@ fault_location_infot
 multi_path_symex_checkert::localize_fault(const irep_idt &property_id) const
 {
   goto_symex_fault_localizert fault_localizer(
-    options, ui_message_handler, equation, property_decider.get_solver());
+    options,
+    ui_message_handler,
+    equation,
+    property_decider.get_solver().decision_procedure_assumptions());
 
   return fault_localizer(property_id);
 }
diff --git a/src/goto-checker/single_path_symex_checker.cpp b/src/goto-checker/single_path_symex_checker.cpp
@@ -122,7 +122,7 @@ goto_tracet single_path_symex_checkert::build_full_trace() const
   build_goto_trace(
     property_decider->get_equation(),
     property_decider->get_equation().SSA_steps.end(),
-    property_decider->get_solver(),
+    property_decider->get_solver().decision_procedure(),
     ns,
     goto_trace);
 
@@ -135,14 +135,15 @@ goto_tracet single_path_symex_checkert::build_shortest_trace() const
   {
     // NOLINTNEXTLINE(whitespace/braces)
     counterexample_beautificationt{ui_message_handler}(
-      dynamic_cast<boolbvt &>(property_decider->get_solver()),
+      dynamic_cast<boolbvt &>(
+        property_decider->get_solver().decision_procedure()),
       property_decider->get_equation());
   }
 
   goto_tracet goto_trace;
   build_goto_trace(
     property_decider->get_equation(),
-    property_decider->get_solver(),
+    property_decider->get_solver().decision_procedure(),
     ns,
     goto_trace);
 
@@ -156,7 +157,7 @@ single_path_symex_checkert::build_trace(const irep_idt &property_id) const
   build_goto_trace(
     property_decider->get_equation(),
     ssa_step_matches_failing_property(property_id),
-    property_decider->get_solver(),
+    property_decider->get_solver().decision_procedure(),
     ns,
     goto_trace);
 
diff --git a/src/goto-checker/solver_factory.cpp b/src/goto-checker/solver_factory.cpp
@@ -80,6 +80,18 @@ solver_factoryt::solvert::decision_procedure_incremental() const
   return *solver;
 }
 
+decision_procedure_assumptionst &
+solver_factoryt::solvert::decision_procedure_assumptions() const
+{
+  PRECONDITION(decision_procedure_ptr != nullptr);
+  decision_procedure_assumptionst *solver =
+    dynamic_cast<decision_procedure_assumptionst *>(&*decision_procedure_ptr);
+  INVARIANT(
+    solver != nullptr,
+    "incremental decision procedure with solving under assumptions required");
+  return *solver;
+}
+
 propt &solver_factoryt::solvert::prop() const
 {
   PRECONDITION(prop_ptr != nullptr);
diff --git a/src/goto-checker/solver_factory.h b/src/goto-checker/solver_factory.h
@@ -14,13 +14,15 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include <memory>
 
+#include <solvers/prop/decision_procedure.h>
+#include <solvers/prop/prop.h>
 #include <solvers/smt2/smt2_dec.h>
 
 class message_handlert;
 class namespacet;
 class optionst;
-class propt;
-class decision_proceduret;
+class decision_procedure_incrementalt;
+class decision_procedure_assumptionst;
 
 class solver_factoryt
 {
@@ -46,6 +48,7 @@ class solver_factoryt
 
     decision_proceduret &decision_procedure() const;
     decision_procedure_incrementalt &decision_procedure_incremental() const;
+    decision_procedure_assumptionst &decision_procedure_assumptions() const;
     propt &prop() const;
 
     void set_decision_procedure(std::unique_ptr<decision_proceduret> p);
@@ -80,8 +83,8 @@ class solver_factoryt
   /// Sets the timeout of \p decision_procedure if the `solver-time-limit`
   /// option has a positive value (in seconds).
   /// \note Most solvers silently ignore the time limit at the moment.
-  void set_decision_procedure_time_limit(
-    decision_proceduret &decision_procedure);
+  void
+  set_decision_procedure_time_limit(decision_proceduret &decision_procedure);
 
   // consistency checks during solver creation
   void no_beautification();
diff --git a/src/solvers/prop/cover_goals.cpp b/src/solvers/prop/cover_goals.cpp
@@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "cover_goals.h"
 
 #include <util/message.h>
+#include <util/threeval.h>
 
 #include "decision_procedure_incremental.h"
 #include "literal_expr.h"
diff --git a/src/solvers/prop/decision_procedure_assumptions.h b/src/solvers/prop/decision_procedure_assumptions.h
@@ -0,0 +1,29 @@
+/*******************************************************************\
+
+Module: Decision procedure with incremental solving under assumptions
+
+Author: Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Decision procedure with incremental solving under assumptions
+
+#ifndef CPROVER_SOLVERS_PROP_DECISION_PROCEDURE_ASSUMPTIONS_H
+#define CPROVER_SOLVERS_PROP_DECISION_PROCEDURE_ASSUMPTIONS_H
+
+#include "decision_procedure_incremental.h"
+
+class decision_procedure_assumptionst : public decision_procedure_incrementalt
+{
+public:
+  /// Set assumptions for the next call to operator() to solve the problem
+  virtual void set_assumptions(const bvt &) = 0;
+
+  /// Returns true if an assumption is in the final conflict
+  virtual bool is_in_conflict(literalt l) const = 0;
+
+  virtual ~decision_procedure_assumptionst() = default;
+};
+
+#endif // CPROVER_SOLVERS_PROP_DECISION_PROCEDURE_ASSUMPTIONS_H
diff --git a/src/solvers/prop/decision_procedure_incremental.cpp b/src/solvers/prop/decision_procedure_incremental.cpp
@@ -1,30 +1,12 @@
 /*******************************************************************\
 
-Module:
+Module: Decision procedure with incremental solving
 
 Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
 #include "decision_procedure_incremental.h"
-#include <algorithm>
-
-/// determine whether a variable is in the final conflict
-bool decision_procedure_incrementalt::is_in_conflict(literalt) const
-{
-  UNREACHABLE;
-  return false;
-}
-
-void decision_procedure_incrementalt::set_assumptions(const bvt &)
-{
-  UNREACHABLE;
-}
-
-void decision_procedure_incrementalt::set_frozen(const literalt)
-{
-  UNREACHABLE;
-}
 
 void decision_procedure_incrementalt::set_frozen(const bvt &bv)
 {
diff --git a/src/solvers/prop/decision_procedure_incremental.h b/src/solvers/prop/decision_procedure_incremental.h
@@ -1,61 +1,36 @@
 /*******************************************************************\
 
-Module:
+Module: Decision procedure with incremental solving
 
 Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
+/// \file
+/// Decision procedure with incremental solving
+
 #ifndef CPROVER_SOLVERS_PROP_DECISION_PROCEDURE_INCREMENTAL_H
 #define CPROVER_SOLVERS_PROP_DECISION_PROCEDURE_INCREMENTAL_H
 
-#include <map>
-#include <string>
-
-#include <util/expr.h>
-#include <util/message.h>
-#include <util/std_expr.h>
-
 #include "decision_procedure.h"
 #include "literal.h"
-#include "literal_expr.h"
-#include "prop.h"
-
-// API that provides a "handle" in the form of a literalt
-// for expressions.
 
 class decision_procedure_incrementalt : public decision_proceduret
 {
 public:
-  virtual ~decision_procedure_incrementalt()
-  {
-  }
-
-  using decision_proceduret::operator();
-
-  // incremental solving
-  virtual void set_frozen(literalt a);
-  virtual void set_frozen(const bvt &);
-  virtual void set_assumptions(const bvt &_assumptions);
-  virtual bool has_set_assumptions() const
-  {
-    return false;
-  }
-  virtual void set_all_frozen()
-  {
-  }
-
-  // returns true if an assumption is in the final conflict
-  virtual bool is_in_conflict(literalt l) const;
-  virtual bool has_is_in_conflict() const
-  {
-    return false;
-  }
-};
+  /// Prevent the solver-level variable associated with literal \p a from being
+  /// optimized away by the decision procedure
+  virtual void set_frozen(literalt a) = 0;
+
+  /// Prevent the solver-level variables in the given bitvector \p bv from being
+  /// optimized away by the decision procedure
+  virtual void set_frozen(const bvt &bv);
 
-//
-// an instance of the above that converts the
-// propositional skeleton by passing it to a propt
-//
+  /// Prevent all solver-level variables encoding symbols occurring in the
+  /// expressions passed to the decision procedure from being optimized away
+  virtual void set_all_frozen() = 0;
+
+  virtual ~decision_procedure_incrementalt() = default;
+};
 
 #endif // CPROVER_SOLVERS_PROP_DECISION_PROCEDURE_INCREMENTAL_H
diff --git a/src/solvers/prop/prop_conv_solver.h b/src/solvers/prop/prop_conv_solver.h
diff --git a/src/solvers/prop/prop_minimize.cpp b/src/solvers/prop/prop_minimize.cpp
diff --git a/src/solvers/prop/prop_minimize.h b/src/solvers/prop/prop_minimize.h
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
diff --git a/src/solvers/smt2/smt2_conv.h b/src/solvers/smt2/smt2_conv.h
diff --git a/src/solvers/smt2/smt2_dec.h b/src/solvers/smt2/smt2_dec.h

Original file line number	Diff line number	Diff line change
`@@ -11,6 +11,8 @@ Author: Daniel Kroening, Peter Schrammel`
`11`	`11`
`12`	`12`	`#include "goto_symex_property_decider.h"`
`13`	`13`
	`14`	`+#include <solvers/prop/literal_expr.h>`
	`15`	`+`
`14`	`16`	`goto_symex_property_decidert::goto_symex_property_decidert(`
`15`	`17`	`const optionst &options,`
`16`	`18`	`ui_message_handlert &ui_message_handler,`
`@@ -108,10 +110,9 @@ decision_proceduret::resultt goto_symex_property_decidert::solve()`
`108`	`110`	`return (*decision_procedure)();`
`109`	`111`	`}`
`110`	`112`
`111`		`-decision_procedure_incrementalt &`
`112`		`-goto_symex_property_decidert::get_solver() const`
	`113`	`+const solver_factoryt::solvert &goto_symex_property_decidert::get_solver() const`
`113`	`114`	`{`
`114`		`- return *decision_procedure;`
	`115`	`+ return *solver;`
`115`	`116`	`}`
`116`	`117`
`117`	`118`	`symex_target_equationt &goto_symex_property_decidert::get_equation() const`