Add contrib/get-symfpu for downloading symfpu. (#1905)

diff --git a/COPYING b/COPYING
index d6d727360533e6d6f248c05a774fa709425e6378..3299f4970a12e4b9cd15bc76dcbc21631c0b140a 100644 (file)
--- a/COPYING
+++ b/COPYING
@@ -79,6 +79,11 @@ licenses/lgpl-3.0.txt for a copy of that license.  Note that according to the
 terms of the LGPL, both CVC4's source, and the combined work (CVC4 linked with
 GMP) may (and do) remain under the more permissive modified BSD license.
 
+The implementation of the floating point solver in CVC4 depends on symfpu
+(https://github.com/martin-cs/symfpu) written by Martin Brain.
+See https://raw.githubusercontent.com/martin-cs/symfpu/CVC4/LICENSE for
+copyright and licensing information.
+
 CVC4 optionally links against the following libraries:
 
   ABC                (https://bitbucket.org/alanmi/abc)

diff --git a/config/symfpu.m4 b/config/symfpu.m4
new file mode 100644 (file)
index 0000000..4e75768
--- /dev/null
+++ b/config/symfpu.m4
@@ -0,0 +1,40 @@
+# CVC4_CHECK_FOR_SYMFPU
+# ------------------
+# Look for symfpu and link it in, but only if user requested.
+AC_DEFUN([CVC4_CHECK_FOR_SYMFPU], [
+AC_MSG_CHECKING([whether user requested symfpu support])
+
+have_symfpu_headers=0
+if test "$with_symfpu" = no; then
+  AC_MSG_RESULT([no, symfpu disabled by user])
+elif test -n "$with_symfpu"; then
+  AC_MSG_RESULT([yes, symfpu requested by user])
+  AC_ARG_VAR(SYMFPU_HOME, [path to top level of symfpu source tree])
+  AC_ARG_WITH(
+    [symfpu-dir],
+    AS_HELP_STRING(
+      [--with-symfpu-dir=PATH],
+      [path to top level of symfpu source tree]
+    ),
+    SYMFPU_HOME="$withval",
+    [ if test -z "$SYMFPU_HOME" && ! test -e "$ac_abs_confdir/symfpu-CVC4/symfpu/core"; then
+        AC_MSG_FAILURE([must give --with-symfpu-dir=PATH, define environment variable SYMFPU_HOME, or use contrib/get-symfpu to setup symfpu for CVC4!])
+      fi
+    ]
+  )
+
+  # Check if symfpu was installed via contrib/get-symfpu or SYMFPU_HOME or --with-symfpu-dir was set
+  AC_MSG_CHECKING([whether symfpu was installed via contrib/get-symfpu])
+  if test -z "$SYMFPU_HOME" && test -e "$ac_abs_confdir/symfpu-CVC4/symfpu/core"; then
+    SYMFPU_HOME="$ac_abs_confdir/symfpu-CVC4"
+    AC_MSG_RESULT([yes, $SYMFPU_HOME])
+    have_symfpu_headers=1
+  else
+    AC_MSG_RESULT([no])
+  fi
+else
+  AC_MSG_RESULT([no, user didn't request symfpu])
+  with_symfpu=no
+fi
+
+])# CVC4_CHECK_FOR_SYMFPU

diff --git a/configure.ac b/configure.ac
index 92053daf642e8a58998f1ba561eafc7f9585fba5..1824da171710ecc6925698a05f61d37d50b2a456 100644 (file)
--- 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.

diff --git a/contrib/Makefile.am b/contrib/Makefile.am
index 72e354d97baaaa8f1f7b4982104da71b22d7fac6..4d61e88f4ac7e0a72fef913e291262e2f2f7ce64 100644 (file)
--- a/contrib/Makefile.am
+++ b/contrib/Makefile.am
@@ -10,8 +10,14 @@ EXTRA_DIST = \
        new-theory \
        configure-in-place \
        depgraph \
+       get-abc \
        get-antlr-3.4 \
+       get-cadical \
        get-cryptominisat \
+       get-glpk-cut-log \
+       get-lfsc-checker \
+       get-script-header.sh \
+       get-symfpu \
        get-win-dependencies \
        mac-build \
        run-script-smtcomp2014 \

diff --git a/contrib/get-symfpu b/contrib/get-symfpu
new file mode 100755 (executable)
index 0000000..f48d2d5
--- /dev/null
+++ b/contrib/get-symfpu
@@ -0,0 +1,24 @@
+#!/bin/bash
+#
+source "$(dirname "$0")/get-script-header.sh"
+
+wdir="symfpu-CVC4"
+
+if [ -e $wdir ]; then
+  echo "error: file or directory "$wdir" exists; please move it out of the way." >&2
+  exit 1
+fi
+
+commit="bdc0ad4cc49b5d590b4d8492199249e392c3368d"
+
+mkdir $wdir
+cd $wdir
+git clone https://github.com/martin-cs/symfpu.git symfpu
+cd symfpu
+git checkout $commit
+
+echo
+echo "Using symfpu commit $commit"
+echo
+echo ===================== Now configure CVC4 with =====================
+echo ./configure --with-symfpu