Add SymFPU licensing information. (#1952)

diff --git a/configure.ac b/configure.ac
index 1824da171710ecc6925698a05f61d37d50b2a456..d3f65d353c7afb2e1155bebba9e87fed057c8468 100644 (file)
--- a/configure.ac
+++ b/configure.ac
@@ -1608,6 +1608,7 @@ GLPK         : $with_glpk
 LFSC         : $with_lfsc
 MP library   : $mplibrary
 Readline     : $with_readline
+SymFPU       : $with_symfpu
 
 CPPFLAGS     : $CPPFLAGS
 CXXFLAGS     : $CXXFLAGS

diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp
index 7ceb648859e4a36d41914b50bbad740aea4c6427..eb068152cba782d75fa09ca51b6e2ef668188ac5 100644 (file)
--- 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 */

diff --git a/src/base/configuration.h b/src/base/configuration.h
index 897f234d744f83d1d8a13427dbcd2a78f13d97c4..f981111810ebaf0bb2136bcec52b6fad9ac0cdd9 100644 (file)
--- a/src/base/configuration.h
+++ b/src/base/configuration.h
@@ -105,6 +105,8 @@ public:
 
   static bool isBuiltWithLfsc();
 
+  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 cf911710073b428bd2adf9827790c271d314b586..018c7f8001d2ae0374818eca4b91c21282eae02a 100644 (file)
--- a/src/base/configuration_private.h
+++ b/src/base/configuration_private.h
@@ -138,6 +138,12 @@ namespace CVC4 {
 #  define IS_READLINE_BUILD false
 #endif /* HAVE_LIBREADLINE */
 
+#ifdef CVC4_USE_SYMFPU
+#define IS_SYMFPU_BUILD true
+#else /* HAVE_SYMFPU_HEADERS */
+#define IS_SYMFPU_BUILD false
+#endif /* HAVE_SYMFPU_HEADERS */
+
 #if CVC4_GPL_DEPS
 #  define IS_GPL_BUILD true
 #else /* CVC4_GPL_DEPS */

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 9b2eb1cb2540cf7381e496f9787c7285aca01d18..41378e245306957bf2b35db12638a41bd9a30f1f 100644 (file)
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -1693,6 +1693,7 @@ void OptionsHandler::showConfiguration(std::string option) {
   print_config_cond("gmp", Configuration::isBuiltWithGmp());
   print_config_cond("lfsc", Configuration::isBuiltWithLfsc());
   print_config_cond("readline", Configuration::isBuiltWithReadline());
+  print_config_cond("symfpu", Configuration::isBuiltWithSymFPU());
   print_config_cond("tls", Configuration::isBuiltWithTlsSupport());
   
   exit(0);