diff options
Diffstat (limited to 'src/base/configuration.cpp')
| -rw-r--r-- | src/base/configuration.cpp | 32 |
1 files changed, 12 insertions, 20 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 */ |