Added get-cryptominisat4 script.

5 files changed, 133 insertions, 18 deletions

diff --git a/config/cryptominisat.m4 b/config/cryptominisat.m4
new file mode 100644
index 000000000..f6e0967bb
--- /dev/null
+++ b/config/cryptominisat.m4
@@ -0,0 +1,60 @@
+# CVC4_CHECK_FOR_CRYPTOMINISAT
+# ------------------
+# Look for cryptominisat and link it in, but only if user requested.
+AC_DEFUN([CVC4_CHECK_FOR_CRYPTOMINISAT], [
+AC_MSG_CHECKING([whether user requested cryptominisat support])
+
+have_libcryptominisat=0
+CRYPTOMINISAT_LIBS=
+CRYPTOMINISAT_LDFLAGS=
+     
+have_libcryptominisat=0
+if test "$with_cryptominisat" = no; then
+  AC_MSG_RESULT([no, cryptominisat disabled by user])
+elif test -n "$with_cryptominisat"; then
+  AC_MSG_RESULT([yes, cryptominisat requested by user])
+  AC_ARG_VAR(CRYPTOMINISAT_HOME, [path to top level of cryptominisat source tree])
+  AC_ARG_WITH(
+    [cryptominisat-dir],
+    AS_HELP_STRING(
+      [--with-cryptominisat-dir=PATH],
+      [path to top level of cryptominisat source tree]
+    ),
+    [CRYPTOMINISAT_HOME="$withval"],
+    [ if test -z "$CRYPTOMINISAT_HOME"; then
+        AC_MSG_FAILURE([must give --with-cryptominisat-dir=PATH or define environment variable CRYPTOMINISAT_HOME!])
+      fi
+    ]
+  )
+
+  if ! test -d "$CRYPTOMINISAT_HOME" || ! test -x "$CRYPTOMINISAT_HOME/bin/cryptominisat" ; then
+    AC_MSG_FAILURE([either $CRYPTOMINISAT_HOME is not an cryptominisat install tree or it's not yet built])
+  fi
+
+  AC_LANG(C++)
+  cvc4_save_LIBS="$LIBS"
+  cvc4_save_LDFLAGS="$LDFLAGS"
+  cvc4_save_CPPFLAGS="$CPPFLAGS"
+
+  CRYPTOMINISAT_LDFLAGS="-L$CRYPTOMINISAT_HOME/lib"
+  CRYPTOMINISAT_LIBS="-lcryptominisat4 -lm4ri"
+
+  LDFLAGS="$LDFLAGS $CRYPTOMINISAT_LDFLAGS"
+  LIBS="$LIBS $CRYPTOMINISAT_LIBS"
+  
+  CPPFLAGS="$CPPFLAGS -I$CRYPTOMINISAT_HOME/include"
+
+  AC_LINK_IFELSE(
+    [AC_LANG_PROGRAM([#include <cryptominisat4/cryptominisat.h>],
+      [CMSat::SATSolver test()])], [have_libcryptominisat=1],
+    [AC_MSG_ERROR([libcryptominisat is not installed.])])
+
+  LDFLAGS="$cvc4_save_LDFLAGS"
+  CPPFLAGS="$cvc4_save_CPPFLAGS"
+  LIBS="$cvc4_save_LIBS"
+else
+  AC_MSG_RESULT([no, user didn't request cryptominisat])
+  with_cryptominisat=no
+fi
+
+])# CVC4_TRY_STATIC_CRYPTOMINISAT_WITH
diff --git a/configure.ac b/configure.ac
index f24d284aa..71f6d2f7f 100644
--- a/configure.ac
+++ b/configure.ac
@@ -794,28 +794,14 @@ AC_SUBST([ABC_LIBS])
 AC_ARG_WITH([cryptominisat],
   [AS_HELP_STRING([--with-cryptominisat],
      [use the CRYPTOMINISAT sat solver])], [], [with_cryptominisat=])
-have_libcryptominisat=0
-if test "$with_cryptominisat" = no; then
-  AC_MSG_RESULT([no, cryptominisat disabled by user])
-elif test -n "$with_cryptominisat"; then
-  AC_MSG_RESULT([yes, cryptominisat requested by user])
-  AC_LANG(C++)
-  SAVED_LDFLAGS=$LDFLAGS
-  LDFLAGS="$LDFLAGS -lcryptominisat4"
-  AC_LINK_IFELSE(
-    [AC_LANG_PROGRAM([#include <cryptominisat4/cryptominisat.h>],
-      [CMSat::SATSolver test()])],
-    [LIBS="$LIBS -lcryptominisat4 -lm4ri"] [have_libcryptominisat=1],
-    [AC_MSG_ERROR([libcryptominisat is not installed.])])
-  LDFLAGS=$SAVED_LDFLAGS
-else
-  AC_MSG_RESULT([no, user didn't request cryptominisat])
-  with_cryptominisat=no
-fi
+CVC4_CHECK_FOR_CRYPTOMINISAT
 if test $have_libcryptominisat -eq 1; then
   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_CRYPTOMINISAT"
+  CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-I$CRYPTOMINISAT_HOME/include"
 fi
 AM_CONDITIONAL([CVC4_USE_CRYPTOMINISAT], [test $have_libcryptominisat -eq 1])
+AC_SUBST([CRYPTOMINISAT_LDFLAGS])
+AC_SUBST([CRYPTOMINISAT_LIBS])
 
 # Build with libglucose
 AC_ARG_WITH([glucose],
diff --git a/contrib/cryptominisat-4.2.0.patch b/contrib/cryptominisat-4.2.0.patch
new file mode 100644
index 000000000..a180762bf
--- /dev/null
+++ b/contrib/cryptominisat-4.2.0.patch
@@ -0,0 +1,11 @@
+--- CMakeLists.txt	2014-07-18 00:17:48.000000000 +0100
++++ ../patched.txt	2015-10-14 16:32:58.632869087 +0100
+@@ -132,7 +132,7 @@
+     set(CMAKE_FIND_LIBRARY_SUFFIXES ".a")
+     SET(Boost_USE_STATIC_LIBS ON)
+     set(CMAKE_EXE_LINKER_FLAGS "-static -Wl,--whole-archive -lpthread -Wl,--no-whole-archive")
+-
++    add_cxx_flag_if_supported("-fPIC")
+     set(NOMYSQL ON)
+ else()
+     add_definitions(-DBOOST_TEST_DYN_LINK)
diff --git a/contrib/get-cryptominisat4 b/contrib/get-cryptominisat4
new file mode 100755
index 000000000..655e0fb8c
--- /dev/null
+++ b/contrib/get-cryptominisat4
@@ -0,0 +1,53 @@
+#!/bin/bash
+#
+set -e
+
+version="4.2.0"
+
+cd "$(dirname "$0")/.."
+
+if ! [ -e src/parser/cvc/Cvc.g ]; then
+  echo "$(basename $0): I expect to be in the contrib/ of a CVC4 source tree," >&2
+  echo "but apparently:" >&2
+  echo >&2
+  echo "  $(pwd)" >&2
+  echo >&2
+  echo "is not a CVC4 source tree ?!" >&2
+  exit 1
+fi
+
+function webget {
+  if which wget &>/dev/null; then
+    wget -c -O "$2" "$1"
+  elif which curl &>/dev/null; then
+    curl "$1" >"$2"
+  else
+    echo "Can't figure out how to download from web.  Please install wget or curl." >&2
+    exit 1
+  fi
+}
+
+if [ -e cryptominisat4 ]; then
+  echo 'error: file or directory "cryptominisat4" exists; please move it out of the way.' >&2
+  exit 1
+fi
+
+mkdir cryptominisat4
+cd cryptominisat4
+CRYPTOMINISAT_PATH=`pwd`
+
+webget https://github.com/msoos/cryptominisat/archive/$version.tar.gz cryptominisat-$version.tar.gz
+gunzip -f cryptominisat-$version.tar.gz
+tar xfv cryptominisat-$version.tar
+cd cryptominisat-$version
+
+patch -p0 < ../../contrib/cryptominisat-4.2.0.patch 
+
+cmake -DCMAKE_INSTALL_PREFIX:PATH=$CRYPTOMINISAT_PATH -DSTATICCOMPILE="ON" ./
+make install 
+
+cd ../
+
+echo
+echo ===================== Now configure CVC4 with =====================
+echo ./configure --with-cryptominisat --with-cryptominisat-dir=`pwd`
diff --git a/src/Makefile.am b/src/Makefile.am
index c92078590..5285e394c 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -461,6 +461,11 @@ libcvc4_la_LIBADD += $(ABC_LIBS)
 libcvc4_la_LDFLAGS += $(ABC_LDFLAGS)
 endif
 
+if CVC4_USE_CRYPTOMINISAT
+libcvc4_la_LIBADD += $(CRYPTOMINISAT_LIBS)
+libcvc4_la_LDFLAGS += $(CRYPTOMINISAT_LDFLAGS)
+endif
+
 BUILT_SOURCES = \
 	theory/rewriter_tables.h \
 	theory/theory_traits.h \