Merge pull request #8421 from tautschnig/no-boolbv-dynamic_cast

Remove dynamic_cast from counterexample beautification code path

Author: kroening

src/goto-checker/goto_symex_property_decider.cpp

@@ -120,6 +120,11 @@ goto_symex_property_decidert::get_decision_procedure() const
   return solver->decision_procedure();
 }
 
+boolbvt &goto_symex_property_decidert::get_boolbv_decision_procedure() const
+{
+  return solver->boolbv_decision_procedure();
+}
+
 symex_target_equationt &goto_symex_property_decidert::get_equation() const
 {
   return equation;

src/goto-checker/goto_symex_property_decider.h

@@ -47,6 +47,9 @@ class goto_symex_property_decidert
   /// Returns the solver instance
   stack_decision_proceduret &get_decision_procedure() const;
 
+  /// Returns the solver instance
+  boolbvt &get_boolbv_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,8 +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_decision_procedure()),
-      equation);
+      property_decider.get_boolbv_decision_procedure(), equation);
   }
 
   goto_tracet goto_trace;

src/goto-checker/single_loop_incremental_symex_checker.cpp

@@ -207,8 +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_decision_procedure()),
-      equation);
+      property_decider.get_boolbv_decision_procedure(), equation);
   }
 
   goto_tracet goto_trace;

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_decision_procedure()),
+      property_decider->get_boolbv_decision_procedure(),
       property_decider->get_equation());
   }
 

src/goto-checker/solver_factory.cpp

@@ -29,7 +29,6 @@ Author: Daniel Kroening, Peter Schrammel
 #include <solvers/sat/satcheck.h>
 #include <solvers/smt2_incremental/smt2_incremental_decision_procedure.h>
 #include <solvers/smt2_incremental/smt_solver_process.h>
-#include <solvers/stack_decision_procedure.h>
 #include <solvers/strings/string_refinement.h>
 
 #include <iostream>
@@ -65,10 +64,28 @@ solver_factoryt::solvert::solvert(
 {
 }
 
+solver_factoryt::solvert::solvert(
+  std::unique_ptr<boolbvt> p1,
+  std::unique_ptr<propt> p2)
+  : prop_ptr(std::move(p2)), decision_procedure_is_boolbvt_ptr(std::move(p1))
+{
+}
+
 stack_decision_proceduret &solver_factoryt::solvert::decision_procedure() const
 {
-  PRECONDITION(decision_procedure_ptr != nullptr);
-  return *decision_procedure_ptr;
+  PRECONDITION(
+    (decision_procedure_ptr != nullptr) !=
+    (decision_procedure_is_boolbvt_ptr != nullptr));
+  if(decision_procedure_ptr)
+    return *decision_procedure_ptr;
+  else
+    return *decision_procedure_is_boolbvt_ptr;
+}
+
+boolbvt &solver_factoryt::solvert::boolbv_decision_procedure() const
+{
+  PRECONDITION(decision_procedure_is_boolbvt_ptr != nullptr);
+  return *decision_procedure_is_boolbvt_ptr;
 }
 
 void solver_factoryt::set_decision_procedure_time_limit(
@@ -81,22 +98,6 @@ void solver_factoryt::set_decision_procedure_time_limit(
     decision_procedure.set_time_limit_seconds(timeout_seconds);
 }
 
-void solver_factoryt::solvert::set_decision_procedure(
-  std::unique_ptr<stack_decision_proceduret> p)
-{
-  decision_procedure_ptr = std::move(p);
-}
-
-void solver_factoryt::solvert::set_prop(std::unique_ptr<propt> p)
-{
-  prop_ptr = std::move(p);
-}
-
-void solver_factoryt::solvert::set_ofstream(std::unique_ptr<std::ofstream> p)
-{
-  ofstream_ptr = std::move(p);
-}
-
 std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_solver()
 {
   if(options.get_bool_option("dimacs"))
@@ -339,8 +340,8 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_default()
 
   set_decision_procedure_time_limit(*bv_pointers);
 
-  return std::make_unique<solvert>(
-    std::move(bv_pointers), std::move(sat_solver));
+  std::unique_ptr<boolbvt> boolbv = std::move(bv_pointers);
+  return std::make_unique<solvert>(std::move(boolbv), std::move(sat_solver));
 }
 
 std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_dimacs()
@@ -352,7 +353,7 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_dimacs()
 
   std::string filename = options.get_option("outfile");
 
-  auto bv_dimacs =
+  std::unique_ptr<boolbvt> bv_dimacs =
     std::make_unique<bv_dimacst>(ns, *prop, message_handler, filename);
 
   return std::make_unique<solvert>(std::move(bv_dimacs), std::move(prop));
@@ -367,7 +368,8 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_external_sat()
   auto prop =
     std::make_unique<external_satt>(message_handler, external_sat_solver);
 
-  auto bv_pointers = std::make_unique<bv_pointerst>(ns, *prop, message_handler);
+  std::unique_ptr<boolbvt> bv_pointers =
+    std::make_unique<bv_pointerst>(ns, *prop, message_handler);
 
   return std::make_unique<solvert>(std::move(bv_pointers), std::move(prop));
 }
@@ -390,7 +392,8 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_bv_refinement()
   info.refine_arithmetic = options.get_bool_option("refine-arithmetic");
   info.message_handler = &message_handler;
 
-  auto decision_procedure = std::make_unique<bv_refinementt>(info);
+  std::unique_ptr<boolbvt> decision_procedure =
+    std::make_unique<bv_refinementt>(info);
   set_decision_procedure_time_limit(*decision_procedure);
   return std::make_unique<solvert>(
     std::move(decision_procedure), std::move(prop));
@@ -415,7 +418,8 @@ solver_factoryt::get_string_refinement()
   info.refine_arithmetic = options.get_bool_option("refine-arithmetic");
   info.message_handler = &message_handler;
 
-  auto decision_procedure = std::make_unique<string_refinementt>(info);
+  std::unique_ptr<boolbvt> decision_procedure =
+    std::make_unique<string_refinementt>(info);
   set_decision_procedure_time_limit(*decision_procedure);
   return std::make_unique<solvert>(
     std::move(decision_procedure), std::move(prop));

src/goto-checker/solver_factory.h

@@ -12,7 +12,7 @@ Author: Daniel Kroening, Peter Schrammel
 #ifndef CPROVER_GOTO_CHECKER_SOLVER_FACTORY_H
 #define CPROVER_GOTO_CHECKER_SOLVER_FACTORY_H
 
-#include <solvers/prop/prop.h>
+#include <solvers/flattening/boolbv.h>
 #include <solvers/smt2/smt2_dec.h>
 
 #include <memory>
@@ -45,17 +45,17 @@ class solver_factoryt final
     solvert(
       std::unique_ptr<stack_decision_proceduret> p1,
       std::unique_ptr<std::ofstream> p2);
+    solvert(std::unique_ptr<boolbvt> p1, std::unique_ptr<propt> p2);
 
     stack_decision_proceduret &decision_procedure() const;
+    boolbvt &boolbv_decision_procedure() const;
 
-    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);
-
+  private:
     // 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<stack_decision_proceduret> decision_procedure_ptr;
+    std::unique_ptr<boolbvt> decision_procedure_is_boolbvt_ptr;
   };
 
   /// Returns a solvert object