diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-06-21 10:11:16 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-06-21 17:11:16 +0000 |
commit | 7c4a214cf3ce2facf4c98cd3bd347562c66f10a6 (patch) | |
tree | acaf71e0d825c817d8ea691b84e130e1b28b9d9f | |
parent | 7e9491574fe63075a4261c5b385f9b8b0e5e3e9a (diff) |
Make CaDiCaL a required dependency. (#6761)
Since the new BV solver is enabled by default and uses CaDiCaL
(and optionally CryptoMiniSat) we make CaDiCaL a required dependency.
-rw-r--r-- | CMakeLists.txt | 7 | ||||
-rw-r--r-- | NEWS | 1 | ||||
-rwxr-xr-x | configure.sh | 8 | ||||
-rw-r--r-- | src/CMakeLists.txt | 6 | ||||
-rw-r--r-- | src/base/configuration.cpp | 19 | ||||
-rw-r--r-- | src/base/configuration.h | 2 | ||||
-rw-r--r-- | src/base/configuration_private.h | 6 | ||||
-rw-r--r-- | src/options/options_handler.cpp | 10 | ||||
-rw-r--r-- | src/options/options_handler.h | 19 | ||||
-rw-r--r-- | src/prop/cadical.cpp | 4 | ||||
-rw-r--r-- | src/prop/cadical.h | 3 | ||||
-rw-r--r-- | src/prop/sat_solver_factory.cpp | 4 | ||||
-rw-r--r-- | test/regress/regress0/bv/eager-inc-cadical.smt2 | 1 |
13 files changed, 13 insertions, 77 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt index b29585f3b..3780b0b5b 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -118,7 +118,6 @@ option(ENABLE_PROFILING "Enable support for gprof profiling") # > allows to detect if set by user (default: IGNORE) # > only necessary for options set for ENABLE_BEST cvc5_option(USE_ABC "Use ABC for AIG bit-blasting") -cvc5_option(USE_CADICAL "Use CaDiCaL SAT solver") cvc5_option(USE_CLN "Use CLN instead of GMP") cvc5_option(USE_CRYPTOMINISAT "Use CryptoMiniSat SAT solver") cvc5_option(USE_GLPK "Use GLPK simplex solver") @@ -417,10 +416,7 @@ if(USE_ABC) add_definitions(-DCVC5_USE_ABC ${ABC_ARCH_FLAGS}) endif() -if(USE_CADICAL) - find_package(CaDiCaL REQUIRED) - add_definitions(-DCVC5_USE_CADICAL) -endif() +find_package(CaDiCaL REQUIRED) if(USE_CLN) set(GPL_LIBS "${GPL_LIBS} cln") @@ -651,7 +647,6 @@ print_config("Java bindings " ${BUILD_BINDINGS_JAVA}) print_config("Python2 " ${USE_PYTHON2}) message("") print_config("ABC " ${USE_ABC}) -print_config("CaDiCaL " ${USE_CADICAL}) print_config("CryptoMiniSat " ${USE_CRYPTOMINISAT}) print_config("GLPK " ${USE_GLPK}) print_config("Kissat " ${USE_KISSAT}) @@ -4,6 +4,7 @@ Changes since CVC4 1.8 ====================== New Features: +* CaDiCaL is now a required dependency. * SymFPU is now a required dependency. * New unsat-core production modes based on the new proof infrastructure (`--unsat-cores-mode=sat-proof`) and on the solving-under-assumption feature diff --git a/configure.sh b/configure.sh index 25203f8a6..4ba153a75 100755 --- a/configure.sh +++ b/configure.sh @@ -59,7 +59,6 @@ The following flags enable optional packages (disable with --no-<option name>). --cln use CLN instead of GMP --glpk use GLPK simplex solver --abc use the ABC AIG library - --cadical use the CaDiCaL SAT solver [default=yes] --cryptominisat use the CryptoMiniSat SAT solver --kissat use the Kissat SAT solver --poly use the LibPoly library [default=yes] @@ -108,7 +107,6 @@ abc=default asan=default assertions=default auto_download=default -cadical=ON cln=default comp_inc=default coverage=default @@ -174,7 +172,6 @@ do # Best configuration --best) abc=ON - cadical=ON cln=ON cryptominisat=ON glpk=ON @@ -198,9 +195,6 @@ do --name) die "missing argument to $1 (try -h)" ;; --name=*) build_dir=${1##*=} ;; - --cadical) cadical=ON;; - --no-cadical) cadical=OFF;; - --cln) cln=ON;; --no-cln) cln=OFF;; @@ -379,8 +373,6 @@ cmake_opts="" && cmake_opts="$cmake_opts -DUSE_EDITLINE=$editline" [ $abc != default ] \ && cmake_opts="$cmake_opts -DUSE_ABC=$abc" -[ $cadical != default ] \ - && cmake_opts="$cmake_opts -DUSE_CADICAL=$cadical" [ $cln != default ] \ && cmake_opts="$cmake_opts -DUSE_CLN=$cln" [ $cryptominisat != default ] \ diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index d7da67cbe..b3f27b703 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -1185,9 +1185,9 @@ if(USE_ABC) target_link_libraries(cvc5 PRIVATE ${ABC_LIBRARIES}) target_include_directories(cvc5 PRIVATE ${ABC_INCLUDE_DIR}) endif() -if(USE_CADICAL) - target_link_libraries(cvc5 PRIVATE CaDiCaL) -endif() + +target_link_libraries(cvc5 PRIVATE CaDiCaL) + if(USE_CLN) target_link_libraries(cvc5 PRIVATE CLN) endif() diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp index 1befb34ea..c6b004574 100644 --- a/src/base/configuration.cpp +++ b/src/base/configuration.cpp @@ -120,24 +120,23 @@ std::string Configuration::copyright() { << "See licenses/antlr3-LICENSE for copyright and licensing information." << "\n\n"; - if (Configuration::isBuiltWithAbc() || Configuration::isBuiltWithCadical() + ss << "This version of cvc5 is linked against the following non-(L)GPL'ed\n" + << "third party libraries.\n\n"; + + ss << " CaDiCaL - Simplified Satisfiability Solver\n" + << " See https://github.com/arminbiere/cadical for copyright " + << "information.\n\n"; + + if (Configuration::isBuiltWithAbc() || Configuration::isBuiltWithCryptominisat() || Configuration::isBuiltWithKissat() || Configuration::isBuiltWithEditline()) { - ss << "This version of cvc5 is linked against the following non-(L)GPL'ed\n" - << "third party libraries.\n\n"; if (Configuration::isBuiltWithAbc()) { ss << " ABC - A System for Sequential Synthesis and Verification\n" << " See http://bitbucket.org/alanmi/abc for copyright and\n" << " licensing information.\n\n"; } - if (Configuration::isBuiltWithCadical()) - { - ss << " CaDiCaL - Simplified Satisfiability Solver\n" - << " See https://github.com/arminbiere/cadical for copyright " - << "information.\n\n"; - } if (Configuration::isBuiltWithCryptominisat()) { ss << " CryptoMiniSat - An Advanced SAT Solver\n" @@ -241,8 +240,6 @@ bool Configuration::isBuiltWithAbc() { return IS_ABC_BUILD; } -bool Configuration::isBuiltWithCadical() { return IS_CADICAL_BUILD; } - bool Configuration::isBuiltWithCryptominisat() { return IS_CRYPTOMINISAT_BUILD; } diff --git a/src/base/configuration.h b/src/base/configuration.h index 2a7df1b4a..71c79c22e 100644 --- a/src/base/configuration.h +++ b/src/base/configuration.h @@ -103,8 +103,6 @@ public: static bool isBuiltWithAbc(); - static bool isBuiltWithCadical(); - static bool isBuiltWithCryptominisat(); static bool isBuiltWithKissat(); diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h index 39c5e89e9..b348da380 100644 --- a/src/base/configuration_private.h +++ b/src/base/configuration_private.h @@ -96,12 +96,6 @@ namespace cvc5 { # define IS_ABC_BUILD false #endif /* CVC5_USE_ABC */ -#if CVC5_USE_CADICAL -#define IS_CADICAL_BUILD true -#else /* CVC5_USE_CADICAL */ -#define IS_CADICAL_BUILD false -#endif /* CVC5_USE_CADICAL */ - #if CVC5_USE_CRYPTOMINISAT # define IS_CRYPTOMINISAT_BUILD true #else /* CVC5_USE_CRYPTOMINISAT */ diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index d31d2e58f..07138dce3 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -146,15 +146,6 @@ void OptionsHandler::checkBvSatSolver(const std::string& option, throw OptionException(ss.str()); } - if (m == SatSolverMode::CADICAL && !Configuration::isBuiltWithCadical()) - { - std::stringstream ss; - ss << "option `" << option - << "' requires a CaDiCaL build of cvc5; this binary was not built with " - "CaDiCaL support"; - throw OptionException(ss.str()); - } - if (m == SatSolverMode::KISSAT && !Configuration::isBuiltWithKissat()) { std::stringstream ss; @@ -397,7 +388,6 @@ void OptionsHandler::showConfiguration(const std::string& option, print_config_cond("abc", Configuration::isBuiltWithAbc()); print_config_cond("cln", Configuration::isBuiltWithCln()); print_config_cond("glpk", Configuration::isBuiltWithGlpk()); - print_config_cond("cadical", Configuration::isBuiltWithCadical()); print_config_cond("cryptominisat", Configuration::isBuiltWithCryptominisat()); print_config_cond("gmp", Configuration::isBuiltWithGmp()); print_config_cond("kissat", Configuration::isBuiltWithKissat()); diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 9aee1df22..3b3f80e6c 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -84,11 +84,6 @@ public: const std::string& flag, const std::string& value); - template <class T> - void checkSatSolverEnabled(const std::string& option, - const std::string& flag, - T m); - void checkBvSatSolver(const std::string& option, const std::string& flag, SatSolverMode m); @@ -171,20 +166,6 @@ public: }; /* class OptionHandler */ -template <class T> -void OptionsHandler::checkSatSolverEnabled(const std::string& option, - const std::string& flag, - T m) -{ -#if !defined(CVC5_USE_CRYPTOMINISAT) && !defined(CVC5_USE_CADICAL) \ - && !defined(CVC5_USE_KISSAT) - std::stringstream ss; - ss << "option `" << option - << "' requires cvc5 to be built with CryptoMiniSat or CaDiCaL or Kissat"; - throw OptionException(ss.str()); -#endif -} - } // namespace options } // namespace cvc5 diff --git a/src/prop/cadical.cpp b/src/prop/cadical.cpp index ec8919b0b..ddf20f5a1 100644 --- a/src/prop/cadical.cpp +++ b/src/prop/cadical.cpp @@ -17,8 +17,6 @@ #include "prop/cadical.h" -#ifdef CVC5_USE_CADICAL - #include "base/check.h" #include "util/statistics_registry.h" @@ -191,5 +189,3 @@ CadicalSolver::Statistics::Statistics(StatisticsRegistry& registry, } // namespace prop } // namespace cvc5 - -#endif // CVC5_USE_CADICAL diff --git a/src/prop/cadical.h b/src/prop/cadical.h index b5e26df9f..46c7c7e42 100644 --- a/src/prop/cadical.h +++ b/src/prop/cadical.h @@ -20,8 +20,6 @@ #ifndef CVC5__PROP__CADICAL_H #define CVC5__PROP__CADICAL_H -#ifdef CVC5_USE_CADICAL - #include "prop/sat_solver.h" #include <cadical.hpp> @@ -103,5 +101,4 @@ class CadicalSolver : public SatSolver } // namespace prop } // namespace cvc5 -#endif // CVC5_USE_CADICAL #endif // CVC5__PROP__CADICAL_H diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp index 446f72451..0855cbda5 100644 --- a/src/prop/sat_solver_factory.cpp +++ b/src/prop/sat_solver_factory.cpp @@ -53,13 +53,9 @@ SatSolver* SatSolverFactory::createCryptoMinisat(StatisticsRegistry& registry, SatSolver* SatSolverFactory::createCadical(StatisticsRegistry& registry, const std::string& name) { -#ifdef CVC5_USE_CADICAL CadicalSolver* res = new CadicalSolver(registry, name); res->init(); return res; -#else - Unreachable() << "cvc5 was not compiled with CaDiCaL support."; -#endif } SatSolver* SatSolverFactory::createKissat(StatisticsRegistry& registry, diff --git a/test/regress/regress0/bv/eager-inc-cadical.smt2 b/test/regress/regress0/bv/eager-inc-cadical.smt2 index 01840dffa..34007f6aa 100644 --- a/test/regress/regress0/bv/eager-inc-cadical.smt2 +++ b/test/regress/regress0/bv/eager-inc-cadical.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: cadical ; COMMAND-LINE: --incremental --bv-sat-solver=cadical --bitblast=eager (set-logic QF_BV) (set-option :incremental true) |