diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-09-02 20:41:08 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-09-02 20:41:08 +0000 |
commit | 1d18e5ebed9a5b20ed6a8fe21d11842acf6fa7ea (patch) | |
tree | 7074f04453914bc377ff6aeb307dd17b82b76ff3 /config/cudd.m4 | |
parent | 74770f1071e6102795393cf65dd0c651038db6b4 (diff) |
Merge from my post-smtcomp branch. Includes:
Dumping infrastructure. Can dump preprocessed queries and clauses. Can
also dump queries (for testing with another solver) to see if any conflicts
are missed, T-propagations are missed, all lemmas are T-valid, etc. For a
full list of options see --dump=help.
CUDD building much cleaner.
Documentation and assertion fixes.
Printer improvements, printing of commands in language-defined way, etc.
Typechecker stuff in expr package now autogenerated, no need to manually
edit the expr package when adding a new theory.
CVC3 compatibility layer (builds as libcompat).
SWIG detection and language binding support (infrastructure).
Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode
(when not in compliance mode).
Copyright and file headers regenerated.
Diffstat (limited to 'config/cudd.m4')
-rw-r--r-- | config/cudd.m4 | 116 |
1 files changed, 116 insertions, 0 deletions
diff --git a/config/cudd.m4 b/config/cudd.m4 new file mode 100644 index 000000000..7a569a3e9 --- /dev/null +++ b/config/cudd.m4 @@ -0,0 +1,116 @@ +# CVC4_CHECK_CUDD +# --------------- +# Check for CUDD libraries and headers. Complicated because different +# packagers have packaged it differently. +AC_DEFUN([CVC4_CHECK_CUDD], [ +CUDD_CPPFLAGS= +CUDD_LDFLAGS= +CUDD_LIBS= +cvc4cudd=no +AC_MSG_CHECKING([whether user requested CUDD support]) +AC_ARG_WITH([cudd], + [AS_HELP_STRING([--with-cudd], [force linking/not linking against CUDD])], + [with_cudd_set=yes], + [with_cudd=check; with_cudd_set=no]) +AC_ARG_WITH([cudd-dir], + [AS_HELP_STRING([--with-cudd-dir=DIR], [path to cudd installation])], + [CUDD_DIR="$withval"], + [if test "$with_cudd_set" = yes -a "$with_cudd" != yes -a "$with_cudd" != no -a "$with_cudd" != check; then + dnl maybe the user gave --with-cudd=DIR ? + CUDD_DIR="$with_cudd" + with_cudd=yes + fi]) +if test -n "$CUDD_DIR" -a "$with_cudd_set" = no; then + dnl if --with-cudd-dir or CUDD_DIR given, force --with-cudd + dnl unless --with-cudd=... given explicitly + with_cudd=yes +fi +if test "$with_cudd" = no; then + AC_MSG_RESULT([no, CUDD disabled by user]) +else + if test "$with_cudd" = check; then + AC_MSG_RESULT([no preference by user, will auto-detect]) + else + AC_MSG_RESULT([yes, CUDD enabled by user]) + fi + if test -z "$CUDD_DIR"; then + dnl default location if unspecified + CUDD_DIR=/usr + fi + AC_MSG_CHECKING([for C++ cudd includes under $CUDD_DIR]) + result="not found" + cvc4save_CPPFLAGS="$CPPFLAGS" + AC_LANG_PUSH([C++]) + for cuddinc in "$CUDD_DIR/include" "$CUDD_DIR/include/cudd" "$CUDD_DIR"; do + CPPFLAGS="$cvc4save_CPPFLAGS -I$cuddinc" + AC_COMPILE_IFELSE( + [AC_LANG_PROGRAM([ +#include <stdio.h> +#include "cuddObj.hh"], + [ +Cudd c; +BDD b = c.bddVar() | c.bddOne(); +])], + [ CUDD_CPPFLAGS="-I$cuddinc" + result="$cuddinc" + cvc4cudd=yes + break + ]) + done + CPPFLAGS="$cvc4save_CPPFLAGS" + AC_MSG_RESULT([$result]) + if test $cvc4cudd = yes; then + AC_MSG_CHECKING([for C++ cudd libraries under $CUDD_DIR]) + cvc4cudd=no + result="not found" + cvc4save_CPPFLAGS="$CPPFLAGS" + CPPFLAGS="$CPPFLAGS $CUDD_CPPFLAGS" + cvc4save_LDFLAGS="$LDFLAGS" + cvc4save_LIBS="$LIBS" + cvc4save_ac_link="$ac_link" + ac_link="libtool --mode=link $ac_link" + dnl This is messy. We try to find Fedora packages, Debian packages, and + dnl a built CUDD source directory. We can't -lutil or -lst because these + dnl names of CUDD libraries conflict with other libraries commonly + dnl installed. So we fall back to naming them directly. The CUDD + dnl sources build static libs only, so we go with that. + for cuddlibdirs in "-L$CUDD_DIR/lib" "-L$CUDD_DIR/lib/cudd" "-L$CUDD_DIR"; do + for cuddlibs in -lcuddxx -lcuddobj; do + LDFLAGS="$cvc4save_LDFLAGS $cuddlibdirs" + LIBS="$cvc4save_LIBS $cuddlibs" + AC_LINK_IFELSE( + [AC_LANG_PROGRAM([ +#include <stdio.h> +#include "cuddObj.hh"], + [ +Cudd c; +BDD b = c.bddVar() | c.bddOne(); +])], + [ CUDD_LDFLAGS="$cuddlibdirs" + CUDD_LIBS="$cuddlibs" + result="$cuddlibdirs $cuddlibs" + cvc4cudd=yes + break + ]) + done + if test -n "$CUDD_LDFLAGS"; then break; fi + done + CPPFLAGS="$cvc4save_CPPFLAGS" + LDFLAGS="$cvc4save_LDFLAGS" + LIBS="$cvc4save_LIBS" + ac_link="$cvc4save_ac_link" + AC_MSG_RESULT([$result]); + if test $cvc4cudd = yes; then + AC_DEFINE_UNQUOTED(CVC4_CUDD, [], [Defined if using the CU Decision Diagram package (cudd).]) + fi + fi + AC_LANG_POP([C++]) +fi +AC_SUBST([CUDD_CPPFLAGS]) +AC_SUBST([CUDD_LDFLAGS]) +AC_SUBST([CUDD_LIBS]) + +if test "$with_cudd" = yes -a "$cvc4cudd" = no; then + AC_ERROR([--with-cudd was given, but cudd not available]) +fi +])# CVC4_CHECK_CUDD |