From df02923c0f0c6589098064d0dfac0de1ef27537c Mon Sep 17 00:00:00 2001
From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Mon, 21 May 2018 17:54:09 -0700
Subject: [PATCH] Add SymFPU licensing information. (#1952)

---
 configure.ac                     |  1 +
 src/base/configuration.cpp       | 14 +++++++++++---
 src/base/configuration.h         |  2 ++
 src/base/configuration_private.h |  6 ++++++
 src/options/options_handler.cpp  |  1 +
 5 files changed, 21 insertions(+), 3 deletions(-)

diff --git a/configure.ac b/configure.ac
index 1824da171..d3f65d353 100644
--- 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 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 */
diff --git a/src/base/configuration.h b/src/base/configuration.h
index 897f234d7..f98111181 100644
--- 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 cf9117100..018c7f800 100644
--- 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 9b2eb1cb2..41378e245 100644
--- 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);
-- 
2.30.2