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 /configure.ac | |
| 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 'configure.ac')
| -rw-r--r-- | configure.ac | 2 |
1 files changed, 2 insertions, 0 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]) |