summaryrefslogtreecommitdiff
path: root/src/base/configuration.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/base/configuration.cpp')
-rw-r--r--src/base/configuration.cpp14
1 files changed, 11 insertions, 3 deletions
diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp
index 7ceb64885..eb068152c 100644
--- a/src/base/configuration.cpp
+++ b/src/base/configuration.cpp
@@ -133,10 +133,10 @@ std::string Configuration::copyright() {
<< "See licenses/antlr3-LICENSE for copyright and licensing information."
<< "\n\n";
- if (Configuration::isBuiltWithAbc()
- || Configuration::isBuiltWithLfsc()
+ if (Configuration::isBuiltWithAbc() || Configuration::isBuiltWithLfsc()
|| Configuration::isBuiltWithCadical()
- || Configuration::isBuiltWithCryptominisat())
+ || Configuration::isBuiltWithCryptominisat()
+ || Configuration::isBuiltWithSymFPU())
{
ss << "This version of CVC4 is linked against the following non-(L)GPL'ed\n"
<< "third party libraries.\n\n";
@@ -162,6 +162,12 @@ std::string Configuration::copyright() {
<< " See https://github.com/msoos/cryptominisat for copyright "
<< "information.\n\n";
}
+ if (Configuration::isBuiltWithSymFPU())
+ {
+ ss << " SymFPU - The Symbolic Floating Point Unit\n"
+ << " See https://github.com/martin-cs/symfpu/tree/CVC4 for copyright "
+ << "information.\n\n";
+ }
}
if (Configuration::isBuiltWithGmp())
@@ -256,6 +262,8 @@ bool Configuration::isBuiltWithLfsc() {
return IS_LFSC_BUILD;
}
+bool Configuration::isBuiltWithSymFPU() { return IS_SYMFPU_BUILD; }
+
unsigned Configuration::getNumDebugTags() {
#if defined(CVC4_DEBUG) && defined(CVC4_TRACING)
/* -1 because a NULL pointer is inserted as the last value */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback