Rename prop_convt to decision_procedure_incrementalt

decision_procedure_incrementalt will then be further split
into support for assumptions and contexts.

Author: peterschrammel

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/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>

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

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)
+  decision_procedure_incrementalt &solver)
   : options(options),
     ui_message_handler(ui_message_handler),
     equation(equation),

src/goto-checker/goto_symex_fault_localizer.h

@@ -18,6 +18,8 @@ Author: Peter Schrammel
 
 #include <goto-symex/symex_target_equation.h>
 
+#include <solvers/prop/decision_procedure_incremental.h>
+
 #include "fault_localization_provider.h"
 
 class goto_symex_fault_localizert
@@ -27,15 +29,15 @@ class goto_symex_fault_localizert
     const optionst &options,
     ui_message_handlert &ui_message_handler,
     const symex_target_equationt &equation,
-    prop_convt &solver);
+    decision_procedure_incrementalt &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;
+  decision_procedure_incrementalt &solver;
 
   /// A localization point is a goto instruction that is potentially at fault
   typedef std::map<literalt, fault_location_infot::score_mapt::iterator>