From 13253bf7fe9d024bfeccf2d1b169ed78970a1acf Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Wed, 20 Jun 2018 13:32:18 -0700
Subject: [PATCH] Resolve CVC4_USE_SYMFPU in headers at config-time (#2077)

As described in issue #2013, we had `#ifdef CVC4_USE_SYMFPU` conditions
in floatingpoint.h, which was problematic when installing the header
files because the definition of `CVC4_USE_SYMFPU` was a compile-flag and
simply including the header files in another project would be missing
that definition. This commit moves floatingpoint.h to a template file
floatingpoint.h.in and substitutes the value of `CVC4_USE_SYMFPU` at
configure-time when generating floatingpoint.h (this is the same
solution that integer.h and rational.h use). I have tested the fix with
the examples provided in #2013 and they work.
---
 configure.ac                                     |  2 ++
 src/Makefile.am                                  |  2 ++
 src/util/Makefile.am                             |  9 ++++++---
 src/util/{floatingpoint.h => floatingpoint.h.in} | 14 +++++++-------
 4 files changed, 17 insertions(+), 10 deletions(-)
 rename src/util/{floatingpoint.h => floatingpoint.h.in} (99%)

diff --git a/configure.ac b/configure.ac
index d3f65d353..222a6b4f6 100644
--- a/configure.ac
+++ b/configure.ac
@@ -941,6 +941,7 @@ if test $have_symfpu_headers -eq 1; then
   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-I$SYMFPU_HOME"
 fi
 AM_CONDITIONAL([CVC4_USE_SYMFPU], [test $have_symfpu_headers -eq 1])
+AC_SUBST([CVC4_USE_SYMFPU], [$have_symfpu_headers])
 
 # Check to see if this version/architecture of GNU C++ explicitly
 # instantiates std::hash<uint64_t> or not.  Some do, some don't.
@@ -1559,6 +1560,7 @@ if test -n "$CVC4_LANGUAGE_BINDINGS"; then
   fi
 fi
 
+CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/floatingpoint.h])
 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/integer.h])
 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/rational.h])
 
diff --git a/src/Makefile.am b/src/Makefile.am
index aa4487c42..ce9f74d9e 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -727,6 +727,7 @@ install-data-local:
 	(echo include/cvc4.h; \
 	 echo include/cvc4_public.h; \
 	 echo include/cvc4parser_public.h; \
+	 echo util/floatingpoint.h; \
 	 echo util/integer.h; \
 	 echo util/rational.h; \
 	 find * -name '*.h' | \
@@ -759,6 +760,7 @@ uninstall-local:
 	-(echo include/cvc4.h; \
 	  echo include/cvc4_public.h; \
 	  echo include/cvc4parser_public.h; \
+	  echo util/floatingpoint.h; \
 	  echo util/integer.h; \
 	  echo util/rational.h; \
 	  find * -name '*.h' | \
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 158464d76..9117b9d6b 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -31,7 +31,6 @@ libutil_la_SOURCES = \
 	divisible.h \
 	dynamic_array.h \
 	floatingpoint.cpp \
-	floatingpoint.h \
 	gmp_util.h \
 	hash.h \
 	index.cpp \
@@ -64,8 +63,9 @@ libutil_la_SOURCES = \
 	utility.h
 
 BUILT_SOURCES = \
-	rational.h \
-	integer.h
+	floatingpoint.h \
+	integer.h \
+	rational.h
 
 if CVC4_CLN_IMP
 libutil_la_SOURCES += \
@@ -84,6 +84,7 @@ EXTRA_DIST = \
 	bool.i \
 	cardinality.i \
 	divisible.i \
+	floatingpoint.h.in \
 	floatingpoint.i \
 	hash.i \
 	integer.h.in \
@@ -109,7 +110,9 @@ EXTRA_DIST = \
 
 
 DISTCLEANFILES = \
+	floatingpoint.h.tmp \
 	integer.h.tmp \
 	rational.h.tmp \
+	floatingpoint.h \
 	integer.h \
 	rational.h
diff --git a/src/util/floatingpoint.h b/src/util/floatingpoint.h.in
similarity index 99%
rename from src/util/floatingpoint.h
rename to src/util/floatingpoint.h.in
index 95bec903e..a0406e360 100644
--- a/src/util/floatingpoint.h
+++ b/src/util/floatingpoint.h.in
@@ -25,9 +25,9 @@
 
 #include <fenv.h>
 
-#ifdef CVC4_USE_SYMFPU
-#include "symfpu/core/unpackedFloat.h"
-#endif
+#if @CVC4_USE_SYMFPU@
+#include <symfpu/core/unpackedFloat.h>
+#endif /* @CVC4_USE_SYMFPU@ */
 
 namespace CVC4 {
   // Inline these!
@@ -186,9 +186,9 @@ namespace CVC4 {
 
     friend wrappedBitVector<!isSigned>;  // To allow conversion between the
                                          // types
-#ifdef CVC4_USE_SYMFPU
+#if @CVC4_USE_SYMFPU@
     friend ::symfpu::ite<prop, wrappedBitVector<isSigned> >;  // For ITE
-#endif
+#endif /* @CVC4_USE_SYMFPU@ */
 
    public:
     wrappedBitVector(const bwt w, const unsigned v) : BitVector(w, v) {}
@@ -287,7 +287,7 @@ namespace CVC4 {
   /**
    * A concrete floating point number
    */
-#ifdef CVC4_USE_SYMFPU
+#if @CVC4_USE_SYMFPU@
   typedef ::symfpu::unpackedFloat<symfpuLiteral::traits> FloatingPointLiteral;
 #else
   class CVC4_PUBLIC FloatingPointLiteral {
@@ -309,7 +309,7 @@ namespace CVC4 {
       return 23;
     }
   };
-#endif
+#endif /* @CVC4_USE_SYMFPU@ */
 
   class CVC4_PUBLIC FloatingPoint {
   protected :
-- 
2.30.2