summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorMathias Preiner <mathias.preiner@gmail.com>2017-10-03 16:09:38 -0700
committerGitHub <noreply@github.com>2017-10-03 16:09:38 -0700
commitb01ea5105589569428be93d121e02ae0c933aef3 (patch)
tree6d70c3d9b77ca7da3588f4ffa29bbc608524b6de /src
parentbca2ee1c42332abc8deb57d620b0fc32b5394634 (diff)
Add Cryptominisat and LFSC to --show-config output. (#1194)
Also removed obsolete CUDD related code.
Diffstat (limited to 'src')
-rw-r--r--src/base/configuration.cpp8
-rw-r--r--src/base/configuration.h4
-rw-r--r--src/options/options_handler.cpp15
3 files changed, 14 insertions, 13 deletions
diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp
index 90e560962..196290b53 100644
--- a/src/base/configuration.cpp
+++ b/src/base/configuration.cpp
@@ -142,14 +142,14 @@ bool Configuration::isBuiltWithReadline() {
return IS_READLINE_BUILD;
}
-bool Configuration::isBuiltWithCudd() {
- return false;
-}
-
bool Configuration::isBuiltWithTlsSupport() {
return USING_TLS;
}
+bool Configuration::isBuiltWithLfsc() {
+ return IS_LFSC_BUILD;
+}
+
unsigned Configuration::getNumDebugTags() {
#if defined(CVC4_DEBUG) && defined(CVC4_TRACING)
/* -1 because a NULL pointer is inserted as the last value */
diff --git a/src/base/configuration.h b/src/base/configuration.h
index 9a6abdb53..31c7b6547 100644
--- a/src/base/configuration.h
+++ b/src/base/configuration.h
@@ -97,10 +97,10 @@ public:
static bool isBuiltWithReadline();
- static bool isBuiltWithCudd();
-
static bool isBuiltWithTlsSupport();
+ static bool isBuiltWithLfsc();
+
/* Return the number of debug tags */
static unsigned getNumDebugTags();
/* Return a sorted array of the debug tags name */
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 87dc1ecc1..9adff0d3d 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -1409,13 +1409,14 @@ void OptionsHandler::showConfiguration(std::string option) {
printf("profiling : %s\n", Configuration::isProfilingBuild() ? "yes" : "no");
printf("competition: %s\n", Configuration::isCompetitionBuild() ? "yes" : "no");
printf("\n");
- printf("cudd : %s\n", Configuration::isBuiltWithCudd() ? "yes" : "no");
- printf("cln : %s\n", Configuration::isBuiltWithCln() ? "yes" : "no");
- printf("gmp : %s\n", Configuration::isBuiltWithGmp() ? "yes" : "no");
- printf("glpk : %s\n", Configuration::isBuiltWithGlpk() ? "yes" : "no");
- printf("abc : %s\n", Configuration::isBuiltWithAbc() ? "yes" : "no");
- printf("readline : %s\n", Configuration::isBuiltWithReadline() ? "yes" : "no");
- printf("tls : %s\n", Configuration::isBuiltWithTlsSupport() ? "yes" : "no");
+ printf("abc : %s\n", Configuration::isBuiltWithAbc() ? "yes" : "no");
+ printf("cln : %s\n", Configuration::isBuiltWithCln() ? "yes" : "no");
+ printf("glpk : %s\n", Configuration::isBuiltWithGlpk() ? "yes" : "no");
+ printf("cryptominisat: %s\n", Configuration::isBuiltWithCryptominisat() ? "yes" : "no");
+ printf("gmp : %s\n", Configuration::isBuiltWithGmp() ? "yes" : "no");
+ printf("lfsc : %s\n", Configuration::isBuiltWithLfsc() ? "yes" : "no");
+ printf("readline : %s\n", Configuration::isBuiltWithReadline() ? "yes" : "no");
+ printf("tls : %s\n", Configuration::isBuiltWithTlsSupport() ? "yes" : "no");
exit(0);
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback