Merge pull request #4587 from peterschrammel/get-decision-procedure

Allow getting specific decision procedure interface

Author: peterschrammel

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/decision_procedure.h>
 
 #include <util/make_unique.h>
 #include <util/ui_message.h>
@@ -42,13 +42,13 @@ 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
@@ -149,14 +149,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>
@@ -356,12 +356,13 @@ std::chrono::duration<double> prepare_property_decider(
   auto solver_start = std::chrono::steady_clock::now();
 
   messaget log(ui_message_handler);
-  log.status() << "Passing problem to "
-               << property_decider.get_solver().decision_procedure_text()
-               << messaget::eom;
+  log.status()
+    << "Passing problem to "
+    << property_decider.get_decision_procedure().decision_procedure_text()
+    << messaget::eom;
 
   convert_symex_target_equation(
-    equation, property_decider.get_solver(), ui_message_handler);
+    equation, property_decider.get_decision_procedure(), ui_message_handler);
   property_decider.update_properties_goals_from_symex_target_equation(
     properties);
   property_decider.convert_goals();
@@ -381,9 +382,10 @@ void run_property_decider(
   auto solver_start = std::chrono::steady_clock::now();
 
   messaget log(ui_message_handler);
-  log.status() << "Running "
-               << property_decider.get_solver().decision_procedure_text()
-               << messaget::eom;
+  log.status()
+    << "Running "
+    << property_decider.get_decision_procedure().decision_procedure_text()
+    << messaget::eom;
 
   property_decider.add_constraint_from_goals(
     [&properties](const irep_idt &property_id) {

src/goto-checker/bmc_util.h

@@ -22,21 +22,21 @@ Author: Daniel Kroening, Peter Schrammel
 #include "incremental_goto_checker.h"
 #include "properties.h"
 
+class decision_proceduret;
 class goto_symex_property_decidert;
 class goto_tracet;
 class memory_model_baset;
 class message_handlert;
 class namespacet;
 class optionst;
-class prop_convt;
 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 +51,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(

src/goto-checker/goto_symex_property_decider.cpp

@@ -73,8 +73,8 @@ void goto_symex_property_decidert::convert_goals()
   {
     // Our goal is to falsify a property, i.e., we will
     // add the negation of the property as goal.
-    goal_pair.second.condition =
-      solver->prop_conv().handle(not_exprt(goal_pair.second.as_expr()));
+    goal_pair.second.condition = solver->decision_procedure().handle(
+      not_exprt(goal_pair.second.as_expr()));
   }
 }
 
@@ -94,17 +94,24 @@ void goto_symex_property_decidert::add_constraint_from_goals(
   }
 
   // this is 'false' if there are no disjuncts
-  solver->prop_conv().set_to_true(disjunction(disjuncts));
+  solver->decision_procedure().set_to_true(disjunction(disjuncts));
 }
 
 decision_proceduret::resultt goto_symex_property_decidert::solve()
 {
-  return solver->prop_conv()();
+  return solver->decision_procedure()();
 }
 
-prop_convt &goto_symex_property_decidert::get_solver() const
+decision_proceduret &
+goto_symex_property_decidert::get_decision_procedure() const
 {
-  return solver->prop_conv();
+  return solver->decision_procedure();
+}
+
+stack_decision_proceduret &
+goto_symex_property_decidert::get_stack_decision_procedure() const
+{
+  return solver->stack_decision_procedure();
 }
 
 symex_target_equationt &goto_symex_property_decidert::get_equation() const
@@ -125,7 +132,9 @@ void goto_symex_property_decidert::update_properties_status_from_goals(
     {
       auto &status = properties.at(goal_pair.first).status;
       if(
-        solver->prop_conv().get(goal_pair.second.condition).is_true() &&
+        solver->decision_procedure()
+          .get(goal_pair.second.condition)
+          .is_true() &&
         status != property_statust::FAIL)
       {
         status |= property_statust::FAIL;

src/goto-checker/goto_symex_property_decider.h

@@ -45,7 +45,10 @@ class goto_symex_property_decidert
   decision_proceduret::resultt solve();
 
   /// Returns the solver instance
-  prop_convt &get_solver() const;
+  decision_proceduret &get_decision_procedure() const;
+
+  /// Returns the solver instance
+  stack_decision_proceduret &get_stack_decision_procedure() const;
 
   /// Return the equation associated with this instance
   symex_target_equationt &get_equation() const;

src/goto-checker/multi_path_symex_checker.cpp

@@ -90,7 +90,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_decision_procedure(),
     ns,
     goto_trace);
 
@@ -103,11 +103,13 @@ 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_stack_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_decision_procedure(), ns, goto_trace);
 
   return goto_trace;
 }
@@ -119,7 +121,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_decision_procedure(),
     ns,
     goto_trace);
 
@@ -146,7 +148,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_stack_decision_procedure());
 
   return fault_localizer(property_id);
 }

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_decision_procedure(),
     ns,
     goto_trace);
 
@@ -135,14 +135,14 @@ 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_stack_decision_procedure()),
       property_decider->get_equation());
   }
 
   goto_tracet goto_trace;
   build_goto_trace(
     property_decider->get_equation(),
-    property_decider->get_solver(),
+    property_decider->get_decision_procedure(),
     ns,
     goto_trace);
 
@@ -156,7 +156,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_decision_procedure(),
     ns,
     goto_trace);