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

Add comment to explain solver_clause_num + 1 in solver hardness, change <int> to <size_t>

Remove sorting of clause set keeping performance in mind

Add additional utility to map program lines to clauses in --dimacs output

clang format

Author: Natasha Yogananda Jeppu

src/solvers/sat/satcheck_minisat2.cpp

@@ -140,10 +140,22 @@ void satcheck_minisat2_baset<T>::lcnf(const bvt &bv)
 
     solver->addClause_(c);
 
-    size_t solver_clause_num = clause_counter;
-    with_solver_hardness([&bv, &solver_clause_num](solver_hardnesst &hardness) {
-      hardness.register_clause(bv, solver_clause_num);
-    });
+    // 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. Here, a clause
+    // is checked to see if it can be thus eliminated. If not, add the clause
+    // index to list of clauses in solver_hardnesst::register_clause().
+    static size_t cnf_clause_index = 0;
+    bvt cnf;
+    bool clause_removed = process_clause(bv, cnf);
+
+    if(!clause_removed)
+      cnf_clause_index++;
+
+    with_solver_hardness(
+      [&bv, &cnf, &clause_removed](solver_hardnesst &hardness) {
+        hardness.register_clause(bv, cnf, cnf_clause_index, !clause_removed);
+      });
     clause_counter++;
   }
   catch(const Minisat::OutOfMemoryException &)

src/solvers/solver_hardness.cpp

@@ -91,7 +91,9 @@ void solver_hardnesst::register_assertion_ssas(
 
 void solver_hardnesst::register_clause(
   const bvt &bv,
-  const size_t solver_clause_num)
+  const bvt &cnf,
+  const size_t cnf_clause_index,
+  bool register_cnf)
 {
   current_hardness.clauses++;
   current_hardness.literals += bv.size();
@@ -101,16 +103,16 @@ void solver_hardnesst::register_clause(
     current_hardness.variables.insert(literal.var_no());
   }
 
+  if(register_cnf)
+  {
 #ifdef DEBUG
-  std::cout << solver_clause_num << ": ";
-  for(const auto &literal : bv)
-    std::cout << literal.dimacs() << " ";
-  std::cout << "0\n";
+    std::cout << cnf_clause_index << ": ";
+    for(const auto &literal : cnf)
+      std::cout << literal.dimacs() << " ";
+    std::cout << "0\n";
 #endif
-
-  // The clause_counter is incremented after the call to register_clause.
-  // Here we add 1 to solver_clause_num to incorporate this increment.
-  current_hardness.clause_set.push_back(solver_clause_num + 1);
+    current_hardness.clause_set.push_back(cnf_clause_index);
+  }
 }
 
 void solver_hardnesst::set_outfile(const std::string &file_name)

src/solvers/solver_hardness.h

@@ -108,7 +108,11 @@ struct solver_hardnesst
   /// \param bv: the clause (vector of literals)
   /// \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 register_clause(
+    const bvt &bv,
+    const bvt &cnf,
+    const size_t cnf_clause_index,
+    bool register_cnf);
 
   void set_outfile(const std::string &file_name);