Merge pull request #7507 from peterschrammel/solver-stats-bug

Fix bug in solver hardness stats

Author: tautschnig

regression/solver-hardness/solver-hardness-simple/main.c

@@ -5,5 +5,6 @@ int main()
   int a;
   int b;
   assert(a + b < 10);
+  assert(a < 10);
   return 0;
 }

regression/solver-hardness/solver-hardness-simple/test.desc

@@ -5,5 +5,6 @@ main.c
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 \"SAT_hardness\":\{(\"ClauseSet\":\[.*\]|\"Clauses\":\d+|\"Variables\":\d+|\"Literals\":\d+),(\"ClauseSet\":\[.*\]|\"Clauses\":\d+|\"Variables\":\d+|\"Literals\":\d+),(\"ClauseSet\":\[.*\]|\"Clauses\":\d+|\"Variables\":\d+|\"Literals\":\d+),(\"ClauseSet\":\[.*\]|\"Clauses\":\d+|\"Variables\":\d+|\"Literals\":\d+)\}
+\"GOTO_ID\":32,\"SAT_hardness\":\{\"ClauseSet\":\[.*,571\],\"Clauses\":571
 --
 ^warning: ignoring

src/goto-checker/goto_symex_property_decider.cpp

@@ -13,6 +13,7 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include <util/ui_message.h>
 
+#include <goto-symex/solver_hardness.h>
 #include <solvers/prop/prop.h> // IWYU pragma: keep
 
 goto_symex_property_decidert::goto_symex_property_decidert(
@@ -83,6 +84,7 @@ void goto_symex_property_decidert::add_constraint_from_goals(
   std::function<bool(const irep_idt &)> select_property)
 {
   exprt::operandst disjuncts;
+  decision_proceduret &decision_procedure = solver->decision_procedure();
 
   for(const auto &goal_pair : goal_map)
   {
@@ -95,7 +97,16 @@ void goto_symex_property_decidert::add_constraint_from_goals(
   }
 
   // this is 'false' if there are no disjuncts
-  solver->decision_procedure().set_to_true(disjunction(disjuncts));
+  exprt goal_disjunction = disjunction(disjuncts);
+  decision_procedure.set_to_true(goal_disjunction);
+
+  with_solver_hardness(decision_procedure, [](solver_hardnesst &hardness) {
+    // SSA expr and involved steps have already been collected
+    // in symex_target_equationt::convert_assertions
+    exprt ssa_expr_unused;
+    std::vector<goto_programt::const_targett> involved_steps_unused;
+    hardness.register_assertion_ssas(ssa_expr_unused, involved_steps_unused);
+  });
 }
 
 decision_proceduret::resultt goto_symex_property_decidert::solve()

src/goto-symex/solver_hardness.cpp

@@ -44,7 +44,7 @@ bool solver_hardnesst::assertion_statst::empty() const
 
 void solver_hardnesst::register_ssa(
   std::size_t ssa_index,
-  const exprt ssa_expression,
+  const exprt &ssa_expression,
   goto_programt::const_targett pc)
 {
   PRECONDITION(ssa_index < hardness_stats.size());
@@ -73,15 +73,16 @@ void solver_hardnesst::register_ssa_size(std::size_t size)
 }
 
 void solver_hardnesst::register_assertion_ssas(
-  const exprt ssa_expression,
+  const exprt &ssa_expression,
   const std::vector<goto_programt::const_targett> &pcs)
 {
   if(assertion_stats.empty())
-    return;
+  {
+    assertion_stats.ssa_expression = expr2string(ssa_expression);
+    assertion_stats.pcs = pcs;
+  }
 
-  assertion_stats.sat_hardness = current_hardness;
-  assertion_stats.ssa_expression = expr2string(ssa_expression);
-  assertion_stats.pcs = pcs;
+  assertion_stats.sat_hardness += current_hardness;
   current_ssa_key = {};
   current_hardness = {};
 }
@@ -378,7 +379,7 @@ solver_hardnesst::goto_instruction2string(goto_programt::const_targett pc)
   return out.str();
 }
 
-std::string solver_hardnesst::expr2string(const exprt expr)
+std::string solver_hardnesst::expr2string(const exprt &expr)
 {
   std::stringstream ss;
   ss << format(expr);

src/goto-symex/solver_hardness.h

@@ -82,7 +82,7 @@ struct solver_hardnesst : public clause_hardness_collectort
   /// \param pc: the GOTO instruction iterator for this SSA step
   void register_ssa(
     std::size_t ssa_index,
-    const exprt ssa_expression,
+    const exprt &ssa_expression,
     goto_programt::const_targett pc);
 
   void register_ssa_size(std::size_t size);
@@ -95,7 +95,7 @@ struct solver_hardnesst : public clause_hardness_collectort
   /// \param pcs: all GOTO instruction iterators that contributed in the
   ///   disjunction
   void register_assertion_ssas(
-    const exprt ssa_expression,
+    const exprt &ssa_expression,
     const std::vector<goto_programt::const_targett> &pcs);
 
   /// Called e.g. from the `satcheck_minisat2::lcnf`, this function adds the
@@ -130,7 +130,7 @@ struct solver_hardnesst : public clause_hardness_collectort
   // A minor modification of \ref goto_programt::output_instruction
   static std::string goto_instruction2string(goto_programt::const_targett pc);
 
-  static std::string expr2string(const exprt expr);
+  static std::string expr2string(const exprt &expr);
 
   std::string outfile;
   std::vector<std::unordered_map<hardness_ssa_keyt, sat_hardnesst>>