From 2a544f72e074b61ffe6eaf459e4578de12bf841e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 1 Jan 2021 17:14:47 +0000 Subject: [PATCH] Make IPASIR 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 IPASIR interface to match these changes. Also fix the status tracking in do_prop_solve as the previous implementation would keep the solver in an UNSAT state, even when assumptions had been modified. This issue was surfaced by the cbmc-incr-oneloop suite of regression tests. To avoid future regressions, make the check-ubuntu-20_04-make-gcc GitHub action use IPASIR with Riss as the back-end solver. --- .github/workflows/pull-request-checks.yaml | 24 ++++--- src/solvers/sat/satcheck_ipasir.cpp | 77 +++++++++++----------- unit/Makefile | 3 + 3 files changed, 57 insertions(+), 47 deletions(-) diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml index 052130a2bc1..39babcfb66a 100644 --- a/.github/workflows/pull-request-checks.yaml +++ b/.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 diff --git a/src/solvers/sat/satcheck_ipasir.cpp b/src/solvers/sat/satcheck_ipasir.cpp index 44192c0a0d3..b3374b9858d 100644 --- a/src/solvers/sat/satcheck_ipasir.cpp +++ b/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"); } } diff --git a/unit/Makefile b/unit/Makefile index 33a32434ef9..6f5bc2816a3 100644 --- a/unit/Makefile +++ b/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" \