Merge pull request #5709 from tautschnig/fix-glucose

Make Glucose configuration build after solver hardness changes

Author: tautschnig

.github/workflows/pull-request-checks.yaml

@@ -164,7 +164,7 @@ jobs:
         run: |
           mkdir build
           cd build
-          cmake .. -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/clang -DCMAKE_CXX_COMPILER=/usr/bin/clang++
+          cmake .. -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/clang -DCMAKE_CXX_COMPILER=/usr/bin/clang++ -Dsat_impl=glucose
       - name: Build with Ninja
         run: cd build; ninja -j2
       - name: Print ccache stats

src/solvers/sat/satcheck_glucose.cpp

@@ -121,8 +121,22 @@ void satcheck_glucose_baset<T>::lcnf(const bvt &bv)
 
     solver->addClause_(c);
 
-    with_solver_hardness(
-      [&bv](solver_hardnesst &hardness) { hardness.register_clause(bv); });
+    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++;
   }