diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml index dbd29fbdcaa..7d90705d787 100644 --- a/.github/workflows/pull-request-checks.yaml +++ b/.github/workflows/pull-request-checks.yaml @@ -332,7 +332,7 @@ jobs: run: | mkdir build cd build - cmake .. -G Ninja -DCMAKE_BUILD_TYPE=Release + cmake .. -G Ninja -DCMAKE_BUILD_TYPE=Release -Dsat_impl=cadical - name: Build using Ninja run: | cd build diff --git a/CMakeLists.txt b/CMakeLists.txt index 38ad7ab671e..0742fe7b2e6 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -65,7 +65,8 @@ endif() set(enable_cbmc_tests on CACHE BOOL "Whether CBMC tests should be enabled") set(sat_impl "minisat2" CACHE STRING - "This setting controls the SAT library which is used. Valid values are 'minisat2' and 'glucose'" + "This setting controls the SAT library which is used. Valid values are + 'minisat2', 'glucose', or 'cadical'" ) if(${enable_cbmc_tests}) diff --git a/scripts/cadical-patch b/scripts/cadical-patch deleted file mode 100644 index 5baec02a370..00000000000 --- a/scripts/cadical-patch +++ /dev/null @@ -1,10 +0,0 @@ ---- a/src/cadical.hpp 2018-03-10 14:22:11.000000000 +0000 -+++ b/src/cadical.hpp 2018-03-31 16:18:32.000000000 +0100 -@@ -141,6 +141,6 @@ - File * output (); // get access to internal 'output' file - }; - --}; -+} - - #endif diff --git a/src/Makefile b/src/Makefile index 19058120bd2..81ca5124eac 100644 --- a/src/Makefile +++ b/src/Makefile @@ -152,15 +152,14 @@ glucose-download: @(cd ../glucose-syrup; patch -p1 < ../scripts/glucose-syrup-patch) @rm glucose-syrup.tgz -cadical_release = rel-06w +cadical_release = rel-1.3.0 cadical-download: @echo "Downloading CaDiCaL $(cadical_release)" @$(DOWNLOADER) https://github.com/arminbiere/cadical/archive/$(cadical_release).tar.gz @$(TAR) xfz $(cadical_release).tar.gz @rm -Rf ../cadical @mv cadical-$(cadical_release) ../cadical - @(cd ../cadical; patch -p1 < ../scripts/cadical-patch) - @cd ../cadical && CXX=$(CXX) CXXFLAGS=-O3 ./configure --debug && make + @cd ../cadical && CXX=$(CXX) ./configure -O3 -s -j && make @$(RM) $(cadical_release).tar.gz doc : diff --git a/src/solvers/CMakeLists.txt b/src/solvers/CMakeLists.txt index f88f9a726c6..d55ec09ffa7 100644 --- a/src/solvers/CMakeLists.txt +++ b/src/solvers/CMakeLists.txt @@ -98,6 +98,36 @@ elseif("${sat_impl}" STREQUAL "glucose") target_sources(solvers PRIVATE ${glucose_source}) target_link_libraries(solvers glucose-condensed) +elseif("${sat_impl}" STREQUAL "cadical") + message(STATUS "Building solvers with cadical") + + download_project(PROJ cadical + URL https://github.com/arminbiere/cadical/archive/rel-1.3.0.tar.gz + PATCH_COMMAND true + COMMAND CXX=${CMAKE_CXX_COMPILER} ./configure -O3 -s -j + URL_MD5 5bd15d1e198d2e904a8af8b7873dd341 + ) + + message(STATUS "Building CaDiCaL") + execute_process(COMMAND make WORKING_DIRECTORY ${cadical_SOURCE_DIR}) + + target_compile_definitions(solvers PUBLIC + SATCHECK_CADICAL HAVE_CADICAL + ) + + add_library(cadical STATIC IMPORTED) + + set_target_properties( + cadical + PROPERTIES IMPORTED_LOCATION ${cadical_SOURCE_DIR}/build/libcadical.a + ) + + target_include_directories(solvers + PUBLIC + ${cadical_SOURCE_DIR}/src + ) + + target_link_libraries(solvers cadical) endif() if(CMAKE_USE_CUDD) diff --git a/src/solvers/refinement/bv_refinement_loop.cpp b/src/solvers/refinement/bv_refinement_loop.cpp index 0f192f78de5..21542ba26d5 100644 --- a/src/solvers/refinement/bv_refinement_loop.cpp +++ b/src/solvers/refinement/bv_refinement_loop.cpp @@ -123,6 +123,10 @@ void bv_refinementt::check_SAT() arrays_overapproximated(); + // get values before modifying the formula + for(approximationt &approximation : this->approximations) + get_values(approximation); + for(approximationt &approximation : this->approximations) check_SAT(approximation); } diff --git a/src/solvers/refinement/refine_arithmetic.cpp b/src/solvers/refinement/refine_arithmetic.cpp index 6b87aee7f1b..59d1ccdc6fb 100644 --- a/src/solvers/refinement/refine_arithmetic.cpp +++ b/src/solvers/refinement/refine_arithmetic.cpp @@ -158,9 +158,6 @@ void bv_refinementt::get_values(approximationt &a) /// refine overapproximation void bv_refinementt::check_SAT(approximationt &a) { - // get values - get_values(a); - // see if the satisfying assignment is spurious in any way const typet &type = a.expr.type(); diff --git a/src/solvers/sat/satcheck_cadical.cpp b/src/solvers/sat/satcheck_cadical.cpp index 93e7e8a16f6..4b28f43bdea 100644 --- a/src/solvers/sat/satcheck_cadical.cpp +++ b/src/solvers/sat/satcheck_cadical.cpp @@ -10,6 +10,7 @@ Author: Michael Tautschnig #include #include +#include #include #ifdef HAVE_CADICAL @@ -23,7 +24,7 @@ tvt satcheck_cadicalt::l_get(literalt a) const tvt result; - if(a.var_no() > static_cast(solver->max())) + if(a.var_no() > narrow(solver->vars())) return tvt(tvt::tv_enumt::TV_UNKNOWN); const int val = solver->val(a.dimacs()); @@ -62,6 +63,23 @@ void satcheck_cadicalt::lcnf(const bvt &bv) } solver->add(0); // terminate clause + 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++; } @@ -72,31 +90,37 @@ propt::resultt satcheck_cadicalt::do_prop_solve() log.statistics() << (no_variables() - 1) << " variables, " << clause_counter << " clauses" << messaget::eom; - if(status == statust::UNSAT) + // if assumptions contains false, we need this to be UNSAT + for(const auto &a : assumptions) { - log.status() << "SAT checker inconsistent: instance is UNSATISFIABLE" - << messaget::eom; - } - else - { - switch(solver->solve()) + if(a.is_false()) { - case 10: - log.status() << "SAT checker: instance is SATISFIABLE" << messaget::eom; - status = statust::SAT; - return resultt::P_SATISFIABLE; - case 20: - log.status() << "SAT checker: instance is UNSATISFIABLE" - << messaget::eom; - break; - default: - log.status() << "SAT checker: solving returned without solution" - << messaget::eom; - throw analysis_exceptiont( - "solving inside CaDiCaL SAT solver has been interrupted"); + log.status() << "got FALSE as assumption: instance is UNSATISFIABLE" + << messaget::eom; + status = statust::UNSAT; + return resultt::P_UNSATISFIABLE; } } + for(const auto &a : assumptions) + solver->assume(a.dimacs()); + + switch(solver->solve()) + { + case 10: + log.status() << "SAT checker: instance is SATISFIABLE" << messaget::eom; + status = statust::SAT; + return resultt::P_SATISFIABLE; + case 20: + log.status() << "SAT checker: instance is UNSATISFIABLE" << messaget::eom; + break; + default: + log.status() << "SAT checker: solving returned without solution" + << messaget::eom; + throw analysis_exceptiont( + "solving inside CaDiCaL SAT solver has been interrupted"); + } + status = statust::UNSAT; return resultt::P_UNSATISFIABLE; } @@ -107,8 +131,8 @@ void satcheck_cadicalt::set_assignment(literalt a, bool value) INVARIANT(false, "method not supported"); } -satcheck_cadicalt::satcheck_cadicalt() : - solver(new CaDiCaL::Solver()) +satcheck_cadicalt::satcheck_cadicalt(message_handlert &message_handler) + : cnf_solvert(message_handler), solver(new CaDiCaL::Solver()) { solver->set("quiet", 1); } @@ -120,13 +144,20 @@ satcheck_cadicalt::~satcheck_cadicalt() void satcheck_cadicalt::set_assumptions(const bvt &bv) { - INVARIANT(false, "method not supported"); + // We filter out 'true' assumptions which cause spurious results with CaDiCaL. + assumptions.clear(); + for(const auto &assumption : bv) + { + if(!assumption.is_true()) + { + assumptions.push_back(assumption); + } + } } bool satcheck_cadicalt::is_in_conflict(literalt a) const { - INVARIANT(false, "method not supported"); - return false; + return solver->failed(a.dimacs()); } #endif diff --git a/src/solvers/sat/satcheck_cadical.h b/src/solvers/sat/satcheck_cadical.h index caaf99c0417..02728ef183f 100644 --- a/src/solvers/sat/satcheck_cadical.h +++ b/src/solvers/sat/satcheck_cadical.h @@ -12,15 +12,17 @@ Author: Michael Tautschnig #include "cnf.h" +#include + namespace CaDiCaL // NOLINT(readability/namespace) { class Solver; // NOLINT(readability/identifiers) } -class satcheck_cadicalt:public cnf_solvert +class satcheck_cadicalt : public cnf_solvert, public hardness_collectort { public: - satcheck_cadicalt(); + explicit satcheck_cadicalt(message_handlert &message_handler); virtual ~satcheck_cadicalt(); const std::string solver_text() override; @@ -32,19 +34,37 @@ class satcheck_cadicalt:public cnf_solvert void set_assumptions(const bvt &_assumptions) override; bool has_set_assumptions() const override { - return false; + return true; } bool has_is_in_conflict() const override { - return false; + return true; } bool is_in_conflict(literalt a) const override; + void + with_solver_hardness(std::function handler) override + { + if(solver_hardness.has_value()) + { + handler(solver_hardness.value()); + } + } + + void enable_hardness_collection() override + { + solver_hardness = solver_hardnesst{}; + } + protected: resultt do_prop_solve() override; // NOLINTNEXTLINE(readability/identifiers) CaDiCaL::Solver * solver; + + bvt assumptions; + + optionalt solver_hardness; }; #endif // CPROVER_SOLVERS_SAT_SATCHECK_CADICAL_H diff --git a/unit/Makefile b/unit/Makefile index 6f5bc2816a3..b63e9e234a4 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -69,6 +69,7 @@ SRC += analyses/ai/ai.cpp \ solvers/lowering/byte_operators.cpp \ solvers/prop/bdd_expr.cpp \ solvers/sat/external_sat.cpp \ + solvers/sat/satcheck_cadical.cpp \ solvers/sat/satcheck_minisat2.cpp \ solvers/strings/array_pool/array_pool.cpp \ solvers/strings/string_constraint_generator_valueof/calculate_max_string_length.cpp \ @@ -228,6 +229,9 @@ endif ifeq ($(MINISAT2),) EXCLUDED_TESTS += satcheck_minisat2.cpp endif +ifeq ($(CADICAL),) +EXCLUDED_TESTS += satcheck_cadical.cpp +endif N_CATCH_TESTS = $(shell \ cat $$(find . -name "*.cpp" \ diff --git a/unit/solvers/sat/satcheck_cadical.cpp b/unit/solvers/sat/satcheck_cadical.cpp new file mode 100644 index 00000000000..e2a170bc375 --- /dev/null +++ b/unit/solvers/sat/satcheck_cadical.cpp @@ -0,0 +1,86 @@ +/*******************************************************************\ + +Module: Unit tests for satcheck_cadical + +Author: Peter Schrammel, Michael Tautschnig + +\*******************************************************************/ + +/// \file +/// Unit tests for satcheck_cadical + +#ifdef HAVE_CADICAL + +# include + +# include +# include +# include + +SCENARIO("satcheck_cadical", "[core][solvers][sat][satcheck_cadical]") +{ + console_message_handlert message_handler; + + GIVEN("A satisfiable formula f") + { + satcheck_cadicalt satcheck(message_handler); + literalt f = satcheck.new_variable(); + satcheck.l_set_to_true(f); + + THEN("is indeed satisfiable") + { + REQUIRE(satcheck.prop_solve() == propt::resultt::P_SATISFIABLE); + } + THEN("is unsatisfiable under a false assumption") + { + bvt assumptions; + assumptions.push_back(const_literal(false)); + satcheck.set_assumptions(assumptions); + REQUIRE(satcheck.prop_solve() == propt::resultt::P_UNSATISFIABLE); + } + } + + GIVEN("An unsatisfiable formula f && !f") + { + satcheck_cadicalt satcheck(message_handler); + literalt f = satcheck.new_variable(); + satcheck.l_set_to_true(satcheck.land(f, !f)); + + THEN("is indeed unsatisfiable") + { + REQUIRE(satcheck.prop_solve() == propt::resultt::P_UNSATISFIABLE); + } + } + + GIVEN("An unsatisfiable formula false implied by a") + { + satcheck_cadicalt satcheck(message_handler); + literalt a = satcheck.new_variable(); + literalt a_implies_false = satcheck.lor(!a, const_literal(false)); + satcheck.l_set_to_true(a_implies_false); + + THEN("is indeed unsatisfiable under assumption a") + { + bvt assumptions; + assumptions.push_back(a); + satcheck.set_assumptions(assumptions); + REQUIRE(satcheck.prop_solve() == propt::resultt::P_UNSATISFIABLE); + } + THEN("is still unsatisfiable under assumption a and true") + { + bvt assumptions; + assumptions.push_back(const_literal(true)); + assumptions.push_back(a); + satcheck.set_assumptions(assumptions); + REQUIRE(satcheck.prop_solve() == propt::resultt::P_UNSATISFIABLE); + } + THEN("becomes satisfiable when assumption a is lifted") + { + bvt assumptions; + satcheck.set_assumptions(assumptions); + REQUIRE(satcheck.prop_solve() == propt::resultt::P_SATISFIABLE); + } + } +} + +#endif