diff options
author | Liana Hadarean <lianahady@gmail.com> | 2016-05-24 22:30:41 -0700 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2016-05-24 22:30:48 -0700 |
commit | 2591fc4f57030b31c2c49d5c2dae9e96d3ce3afa (patch) | |
tree | 0296cb4f8194aef27813ef5251e88f475c9a6ffb /config | |
parent | beaf8b212dfadb47328942c23a7649ab44a014cb (diff) |
Merged cryptominisat from experimental branch.
Diffstat (limited to 'config')
-rw-r--r-- | config/cryptominisat.m4 | 87 |
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 + |