Refactoring hardness collection to not expose prop

Author: hannes-steffenhagen-diffblue

src/goto-checker/bmc_util.cpp

@@ -26,7 +26,6 @@ Author: Daniel Kroening, Peter Schrammel
 #include <linking/static_lifetime_init.h>
 
 #include <solvers/decision_procedure.h>
-#include <solvers/flattening/boolbv.h>
 
 #include <util/make_unique.h>
 #include <util/ui_message.h>
@@ -150,22 +149,13 @@ void output_graphml(
 
 void convert_symex_target_equation(
   symex_target_equationt &equation,
-  goto_symex_property_decidert &property_decider,
+  decision_proceduret &decision_procedure,
   message_handlert &message_handler)
 {
   messaget msg(message_handler);
   msg.status() << "converting SSA" << messaget::eom;
 
-  // convert SSA
-  if(dynamic_cast<boolbvt *>(&property_decider.get_decision_procedure()))
-  {
-    equation.convert(
-      property_decider.get_decision_procedure(), property_decider.get_prop());
-  }
-  else
-  {
-    equation.convert(property_decider.get_decision_procedure());
-  }
+  equation.convert(decision_procedure);
 }
 
 std::unique_ptr<memory_model_baset>
@@ -370,7 +360,8 @@ std::chrono::duration<double> prepare_property_decider(
     << property_decider.get_decision_procedure().decision_procedure_text()
     << messaget::eom;
 
-  convert_symex_target_equation(equation, property_decider, ui_message_handler);
+  convert_symex_target_equation(
+    equation, property_decider.get_decision_procedure(), ui_message_handler);
   property_decider.update_properties_goals_from_symex_target_equation(
     properties);
   property_decider.convert_goals();

src/goto-checker/bmc_util.h

@@ -35,9 +35,9 @@ struct trace_optionst;
 class ui_message_handlert;
 
 void convert_symex_target_equation(
-  symex_target_equationt &,
-  goto_symex_property_decidert &,
-  message_handlert &);
+  symex_target_equationt &equation,
+  decision_proceduret &decision_procedure,
+  message_handlert &message_handler);
 
 /// Returns a function that checks whether an SSA step is an assertion
 /// with \p property_id. Usually used for `build_goto_trace`.

src/goto-checker/goto_symex_property_decider.cpp

@@ -110,11 +110,6 @@ goto_symex_property_decidert::get_decision_procedure() const
   return solver->decision_procedure();
 }
 
-propt &goto_symex_property_decidert::get_prop() const
-{
-  return solver->prop();
-}
-
 stack_decision_proceduret &
 goto_symex_property_decidert::get_stack_decision_procedure() const
 {

src/goto-checker/goto_symex_property_decider.h

@@ -44,9 +44,6 @@ class goto_symex_property_decidert
   /// Calls solve() on the solver instance
   decision_proceduret::resultt solve();
 
-  /// Returns the prop
-  propt &get_prop() const;
-
   /// Returns the solver instance
   decision_proceduret &get_decision_procedure() const;
 
@@ -68,7 +65,6 @@ class goto_symex_property_decidert
     std::unordered_set<irep_idt> &updated_properties,
     decision_proceduret::resultt dec_result,
     bool set_pass = true) const;
-
 protected:
   const optionst &options;
   ui_message_handlert &ui_message_handler;

src/goto-checker/multi_path_symex_checker.cpp

@@ -13,6 +13,8 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include <chrono>
 
+#include <solvers/hardness_collector.h>
+
 #include "bmc_util.h"
 #include "counterexample_beautification.h"
 #include "goto_symex_fault_localizer.h"
