diff options
Diffstat (limited to 'src/base')
| -rw-r--r-- | src/base/configuration.cpp | 32 | ||||
| -rw-r--r-- | src/base/configuration.h | 4 | ||||
| -rw-r--r-- | src/base/configuration_private.h | 12 |
3 files changed, 12 insertions, 36 deletions
diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp index 61951841b..c6b004574 100644 --- a/src/base/configuration.cpp +++ b/src/base/configuration.cpp @@ -120,25 +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::isBuiltWithSymFPU() || 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" @@ -151,12 +149,6 @@ std::string Configuration::copyright() { << " See https://fmv.jku.at/kissat for copyright " << "information.\n\n"; } - if (Configuration::isBuiltWithSymFPU()) - { - ss << " SymFPU - The Symbolic Floating Point Unit\n" - << " See https://github.com/martin-cs/symfpu/tree/cvc5 for copyright " - << "information.\n\n"; - } if (Configuration::isBuiltWithEditline()) { ss << " Editline Library\n" @@ -165,6 +157,10 @@ std::string Configuration::copyright() { } } + ss << " SymFPU - The Symbolic Floating Point Unit\n" + << " See https://github.com/martin-cs/symfpu/tree/cvc5 for copyright " + << "information.\n\n"; + if (Configuration::isBuiltWithGmp() || Configuration::isBuiltWithPoly()) { ss << "This version of cvc5 is linked against the following third party\n" @@ -244,8 +240,6 @@ bool Configuration::isBuiltWithAbc() { return IS_ABC_BUILD; } -bool Configuration::isBuiltWithCadical() { return IS_CADICAL_BUILD; } - bool Configuration::isBuiltWithCryptominisat() { return IS_CRYPTOMINISAT_BUILD; } @@ -259,8 +253,6 @@ bool Configuration::isBuiltWithPoly() return IS_POLY_BUILD; } -bool Configuration::isBuiltWithSymFPU() { return IS_SYMFPU_BUILD; } - unsigned Configuration::getNumDebugTags() { #if defined(CVC5_DEBUG) && defined(CVC5_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 78e86f920..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(); @@ -113,8 +111,6 @@ public: static bool isBuiltWithPoly(); - static bool isBuiltWithSymFPU(); - /* Return the number of debug tags */ static unsigned getNumDebugTags(); /* Return a sorted array of the debug tags name */ diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h index 3027b23bc..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 */ @@ -126,12 +120,6 @@ namespace cvc5 { #define IS_EDITLINE_BUILD false #endif /* HAVE_LIBEDITLINE */ -#ifdef CVC5_USE_SYMFPU -#define IS_SYMFPU_BUILD true -#else /* HAVE_SYMFPU_HEADERS */ -#define IS_SYMFPU_BUILD false -#endif /* HAVE_SYMFPU_HEADERS */ - #if CVC5_GPL_DEPS # define IS_GPL_BUILD true #else /* CVC5_GPL_DEPS */ |