Make IPASIR configuration build after solver hardness changes

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

To avoid future regressions, make the check-macos-10_15-make-clang
GitHub action use IPASIR with Riss as the back-end solver.

Author: tautschnig

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

@@ -105,7 +105,7 @@ jobs:
         with:
           submodules: recursive
       - name: Fetch dependencies
-        run: brew install maven flex bison parallel ccache
+        run: brew install maven flex bison parallel ccache cmake
       - name: Prepare ccache
         uses: actions/cache@v2
         with:
@@ -122,11 +122,16 @@ jobs:
         run: ccache -z --max-size=500M
       - name: Build using Make
         run: |
-          make -C src minisat2-download
-          make -C src -j2 CXX="ccache clang++"
-          make -C jbmc/src -j2 CXX="ccache clang++"
-          make -C unit "CXX=ccache clang++"
-          make -C jbmc/unit "CXX=ccache clang++"
+          git clone https://github.com/conp-solutions/riss riss.git
+          cmake -Hriss.git -Briss.git/release -DCMAKE_BUILD_TYPE=Release
+          make -C riss.git/release riss-coprocessor-lib-static -j2
+          make -C src -j2 CXX="ccache clang++" LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss
+          make -C jbmc/src -j2 CXX="ccache clang++" LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss
+
+          make -C unit "CXX=ccache clang++" LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss
+
+          make -C jbmc/unit "CXX=ccache clang++" LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss
+
       - name: Print ccache stats
         run: ccache -s
       - name: Run unit tests

src/solvers/sat/satcheck_ipasir.cpp

@@ -91,7 +91,22 @@ void satcheck_ipasirt::lcnf(const bvt &bv)
   ipasir_add(solver, 0); // terminate clause
 
   with_solver_hardness(
-    [&bv](solver_hardnesst &hardness) { hardness.register_clause(bv); });
+    [&bv, &cnf, &clause_removed](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++;
 }