diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-03-20 16:11:15 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-03-20 16:11:15 -0700 |
commit | 614670f98a9ab2d3cfcb9f364a1b06d78f63ebb0 (patch) | |
tree | 7dbdfbbae495fed26877c51267f6775f618f5d33 /src/base | |
parent | 62f58d62c6c597eeb9cae5e08d74f21c4a5c5c40 (diff) |
Add support for CaDiCaL as eager BV SAT solver. (#1675)
Diffstat (limited to 'src/base')
-rw-r--r-- | src/base/configuration.cpp | 28 | ||||
-rw-r--r-- | src/base/configuration.h | 2 | ||||
-rw-r--r-- | src/base/configuration_private.h | 6 |
3 files changed, 28 insertions, 8 deletions
diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp index 7e7da1500..7ceb64885 100644 --- a/src/base/configuration.cpp +++ b/src/base/configuration.cpp @@ -134,7 +134,10 @@ std::string Configuration::copyright() { << "\n\n"; if (Configuration::isBuiltWithAbc() - || Configuration::isBuiltWithLfsc()) { + || Configuration::isBuiltWithLfsc() + || Configuration::isBuiltWithCadical() + || Configuration::isBuiltWithCryptominisat()) + { ss << "This version of CVC4 is linked against the following non-(L)GPL'ed\n" << "third party libraries.\n\n"; if (Configuration::isBuiltWithAbc()) { @@ -147,10 +150,22 @@ std::string Configuration::copyright() { << " See http://github.com/CVC4/LFSC 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" + << " See https://github.com/msoos/cryptominisat for copyright " + << "information.\n\n"; + } } - if (Configuration::isBuiltWithGmp() - || Configuration::isBuiltWithCryptominisat()) { + if (Configuration::isBuiltWithGmp()) + { ss << "This version of CVC4 is linked against the following third party\n" << "libraries covered by the LGPLv3 license.\n" << "See licenses/lgpl-3.0.txt for more information.\n\n"; @@ -158,11 +173,6 @@ std::string Configuration::copyright() { ss << " GMP - Gnu Multi Precision Arithmetic Library\n" << " See http://gmplib.org for copyright information.\n\n"; } - if (Configuration::isBuiltWithCryptominisat()) { - ss << " CryptoMiniSat - An Advanced SAT Solver\n" - << " See http://github.com/msoos/cryptominisat for copyright " - << "information.\n\n"; - } } if (Configuration::isBuiltWithCln() @@ -228,6 +238,8 @@ 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 29f23ab18..897f234d7 100644 --- a/src/base/configuration.h +++ b/src/base/configuration.h @@ -95,6 +95,8 @@ public: static bool isBuiltWithAbc(); + static bool isBuiltWithCadical(); + static bool isBuiltWithCryptominisat(); static bool isBuiltWithReadline(); diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h index eba45cc61..cf9117100 100644 --- a/src/base/configuration_private.h +++ b/src/base/configuration_private.h @@ -114,6 +114,12 @@ namespace CVC4 { # define IS_ABC_BUILD false #endif /* CVC4_USE_ABC */ +#if CVC4_USE_CADICAL +#define IS_CADICAL_BUILD true +#else /* CVC4_USE_CADICAL */ +#define IS_CADICAL_BUILD false +#endif /* CVC4_USE_CADICAL */ + #if CVC4_USE_CRYPTOMINISAT # define IS_CRYPTOMINISAT_BUILD true #else /* CVC4_USE_CRYPTOMINISAT */ |