Merge pull request #5710 from tautschnig/fix-ipasir

Make IPASIR configuration build after solver hardness changes

Author: tautschnig

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

@@ -16,8 +16,7 @@ jobs:
           # user input
           DEBIAN_FRONTEND: noninteractive
         run: |
-          sudo apt-get install --no-install-recommends -yq gcc gdb g++ maven jq flex bison libxml2-utils ccache
-          make -C src minisat2-download
+          sudo apt-get install --no-install-recommends -yq gcc gdb g++ maven jq flex bison libxml2-utils ccache cmake
       - name: Prepare ccache
         uses: actions/cache@v2
         with:
@@ -34,19 +33,24 @@ jobs:
         run: ccache -z --max-size=500M
       - name: Build with make
         run: |
-          make -C src CXX='ccache /usr/bin/g++' -j2
-          make -C unit CXX='ccache /usr/bin/g++' -j2
-          make -C jbmc/src  CXX='ccache /usr/bin/g++' -j2
-          make -C jbmc/unit CXX='ccache /usr/bin/g++' -j2
+          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 g++" LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss
+          make -C jbmc/src -j2 CXX="ccache g++" LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss
+
+          make -C unit -j2 CXX="ccache g++" LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss
+
+          make -C jbmc/unit -j2 CXX="ccache g++" 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
         run: |
-          make -C unit test
-          make -C jbmc/unit test
+          make -C unit test IPASIR=$PWD/riss.git/riss
+          make -C jbmc/unit test IPASIR=$PWD/riss.git/riss
           echo "Running expected failure tests"
-          make TAGS="[!shouldfail]" -C unit test
-          make TAGS="[!shouldfail]" -C jbmc/unit test
+          make TAGS="[!shouldfail]" -C unit test IPASIR=$PWD/riss.git/riss
+          make TAGS="[!shouldfail]" -C jbmc/unit test IPASIR=$PWD/riss.git/riss
       - name: Run regression tests
         run: |
           make -C regression test-parallel JOBS=2

src/solvers/sat/satcheck_ipasir.cpp

@@ -90,8 +90,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); });
+  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++;
 }
@@ -103,51 +117,40 @@ propt::resultt satcheck_ipasirt::do_prop_solve()
   log.statistics() << (no_variables() - 1) << " variables, " << clause_counter
                    << " clauses" << messaget::eom;
 
-  // use the internal representation, as ipasir does not support reporting the
-  // status
-  if(status==statust::UNSAT)
+  // if assumptions contains false, we need this to be UNSAT
+  bvt::const_iterator it =
+    std::find_if(assumptions.begin(), assumptions.end(), is_false);
+  const bool has_false = it != assumptions.end();
+
+  if(has_false)
   {
-    log.status() << "SAT checker inconsistent: instance is UNSATISFIABLE"
+    log.status() << "got FALSE as assumption: instance is UNSATISFIABLE"
                  << messaget::eom;
   }
   else
   {
-    // if assumptions contains false, we need this to be UNSAT
-    bvt::const_iterator it = std::find_if(assumptions.begin(),
-      assumptions.end(), is_false);
-    const bool has_false = it != assumptions.end();
+    forall_literals(it, assumptions)
+      if(!it->is_false())
+        ipasir_assume(solver, it->dimacs());
 
-    if(has_false)
+    // solve the formula, and handle the return code (10=SAT, 20=UNSAT)
+    int solver_state = ipasir_solve(solver);
+    if(10 == solver_state)
     {
-      log.status() << "got FALSE as assumption: instance is UNSATISFIABLE"
-                   << messaget::eom;
+      log.status() << "SAT checker: instance is SATISFIABLE" << messaget::eom;
+      status = statust::SAT;
+      return resultt::P_SATISFIABLE;
+    }
+    else if(20 == solver_state)
+    {
+      log.status() << "SAT checker: instance is UNSATISFIABLE" << messaget::eom;
     }
     else
     {
-      forall_literals(it, assumptions)
-        if(!it->is_false())
-          ipasir_assume(solver, it->dimacs());
-
-      // solve the formula, and handle the return code (10=SAT, 20=UNSAT)
-      int solver_state=ipasir_solve(solver);
-      if(10==solver_state)
-      {
-        log.status() << "SAT checker: instance is SATISFIABLE" << messaget::eom;
-        status=statust::SAT;
-        return resultt::P_SATISFIABLE;
-      }
-      else if(20==solver_state)
-      {
-        log.status() << "SAT checker: instance is UNSATISFIABLE"
-                     << messaget::eom;
-      }
-      else
-      {
-        log.status() << "SAT checker: solving returned without solution"
-                     << messaget::eom;
-        throw analysis_exceptiont(
-          "solving inside IPASIR SAT solver has been interrupted");
-      }
+      log.status() << "SAT checker: solving returned without solution"
+                   << messaget::eom;
+      throw analysis_exceptiont(
+        "solving inside IPASIR SAT solver has been interrupted");
     }
   }
 

unit/Makefile

@@ -225,6 +225,9 @@ EXCLUDED_TESTS=expr_undefined_casts.cpp
 ifneq ($(WITH_MEMORY_ANALYZER),1)
 EXCLUDED_TESTS += gdb_api.cpp
 endif
+ifeq ($(MINISAT2),)
+EXCLUDED_TESTS += satcheck_minisat2.cpp
+endif
 
 N_CATCH_TESTS = $(shell \
                   cat $$(find . -name "*.cpp" \