satcheck minisat2: make all solver hardness processing conditional

There is no need to run process_clause when its output wouldn't even be
used.

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,24 @@ 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) {
+      [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 &)