summaryrefslogtreecommitdiff
path: root/src/util
diff options
context:
space:
mode:
Diffstat (limited to 'src/util')
-rw-r--r--src/util/Makefile.am9
-rw-r--r--src/util/floatingpoint.h.in (renamed from src/util/floatingpoint.h)14
2 files changed, 13 insertions, 10 deletions
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 :
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback