Make Glucose configuration build after solver hardness changes

In #5480 the solver hardness interface was updated, but changes were
only implemented in the Minisat2 interface. Update the Glucose interface
to match these changes.

To avoid future regressions, make the check-ubuntu-20_04-cmake-gcc
GitHub action use Glucose.

Author: tautschnig

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

@@ -83,7 +83,7 @@ jobs:
         run: |
           mkdir build
           cd build
-          cmake .. -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++
+          cmake .. -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ -Dsat_impl=glucose
       - name: Zero ccache stats and limit in size
         run: ccache -z --max-size=500M
       - name: Build with Ninja

src/solvers/sat/satcheck_glucose.cpp

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