summaryrefslogtreecommitdiff
path: root/configure.ac
diff options
context:
space:
mode:
authorMathias Preiner <mathias.preiner@gmail.com>2018-05-14 15:36:52 -0700
committerGitHub <noreply@github.com>2018-05-14 15:36:52 -0700
commit0c6681152ca422f7ace1bd1d3c3dac7823de2c14 (patch)
tree84b7ab5df824cb26df70b437b6bb7ad41c30aadb /configure.ac
parentb5264346e85bc7ca0235048f686cc252c60b0014 (diff)
Add contrib/get-symfpu for downloading symfpu. (#1905)
Diffstat (limited to 'configure.ac')
-rw-r--r--configure.ac18
1 files changed, 17 insertions, 1 deletions
diff --git a/configure.ac b/configure.ac
index 92053daf6..1824da171 100644
--- a/configure.ac
+++ b/configure.ac
@@ -133,7 +133,8 @@ if test -z "${enable_optimized+set}" -a \
-z "${with_abc+set}" -a \
-z "${with_cadical+set}" -a \
-z "${with_cryptominisat+set}" -a \
- -z "${with_lfsc+set}"; then
+ -z "${with_lfsc+set}" -a \
+ -z "${with_symfpu+set}"; then
custom_build_profile=no
else
custom_build_profile=yes
@@ -253,6 +254,11 @@ if test -n "${with_lfsc+set}"; then
btargs="$btargs lfsc"
fi
fi
+if test -n "${with_symfpu+set}"; then
+ if test "$with_symfpu" = yes; then
+ btargs="$btargs symfpu"
+ fi
+fi
AC_MSG_RESULT([$with_build])
@@ -925,6 +931,16 @@ AM_CONDITIONAL([CVC4_USE_LFSC], [test $have_liblfsc -eq 1])
AC_SUBST([LFSC_LDFLAGS])
AC_SUBST([LFSC_LIBS])
+# Build with symfpu
+AC_ARG_WITH([symfpu],
+ [AS_HELP_STRING([--with-symfpu],
+ [use symfpu for floating point solver])], [], [with_symfpu=])
+CVC4_CHECK_FOR_SYMFPU
+if test $have_symfpu_headers -eq 1; then
+ CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_SYMFPU"
+ CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-I$SYMFPU_HOME"
+fi
+AM_CONDITIONAL([CVC4_USE_SYMFPU], [test $have_symfpu_headers -eq 1])
# Check to see if this version/architecture of GNU C++ explicitly
# instantiates std::hash<uint64_t> or not. Some do, some don't.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback