Context-based solver interface for incremental solvers [depends: 4451, blocks: 4361]

jbmc/src/jbmc/all_properties.cpp

@@ -20,7 +20,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/json.h>
 #include <util/xml.h>
 
-#include <solvers/prop/prop_conv.h>
+#include <solvers/prop/decision_procedure.h>
 #include <solvers/sat/satcheck.h>
 
 #include <goto-programs/json_goto_trace.h>
@@ -61,7 +61,7 @@ safety_checkert::resultt bmc_all_propertiest::operator()()
   auto solver_start = std::chrono::steady_clock::now();
 
   convert_symex_target_equation(
-    bmc.equation, bmc.prop_conv, get_message_handler());
+    bmc.equation, bmc.decision_procedure, get_message_handler());
   bmc.freeze_program_variables();
 
   // Collect _all_ goals in `goal_map'.
@@ -301,7 +301,8 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals)
 safety_checkert::resultt
 bmct::all_properties(const goto_functionst &goto_functions)
 {
-  bmc_all_propertiest bmc_all_properties(goto_functions, prop_conv, *this);
+  bmc_all_propertiest bmc_all_properties(
+    goto_functions, decision_procedure, *this);
   bmc_all_properties.set_message_handler(get_message_handler());
   return bmc_all_properties();
 }

jbmc/src/jbmc/all_properties_class.h

@@ -22,7 +22,7 @@ class bmc_all_propertiest : public cover_goalst::observert, public messaget
 public:
   bmc_all_propertiest(
     const goto_functionst &_goto_functions,
-    prop_convt &_solver,
+    decision_procedure_incrementalt &_solver,
     bmct &_bmc)
     : goto_functions(_goto_functions), solver(_solver), bmc(_bmc)
   {
@@ -96,7 +96,7 @@ class bmc_all_propertiest : public cover_goalst::observert, public messaget
 
 protected:
   const goto_functionst &goto_functions;
-  prop_convt &solver;
+  decision_procedure_incrementalt &solver;
   bmct &bmc;
 
   virtual void report(const cover_goalst &cover_goals);

jbmc/src/jbmc/bmc.cpp

@@ -42,19 +42,20 @@ void bmct::freeze_program_variables()
 
 decision_proceduret::resultt bmct::run_decision_procedure()
 {
-  status() << "Passing problem to " << prop_conv.decision_procedure_text()
-           << eom;
+  status() << "Passing problem to "
+           << decision_procedure.decision_procedure_text() << eom;
 
   auto solver_start = std::chrono::steady_clock::now();
 
-  convert_symex_target_equation(equation, prop_conv, get_message_handler());
+  convert_symex_target_equation(
+    equation, decision_procedure, get_message_handler());
 
   // hook for cegis to freeze synthesis program vars
   freeze_program_variables();
 
-  status() << "Running " << prop_conv.decision_procedure_text() << eom;
+  status() << "Running " << decision_procedure.decision_procedure_text() << eom;
 
-  decision_proceduret::resultt dec_result = prop_conv();
+  decision_proceduret::resultt dec_result = decision_procedure();
 
   {
     auto solver_stop = std::chrono::steady_clock::now();
@@ -207,11 +208,11 @@ safety_checkert::resultt bmct::stop_on_fail()
       {
         // NOLINTNEXTLINE(whitespace/braces)
         counterexample_beautificationt{ui_message_handler}(
-          dynamic_cast<boolbvt &>(prop_conv), equation);
+          dynamic_cast<boolbvt &>(decision_procedure), equation);
       }
 
       build_error_trace(
-        error_trace, ns, equation, prop_conv, ui_message_handler);
+        error_trace, ns, equation, decision_procedure, ui_message_handler);
       output_error_trace(error_trace, ns, trace_options(), ui_message_handler);
       output_graphml(error_trace, ns, options);
     }
@@ -265,12 +266,11 @@ int bmct::do_language_agnostic_bmc(
     {
       std::unique_ptr<solver_factoryt::solvert> cbmc_solver =
         solvers.get_solver();
-      prop_convt &pc = cbmc_solver->prop_conv();
       bmct bmc(
         opts,
         symbol_table,
         ui,
-        pc,
+        cbmc_solver->decision_procedure_incremental(),
         *worklist,
         callback_after_symex,
         guard_manager);
@@ -314,13 +314,12 @@ int bmct::do_language_agnostic_bmc(
     {
       std::unique_ptr<solver_factoryt::solvert> cbmc_solver =
         solvers.get_solver();
-      prop_convt &pc = cbmc_solver->prop_conv();
       path_storaget::patht &resume = worklist->peek();
       path_explorert pe(
         opts,
         symbol_table,
         ui,
-        pc,
+        cbmc_solver->decision_procedure_incremental(),
         resume.equation,
         resume.state,
         *worklist,

jbmc/src/jbmc/bmc.h

@@ -30,7 +30,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/safety_checker.h>
 #include <goto-symex/memory_model.h>
 
-#include <solvers/prop/decision_procedure.h>
+#include <solvers/prop/decision_procedure_incremental.h>
 
 class cbmc_solverst;
 
@@ -68,7 +68,7 @@ class bmct : public safety_checkert
     const optionst &_options,
     const symbol_tablet &outer_symbol_table,
     ui_message_handlert &_message_handler,
-    prop_convt &_prop_conv,
+    decision_procedure_incrementalt &_decision_procedure,
     path_storaget &_path_storage,
     std::function<bool(void)> callback_after_symex,
     guard_managert &guard_manager)
@@ -86,7 +86,7 @@ class bmct : public safety_checkert
         options,
         path_storage,
         guard_manager),
-      prop_conv(_prop_conv),
+      decision_procedure(_decision_procedure),
       ui_message_handler(_message_handler),
       driver_callback_after_symex(callback_after_symex)
   {
@@ -141,7 +141,7 @@ class bmct : public safety_checkert
     const optionst &_options,
     const symbol_tablet &outer_symbol_table,
     ui_message_handlert &_message_handler,
-    prop_convt &_prop_conv,
+    decision_procedure_incrementalt &_decision_procedure,
     symex_target_equationt &_equation,
     path_storaget &_path_storage,
     std::function<bool(void)> callback_after_symex,
@@ -160,7 +160,7 @@ class bmct : public safety_checkert
         options,
         path_storage,
         guard_manager),
-      prop_conv(_prop_conv),
+      decision_procedure(_decision_procedure),
       ui_message_handler(_message_handler),
       driver_callback_after_symex(callback_after_symex)
   {
@@ -180,7 +180,7 @@ class bmct : public safety_checkert
   guard_managert &guard_manager;
   path_storaget &path_storage;
   symex_bmct symex;
-  prop_convt &prop_conv;
+  decision_procedure_incrementalt &decision_procedure;
   std::unique_ptr<memory_model_baset> memory_model;
   // use gui format
   ui_message_handlert &ui_message_handler;
@@ -235,7 +235,7 @@ class path_explorert : public bmct
     const optionst &_options,
     const symbol_tablet &outer_symbol_table,
     ui_message_handlert &_message_handler,
-    prop_convt &_prop_conv,
+    decision_procedure_incrementalt &_decision_procedure,
     symex_target_equationt &saved_equation,
     const goto_symex_statet &saved_state,
     path_storaget &path_storage,
@@ -245,7 +245,7 @@ class path_explorert : public bmct
         _options,
         outer_symbol_table,
         _message_handler,
-        _prop_conv,
+        _decision_procedure,
         saved_equation,
         path_storage,
         callback_after_symex,

src/cbmc/README.md

@@ -96,7 +96,7 @@ each assertion was violated. This is constructed using `build_goto_trace`, which
 queries the backend asking what value was chosen for each program variable on
 the path from the start of the program to the relevant assertion. For more
 details on how the trace is populated see the documentation for
-`build_goto_trace` for `prop_convt::get`, the function used to query the
+`build_goto_trace` for `decision_proceduret::get`, the function used to query the
 backend.
 
 ## Path-symex

src/goto-checker/bmc_util.cpp

@@ -25,7 +25,7 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include <linking/static_lifetime_init.h>
 
-#include <solvers/prop/prop_conv.h>
+#include <solvers/prop/decision_procedure.h>
 
 #include <util/make_unique.h>
 #include <util/ui_message.h>
@@ -42,23 +42,23 @@ void build_error_trace(
   goto_tracet &goto_trace,
   const namespacet &ns,
   const symex_target_equationt &symex_target_equation,
-  const prop_convt &prop_conv,
+  const decision_proceduret &decision_procedure,
   ui_message_handlert &ui_message_handler)
 {
   messaget log(ui_message_handler);
   message_building_error_trace(log);
 
-  build_goto_trace(symex_target_equation, prop_conv, ns, goto_trace);
+  build_goto_trace(symex_target_equation, decision_procedure, ns, goto_trace);
 }
 
 ssa_step_predicatet
 ssa_step_matches_failing_property(const irep_idt &property_id)
 {
   return [property_id](
            symex_target_equationt::SSA_stepst::const_iterator step,
-           const prop_convt &prop_conv) {
+           const decision_proceduret &decision_procedure) {
     return step->is_assert() && step->get_property_id() == property_id &&
-           prop_conv.l_get(step->cond_literal).is_false();
+           decision_procedure.l_get(step->cond_literal).is_false();
   };
 }
 
@@ -105,14 +105,14 @@ void output_error_trace(
 
 void freeze_guards(
   const symex_target_equationt &equation,
-  prop_convt &prop_conv)
+  decision_procedure_incrementalt &decision_procedure)
 {
   for(const auto &step : equation.SSA_steps)
   {
     if(!step.guard_literal.is_constant())
-      prop_conv.set_frozen(step.guard_literal);
+      decision_procedure.set_frozen(step.guard_literal);
     if(step.is_assert() && !step.cond_literal.is_constant())
-      prop_conv.set_frozen(step.cond_literal);
+      decision_procedure.set_frozen(step.cond_literal);
   }
 }
 
@@ -162,14 +162,14 @@ void output_graphml(
 
 void convert_symex_target_equation(
   symex_target_equationt &equation,
-  prop_convt &prop_conv,
+  decision_proceduret &decision_procedure,
   message_handlert &message_handler)
 {
   messaget msg(message_handler);
   msg.status() << "converting SSA" << messaget::eom;
 
   // convert SSA
-  equation.convert(prop_conv);
+  equation.convert(decision_procedure);
 }
 
 std::unique_ptr<memory_model_baset>
@@ -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(

src/goto-checker/bmc_util.h

@@ -28,15 +28,16 @@ class memory_model_baset;
 class message_handlert;
 class namespacet;
 class optionst;
-class prop_convt;
+class decision_proceduret;
+class decision_procedure_incrementalt;
 class symex_bmct;
 class symex_target_equationt;
 struct trace_optionst;
 class ui_message_handlert;
 
 void convert_symex_target_equation(
   symex_target_equationt &,
-  prop_convt &,
+  decision_proceduret &,
   message_handlert &);
 
 /// Returns a function that checks whether an SSA step is an assertion
@@ -51,7 +52,7 @@ void build_error_trace(
   goto_tracet &,
   const namespacet &,
   const symex_target_equationt &,
-  const prop_convt &,
+  const decision_proceduret &,
   ui_message_handlert &);
 
 void output_error_trace(
@@ -60,7 +61,9 @@ void output_error_trace(
   const trace_optionst &,
   ui_message_handlert &);
 
-void freeze_guards(const symex_target_equationt &, prop_convt &);
+void freeze_guards(
+  const symex_target_equationt &,
+  decision_procedure_incrementalt &);
 
 void output_graphml(const goto_tracet &, const namespacet &, const optionst &);
 void output_graphml(

src/goto-checker/counterexample_beautification.cpp

@@ -26,7 +26,7 @@ counterexample_beautificationt::counterexample_beautificationt(
 }
 
 void counterexample_beautificationt::get_minimization_list(
-  prop_convt &prop_conv,
+  decision_proceduret &decision_procedure,
   const symex_target_equationt &equation,
   minimization_listt &minimization_list)
 {
@@ -41,7 +41,7 @@ void counterexample_beautificationt::get_minimization_list(
       it->is_assignment() &&
       it->assignment_type == symex_targett::assignment_typet::STATE)
     {
-      if(!prop_conv.l_get(it->guard_literal).is_false())
+      if(!decision_procedure.l_get(it->guard_literal).is_false())
       {
         const typet &type = it->ssa_lhs.type();
 
@@ -69,7 +69,7 @@ void counterexample_beautificationt::get_minimization_list(
 
 symex_target_equationt::SSA_stepst::const_iterator
 counterexample_beautificationt::get_failed_property(
-  const prop_convt &prop_conv,
+  const decision_proceduret &decision_procedure,
   const symex_target_equationt &equation)
 {
   // find failed property
@@ -79,8 +79,9 @@ counterexample_beautificationt::get_failed_property(
       it != equation.SSA_steps.end();
       it++)
     if(
-      it->is_assert() && prop_conv.l_get(it->guard_literal).is_true() &&
-      prop_conv.l_get(it->cond_literal).is_false())
+      it->is_assert() &&
+      decision_procedure.l_get(it->guard_literal).is_true() &&
+      decision_procedure.l_get(it->cond_literal).is_false())
       return it;
 
   UNREACHABLE;

src/goto-checker/counterexample_beautification.h

@@ -28,14 +28,14 @@ class counterexample_beautificationt
 
 protected:
   void get_minimization_list(
-    prop_convt &prop_conv,
+    decision_proceduret &decision_procedure,
     const symex_target_equationt &equation,
     minimization_listt &minimization_list);
 
   void minimize(const exprt &expr, class prop_minimizet &prop_minimize);
 
   symex_target_equationt::SSA_stepst::const_iterator get_failed_property(
-    const prop_convt &prop_conv,
+    const decision_proceduret &decision_procedure,
     const symex_target_equationt &equation);
 
   // the failed property