diff options
| -rw-r--r-- | configure.ac | 2 | ||||
| -rw-r--r-- | src/Makefile.am | 2 | ||||
| -rw-r--r-- | src/util/Makefile.am | 9 | ||||
| -rw-r--r-- | src/util/floatingpoint.h.in (renamed from src/util/floatingpoint.h) | 14 |
4 files changed, 17 insertions, 10 deletions
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 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 : |