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

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)

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

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.

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 \

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