diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-06-20 13:32:18 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-06-20 13:32:18 -0700 |
| commit | 13253bf7fe9d024bfeccf2d1b169ed78970a1acf (patch) | |
| tree | 77df6a092634963e7f7086a72c83b3f4cb4a80f7 /src/util/Makefile.am | |
| parent | 06f9525d675048ba7d945c8d9acdf84896eb5fbb (diff) | |
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.
Diffstat (limited to 'src/util/Makefile.am')
| -rw-r--r-- | src/util/Makefile.am | 9 |
1 files changed, 6 insertions, 3 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 |