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 /src/prop | |
| 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.
Diffstat (limited to 'src/prop')
| -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 |
3 files changed, 0 insertions, 11 deletions
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, |