Resolve CVC4_USE_SYMFPU in headers at config-time (#2077)
authorAndres Noetzli <andres.noetzli@gmail.com>
Wed, 20 Jun 2018 20:32:18 +0000 (13:32 -0700)
committerGitHub <noreply@github.com>
Wed, 20 Jun 2018 20:32:18 +0000 (13:32 -0700)
commit13253bf7fe9d024bfeccf2d1b169ed78970a1acf
tree77df6a092634963e7f7086a72c83b3f4cb4a80f7
parent06f9525d675048ba7d945c8d9acdf84896eb5fbb
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
src/Makefile.am
src/util/Makefile.am
src/util/floatingpoint.h [deleted file]
src/util/floatingpoint.h.in [new file with mode: 0644]