Merge pull request #8408 from tautschnig/solver-factory-no-dynamic_cast

Solver factory: all solvers are stack_decision_proceduret

Author: tautschnig

src/goto-checker/goto_symex_property_decider.cpp

@@ -114,18 +114,12 @@ decision_proceduret::resultt goto_symex_property_decidert::solve()
   return solver->decision_procedure()();
 }
 
-decision_proceduret &
+stack_decision_proceduret &
 goto_symex_property_decidert::get_decision_procedure() const
 {
   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
 {
   return equation;

src/goto-checker/goto_symex_property_decider.h

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

src/goto-checker/multi_path_symex_checker.cpp

@@ -113,7 +113,7 @@ goto_tracet multi_path_symex_checkert::build_shortest_trace() const
   {
     // NOLINTNEXTLINE(whitespace/braces)
     counterexample_beautificationt{ui_message_handler}(
-      dynamic_cast<boolbvt &>(property_decider.get_stack_decision_procedure()),
+      dynamic_cast<boolbvt &>(property_decider.get_decision_procedure()),
       equation);
   }
 
@@ -161,7 +161,7 @@ multi_path_symex_checkert::localize_fault(const irep_idt &property_id) const
     options,
     ui_message_handler,
     equation,
-    property_decider.get_stack_decision_procedure());
+    property_decider.get_decision_procedure());
 
   return fault_localizer(property_id);
 }

src/goto-checker/single_loop_incremental_symex_checker.cpp

@@ -44,7 +44,7 @@ single_loop_incremental_symex_checkert::single_loop_incremental_symex_checkert(
 
   // Freeze all symbols if we are using a prop_conv_solvert
   prop_conv_solvert *prop_conv_solver = dynamic_cast<prop_conv_solvert *>(
-    &property_decider.get_stack_decision_procedure());
+    &property_decider.get_decision_procedure());
   if(prop_conv_solver != nullptr)
     prop_conv_solver->set_all_frozen();
 }
@@ -114,7 +114,7 @@ operator()(propertiest &properties)
           properties);
 
         // We convert the assertions in a new context.
-        property_decider.get_stack_decision_procedure().push();
+        property_decider.get_decision_procedure().push();
         equation.convert_assertions(
           property_decider.get_decision_procedure(), false);
         property_decider.convert_goals();
@@ -154,7 +154,7 @@ operator()(propertiest &properties)
 
       // Nothing else to do with the current set of assertions.
       // Let's pop them.
-      property_decider.get_stack_decision_procedure().pop();
+      property_decider.get_decision_procedure().pop();
     }
 
     // Now we are finally done.
@@ -207,7 +207,7 @@ goto_tracet single_loop_incremental_symex_checkert::build_shortest_trace() const
   {
     // NOLINTNEXTLINE(whitespace/braces)
     counterexample_beautificationt{ui_message_handler}(
-      dynamic_cast<boolbvt &>(property_decider.get_stack_decision_procedure()),
+      dynamic_cast<boolbvt &>(property_decider.get_decision_procedure()),
       equation);
   }
 

src/goto-checker/single_path_symex_checker.cpp

@@ -144,7 +144,7 @@ goto_tracet single_path_symex_checkert::build_shortest_trace() const
   {
     // NOLINTNEXTLINE(whitespace/braces)
     counterexample_beautificationt{ui_message_handler}(
-      dynamic_cast<boolbvt &>(property_decider->get_stack_decision_procedure()),
+      dynamic_cast<boolbvt &>(property_decider->get_decision_procedure()),
       property_decider->get_equation());
   }
 

src/goto-checker/solver_factory.cpp

@@ -46,41 +46,31 @@ solver_factoryt::solver_factoryt(
 {
 }
 
-solver_factoryt::solvert::solvert(std::unique_ptr<decision_proceduret> p)
+solver_factoryt::solvert::solvert(std::unique_ptr<stack_decision_proceduret> p)
   : decision_procedure_ptr(std::move(p))
 {
 }
 
 solver_factoryt::solvert::solvert(
-  std::unique_ptr<decision_proceduret> p1,
+  std::unique_ptr<stack_decision_proceduret> p1,
   std::unique_ptr<propt> p2)
   : prop_ptr(std::move(p2)), decision_procedure_ptr(std::move(p1))
 {
 }
 
 solver_factoryt::solvert::solvert(
-  std::unique_ptr<decision_proceduret> p1,
+  std::unique_ptr<stack_decision_proceduret> p1,
   std::unique_ptr<std::ofstream> p2)
   : ofstream_ptr(std::move(p2)), decision_procedure_ptr(std::move(p1))
 {
 }
 
-decision_proceduret &solver_factoryt::solvert::decision_procedure() const
+stack_decision_proceduret &solver_factoryt::solvert::decision_procedure() const
 {
   PRECONDITION(decision_procedure_ptr != nullptr);
   return *decision_procedure_ptr;
 }
 
-stack_decision_proceduret &
-solver_factoryt::solvert::stack_decision_procedure() const
-{
-  PRECONDITION(decision_procedure_ptr != nullptr);
-  stack_decision_proceduret *solver =
-    dynamic_cast<stack_decision_proceduret *>(&*decision_procedure_ptr);
-  INVARIANT(solver != nullptr, "stack decision procedure required");
-  return *solver;
-}
-
 void solver_factoryt::set_decision_procedure_time_limit(
   solver_resource_limitst &decision_procedure)
 {
@@ -92,7 +82,7 @@ void solver_factoryt::set_decision_procedure_time_limit(
 }
 
 void solver_factoryt::solvert::set_decision_procedure(
-  std::unique_ptr<decision_proceduret> p)
+  std::unique_ptr<stack_decision_proceduret> p)
 {
   decision_procedure_ptr = std::move(p);
 }

src/goto-checker/solver_factory.h

@@ -22,7 +22,6 @@ class message_handlert;
 class namespacet;
 class optionst;
 class solver_resource_limitst;
-class stack_decision_proceduret;
 
 class solver_factoryt final
 {
@@ -39,23 +38,24 @@ class solver_factoryt final
   class solvert final
   {
   public:
-    explicit solvert(std::unique_ptr<decision_proceduret> p);
-    solvert(std::unique_ptr<decision_proceduret> p1, std::unique_ptr<propt> p2);
+    explicit solvert(std::unique_ptr<stack_decision_proceduret> p);
     solvert(
-      std::unique_ptr<decision_proceduret> p1,
+      std::unique_ptr<stack_decision_proceduret> p1,
+      std::unique_ptr<propt> p2);
+    solvert(
+      std::unique_ptr<stack_decision_proceduret> p1,
       std::unique_ptr<std::ofstream> p2);
 
-    decision_proceduret &decision_procedure() const;
-    stack_decision_proceduret &stack_decision_procedure() const;
+    stack_decision_proceduret &decision_procedure() const;
 
-    void set_decision_procedure(std::unique_ptr<decision_proceduret> p);
+    void set_decision_procedure(std::unique_ptr<stack_decision_proceduret> p);
     void set_prop(std::unique_ptr<propt> p);
     void set_ofstream(std::unique_ptr<std::ofstream> p);
 
     // the objects are deleted in the opposite order they appear below
     std::unique_ptr<std::ofstream> ofstream_ptr;
     std::unique_ptr<propt> prop_ptr;
-    std::unique_ptr<decision_proceduret> decision_procedure_ptr;
+    std::unique_ptr<stack_decision_proceduret> decision_procedure_ptr;
   };
 
   /// Returns a solvert object