move solver_hardness.* from solvers/ to goto-symex/

kroening · kroening · commit 76cbf3e71979 · 2022-01-04T22:54:22.000Z
This class is inherently linked to goto-programs and goto-symex, and
introduces a surprising dependency on these corresponding includes into the
solver classes.

This commit moves these classes into the goto-symex directory, removing the
dependency by introducing a base class for the callback.
diff --git a/src/goto-checker/multi_path_symex_checker.cpp b/src/goto-checker/multi_path_symex_checker.cpp
@@ -15,7 +15,7 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include <util/ui_message.h>
 
-#include <solvers/hardness_collector.h>
+#include <goto-symex/solver_hardness.h>
 
 #include "bmc_util.h"
 #include "counterexample_beautification.h"
diff --git a/src/goto-checker/solver_factory.cpp b/src/goto-checker/solver_factory.cpp
@@ -36,6 +36,8 @@ Author: Daniel Kroening, Peter Schrammel
 #include <solvers/smt2_incremental/smt_solver_process.h>
 #include <solvers/strings/string_refinement.h>
 
+#include <goto-symex/solver_hardness.h>
+
 solver_factoryt::solver_factoryt(
   const optionst &_options,
   const namespacet &_ns,
@@ -190,11 +192,10 @@ make_satcheck_prop(message_handlert &message_handler, const optionst &options)
     if(
       auto hardness_collector = dynamic_cast<hardness_collectort *>(&*satcheck))
     {
-      hardness_collector->enable_hardness_collection();
-      hardness_collector->with_solver_hardness(
-        [&options](solver_hardnesst &hardness) {
-          hardness.set_outfile(options.get_option("write-solver-stats-to"));
-        });
+      std::unique_ptr<solver_hardnesst> solver_hardness =
+        util_make_unique<solver_hardnesst>();
+      solver_hardness->set_outfile(options.get_option("write-solver-stats-to"));
+      hardness_collector->solver_hardness = std::move(solver_hardness);
     }
     else
     {
diff --git a/src/goto-symex/Makefile b/src/goto-symex/Makefile
@@ -17,6 +17,7 @@ SRC = auto_objects.cpp \
       show_program.cpp \
       show_vcc.cpp \
       slice.cpp \
+      solver_hardness.cpp \
       ssa_step.cpp \
       symex_assign.cpp \
       symex_atomic_section.cpp \
diff --git a/src/goto-symex/solver_hardness.cpp b/src/goto-symex/solver_hardness.cpp
diff --git a/src/goto-symex/solver_hardness.h b/src/goto-symex/solver_hardness.h
@@ -9,7 +9,8 @@ Author: Diffblue Ltd.
 #ifndef CPROVER_SOLVERS_SOLVER_HARDNESS_H
 #define CPROVER_SOLVERS_SOLVER_HARDNESS_H
 
-#include <solvers/prop/literal.h>
+#include <solvers/hardness_collector.h>
+#include <solvers/prop/prop_conv_solver.h>
 
 #include <fstream>
 #include <string>
@@ -38,7 +39,7 @@ Author: Diffblue Ltd.
 /// derived class of \ref cnft for SAT solving). For this purpose the object
 /// lives in the \ref solver_factoryt::solvert and pointers are passed to both
 /// \ref decision_proceduret and \ref propt.
-struct solver_hardnesst
+struct solver_hardnesst : public clause_hardness_collectort
 {
   // From SAT solver we collect the number of clauses, the number of literals
   // and the number of distinct variables that were used in all clauses.
@@ -160,4 +161,26 @@ struct hash<solver_hardnesst::hardness_ssa_keyt>
 };
 } // namespace std
 
+static inline void with_solver_hardness(
+  decision_proceduret &maybe_hardness_collector,
+  std::function<void(solver_hardnesst &hardness)> handler)
+{
+  // FIXME I am wondering if there is a way to do this that is a bit less
+  // dynamically typed.
+  if(
+    auto prop_conv_solver =
+      dynamic_cast<prop_conv_solvert *>(&maybe_hardness_collector))
+  {
+    if(auto hardness_collector = prop_conv_solver->get_hardness_collector())
+    {
+      if(hardness_collector->solver_hardness)
+      {
+        auto &solver_hardness = static_cast<solver_hardnesst &>(
+          *(hardness_collector->solver_hardness));
+        handler(solver_hardness);
+      }
+    }
+  }
+}
+
 #endif // CPROVER_SOLVERS_SOLVER_HARDNESS_H
diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp
@@ -16,12 +16,10 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/std_expr.h>
 
-#include <solvers/decision_procedure.h>
-#include <solvers/hardness_collector.h>
-
+#include "solver_hardness.h"
 #include "ssa_step.h"
 
-static hardness_collectort::handlert
+static std::function<void(solver_hardnesst &)>
 hardness_register_ssa(std::size_t step_index, const SSA_stept &step)
 {
   return [step_index, &step](solver_hardnesst &hardness) {
diff --git a/src/solvers/Makefile b/src/solvers/Makefile
@@ -80,7 +80,6 @@ SRC = $(BOOLEFORCE_SRC) \
       $(SQUOLEM2_SRC) \
       $(CADICAL_SRC) \
       decision_procedure.cpp \
-      solver_hardness.cpp \
       flattening/arrays.cpp \
       flattening/boolbv.cpp \
       flattening/boolbv_abs.cpp \
diff --git a/src/solvers/flattening/arrays.h b/src/solvers/flattening/arrays.h
@@ -20,6 +20,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "equality.h"
 
+class array_comprehension_exprt;
+class array_exprt;
 class array_of_exprt;
 class equal_exprt;
 class if_exprt;
diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h
@@ -37,6 +37,7 @@ class floatbv_typecast_exprt;
 class ieee_float_op_exprt;
 class member_exprt;
 class replication_exprt;
+class union_typet;
 
 class boolbvt:public arrayst
 {
diff --git a/src/solvers/flattening/boolbv_get.cpp b/src/solvers/flattening/boolbv_get.cpp
@@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
+#include <util/namespace.h>
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
 #include <util/threeval.h>
diff --git a/src/solvers/flattening/boolbv_member.cpp b/src/solvers/flattening/boolbv_member.cpp
@@ -9,6 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "boolbv.h"
 
 #include <util/c_types.h>
+#include <util/namespace.h>
 
 static bvt convert_member_struct(
   const member_exprt &expr,
diff --git a/src/solvers/flattening/boolbv_struct.cpp b/src/solvers/flattening/boolbv_struct.cpp
@@ -8,6 +8,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "boolbv.h"
 
+#include <util/namespace.h>
+
 bvt boolbvt::convert_struct(const struct_exprt &expr)
 {
   const struct_typet &struct_type=to_struct_type(ns.follow(expr.type()));
diff --git a/src/solvers/flattening/boolbv_typecast.cpp b/src/solvers/flattening/boolbv_typecast.cpp
@@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/bitvector_types.h>
 #include <util/c_types.h>
+#include <util/namespace.h>
 
 #include <solvers/floatbv/float_utils.h>
 
diff --git a/src/solvers/flattening/boolbv_update.cpp b/src/solvers/flattening/boolbv_update.cpp
@@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
+#include <util/namespace.h>
 
 bvt boolbvt::convert_update(const update_exprt &expr)
 {
diff --git a/src/solvers/flattening/boolbv_with.cpp b/src/solvers/flattening/boolbv_with.cpp
@@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
+#include <util/namespace.h>
 #include <util/std_expr.h>
 
 bvt boolbvt::convert_with(const with_exprt &expr)
diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp
@@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/c_types.h>
 #include <util/config.h>
 #include <util/exception_utils.h>
+#include <util/namespace.h>
 #include <util/pointer_expr.h>
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
diff --git a/src/solvers/hardness_collector.h b/src/solvers/hardness_collector.h
@@ -14,32 +14,37 @@ Author: Diffblue Ltd.
 #ifndef CPROVER_SOLVERS_HARDNESS_COLLECTOR_H
 #define CPROVER_SOLVERS_HARDNESS_COLLECTOR_H
 
-#include <functional>
-#include <solvers/solver_hardness.h>
+#include <solvers/prop/literal.h>
 
-class exprt;
+#include <memory>
 
-class hardness_collectort
+struct solver_hardnesst;
+
+class clause_hardness_collectort
 {
 public:
-  using handlert = std::function<void(solver_hardnesst &)>;
-  virtual void with_solver_hardness(handlert handler) = 0;
-  virtual void enable_hardness_collection() = 0;
-  virtual ~hardness_collectort() = default;
+  /// Called e.g. from the `satcheck_minisat2::lcnf`, this function adds the
+  ///   complexity statistics from the last SAT query to the `current_ssa_key`.
+  /// \param bv: the clause (vector of literals)
+  /// \param cnf: processed clause
+  /// \param cnf_clause_index: index of clause in dimacs output
+  /// \param register_cnf: negation of boolean variable tracking if the clause
+  /// can be eliminated
+  virtual void register_clause(
+    const bvt &bv,
+    const bvt &cnf,
+    const size_t cnf_clause_index,
+    bool register_cnf) = 0;
+
+  virtual ~clause_hardness_collectort()
+  {
+  }
 };
 
-template <typename T>
-void with_solver_hardness(
-  T &maybe_hardness_collector,
-  hardness_collectort::handlert handler)
+class hardness_collectort
 {
-  // FIXME I am wondering if there is a way to do this that is a bit less
-  // dynamically typed.
-  if(
-    auto hardness_collector =
-      dynamic_cast<hardness_collectort *>(&maybe_hardness_collector))
-  {
-    hardness_collector->with_solver_hardness(handler);
-  }
-}
+public:
+  std::unique_ptr<clause_hardness_collectort> solver_hardness;
+};
+
 #endif // CPROVER_SOLVERS_HARDNESS_COLLECTOR_H
diff --git a/src/solvers/module_dependencies.txt b/src/solvers/module_dependencies.txt
@@ -1,5 +1,4 @@
 cplusplus # cudd
 cudd
-goto-programs
 solvers
 util
diff --git a/src/solvers/prop/prop_conv_solver.cpp b/src/solvers/prop/prop_conv_solver.cpp
@@ -559,16 +559,3 @@ std::string prop_conv_solvert::decision_procedure_text() const
 {
   return "propositional reduction";
 }
-
-void prop_conv_solvert::with_solver_hardness(
-  hardness_collectort::handlert handler)
-{
-  ::with_solver_hardness(prop, handler);
-}
-void prop_conv_solvert::enable_hardness_collection()
-{
-  if(auto hardness_collector = dynamic_cast<hardness_collectort *>(&prop))
-  {
-    hardness_collector->enable_hardness_collection();
-  }
-}
diff --git a/src/solvers/prop/prop_conv_solver.h b/src/solvers/prop/prop_conv_solver.h
@@ -22,10 +22,11 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "prop_conv.h"
 #include "solver_resource_limits.h"
 
+class equal_exprt;
+
 class prop_conv_solvert : public conflict_providert,
                           public prop_convt,
-                          public solver_resource_limitst,
-                          public hardness_collectort
+                          public solver_resource_limitst
 {
 public:
   prop_conv_solvert(propt &_prop, message_handlert &message_handler)
@@ -95,8 +96,10 @@ class prop_conv_solvert : public conflict_providert,
 
   std::size_t get_number_of_solver_calls() const override;
 
-  void with_solver_hardness(handlert handler) override;
-  void enable_hardness_collection() override;
+  hardness_collectort *get_hardness_collector()
+  {
+    return dynamic_cast<hardness_collectort *>(&prop);
+  }
 
 protected:
   virtual void post_process();
diff --git a/src/solvers/sat/satcheck_cadical.cpp b/src/solvers/sat/satcheck_cadical.cpp
@@ -63,7 +63,8 @@ void satcheck_cadicalt::lcnf(const bvt &bv)
   }
   solver->add(0); // terminate clause
 
-  with_solver_hardness([this, &bv](solver_hardnesst &hardness) {
+  if(solver_hardness)
+  {
     // To map clauses to lines of program code, track clause indices in the
     // dimacs cnf output. Dimacs output is generated after processing
     // clauses to remove duplicates and clauses that are trivially true.
@@ -77,8 +78,9 @@ void satcheck_cadicalt::lcnf(const bvt &bv)
     if(!clause_removed)
       cnf_clause_index++;
 
-    hardness.register_clause(bv, cnf, cnf_clause_index, !clause_removed);
-  });
+    solver_hardness->register_clause(
+      bv, cnf, cnf_clause_index, !clause_removed);
+  }
 
   clause_counter++;
 }
diff --git a/src/solvers/sat/satcheck_cadical.h b/src/solvers/sat/satcheck_cadical.h
@@ -42,29 +42,13 @@ class satcheck_cadicalt : public cnf_solvert, public hardness_collectort
   }
   bool is_in_conflict(literalt a) const override;
 
-  void
-  with_solver_hardness(std::function<void(solver_hardnesst &)> handler) override
-  {
-    if(solver_hardness.has_value())
-    {
-      handler(solver_hardness.value());
-    }
-  }
-
-  void enable_hardness_collection() override
-  {
-    solver_hardness = solver_hardnesst{};
-  }
-
 protected:
   resultt do_prop_solve() override;
 
   // NOLINTNEXTLINE(readability/identifiers)
   CaDiCaL::Solver * solver;
 
   bvt assumptions;
-
-  optionalt<solver_hardnesst> solver_hardness;
 };
 
 #endif // CPROVER_SOLVERS_SAT_SATCHECK_CADICAL_H
diff --git a/src/solvers/sat/satcheck_glucose.cpp b/src/solvers/sat/satcheck_glucose.cpp
@@ -123,7 +123,8 @@ void satcheck_glucose_baset<T>::lcnf(const bvt &bv)
 
     solver->addClause_(c);
 
-    with_solver_hardness([this, &bv](solver_hardnesst &hardness) {
+    if(solver_hardness)
+    {
       // To map clauses to lines of program code, track clause indices in the
       // dimacs cnf output. Dimacs output is generated after processing
       // clauses to remove duplicates and clauses that are trivially true.
@@ -137,8 +138,9 @@ void satcheck_glucose_baset<T>::lcnf(const bvt &bv)
       if(!clause_removed)
         cnf_clause_index++;
 
-      hardness.register_clause(bv, cnf, cnf_clause_index, !clause_removed);
-    });
+      solver_hardness->register_clause(
+        bv, cnf, cnf_clause_index, !clause_removed);
+    }
 
     clause_counter++;
   }
diff --git a/src/solvers/sat/satcheck_glucose.h b/src/solvers/sat/satcheck_glucose.h
@@ -57,29 +57,13 @@ class satcheck_glucose_baset : public cnf_solvert, public hardness_collectort
     return true;
   }
 
-  void
-  with_solver_hardness(std::function<void(solver_hardnesst &)> handler) override
-  {
-    if(solver_hardness.has_value())
-    {
-      handler(solver_hardness.value());
-    }
-  }
-
-  void enable_hardness_collection() override
-  {
-    solver_hardness = solver_hardnesst{};
-  }
-
 protected:
   resultt do_prop_solve() override;
 
   std::unique_ptr<T> solver;
 
   void add_variables();
   bvt assumptions;
-
-  optionalt<solver_hardnesst> solver_hardness;
 };
 
 class satcheck_glucose_no_simplifiert:
diff --git a/src/solvers/sat/satcheck_ipasir.cpp b/src/solvers/sat/satcheck_ipasir.cpp
diff --git a/src/solvers/sat/satcheck_ipasir.h b/src/solvers/sat/satcheck_ipasir.h
diff --git a/src/solvers/sat/satcheck_minisat2.cpp b/src/solvers/sat/satcheck_minisat2.cpp
diff --git a/src/solvers/sat/satcheck_minisat2.h b/src/solvers/sat/satcheck_minisat2.h
diff --git a/src/solvers/strings/string_constraint.cpp b/src/solvers/strings/string_constraint.cpp
diff --git a/unit/solvers/bdd/miniBDD/miniBDD.cpp b/unit/solvers/bdd/miniBDD/miniBDD.cpp

Original file line number	Diff line number	Diff line change
`@@ -37,6 +37,7 @@ class floatbv_typecast_exprt;`
`37`	`37`	`class ieee_float_op_exprt;`
`38`	`38`	`class member_exprt;`
`39`	`39`	`class replication_exprt;`
	`40`	`+class union_typet;`
`40`	`41`
`41`	`42`	`class boolbvt:public arrayst`
`42`	`43`	`{`