diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml index f2d59256315..eb8d0417fa5 100644 --- a/.github/workflows/pull-request-checks.yaml +++ b/.github/workflows/pull-request-checks.yaml @@ -92,7 +92,7 @@ jobs: run: | sudo apt-get update sudo apt-get install --no-install-recommends -yq clang-10 clang++-10 gdb maven jq flex bison libxml2-utils cpanminus ccache z3 - make -C src minisat2-download + make -C src minisat2-download cadical-download cpanm Thread::Pool::Simple - name: Confirm z3 solver is available and log the version installed run: z3 --version @@ -118,7 +118,7 @@ jobs: run: ccache -z --max-size=500M - name: Build with make run: | - make -C src -j2 + make -C src -j2 MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical make -C unit -j2 make -C jbmc/src -j2 make -C jbmc/unit -j2 @@ -223,7 +223,7 @@ jobs: echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV - name: Configure using CMake - run: cmake -S . -B build -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ + run: cmake -S . -B build -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ -Dsat_impl="minisat2;cadical" - name: Check that doc task works run: ninja -C build doc - name: Zero ccache stats and limit in size @@ -260,7 +260,7 @@ jobs: run: | sudo apt-get update sudo apt-get install --no-install-recommends -yq clang clang-14 gdb maven jq flex bison libxml2-utils cpanminus ccache z3 - make -C src minisat2-download + make -C src minisat2-download cadical-download cpanm Thread::Pool::Simple - name: Confirm z3 solver is available and log the version installed run: z3 --version @@ -290,7 +290,7 @@ jobs: make -C src/cpp library_check - name: Build with make run: | - make -C src -j2 + make -C src -j2 MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical make -C unit -j2 make -C jbmc/src -j2 make -C jbmc/unit -j2 @@ -348,7 +348,7 @@ jobs: echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV - name: Configure using CMake - run: cmake -S . -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ + run: cmake -S . -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ -Dsat_impl="minisat2;cadical" - name: Check that doc task works run: ninja -C build doc - name: Zero ccache stats and limit in size @@ -439,7 +439,7 @@ jobs: echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV - name: Configure using CMake - run: cmake -H. -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ + run: cmake -H. -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ -Dsat_impl="minisat2;cadical" - name: Zero ccache stats and limit in size run: ccache -z --max-size=500M - name: Build with Ninja @@ -482,8 +482,8 @@ jobs: run: ccache -z --max-size=500M - name: Build using Make run: | - make -C src minisat2-download - make -C src -j3 CXX="ccache clang++" + make -C src minisat2-download cadical-download + make -C src -j3 CXX="ccache clang++" MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical make -C jbmc/src -j3 CXX="ccache clang++" make -C unit "CXX=ccache clang++" make -C jbmc/unit "CXX=ccache clang++" diff --git a/.github/workflows/release-packages.yaml b/.github/workflows/release-packages.yaml index 80e60fa12af..05803c4841c 100644 --- a/.github/workflows/release-packages.yaml +++ b/.github/workflows/release-packages.yaml @@ -39,7 +39,7 @@ jobs: echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV - name: Configure CMake - run: cmake -S . -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ + run: cmake -S . -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ -Dsat_impl="minisat2;cadical" - name: Zero ccache stats and limit in size run: ccache -z --max-size=500M - name: Build using Ninja @@ -112,7 +112,7 @@ jobs: run: | mkdir build cd build - cmake .. -G Ninja -DCMAKE_BUILD_TYPE=Release + cmake .. -G Ninja -DCMAKE_BUILD_TYPE=Release -Dsat_impl="minisat2;cadical" - name: Zero ccache stats and limit in size run: ccache -z --max-size=500M - name: Build using Ninja @@ -198,7 +198,7 @@ jobs: run: | mkdir build cd build - cmake .. -G Ninja -DCMAKE_BUILD_TYPE=Release + cmake .. -G Ninja -DCMAKE_BUILD_TYPE=Release -Dsat_impl="minisat2;cadical" - name: Zero ccache stats and limit in size run: ccache -z --max-size=500M - name: Build using Ninja diff --git a/.gitignore b/.gitignore index fb967b1854f..42e61604ab8 100644 --- a/.gitignore +++ b/.gitignore @@ -74,6 +74,7 @@ jbmc/regression/**/tests-symex-driven-loading.log # libs downloaded by make [name]-download minisat*/ +cadical*/ glucose-syrup/ # flex/bison generated files diff --git a/CMakeLists.txt b/CMakeLists.txt index 16d9d162c17..fb7fcdda21c 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -273,7 +273,8 @@ else() FetchContent_MakeAvailable(Corrosion) corrosion_import_crate(MANIFEST_PATH src/libcprover-rust/Cargo.toml) - corrosion_set_env_vars(cprover-api-rust CBMC_BUILD_DIR=${CMAKE_BINARY_DIR} SAT_IMPL=${sat_impl}) + list(JOIN sat_impl " " sat_impl_str) + corrosion_set_env_vars(cprover-api-rust CBMC_BUILD_DIR=${CMAKE_BINARY_DIR} "SAT_IMPL=${sat_impl_str}") corrosion_link_libraries(cprover-api-rust cprover-api-cpp) install(TARGETS cprover-api-rust RUNTIME DESTINATION lib) # NOTE: We want to rename to a name consistent with the name of the diff --git a/COMPILING.md b/COMPILING.md index a980a444a9f..680a183a187 100644 --- a/COMPILING.md +++ b/COMPILING.md @@ -82,7 +82,7 @@ files. to generate IDE projects by supplying the `-G` flag. Run `cmake -G` for a comprehensive list of supported back-ends. - As part of this step, CMake will download the back-end solver (see Section + As part of this step, CMake will download the back-end solvers (see Section "Compiling with alternative SAT solvers" in this document for configuration options). Should it be necessary to perform this step without network access, a solver can be downloaded ahead of the above `cmake` invocation as follows: @@ -371,28 +371,40 @@ compilation flag: ## Compiling with alternative SAT solvers For the packaged builds of CBMC on our release page we currently build CBMC -with the MiniSat2 SAT solver statically linked at compile time. However it is -also possible to build CBMC using alternative SAT solvers. +with the MiniSat2 and CaDiCaL SAT solvers statically linked at compile time. +However it is also possible to build CBMC using alternative SAT solvers. ### Compiling CBMC Using Solver Native Interfaces The following solvers are supported by CBMC using custom interfaces and can -by downloaded and compiled by the build process: MiniSAT2, CaDiCaL, and Glucose. +be downloaded and compiled by the build process: MiniSAT2, CaDiCaL, and Glucose. -For `make` alternatives to the default (i.e. not MiniSAT) can be built with the -following commands for CaDiCaL: -``` -make -C src cadical-download -make -C src CADICAL=../../cadical -``` -and for glucose +For `make`, alternatives to the default (i.e. not MiniSAT and CaDiCaL) can be +built with the following commands for glucose: ``` make -C src glucose-download make -C src GLUCOSE=../../glucose-syrup ``` +CBMC can be built with multiple solvers, which can then be selected at runtime +using the `--sat-solver` option. +For example, to build CBMC with MiniSAT2 and Glucose, do: +``` +make -C src minisat2-download glucose-download +make -C src MINISAT2=../../minisat-2.2.1 GLUCOSE=../../glucose-syrup +``` +The build sets the default solver based on the priority defined by the +`#if/#elif` tree defined at the end of +[`src/solvers/sat/satcheck.h`](https://github.com/diffblue/cbmc/blob/develop/src/solvers/sat/satcheck.h). +In the above example, MiniSAT2 will be set as the default solver because it is +listed before Glucose. To switch to glucose at runtime, run CBMC with +`--sat-solver glucose`. For CMake the alternatives can be built with the following arguments to `cmake` -for CaDiCaL `-Dsat_impl=cadical` and for glucose `-Dsat_impl=glucose`. +for glucose `-Dsat_impl=glucose`. +To build CBMC with multiple solvers, specify the solvers in a semicolon-separated list to `-Dsat_impl`, e.g.: +``` +cmake -S . -Bbuild -Dsat_impl="minisat2;glucose" +``` ### Compiling with IPASIR Interface @@ -520,7 +532,7 @@ successfully on Windows or macOS. This document assumes you have already been able to build CPROVER on your chosen architecture. -#RUNNING REGRESSION AND UNIT TESTS +# RUNNING REGRESSION AND UNIT TESTS Regression and unit tests can be run using cmake or make. Your choice here should be the same as the compiling of the project itself. diff --git a/Dockerfile b/Dockerfile index 627b7ea5831..e73e6fda280 100644 --- a/Dockerfile +++ b/Dockerfile @@ -10,6 +10,7 @@ RUN echo 'tzdata tzdata/Areas select Etc' | debconf-set-selections; \ echo 'tzdata tzdata/Zones/Etc select UTC' | debconf-set-selections; \ apt-get update && apt-get upgrade -y && apt-get install --no-install-recommends -y \ cmake \ + make \ ninja-build \ gcc \ g++ \ diff --git a/doc/man/cbmc.1 b/doc/man/cbmc.1 index 49384614555..6514c809b1f 100644 --- a/doc/man/cbmc.1 +++ b/doc/man/cbmc.1 @@ -388,6 +388,9 @@ enable caching of repeated dereferences \fB\-\-object\-bits\fR n number of bits used for object addresses .TP +\fB\-\-sat\-solver\fR solver +use specified SAT solver +.TP \fB\-\-external\-sat\-solver\fR cmd command to invoke SAT solver process .TP diff --git a/doc/man/jbmc.1 b/doc/man/jbmc.1 index 8620e2e648b..1482f67bd31 100644 --- a/doc/man/jbmc.1 +++ b/doc/man/jbmc.1 @@ -382,6 +382,9 @@ enable caching of repeated dereferences \fB\-\-object\-bits\fR n number of bits used for object addresses .TP +\fB\-\-sat\-solver\fR solver +use specified SAT solver +.TP \fB\-\-external\-sat\-solver\fR \fIcmd\fR command to invoke SAT solver process .TP diff --git a/regression/cbmc/sat-solver-error/test.c b/regression/cbmc/sat-solver-error/test.c new file mode 100644 index 00000000000..af0a7f7f115 --- /dev/null +++ b/regression/cbmc/sat-solver-error/test.c @@ -0,0 +1,9 @@ +#include + +int main() +{ + unsigned x; + unsigned y = 0; + assert(x * y == y); + return 0; +} diff --git a/regression/cbmc/sat-solver-error/test.desc b/regression/cbmc/sat-solver-error/test.desc new file mode 100644 index 00000000000..4b262e9e3b4 --- /dev/null +++ b/regression/cbmc/sat-solver-error/test.desc @@ -0,0 +1,7 @@ +CORE broken-z3-smt-backend broken-cprover-smt-backend paths-lifo-expected-failure +test.c +--sat-solver non-existing-solver +^EXIT=1$ +^SIGNAL=0$ +unknown solver 'non-existing-solver' +-- diff --git a/regression/cbmc/sat-solver-warning/test.c b/regression/cbmc/sat-solver-warning/test.c new file mode 100644 index 00000000000..4127814cad1 --- /dev/null +++ b/regression/cbmc/sat-solver-warning/test.c @@ -0,0 +1,11 @@ +#include + +int main() +{ + unsigned x; + unsigned y = x; + x /= 2; + y /= 2; + assert(x == y); + return 0; +} diff --git a/regression/cbmc/sat-solver-warning/test.desc b/regression/cbmc/sat-solver-warning/test.desc new file mode 100644 index 00000000000..fdae1889d84 --- /dev/null +++ b/regression/cbmc/sat-solver-warning/test.desc @@ -0,0 +1,9 @@ +CORE broken-z3-smt-backend broken-cprover-smt-backend +test.c +--sat-solver lingeling +^EXIT=0$ +^SIGNAL=0$ +The specified solver, 'lingeling', is not available\. The default solver will be used instead\. +\[main\.assertion\.1] line \d+ assertion x == y: SUCCESS +^VERIFICATION SUCCESSFUL$ +-- diff --git a/regression/cbmc/sat-solver/test.c b/regression/cbmc/sat-solver/test.c new file mode 100644 index 00000000000..fa6eaa3b1d6 --- /dev/null +++ b/regression/cbmc/sat-solver/test.c @@ -0,0 +1,10 @@ +#include + +int main() +{ + unsigned x; + unsigned y = x / 2; + assert(y != x); + assert(y <= x); + return 0; +} diff --git a/regression/cbmc/sat-solver/test.desc b/regression/cbmc/sat-solver/test.desc new file mode 100644 index 00000000000..ec0d32f5b36 --- /dev/null +++ b/regression/cbmc/sat-solver/test.desc @@ -0,0 +1,10 @@ +CORE broken-z3-smt-backend broken-cprover-smt-backend +test.c +--sat-solver cadical +^EXIT=10$ +^SIGNAL=0$ +Solving with CaDiCaL|The specified solver, 'cadical', is not available. The default solver will be used instead. +\[main\.assertion\.1] line \d+ assertion y != x: FAILURE +\[main\.assertion\.2] line \d+ assertion y <= x: SUCCESS +^VERIFICATION FAILED$ +-- diff --git a/regression/validate-trace-xml-schema/check.py b/regression/validate-trace-xml-schema/check.py index adfe67d166e..4405f5c3f92 100644 --- a/regression/validate-trace-xml-schema/check.py +++ b/regression/validate-trace-xml-schema/check.py @@ -42,6 +42,7 @@ ['bad_option', 'test_multiple.desc'], ['bad_option', 'test.desc'], ['unknown-argument-suggestion', 'test.desc'], + ['sat-solver-error', 'test.desc'], # this one produces XML intermingled with main XML output when used with --xml-ui ['graphml_witness2', 'test.desc'], # these are producing coverage goals which aren't included in the schema diff --git a/scripts/cadical-1.4.1-patch b/scripts/cadical-1.4.1-patch new file mode 100644 index 00000000000..ef536d3cacc --- /dev/null +++ b/scripts/cadical-1.4.1-patch @@ -0,0 +1,34 @@ +diff --git a/scripts/make-build-header.sh b/scripts/make-build-header.sh +index e8f6746..1290024 100755 +--- a/scripts/make-build-header.sh ++++ b/scripts/make-build-header.sh +@@ -20,7 +20,7 @@ warning () { + + #--------------------------------------------------------------------------# + +-[ ! -f VERSION -a ! -f ../VERSION ] && \ ++[ ! -f VERSION.txt -a ! -f ../VERSION.txt ] && \ + die "needs to be called from build sub-directory" + + [ -f makefile ] || \ +@@ -29,7 +29,7 @@ warning "could not find 'makefile'" + #--------------------------------------------------------------------------# + # The version. + # +-VERSION="`cat ../VERSION`" ++VERSION="`cat ../VERSION.txt`" + if [ x"$VERSION" = x ] + then + warning "could not determine 'VERSION'" +diff --git a/src/lookahead.cpp b/src/lookahead.cpp +index 9e8a16b..3d5721a 100644 +--- a/src/lookahead.cpp ++++ b/src/lookahead.cpp +@@ -390,6 +390,7 @@ int Internal::lookahead_probing() { + CubesWithStatus Internal::generate_cubes(int depth, int min_depth) { + if (!active() || depth == 0) { + CubesWithStatus cubes; ++ cubes.status = 0; + cubes.cubes.push_back(std::vector()); + return cubes; + } diff --git a/scripts/cadical_CMakeLists.txt b/scripts/cadical_CMakeLists.txt new file mode 100644 index 00000000000..0ef36e66e3a --- /dev/null +++ b/scripts/cadical_CMakeLists.txt @@ -0,0 +1,27 @@ +file(GLOB sources "src/*.cpp" "src/*.hpp" "src/*.h") +# Remove "app" sources from list +list(REMOVE_ITEM sources + "${CMAKE_CURRENT_SOURCE_DIR}/src/cadical.cpp" + "${CMAKE_CURRENT_SOURCE_DIR}/src/mobical.cpp" +) + +add_library(cadical ${sources}) + +# Pass -DNBUILD to disable including the version information, which is not +# needed since cbmc doesn't run the cadical binary +target_compile_options(cadical PUBLIC -DNBUILD) + +set_target_properties( + cadical + PROPERTIES + CXX_STANDARD 11 + CXX_STANDARD_REQUIRED true + XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY "Developer ID Application: Daniel Kroening" +) + +target_include_directories(cadical + PUBLIC + ${CMAKE_CURRENT_SOURCE_DIR}/src +) + +target_link_libraries(cadical util) diff --git a/src/Makefile b/src/Makefile index e176aac6270..640b600e94f 100644 --- a/src/Makefile +++ b/src/Makefile @@ -177,7 +177,11 @@ cadical-download: @$(TAR) xfz $(cadical_release).tar.gz @rm -Rf ../cadical @mv cadical-$(cadical_release) ../cadical - @cd ../cadical && CXX=$(CXX) ./configure -O3 -s && make -j + @(cd ../cadical; patch -p1 < ../scripts/cadical-1.4.1-patch) + @(cd ../cadical && ./configure) + # Need to rename VERSION so that it isn't picked up by `#include` on + # macOS which is case insensitive + @(cd ../cadical && mv VERSION VERSION.txt) @$(RM) $(cadical_release).tar.gz doc : diff --git a/src/goto-checker/solver_factory.cpp b/src/goto-checker/solver_factory.cpp index 7a88b886ca6..7fcf31d6751 100644 --- a/src/goto-checker/solver_factory.cpp +++ b/src/goto-checker/solver_factory.cpp @@ -13,6 +13,7 @@ Author: Daniel Kroening, Peter Schrammel #include #include +#include #include #include #include @@ -216,17 +217,145 @@ make_satcheck_prop(message_handlert &message_handler, const optionst &options) std::unique_ptr solver_factoryt::get_default() { auto solver = util_make_unique(); - if( - options.get_bool_option("beautify") || - !options.get_bool_option("sat-preprocessor")) // no simplifier + bool solver_set = false; + if(options.is_set("sat-solver")) { - // simplifier won't work with beautification - solver->set_prop( - make_satcheck_prop(message_handler, options)); + const std::string &solver_option = options.get_option("sat-solver"); + if(solver_option == "zchaff") + { +#if defined SATCHECK_ZCHAFF + solver->set_prop( + make_satcheck_prop(message_handler, options)); + solver_set = true; +#else + emit_solver_warning("zchaff"); +#endif + } + else if(solver_option == "booleforce") + { +#if defined SATCHECK_BOOLERFORCE + solver->set_prop( + make_satcheck_prop(message_handler, options)); + solver_set = true; +#else + emit_solver_warning("booleforce"); +#endif + } + else if(solver_option == "minisat1") + { +#if defined SATCHECK_MINISAT1 + solver->set_prop( + make_satcheck_prop(message_handler, options)); + solver_set = true; +#else + emit_solver_warning("minisat1"); +#endif + } + else if(solver_option == "minisat2") + { +#if defined SATCHECK_MINISAT2 + if( + options.get_bool_option("beautify") || + !options.get_bool_option("sat-preprocessor")) // no simplifier + { + // simplifier won't work with beautification + solver->set_prop(make_satcheck_prop( + message_handler, options)); + } + else // with simplifier + { + solver->set_prop(make_satcheck_prop( + message_handler, options)); + } + solver_set = true; +#else + emit_solver_warning("minisat2"); +#endif + } + else if(solver_option == "ipasir") + { +#if defined SATCHECK_IPASIR + solver->set_prop( + make_satcheck_prop(message_handler, options)); + solver_set = true; +#else + emit_solver_warning("ipasir"); +#endif + } + else if(solver_option == "picosat") + { +#if defined SATCHECK_PICOSAT + solver->set_prop( + make_satcheck_prop(message_handler, options)); + solver_set = true; +#else + emit_solver_warning("picosat"); +#endif + } + else if(solver_option == "lingeling") + { +#if defined SATCHECK_LINGELING + solver->set_prop( + make_satcheck_prop(message_handler, options)); + solver_set = true; +#else + emit_solver_warning("lingeling"); +#endif + } + else if(solver_option == "glucose") + { +#if defined SATCHECK_GLUCOSE + if( + options.get_bool_option("beautify") || + !options.get_bool_option("sat-preprocessor")) // no simplifier + { + // simplifier won't work with beautification + solver->set_prop(make_satcheck_prop( + message_handler, options)); + } + else // with simplifier + { + solver->set_prop(make_satcheck_prop( + message_handler, options)); + } + solver_set = true; +#else + emit_solver_warning("glucose"); +#endif + } + else if(solver_option == "cadical") + { +#if defined SATCHECK_CADICAL + solver->set_prop( + make_satcheck_prop(message_handler, options)); + solver_set = true; +#else + emit_solver_warning("cadical"); +#endif + } + else + { + messaget log(message_handler); + log.error() << "unknown solver '" << solver_option << "'" + << messaget::eom; + exit(CPROVER_EXIT_USAGE_ERROR); + } } - else // with simplifier + if(!solver_set) { - solver->set_prop(make_satcheck_prop(message_handler, options)); + // default solver + if( + options.get_bool_option("beautify") || + !options.get_bool_option("sat-preprocessor")) // no simplifier + { + // simplifier won't work with beautification + solver->set_prop( + make_satcheck_prop(message_handler, options)); + } + else // with simplifier + { + solver->set_prop(make_satcheck_prop(message_handler, options)); + } } bool get_array_constraints = @@ -245,6 +374,14 @@ std::unique_ptr solver_factoryt::get_default() return solver; } +void solver_factoryt::emit_solver_warning(const std::string &solver) +{ + messaget log(message_handler); + log.warning() << "The specified solver, '" << solver + << "', is not available. " + << "The default solver will be used instead." << messaget::eom; +} + std::unique_ptr solver_factoryt::get_dimacs() { no_beautification(); @@ -517,6 +654,9 @@ static void parse_sat_options(const cmdlinet &cmdline, optionst &options) if(cmdline.isset("dimacs")) options.set_option("dimacs", true); + + if(cmdline.isset("sat-solver")) + options.set_option("sat-solver", cmdline.get_value("sat-solver")); } static void parse_smt2_options(const cmdlinet &cmdline, optionst &options) diff --git a/src/goto-checker/solver_factory.h b/src/goto-checker/solver_factory.h index b9507f5a149..63c1a0dec64 100644 --- a/src/goto-checker/solver_factory.h +++ b/src/goto-checker/solver_factory.h @@ -89,6 +89,9 @@ class solver_factoryt final // consistency checks during solver creation void no_beautification(); void no_incremental_check(); + + // emit a warning for non-existent solver + void emit_solver_warning(const std::string &solver); }; /// Parse solver-related command-line parameters in \p cmdline and set @@ -104,6 +107,7 @@ void parse_solver_options(const cmdlinet &cmdline, optionst &options); "(mathsat)" \ "(cprover-smt2)" \ "(incremental-smt2-solver):" \ + "(sat-solver):" \ "(external-sat-solver):" \ "(no-sat-preprocessor)" \ "(beautify)" \ @@ -126,6 +130,7 @@ void parse_solver_options(const cmdlinet &cmdline, optionst &options); " --smt2 use default SMT2 solver (Z3)\n" \ " --bitwuzla use Bitwuzla\n" \ " --boolector use Boolector\n" \ + " --sat-solver solver use specified SAT solver\n" \ " --cprover-smt2 use CPROVER SMT2 solver\n" \ " --cvc3 use CVC3\n" \ " --cvc4 use CVC4\n" \ diff --git a/src/libcprover-rust/build.rs b/src/libcprover-rust/build.rs index a845ba3cc72..028e5b52d40 100644 --- a/src/libcprover-rust/build.rs +++ b/src/libcprover-rust/build.rs @@ -40,20 +40,26 @@ fn get_cadical_build_dir() -> std::io::Result { )) } -fn get_sat_library() -> std::io::Result<&'static str> { +fn get_sat_libraries() -> std::io::Result> { let env_var_name = "SAT_IMPL"; let env_var_fetch_result = env::var(env_var_name); - if let Ok(sat_impl) = env_var_fetch_result { - let solver_lib = match sat_impl.as_str() { - "minisat2" => Ok("minisat2-condensed"), - "glucose" => Ok("glucose-condensed"), - "cadical" => Ok("cadical"), - _ => Err(Error::new( - ErrorKind::Other, - "no identifiable solver detected", - )), - }; - return solver_lib; + if let Ok(sat_impls) = env_var_fetch_result { + let mut solver_libs = Vec::new(); + for sat_impl in sat_impls.split(" ") { + let solver_lib = match sat_impl { + "minisat2" => "minisat2-condensed", + "glucose" => "glucose-condensed", + "cadical" => "cadical", + _ => { + return Err(Error::new( + ErrorKind::Other, + "no identifiable solver detected", + )) + } + }; + solver_libs.push(solver_lib); + } + return Ok(solver_libs); } Err(Error::new( ErrorKind::Other, @@ -80,23 +86,25 @@ fn main() { Err(err) => panic!("Error: {}", err), }; - let solver_lib = match get_sat_library() { - Ok(solver) => solver, + let solver_libs = match get_sat_libraries() { + Ok(solvers) => solvers, Err(err) => panic!("Error: {}", err), }; - // Cadical is being built in its own directory, with the resultant artefacts being - // present only there. Hence, we need to instruct cargo to look for them in cadical's - // build directory, otherwise we're going to get build errors. - if solver_lib == "cadical" { - let cadical_build_dir = match get_cadical_build_dir() { - Ok(cadical_directory) => cadical_directory, - Err(err) => panic!("Error: {}", err), - }; - println!( - "cargo:rustc-link-search=native={}", - cadical_build_dir.display() - ); + for solver_lib in solver_libs.iter() { + // Cadical is being built in its own directory, with the resultant artefacts being + // present only there. Hence, we need to instruct cargo to look for them in cadical's + // build directory, otherwise we're going to get build errors. + if *solver_lib == "cadical" { + let cadical_build_dir = match get_cadical_build_dir() { + Ok(cadical_directory) => cadical_directory, + Err(err) => panic!("Error: {}", err), + }; + println!( + "cargo:rustc-link-search=native={}", + cadical_build_dir.display() + ); + } } println!( @@ -122,7 +130,9 @@ fn main() { println!("cargo:rustc-link-lib=static=statement-list"); println!("cargo:rustc-link-lib=static=goto-symex"); println!("cargo:rustc-link-lib=static=pointer-analysis"); - println!("cargo:rustc-link-lib=static={}", solver_lib); + for solver_lib in solver_libs { + println!("cargo:rustc-link-lib=static={}", solver_lib); + } println!("cargo:rustc-link-lib=static=cbmc-lib"); println!("cargo:rustc-link-lib=static=cprover-api-cpp"); } diff --git a/src/solvers/CMakeLists.txt b/src/solvers/CMakeLists.txt index 9a37ca5ce9d..e941c134d69 100644 --- a/src/solvers/CMakeLists.txt +++ b/src/solvers/CMakeLists.txt @@ -64,137 +64,132 @@ add_library(solvers ${sources}) include("${CBMC_SOURCE_DIR}/../cmake/DownloadProject.cmake") -if("${sat_impl}" STREQUAL "minisat2") - message(STATUS "Building solvers with minisat2") - - # once we upgrade to CMake 3.7 or higher we can specify multiple URLs as a - # fall-back in case the first URL fails (the Makefile-based build retries up - # to 2 times) - download_project(PROJ minisat2 - URL http://ftp.debian.org/debian/pool/main/m/minisat2/minisat2_2.2.1.orig.tar.gz - PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/minisat-2.2.1-patch - COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/../scripts/minisat2_CMakeLists.txt CMakeLists.txt - URL_MD5 27faa19ee0508660bd6fb7f894646d42 - ) +foreach(SOLVER ${sat_impl}) + if("${SOLVER}" STREQUAL "minisat2") + message(STATUS "Building solvers with minisat2") + + # once we upgrade to CMake 3.7 or higher we can specify multiple URLs as a + # fall-back in case the first URL fails (the Makefile-based build retries up + # to 2 times) + download_project(PROJ minisat2 + URL http://ftp.debian.org/debian/pool/main/m/minisat2/minisat2_2.2.1.orig.tar.gz + PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/minisat-2.2.1-patch + COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/../scripts/minisat2_CMakeLists.txt CMakeLists.txt + URL_MD5 27faa19ee0508660bd6fb7f894646d42 + ) - add_subdirectory(${minisat2_SOURCE_DIR} ${minisat2_BINARY_DIR}) + add_subdirectory(${minisat2_SOURCE_DIR} ${minisat2_BINARY_DIR}) - target_compile_definitions(solvers PUBLIC - SATCHECK_MINISAT2 HAVE_MINISAT2 __STDC_FORMAT_MACROS __STDC_LIMIT_MACROS - ) - - target_sources(solvers PRIVATE ${minisat2_source}) + target_compile_definitions(solvers PUBLIC + SATCHECK_MINISAT2 HAVE_MINISAT2 __STDC_FORMAT_MACROS __STDC_LIMIT_MACROS + ) - target_link_libraries(solvers minisat2-condensed) -elseif("${sat_impl}" STREQUAL "glucose") - message(STATUS "Building solvers with glucose") + target_sources(solvers PRIVATE ${minisat2_source}) - download_project(PROJ glucose - URL https://github.com/BrunoDutertre/glucose-syrup/archive/0bb2afd3b9baace6981cbb8b4a1c7683c44968b7.tar.gz - PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/glucose-syrup-patch - COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/../scripts/glucose_CMakeLists.txt CMakeLists.txt - URL_MD5 7c539c62c248b74210aef7414787323a - ) + target_link_libraries(solvers minisat2-condensed) + elseif("${SOLVER}" STREQUAL "glucose") + message(STATUS "Building solvers with glucose") - add_subdirectory(${glucose_SOURCE_DIR} ${glucose_BINARY_DIR}) + download_project(PROJ glucose + URL https://github.com/BrunoDutertre/glucose-syrup/archive/0bb2afd3b9baace6981cbb8b4a1c7683c44968b7.tar.gz + PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/glucose-syrup-patch + COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/../scripts/glucose_CMakeLists.txt CMakeLists.txt + URL_MD5 7c539c62c248b74210aef7414787323a + ) - target_compile_definitions(solvers PUBLIC - SATCHECK_GLUCOSE HAVE_GLUCOSE __STDC_FORMAT_MACROS __STDC_LIMIT_MACROS - ) + add_subdirectory(${glucose_SOURCE_DIR} ${glucose_BINARY_DIR}) - target_sources(solvers PRIVATE ${glucose_source}) + target_compile_definitions(solvers PUBLIC + SATCHECK_GLUCOSE HAVE_GLUCOSE __STDC_FORMAT_MACROS __STDC_LIMIT_MACROS + ) - target_link_libraries(solvers glucose-condensed) -elseif("${sat_impl}" STREQUAL "cadical") - message(STATUS "Building solvers with cadical") + target_sources(solvers PRIVATE ${glucose_source}) - download_project(PROJ cadical - URL https://github.com/arminbiere/cadical/archive/rel-1.4.1.tar.gz - PATCH_COMMAND true - COMMAND CXX=${CMAKE_CXX_COMPILER} ./configure -O3 -s CXXFLAGS=-std=c++14 - URL_MD5 b44874501a175106424f4bd5de29aa59 - ) + target_link_libraries(solvers glucose-condensed) + elseif("${SOLVER}" STREQUAL "cadical") + message(STATUS "Building solvers with cadical") - message(STATUS "Building CaDiCaL") - execute_process(COMMAND make -j WORKING_DIRECTORY ${cadical_SOURCE_DIR}) + download_project(PROJ cadical + URL https://github.com/arminbiere/cadical/archive/rel-1.4.1.tar.gz + PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/cadical-1.4.1-patch + COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/../scripts/cadical_CMakeLists.txt CMakeLists.txt + COMMAND ./configure + URL_MD5 b44874501a175106424f4bd5de29aa59 + ) - target_compile_definitions(solvers PUBLIC - SATCHECK_CADICAL HAVE_CADICAL - ) + add_subdirectory(${cadical_SOURCE_DIR} ${cadical_BINARY_DIR}) - add_library(cadical STATIC IMPORTED) + target_compile_definitions(solvers PUBLIC + SATCHECK_CADICAL HAVE_CADICAL + ) - set_target_properties( - cadical - PROPERTIES IMPORTED_LOCATION ${cadical_SOURCE_DIR}/build/libcadical.a - ) + target_include_directories(solvers + PUBLIC + ${cadical_SOURCE_DIR}/src + ) - target_include_directories(solvers - PUBLIC - ${cadical_SOURCE_DIR}/src - ) + target_link_libraries(solvers cadical) + elseif("${SOLVER}" STREQUAL "ipasir-cadical") + message(STATUS "Building with IPASIR solver linking against: CaDiCaL") - target_link_libraries(solvers cadical) -elseif("${sat_impl}" STREQUAL "ipasir-cadical") - message(STATUS "Building with IPASIR solver linking against: CaDiCaL") + download_project(PROJ cadical + URL https://github.com/arminbiere/cadical/archive/rel-1.4.1.tar.gz + PATCH_COMMAND true + COMMAND CXX=${CMAKE_CXX_COMPILER} ./configure -O3 -s CXXFLAGS=-std=c++14 + URL_MD5 b44874501a175106424f4bd5de29aa59 + ) - download_project(PROJ cadical - URL https://github.com/arminbiere/cadical/archive/rel-1.4.1.tar.gz - PATCH_COMMAND true - COMMAND CXX=${CMAKE_CXX_COMPILER} ./configure -O3 -s CXXFLAGS=-std=c++14 - URL_MD5 b44874501a175106424f4bd5de29aa59 - ) + message(STATUS "Building CaDiCaL") + execute_process(COMMAND make WORKING_DIRECTORY ${cadical_SOURCE_DIR}) - message(STATUS "Building CaDiCaL") - execute_process(COMMAND make WORKING_DIRECTORY ${cadical_SOURCE_DIR}) + target_compile_definitions(solvers PUBLIC + SATCHECK_IPASIR HAVE_IPASIR IPASIR=${cadical_SOURCE_DIR}/src + ) - target_compile_definitions(solvers PUBLIC - SATCHECK_IPASIR HAVE_IPASIR IPASIR=${cadical_SOURCE_DIR}/src - ) + add_library(cadical_ipasir STATIC IMPORTED) + set_property(TARGET cadical_ipasir + PROPERTY IMPORTED_LOCATION ${cadical_SOURCE_DIR}/build/libcadical.a + ) - add_library(cadical_ipasir STATIC IMPORTED) - set_property(TARGET cadical_ipasir - PROPERTY IMPORTED_LOCATION ${cadical_SOURCE_DIR}/build/libcadical.a - ) + target_include_directories(solvers + PUBLIC + ${cadical_SOURCE_DIR}/src + ) + target_link_libraries(solvers cadical_ipasir) + elseif("${SOLVER}" STREQUAL "ipasir-custom") + message(STATUS "Building with IPASIR solver linking: custom solver provided") + + if (NOT DEFINED IPASIR) + message(FATAL_ERROR + "IPASIR solver source code not provided. Please use -DIPASIR= " + "with being the path to the IPASIR solver source code." + ) + endif() + + if (NOT DEFINED IPASIR_LIB) + message(FATAL_ERROR + "IPASIR solver library not provided. Please use -DIPASIR_LIB= " + "with being the path to the IPASIR solver precompiled static " + "library." + ) + endif() + + target_compile_definitions(solvers PUBLIC + SATCHECK_IPASIR HAVE_IPASIR IPASIR=${IPASIR} + ) - target_include_directories(solvers - PUBLIC - ${cadical_SOURCE_DIR}/src - ) - target_link_libraries(solvers cadical_ipasir) -elseif("${sat_impl}" STREQUAL "ipasir-custom") - message(STATUS "Building with IPASIR solver linking: custom solver provided") - - if (NOT DEFINED IPASIR) - message(FATAL_ERROR - "IPASIR solver source code not provided. Please use -DIPASIR= " - "with being the path to the IPASIR solver source code." + add_library(ipasir_custom STATIC IMPORTED) + set_property(TARGET ipasir_custom + PROPERTY IMPORTED_LOCATION ${IPASIR_LIB} ) - endif() - if (NOT DEFINED IPASIR_LIB) - message(FATAL_ERROR - "IPASIR solver library not provided. Please use -DIPASIR_LIB= " - "with being the path to the IPASIR solver precompiled static " - "library." + target_include_directories(solvers + PUBLIC + ${IPASIR} ) + target_link_libraries(solvers ipasir_custom pthread) endif() - - target_compile_definitions(solvers PUBLIC - SATCHECK_IPASIR HAVE_IPASIR IPASIR=${IPASIR} - ) - - add_library(ipasir_custom STATIC IMPORTED) - set_property(TARGET ipasir_custom - PROPERTY IMPORTED_LOCATION ${IPASIR_LIB} - ) - - target_include_directories(solvers - PUBLIC - ${IPASIR} - ) - target_link_libraries(solvers ipasir_custom pthread) -endif() +endforeach() if(CMAKE_USE_CUDD) target_link_libraries(solvers util cudd-cplusplus cudd) diff --git a/src/solvers/Makefile b/src/solvers/Makefile index bae30d36478..e2d0662981d 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -66,6 +66,7 @@ ifneq ($(CADICAL),) CADICAL_INCLUDE=-I $(CADICAL)/src CADICAL_LIB=$(CADICAL)/build/libcadical$(LIBEXT) CP_CXXFLAGS += -DHAVE_CADICAL + CLEANFILES += $(CADICAL_LIB) $(patsubst %$(OBJEXT), %$(DEPEXT), $(CADICAL_LIB)) endif SRC = $(BOOLEFORCE_SRC) \ @@ -275,6 +276,9 @@ endif solvers$(LIBEXT): $(OBJ) $(SOLVER_LIB) $(LINKLIB) +../../cadical/build/libcadical$(LIBEXT): + $(MAKE) $(MAKEARGS) -C $(CADICAL)/build libcadical.a CXX="$(CXX)" CXXFLAGS="$(CP_CXXFLAGS)" + -include smt2/smt2_solver$(DEPEXT) smt2_solver$(EXEEXT): $(OBJ) smt2/smt2_solver$(OBJEXT) \ diff --git a/src/solvers/sat/satcheck.h b/src/solvers/sat/satcheck.h index c7175fa414c..733896086aa 100644 --- a/src/solvers/sat/satcheck.h +++ b/src/solvers/sat/satcheck.h @@ -60,65 +60,83 @@ Author: Daniel Kroening, kroening@kroening.com #endif #if defined SATCHECK_ZCHAFF +# include "satcheck_zchaff.h" +#endif + +#if defined SATCHECK_BOOLEFORCE +# include "satcheck_booleforce.h" +#endif + +#if defined SATCHECK_MINISAT1 +# include "satcheck_minisat.h" +#endif + +#if defined SATCHECK_MINISAT2 +# include "satcheck_minisat2.h" +#endif + +#if defined SATCHECK_IPASIR +# include "satcheck_ipasir.h" +#endif + +#if defined SATCHECK_PICOSAT +# include "satcheck_picosat.h" +#endif + +#if defined SATCHECK_LINGELING +# include "satcheck_lingeling.h" +#endif -#include "satcheck_zchaff.h" +#if defined SATCHECK_GLUCOSE +# include "satcheck_glucose.h" +#endif + +#if defined SATCHECK_CADICAL +# include "satcheck_cadical.h" +#endif + +#if defined SATCHECK_ZCHAFF typedef satcheck_zchafft satcheckt; typedef satcheck_zchafft satcheck_no_simplifiert; #elif defined SATCHECK_BOOLEFORCE -#include "satcheck_booleforce.h" - typedef satcheck_booleforcet satcheckt; typedef satcheck_booleforcet satcheck_no_simplifiert; #elif defined SATCHECK_MINISAT1 -#include "satcheck_minisat.h" - typedef satcheck_minisat1t satcheckt; typedef satcheck_minisat1t satcheck_no_simplifiert; #elif defined SATCHECK_MINISAT2 -#include "satcheck_minisat2.h" - typedef satcheck_minisat_simplifiert satcheckt; typedef satcheck_minisat_no_simplifiert satcheck_no_simplifiert; #elif defined SATCHECK_IPASIR -#include "satcheck_ipasir.h" - typedef satcheck_ipasirt satcheckt; typedef satcheck_ipasirt satcheck_no_simplifiert; #elif defined SATCHECK_PICOSAT -#include "satcheck_picosat.h" - typedef satcheck_picosatt satcheckt; typedef satcheck_picosatt satcheck_no_simplifiert; #elif defined SATCHECK_LINGELING -#include "satcheck_lingeling.h" - typedef satcheck_lingelingt satcheckt; typedef satcheck_lingelingt satcheck_no_simplifiert; #elif defined SATCHECK_GLUCOSE -#include "satcheck_glucose.h" - typedef satcheck_glucose_simplifiert satcheckt; typedef satcheck_glucose_no_simplifiert satcheck_no_simplifiert; #elif defined SATCHECK_CADICAL -#include "satcheck_cadical.h" - typedef satcheck_cadicalt satcheckt; typedef satcheck_cadicalt satcheck_no_simplifiert;