From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Mon, 14 May 2018 22:36:52 +0000 (-0700)
Subject: Add contrib/get-symfpu for downloading symfpu. (#1905)
X-Git-Tag: cvc5-1.0.0~5055
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0c6681152ca422f7ace1bd1d3c3dac7823de2c14;p=cvc5.git

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

diff --git a/COPYING b/COPYING
index d6d727360..3299f4970 100644
--- 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
index 000000000..4e757685b
--- /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 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.
diff --git a/contrib/Makefile.am b/contrib/Makefile.am
index 72e354d97..4d61e88f4 100644
--- 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
index 000000000..f48d2d5b4
--- /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