Store clause counter value from satcheck_minisat instead of storing the clause itself

Author: Natasha Yogananda Jeppu

src/solvers/sat/satcheck_minisat2.cpp

@@ -140,8 +140,10 @@ void satcheck_minisat2_baset<T>::lcnf(const bvt &bv)
 
     solver->addClause_(c);
 
-    with_solver_hardness(
-      [&bv](solver_hardnesst &hardness) { hardness.register_clause(bv); });
+    size_t solver_clause_num = clause_counter;
+    with_solver_hardness([&bv, &solver_clause_num](solver_hardnesst &hardness) {
+      hardness.register_clause(bv, solver_clause_num);
+    });
     clause_counter++;
   }
   catch(const Minisat::OutOfMemoryException &)

src/solvers/solver_hardness.cpp

@@ -89,24 +89,28 @@ void solver_hardnesst::register_assertion_ssas(
   current_hardness = {};
 }
 
-void solver_hardnesst::register_clause(const bvt &bv)
+void solver_hardnesst::register_clause(
+  const bvt &bv,
+  const size_t solver_clause_num)
 {
   current_hardness.clauses++;
   current_hardness.literals += bv.size();
-  std::vector<int> clause;
 
   for(const auto &literal : bv)
   {
     current_hardness.variables.insert(literal.var_no());
-
-    int signed_literal = literal.var_no();
-    if(literal.sign())
-      signed_literal = -signed_literal;
-    clause.push_back(signed_literal);
   }
-  clause.push_back(0);
-  std::sort(clause.begin(), clause.end());
-  current_hardness.clause_set.push_back(clause);
+
+#ifdef DEBUG
+  std::cout << solver_clause_num << ": ";
+  for(const auto &literal : bv)
+    std::cout << literal.dimacs() << " ";
+  std::cout << "0\n";
+#endif
+
+  current_hardness.clause_set.push_back(solver_clause_num + 1);
+  std::sort(
+    current_hardness.clause_set.begin(), current_hardness.clause_set.end());
 }
 
 void solver_hardnesst::set_outfile(const std::string &file_name)
@@ -166,10 +170,8 @@ void solver_hardnesst::produce_report()
       json_arrayt sat_hardness_clause_set_json;
       for(auto const &clause : hardness.clause_set)
       {
-        json_arrayt clause_json;
-        for(auto const &lit : clause)
-          clause_json.push_back(json_numbert{std::to_string(lit)});
-        sat_hardness_clause_set_json.push_back(clause_json);
+        sat_hardness_clause_set_json.push_back(
+          json_numbert{std::to_string(clause)});
       }
       sat_hardness_json["ClauseSet"] = sat_hardness_clause_set_json;
 
@@ -208,10 +210,8 @@ void solver_hardnesst::produce_report()
     json_arrayt assertion_sat_hardness_clause_set_json;
     for(auto const &clause : assertion_stats.sat_hardness.clause_set)
     {
-      json_arrayt clause_json;
-      for(auto const &lit : clause)
-        clause_json.push_back(json_numbert{std::to_string(lit)});
-      assertion_sat_hardness_clause_set_json.push_back(clause_json);
+      assertion_sat_hardness_clause_set_json.push_back(
+        json_numbert{std::to_string(clause)});
     }
     assertion_hardness_json["ClauseSet"] =
       assertion_sat_hardness_clause_set_json;

src/solvers/solver_hardness.h

@@ -50,7 +50,7 @@ struct solver_hardnesst
     size_t clauses = 0;
     size_t literals = 0;
     std::unordered_set<size_t> variables = {};
-    std::vector<std::vector<int>> clause_set = {};
+    std::vector<int> clause_set = {};
 
     sat_hardnesst &operator+=(const sat_hardnesst &other);
   };
@@ -106,7 +106,9 @@ struct solver_hardnesst
   /// 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)
-  void register_clause(const bvt &bv);
+  /// \param solver_clause_num: clause counter value passed from
+  /// `satcheck_minisat2::lcnf`
+  void register_clause(const bvt &bv, const size_t solver_clause_num);
 
   void set_outfile(const std::string &file_name);