@@ -25,17 +27,6 @@ multi_path_symex_checkert::multi_path_symex_checkert(
     equation_generated(false),
     property_decider(options, ui_message_handler, equation, ns)
 {
-  if(options.is_set("write-solver-stats-to"))
-  {
-    if(
-      auto hardness_collector =
-        dynamic_cast<hardness_collectort *>(&property_decider.get_prop()))
-    {
-      hardness_collector->enable_hardness_collection();
-      hardness_collector->get_solver_hardness().set_outfile(
-        options.get_option("write-solver-stats-to"));
-    }
-  }
 }
 
 incremental_goto_checkert::resultt multi_path_symex_checkert::
@@ -171,14 +162,8 @@ void multi_path_symex_checkert::report()
 {
   if(options.is_set("write-solver-stats-to"))
   {
-    if(
-      auto hardness_collector =
-        dynamic_cast<hardness_collectort *>(&property_decider.get_prop()))
-    {
-      if(hardness_collector->is_hardness_collection_enabled())
-      {
-        hardness_collector->get_solver_hardness().produce_report();
-      }
-    }
+    with_solver_hardness(
+      property_decider.get_decision_procedure(),
+      [](solver_hardnesst &hardness) { hardness.produce_report(); });
   }
 }

src/goto-checker/single_loop_incremental_symex_checker.cpp

@@ -89,15 +89,15 @@ operator()(propertiest &properties)
 
         log.status() << "converting SSA" << messaget::eom;
         equation.convert_without_assertions(
-          property_decider.get_decision_procedure(), nullptr);
+          property_decider.get_decision_procedure());
 
         property_decider.update_properties_goals_from_symex_target_equation(
           properties);
 
         // We convert the assertions in a new context.
         property_decider.get_stack_decision_procedure().push();
         equation.convert_assertions(
-          property_decider.get_decision_procedure(), nullptr, false);
+          property_decider.get_decision_procedure(), false);
         property_decider.convert_goals();
 
         current_equation_converted = true;

src/goto-checker/solver_factory.cpp

@@ -173,21 +173,35 @@ smt2_dect::solvert solver_factoryt::get_smt2_solver_type() const
   return s;
 }
 
+template <typename SatcheckT>
+static std::unique_ptr<SatcheckT>
+make_satcheck_prop(message_handlert &message_handler, const optionst &options)
+{
+  auto satcheck = util_make_unique<SatcheckT>(message_handler);
+  if(options.is_set("write-solver-stats-to"))
+  {
+    satcheck->enable_hardness_collection();
+    satcheck->with_solver_hardness([&options](solver_hardnesst &hardness) {
+      hardness.set_outfile(options.get_option("write-solver-stats-to"));
+    });
+  }
+  return satcheck;
+}
+
 std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_default()
 {
   auto solver = util_make_unique<solvert>();
-
   if(
     options.get_bool_option("beautify") ||
     !options.get_bool_option("sat-preprocessor")) // no simplifier
   {
     // simplifier won't work with beautification
     solver->set_prop(
-      util_make_unique<satcheck_no_simplifiert>(message_handler));
+      make_satcheck_prop<satcheck_no_simplifiert>(message_handler, options));
   }
   else // with simplifier
   {
-    solver->set_prop(util_make_unique<satcheckt>(message_handler));
+    solver->set_prop(make_satcheck_prop<satcheckt>(message_handler, options));
   }
 
   auto bv_pointers =
@@ -225,9 +239,10 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_bv_refinement()
     if(options.get_bool_option("sat-preprocessor"))
     {
       no_beautification();
-      return util_make_unique<satcheckt>(message_handler);
+      return make_satcheck_prop<satcheckt>(message_handler, options);
     }
-    return util_make_unique<satcheck_no_simplifiert>(message_handler);
+    return make_satcheck_prop<satcheck_no_simplifiert>(
+      message_handler, options);
   }();
 
   bv_refinementt::infot info;
@@ -258,7 +273,8 @@ solver_factoryt::get_string_refinement()
 {
   string_refinementt::infot info;
   info.ns = &ns;
-  auto prop = util_make_unique<satcheck_no_simplifiert>(message_handler);
+  auto prop =
+    make_satcheck_prop<satcheck_no_simplifiert>(message_handler, options);
   info.prop = prop.get();
   info.refinement_bound = DEFAULT_MAX_NB_REFINEMENT;
   info.output_xml = output_xml_in_refinement;