summaryrefslogtreecommitdiff
path: root/config
diff options
context:
space:
mode:
Diffstat (limited to 'config')
-rw-r--r--config/cryptominisat.m487
1 files changed, 87 insertions, 0 deletions
diff --git a/config/cryptominisat.m4 b/config/cryptominisat.m4
new file mode 100644
index 000000000..f7d3a1544
--- /dev/null
+++ b/config/cryptominisat.m4
@@ -0,0 +1,87 @@
+# 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/install/bin/cryptominisat" ; then
+ AC_MSG_FAILURE([either $CRYPTOMINISAT_HOME is not an cryptominisat install tree or it's not yet built])
+ fi
+
+ CPPFLAGS="$CPPFLAGS -I$CRYPTOMINISAT_HOME/install/include"
+
+ AC_MSG_CHECKING([how to link cryptominisat])
+
+ dnl TODO FIXME:
+ dnl For some reason the CVC4_TRY_CRYPTOMINISAT is not working correctly
+ CVC4_TRY_CRYPTOMINISAT_WITH([])
+ CVC4_TRY_CRYPTOMINISAT_WITH([-lm4ri])
+
+ if test -z "$CRYPTOMINISAT_LIBS"; then
+ AC_MSG_FAILURE([cannot link against libcryptominisat!])
+ else
+ AC_MSG_RESULT([$CRYPTOMINISAT_LIBS])
+ have_libcryptominisat=1
+ fi
+
+ CRYPTOMINISAT_LDFLAGS="-L$CRYPTOMINISAT_HOME/install/lib"
+ CRYPTOMINISAT_LIBS="-lcryptominisat4 -lm4ri"
+
+else
+ AC_MSG_RESULT([no, user didn't request cryptominisat])
+ with_cryptominisat=no
+fi
+
+])# CVC4_CHECK_FOR_CRYPTOMINISAT
+
+# CVC4_TRY_STATIC_CRYPTOMINISAT_WITH(LIBS)
+# ------------------------------
+# Try AC_CHECK_LIB(cryptominisat) with the given linking libraries
+AC_DEFUN([CVC4_TRY_CRYPTOMINISAT_WITH], [
+if test -z "$CRYPTOMINISAT_LIBS"; then
+ AC_LANG_PUSH([C++])
+
+ cvc4_save_LIBS="$LIBS"
+ cvc4_save_LDFLAGS="$LDFLAGS"
+ cvc4_save_CPPFLAGS="$CPPFLAGS"
+
+ LDFLAGS="-L$CRYPTOMINISAT_HOME/install/lib"
+ LIBS="-lcryptominisat4 $1"
+
+
+ AC_LINK_IFELSE(
+ [AC_LANG_PROGRAM([#include <cryptominisat4/cryptominisat.h>],
+ [CMSat::SATSolver test()])], [CRYPTOMINISAT_LIBS="-lcryptominisat4 $1"],
+ [CRYPTOMINISAT_LIBS=])
+
+ LDFLAGS="$cvc4_save_LDFLAGS"
+ CPPFLAGS="$cvc4_save_CPPFLAGS"
+ LIBS="$cvc4_save_LIBS"
+
+ AC_LANG_POP([C++])
+fi
+])# CVC4_TRY_CRYPTOMINISAT_WITH
+
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback