Merge pull request #5708 from tautschnig/minisat-cleanup

satcheck minisat2: make all solver hardness processing conditional

Author: tautschnig

src/solvers/sat/cnf.cpp

@@ -413,7 +413,7 @@ bvt cnft::eliminate_duplicates(const bvt &bv)
 
 /// filter 'true' from clause, eliminate duplicates, recognise trivially
 /// satisfied clauses
-bool cnft::process_clause(const bvt &bv, bvt &dest)
+bool cnft::process_clause(const bvt &bv, bvt &dest) const
 {
   dest.clear();
 

src/solvers/sat/cnf.h

@@ -55,7 +55,7 @@ class cnft:public propt
 
   size_t _no_variables;
 
-  bool process_clause(const bvt &bv, bvt &dest);
+  bool process_clause(const bvt &bv, bvt &dest) const;
 
   static bool is_all(const bvt &bv, literalt l)
   {

src/solvers/sat/satcheck_minisat2.cpp

@@ -140,22 +140,23 @@ void satcheck_minisat2_baset<T>::lcnf(const bvt &bv)
 
     solver->addClause_(c);
 
-    // 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);
-      });
+    with_solver_hardness([this, &bv](solver_hardnesst &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.
+      // 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++;
+
+      hardness.register_clause(bv, cnf, cnf_clause_index, !clause_removed);
+    });
+
     clause_counter++;
   }
   catch(const Minisat::OutOfMemoryException &)