Optional: SWIG 2.0.x (Simplified Wrapper and Interface Generator)
Optional: CLN v1.3 or newer (Class Library for Numbers)
- Optional: CUDD v2.4.2 or newer (Colorado University Decision Diagram package)
Optional: GNU Readline library (for an improved interactive experience)
Optional: The Boost C++ threading library (libboost_thread)
Optional: CxxTest unit testing framework
COPYING in the CVC4 source distribution for details.) Please visit
http://www.ginac.de/CLN/ for more details about CLN.
-CUDD is a decision diagram package that changes the behavior of the
-CVC4 arithmetic solver in some cases; it may or may not improve the
-arithmetic solver's performance. See below for instructions on
-obtaining and building CUDD.
-
The GNU Readline library is optionally used to provide command
editing, tab completion, and history functionality at the CVC prompt
(when running in interactive mode). Check your distribution for a
source tree. However, if you're interested, you can download CxxTest
at http://cxxtest.com/ .
-*** Building with CUDD (optional)
-
-CUDD, if desired, must be installed delicately. The CVC4 configure
-script attempts to auto-detect the locations and names of CUDD headers
-and libraries the way that the Fedora RPMs install them, the way that
-our NYU-provided Debian packages install them, and the way they exist
-when you download and build the CUDD sources directly. If you install
-from Fedora RPMs or our Debian packages, the process should be
-completely automatic, since the libraries and headers are installed in
-a standard location. If you download the sources yourself, you need
-to build them in a special way. Fortunately, the
-"contrib/build-cudd-2.4.2-with-libtool.sh" script in the CVC4 source
-tree does exactly what you need: it patches the CUDD makefiles to use
-libtool, builds the libtool libraries, then reverses the patch to
-leave the makefiles as they were. Once you run this script on an
-unpacked CUDD 2.4.2 source distribution, then CVC4's configure script
-should pick up the libraries if you provide
---with-cudd-dir=/PATH/TO/CUDD/SOURCES.
-
-If you want to force linking to CUDD, provide --with-cudd to the
-configure script; this makes it a hard requirement rather than an
-optional add-on.
-
-The NYU-provided Debian packaging of CUDD 2.4.2 and CUDD 2.5.0 are
-here (along with the CVC4 Debian packages):
-
- deb http://cvc4.cs.nyu.edu/debian/ unstable/
-
-On Debian (and Debian-derived distributions like Ubuntu), you only
-need to drop that one line in your /etc/apt/sources.list file, and
-then install with your favorite package manager.
-
-The Debian source package "cudd", available from the same repository,
-includes a diff of all changes made to cudd makefiles.
-
*** Language bindings
There are several options available for using CVC4 from the API.
exit 1; \
fi
./autogen.sh
- ./configure competition --disable-shared --enable-static-binary --with-cln --without-cudd
+ ./configure competition --disable-shared --enable-static-binary --with-cln
$(MAKE)
strip builds/bin/cvc4
$(MAKE) check
exit 1; \
fi
./autogen.sh
- ./configure competition --disable-shared --enable-static-binary --with-cln --without-cudd CXXFLAGS=-DCVC4_SMTCOMP_APPLICATION_TRACK CFLAGS=-DCVC4_SMTCOMP_APPLICATION_TRACK
+ ./configure competition --disable-shared --enable-static-binary --with-cln CXXFLAGS=-DCVC4_SMTCOMP_APPLICATION_TRACK CFLAGS=-DCVC4_SMTCOMP_APPLICATION_TRACK
$(MAKE)
strip builds/bin/cvc4
$(MAKE) check
exit 1; \
fi
./autogen.sh
- ./configure competition --disable-shared --enable-static-binary --with-gmp --without-cudd --with-portfolio
+ ./configure competition --disable-shared --enable-static-binary --with-gmp --with-portfolio
$(MAKE)
strip builds/bin/pcvc4
# some test cases fail (and are known to fail)
+++ /dev/null
-# 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=no; 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
- if test "$with_cudd_set" = no; then
- AC_MSG_RESULT([no (enable with --with-cudd)])
- else
- AC_MSG_RESULT([no, CUDD disabled by user])
- fi
-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
[Defined to 1 if ffs() is supported by the platform.])],
[AC_LIBOBJ([ffs])])
-# Check for the presence of CUDD libraries
-CVC4_CHECK_CUDD
-
# Check for antlr C++ runtime (defined in config/antlr.m4)
AC_LIB_ANTLR
Proof tests : $support_proof_tests
gcov support : $enable_coverage
gprof support: $enable_profiling
-CUDD : $cvc4cudd
Readline : $with_readline
Static libs : $enable_static
configure-in-place \
depgraph \
get-antlr-3.4 \
- build-cudd-2.4.2-with-libtool.sh \
- build-cudd-2.5.0-with-libtool.sh \
mac-build \
win32-build \
run-script-smtcomp2012 \
+++ /dev/null
-#!/bin/bash
-#
-# Patch to cudd build system to build everything with libtool, supporting
-# shared libraries. Also all libraries are combined into a single one.
-#
-# This script applies the patch, builds cudd, and, assuming there are no
-# errors, reverses the patch.
-#
-# -- Morgan Deters <mdeters@cs.nyu.edu> Wed, 13 Jul 2011 18:03:11 -0400
-#
-
-cd "$(dirname "$0")"
-if [ $# -ne 1 -o "$1" = -h -o "$1" = -help -o "$1" = --help ]; then
- echo "usage: $(basename "$0") cudd-dir" >&2
- exit 1
-fi
-
-patch="$(pwd)/$(basename "$0")"
-if [ ! -r "$patch" ]; then
- echo "error: can't read patch at \`$patch'" >&2
- exit 1
-fi
-if ! expr "$1" : / &>/dev/null; then
- echo "error: must specify an absolute path to cudd sources" >&2
- exit 1
-fi
-cudd_dir="$1"
-
-arch=$(../config/config.guess | cut -f1 -d-)
-case "$arch" in
- i?86) XCFLAGS='-mtune=pentium4 -malign-double -DHAVE_IEEE_754 -DBSD' ;;
- x86_64) XCFLAGS='-mtune=native -DHAVE_IEEE_754 -DBSD -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8' ;;
- *) XCFLAGS= ;;
-esac
-
-set -ex
-
-XCFLAGS="$XCFLAGS"
-
-version_info=0:0:0
-
-prefix="$cudd_dir"
-eprefix="$prefix"
-bindir="$eprefix/bin"
-datadir="$prefix/share"
-includedir="$prefix/include"
-libdir="$prefix/lib"
-mandir="$datadir/man/man1"
-docdir="$datadir/doc"
-
-cd "$cudd_dir"
-patch -p1 < "$patch"
-make "XCFLAGS=$XCFLAGS" "CC=libtool --mode=compile gcc" "CPP=libtool --mode=compile g++" libdir="$libdir" version_info="$version_info" DDDEBUG= MTRDEBUG= ICFLAGS=-O2
-mkdir -p "$libdir"
-libtool --mode=install cp libcudd.la "$libdir/libcudd.la"
-libtool --mode=install cp libcuddxx.la "$libdir/libcuddxx.la"
-libtool --mode=install cp libdddmp.la "$libdir/libdddmp.la"
-libtool --finish "$libdir"
-patch -p1 -R < "$patch"
-exit
-
-# patch follows
-
---- a/Makefile
-+++ b/Makefile
-@@ -221,11 +221,16 @@
-
- build:
- sh ./setup.sh
-- @for dir in $(DIRS); do \
-+ +@for dir in $(BDIRS) obj; do \
- (cd $$dir; \
- echo Making $$dir ...; \
-- make CC=$(CC) RANLIB=$(RANLIB) MFLAG= MNEMLIB= ICFLAGS="$(ICFLAGS)" XCFLAGS="$(XCFLAGS)" DDDEBUG="$(DDDEBUG)" MTRDEBUG="$(MTRDEBUG)" LDFLAGS="$(LDFLAGS)" PURE="$(PURE)" EXE="$(EXE)" )\
-+ make CC="$(CC)" RANLIB="$(RANLIB)" MFLAG= MNEMLIB= ICFLAGS="$(ICFLAGS)" XCFLAGS="$(XCFLAGS)" DDDEBUG="$(DDDEBUG)" MTRDEBUG="$(MTRDEBUG)" LDFLAGS="$(LDFLAGS)" PURE="$(PURE)" EXE="$(EXE)" )\
- done
-+ libtool --mode=link gcc -rpath "$(libdir)" -version-info "$(version_info)" -o libcudd.la cudd/libcudd.la mtr/libmtr.la epd/libepd.la util/libutil.la st/libst.la -lm
-+ libtool --mode=link gcc -rpath "${libdir}" -version-info "$(version_info)" -o libdddmp.la dddmp/libdddmp.la
-+ libtool --mode=link g++ -rpath "$(libdir)" -version-info "$(version_info)" -o libcuddxx.la obj/libobj.la -lcudd
-+ +@(cd nanotrav; \
-+ make CC="$(CC)" RANLIB="$(RANLIB)" MFLAG= MNEMLIB= ICFLAGS="$(ICFLAGS)" XCFLAGS="$(XCFLAGS)" DDDEBUG="$(DDDEBUG)" MTRDEBUG="$(MTRDEBUG)" LDFLAGS="$(LDFLAGS)" PURE="$(PURE)" EXE="$(EXE)" )
-
- nanotrav: build
-
-@@ -319,4 +324,6 @@
- echo Cleaning $$dir ...; \
- make -s EXE="$(EXE)" distclean ) \
- done
-+ rm -f libcudd* libdddmp*
-+ rm -fr .libs
- sh ./shutdown.sh
---- a/cudd/Makefile
-+++ b/cudd/Makefile
-@@ -59,7 +59,7 @@
- cuddZddPort.c cuddZddReord.c cuddZddSetop.c cuddZddSymm.c \
- cuddZddUtil.c
- PHDR = cudd.h cuddInt.h
--POBJ = $(PSRC:.c=.o)
-+POBJ = $(PSRC:.c=.lo)
- PUBJ = $(PSRC:.c=.u)
- TARGET = test$(P)$(EXE)
- TARGETu = test$(P)-u
-@@ -71,12 +71,11 @@
-
- #------------------------------------------------------
-
--lib$(P).a: $(POBJ)
-- ar rv $@ $?
-- $(RANLIB) $@
-+lib$(P).la: $(POBJ)
-+ libtool --mode=link gcc -o $@ $?
-
--.c.o: $(PSRC) $(PHDR)
-- $(CC) -c $< -I$(INCLUDE) $(CFLAGS) $(DDDEBUG)
-+%.lo: %.c
-+ $(CC) -c -o $@ $< -I$(INCLUDE) $(CFLAGS) $(DDDEBUG)
-
- optimize_dec: lib$(P).b
-
-@@ -116,9 +115,10 @@
- programs: $(TARGET) $(TARGETu) lintpgm
-
- clean:
-- rm -f *.o *.u mon.out gmon.out *.pixie *.Addrs *.Counts mnem.* \
-+ rm -f *.o *.lo *.u mon.out gmon.out *.pixie *.Addrs *.Counts mnem.* \
- .pure core *.warnings
-
- distclean: clean
-- rm -f $(TARGET) $(TARGETu) lib*.a lib$(P).b llib-l$(P).ln \
-+ rm -f $(TARGET) $(TARGETu) lib*.a lib*.la lib$(P).b llib-l$(P).ln \
- *.bak *~ tags .gdb_history *.qv *.qx
-+ rm -fr .libs
---- a/dddmp/Makefile
-+++ b/dddmp/Makefile
-@@ -148,7 +148,7 @@
- dddmpStoreMisc.c dddmpUtil.c dddmpBinary.c dddmpConvert.c \
- dddmpDbg.c
- PHDR = dddmp.h dddmpInt.h $(INCLUDE)/cudd.h $(INCLUDE)/cuddInt.h
--POBJ = $(PSRC:.c=.o)
-+POBJ = $(PSRC:.c=.lo)
- PUBJ = $(PSRC:.c=.u)
- TARGET = test$(P)$(EXE)
- TARGETu = test$(P)-u
-@@ -182,12 +182,11 @@
- $(WHERE)/mtr/llib-lmtr.ln $(WHERE)/st/llib-lst.ln \
- $(WHERE)/util/llib-lutil.ln
-
--lib$(P).a: $(POBJ)
-- ar rv $@ $?
-- $(RANLIB) $@
-+lib$(P).la: $(POBJ)
-+ libtool --mode=link gcc -o $@ $?
-
--.c.o: $(PHDR)
-- $(CC) -c $< -I$(INCLUDE) $(ICFLAGS) $(XCFLAGS) $(DDDEBUG) $(MTRDEBUG) $(DDDMPDEBUG) $(LDFLAGS)
-+%.lo: %.c
-+ $(CC) -c -o $@ $< -I$(INCLUDE) $(ICFLAGS) $(XCFLAGS) $(DDDEBUG) $(MTRDEBUG) $(DDDMPDEBUG) $(LDFLAGS)
-
- optimize_dec: lib$(P).b
-
-@@ -231,12 +230,13 @@
- #----------------------------------------------------------------------------#
-
- clean:
-- rm -f *.o *.u mon.out gmon.out *.pixie *.Addrs *.Counts mnem.* \
-+ rm -f *.o *.lo *.u mon.out gmon.out *.pixie *.Addrs *.Counts mnem.* \
- .pure core *.warnings
-
- distclean: clean
-- rm -f $(TARGET) $(TARGETu) lib*.a lib$(P).b llib-l$(P).ln \
-+ rm -f $(TARGET) $(TARGETu) lib*.a lib*.la lib$(P).b llib-l$(P).ln \
- *.bak *~ tags .gdb_history *.qv *.qx
-+ rm -fr .libs
-
-
-
---- a/epd/Makefile
-+++ b/epd/Makefile
-@@ -19,7 +19,7 @@
- P = epd
- PSRC = epd.c
- PHDR = epd.h
--POBJ = $(PSRC:.c=.o)
-+POBJ = $(PSRC:.c=.lo)
- PUBJ = $(PSRC:.c=.u)
-
- WHERE = ..
-@@ -27,12 +27,11 @@
-
- #---------------------------
-
--lib$(P).a: $(POBJ)
-- ar rv $@ $?
-- $(RANLIB) $@
-+lib$(P).la: $(POBJ)
-+ libtool --mode=link gcc -o $@ $?
-
--.c.o: $(PSRC) $(PHDR)
-- $(CC) -c $< -I$(INCLUDE) $(CFLAGS)
-+%.lo: %.c
-+ $(CC) -c -o $@ $< -I$(INCLUDE) $(CFLAGS)
-
- optimize_dec: lib$(P).b
-
-@@ -58,7 +57,8 @@
- all: lib$(P).a lib$(P).b llib-l$(P).ln tags
-
- clean:
-- rm -f *.o *.u .pure *.warnings
-+ rm -f *.o *.lo *.u .pure *.warnings
-
- distclean: clean
-- rm -f lib*.a lib$(P).b llib-l$(P).ln tags *~ *.bak *.qv *.qx
-+ rm -f lib*.a lib*.la lib$(P).b llib-l$(P).ln tags *~ *.bak *.qv *.qx
-+ rm -fr .libs
---- a/mtr/Makefile
-+++ b/mtr/Makefile
-@@ -30,7 +30,7 @@
- P = mtr
- PSRC = mtrBasic.c mtrGroup.c
- PHDR = mtr.h
--POBJ = $(PSRC:.c=.o)
-+POBJ = $(PSRC:.c=.lo)
- PUBJ = $(PSRC:.c=.u)
- SRC = test$(P).c
- HDR =
-@@ -49,12 +49,11 @@
-
- #---------------------------
-
--lib$(P).a: $(POBJ)
-- ar rv $@ $?
-- $(RANLIB) $@
-+lib$(P).la: $(POBJ)
-+ libtool --mode=link gcc -o $@ $?
-
--.c.o: $(PSRC) $(PHDR)
-- $(CC) -c $< -I$(INCLUDE) $(CFLAGS) $(MTRDEBUG)
-+%.lo: %.c
-+ $(CC) -c -o $@ $< -I$(INCLUDE) $(CFLAGS) $(MTRDEBUG)
-
- optimize_dec: lib$(P).b
-
-@@ -88,9 +87,10 @@
- cc -O3 $(XCFLAGS) $(LDFLAGS) -o $@ $(UBJ) $(BLIBS) -lm
-
- clean:
-- rm -f *.o *.u mon.out gmon.out *.pixie *.Addrs *.Counts mnem.* \
-+ rm -f *.o *.lo *.u mon.out gmon.out *.pixie *.Addrs *.Counts mnem.* \
- .pure core *.warnings
-
- distclean: clean
-- rm -f $(TARGET) $(TARGETu) lib*.a lib$(P).b llib-l$(P).ln \
-+ rm -f $(TARGET) $(TARGETu) lib*.a lib*.la lib$(P).b llib-l$(P).ln \
- *.bak *~ tags *.qv *.qx
-+ rm -fr .libs
---- a/nanotrav/Makefile
-+++ b/nanotrav/Makefile
-@@ -19,9 +19,7 @@
-
- INCLUDE = $(WHERE)/include
-
--LIBS = $(WHERE)/dddmp/libdddmp.a $(WHERE)/cudd/libcudd.a \
-- $(WHERE)/mtr/libmtr.a $(WHERE)/st/libst.a $(WHERE)/util/libutil.a \
-- $(WHERE)/epd/libepd.a
-+LIBS = $(WHERE)/libcudd.la $(WHERE)/libdddmp.la
-
- MNEMLIB =
- #MNEMLIB = $(WHERE)/mnemosyne/libmnem.a
-@@ -39,7 +37,7 @@
- HDR = bnet.h ntr.h $(WHERE)/include/dddmp.h $(WHERE)/include/cudd.h \
- $(WHERE)/include/cuddInt.h
-
--OBJ = $(SRC:.c=.o)
-+OBJ = $(SRC:.c=.lo)
- UBJ = $(SRC:.c=.u)
-
- MFLAG =
-@@ -61,10 +59,10 @@
- #------------------------------------------------------
-
- $(TARGET): $(SRC) $(OBJ) $(HDR) $(LIBS) $(MNEMLIB)
-- $(PURE) $(CC) $(CFLAGS) $(LDFLAGS) -o $@ $(OBJ) $(LIBS) $(MNEMLIB) -lm
-+ libtool --mode=link gcc $(CFLAGS) $(LDFLAGS) -o $@ $(OBJ) $(LIBS) $(MNEMLIB) -lm
-
--.c.o: $(HDR)
-- $(CC) -c $< -I$(INCLUDE) $(CFLAGS) $(DDDEBUG)
-+%.lo: %.c
-+ $(CC) -c -o $@ $< -I$(INCLUDE) $(CFLAGS) $(DDDEBUG)
-
- # if the header files change, recompile
- $(OBJ): $(HDR)
-@@ -91,8 +89,9 @@
- pixie $(TARGETu)
-
- clean:
-- rm -f *.o *.u mon.out gmon.out *.pixie *.Addrs *.Counts mnem.* \
-+ rm -f *.o *.lo *.u mon.out gmon.out *.pixie *.Addrs *.Counts mnem.* \
- .pure core *.warnings
-
- distclean: clean
- rm -f $(TARGET) $(TARGETu) *.bak *~ .gdb_history *.qv *.qx
-+ rm -fr .libs
---- a/obj/Makefile
-+++ b/obj/Makefile
-@@ -45,7 +45,7 @@
- P = obj
- PSRC = cuddObj.cc
- PHDR = cuddObj.hh $(INCLUDE)/cudd.h
--POBJ = $(PSRC:.cc=.o)
-+POBJ = $(PSRC:.cc=.lo)
- PUBJ = $(PSRC:.cc=.u)
- TARGET = test$(P)$(EXE)
- TARGETu = test$(P)-u
-@@ -57,12 +57,11 @@
-
- #------------------------------------------------------
-
--lib$(P).a: $(POBJ)
-- ar rv $@ $?
-- $(RANLIB) $@
-+lib$(P).la: $(POBJ)
-+ libtool --mode=link g++ -o $@ $?
-
--.cc.o: $(PHDR)
-- $(CPP) -c $< -I$(INCLUDE) $(CFLAGS) $(DDDEBUG)
-+%.lo: %.cc
-+ $(CPP) -c -o $@ $< -I$(INCLUDE) $(CFLAGS) $(DDDEBUG)
-
- optimize_dec: lib$(P).b
-
-@@ -102,9 +101,10 @@
- programs: $(TARGET) $(TARGETu) lintpgm
-
- clean:
-- rm -f *.o *.u mon.out gmon.out *.pixie *.Addrs *.Counts mnem.* \
-+ rm -f *.o *.lo *.u mon.out gmon.out *.pixie *.Addrs *.Counts mnem.* \
- .pure core *.warnings
-
- distclean: clean
-- rm -f $(TARGET) $(TARGETu) lib*.a lib$(P).b llib-l$(P).ln \
-+ rm -f $(TARGET) $(TARGETu) lib*.a lib*.la lib$(P).b llib-l$(P).ln \
- *.bak *~ tags .gdb_history *.qv *.qx
-+ rm -fr .libs
---- a/st/Makefile
-+++ b/st/Makefile
-@@ -19,7 +19,7 @@
- P = st
- PSRC = st.c
- PHDR = st.h
--POBJ = $(PSRC:.c=.o)
-+POBJ = $(PSRC:.c=.lo)
- PUBJ = $(PSRC:.c=.u)
-
- WHERE = ..
-@@ -27,12 +27,11 @@
-
- #---------------------------
-
--lib$(P).a: $(POBJ)
-- ar rv $@ $?
-- $(RANLIB) $@
-+lib$(P).la: $(POBJ)
-+ libtool --mode=link gcc -o $@ $?
-
--.c.o: $(PHDR)
-- $(CC) -c $< -I$(INCLUDE) $(CFLAGS)
-+%.lo: %.c
-+ $(CC) -c -o $@ $< -I$(INCLUDE) $(CFLAGS)
-
- optimize_dec: lib$(P).b
-
-@@ -58,7 +57,8 @@
- all: lib$(P).a lib$(P).b llib-l$(P).ln tags
-
- clean:
-- rm -f *.o *.u .pure *.warnings
-+ rm -f *.o *.lo *.u .pure *.warnings
-
- distclean: clean
-- rm -f lib*.a lib$(P).b llib-l$(P).ln tags *~ *.bak *.qv *.qx
-+ rm -f lib*.a lib*.la lib$(P).b llib-l$(P).ln tags *~ *.bak *.qv *.qx
-+ rm -fr .libs
---- a/util/Makefile
-+++ b/util/Makefile
-@@ -21,19 +21,18 @@
- PSRC = cpu_time.c cpu_stats.c getopt.c safe_mem.c strsav.c texpand.c \
- ptime.c prtime.c pipefork.c pathsearch.c stub.c \
- tmpfile.c datalimit.c
--POBJ = $(PSRC:.c=.o)
-+POBJ = $(PSRC:.c=.lo)
- PUBJ = $(PSRC:.c=.u)
- PHDR = util.h
-
- WHERE = ..
- INCLUDE = $(WHERE)/include
-
--lib$(P).a: $(POBJ)
-- ar rv $@ $?
-- $(RANLIB) $@
-+lib$(P).la: $(POBJ)
-+ libtool --mode=link gcc -o $@ $?
-
--.c.o: $(PHDR)
-- $(CC) -c $< -I$(INCLUDE) $(FLAGS) $(CFLAGS)
-+%.lo: %.c
-+ $(CC) -c -o $@ $< -I$(INCLUDE) $(FLAGS) $(CFLAGS)
-
- optimize_dec: lib$(P).b
-
-@@ -59,7 +58,8 @@
- all: lib$(P).a lib$(P).b llib-l$(P).ln tags
-
- clean:
-- rm -f *.o *.u core *.warnings
-+ rm -f *.o *.lo *.u core *.warnings
-
- distclean: clean
-- rm -f lib$(P).a lib$(P).b llib-l$(P).ln tags *.bak *~ .pure
-+ rm -f lib$(P).a lib$(P).la lib$(P).b llib-l$(P).ln tags *.bak *~ .pure
-+ rm -fr .libs
+++ /dev/null
-#!/bin/bash
-#
-# Patch to cudd build system to build everything with libtool, supporting
-# shared libraries. Also all libraries are combined into a single one.
-#
-# This script applies the patch, builds cudd, and, assuming there are no
-# errors, reverses the patch.
-#
-# -- Morgan Deters <mdeters@cs.nyu.edu> Wed, 13 Jul 2011 18:03:11 -0400
-#
-
-cd "$(dirname "$0")"
-if [ $# -ne 1 -o "$1" = -h -o "$1" = -help -o "$1" = --help ]; then
- echo "usage: $(basename "$0") cudd-dir" >&2
- exit 1
-fi
-
-patch="$(pwd)/$(basename "$0")"
-if [ ! -r "$patch" ]; then
- echo "error: can't read patch at \`$patch'" >&2
- exit 1
-fi
-if ! expr "$1" : / &>/dev/null; then
- echo "error: must specify an absolute path to cudd sources" >&2
- exit 1
-fi
-cudd_dir="$1"
-
-arch=$(../config/config.guess | cut -f1 -d-)
-case "$arch" in
- i?86) XCFLAGS='-mtune=pentium4 -malign-double -DHAVE_IEEE_754 -DBSD' ;;
- x86_64) XCFLAGS='-mtune=native -DHAVE_IEEE_754 -DBSD -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8' ;;
- *) XCFLAGS= ;;
-esac
-
-set -ex
-
-XCFLAGS="$XCFLAGS"
-
-version_info=1:0:0
-
-prefix="$cudd_dir"
-eprefix="$prefix"
-bindir="$eprefix/bin"
-datadir="$prefix/share"
-includedir="$prefix/include"
-libdir="$prefix/lib"
-mandir="$datadir/man/man1"
-docdir="$datadir/doc"
-
-cd "$cudd_dir"
-patch -p1 < "$patch"
-make "XCFLAGS=$XCFLAGS" "CC=libtool --mode=compile gcc" "CPP=libtool --mode=compile g++" libdir="$libdir" version_info="$version_info" DDDEBUG= MTRDEBUG= ICFLAGS=-O2
-mkdir -p "$libdir"
-libtool --mode=install cp libcudd.la "$libdir/libcudd.la"
-libtool --mode=install cp libcuddxx.la "$libdir/libcuddxx.la"
-libtool --mode=install cp libdddmp.la "$libdir/libdddmp.la"
-libtool --finish "$libdir"
-patch -p1 -R < "$patch"
-exit
-
-# patch follows
-
---- cudd-2.5.0.orig/Makefile
-+++ cudd-2.5.0/Makefile
-@@ -220,11 +220,16 @@ DIRS = $(BDIRS) nanotrav
-
- build:
- sh ./setup.sh
-- @for dir in $(DIRS); do \
-+ +@for dir in $(BDIRS) obj; do \
- (cd $$dir; \
- echo Making $$dir ...; \
-- make CC=$(CC) RANLIB=$(RANLIB) MFLAG= MNEMLIB= ICFLAGS="$(ICFLAGS)" XCFLAGS="$(XCFLAGS)" DDDEBUG="$(DDDEBUG)" MTRDEBUG="$(MTRDEBUG)" LDFLAGS="$(LDFLAGS)" PURE="$(PURE)" EXE="$(EXE)" )\
-+ make CC="$(CC)" RANLIB="$(RANLIB)" MFLAG= MNEMLIB= ICFLAGS="$(ICFLAGS)" XCFLAGS="$(XCFLAGS)" DDDEBUG="$(DDDEBUG)" MTRDEBUG="$(MTRDEBUG)" LDFLAGS="$(LDFLAGS)" PURE="$(PURE)" EXE="$(EXE)" )\
- done
-+ libtool --mode=link gcc -rpath "$(libdir)" -version-info "$(version_info)" -o libcudd.la cudd/libcudd.la mtr/libmtr.la epd/libepd.la util/libutil.la st/libst.la -lm
-+ libtool --mode=link gcc -rpath "${libdir}" -version-info "$(version_info)" -o libdddmp.la dddmp/libdddmp.la
-+ libtool --mode=link g++ -rpath "$(libdir)" -version-info "$(version_info)" -o libcuddxx.la obj/libobj.la -lcudd
-+ +@(cd nanotrav; \
-+ make CC="$(CC)" RANLIB="$(RANLIB)" MFLAG= MNEMLIB= ICFLAGS="$(ICFLAGS)" XCFLAGS="$(XCFLAGS)" DDDEBUG="$(DDDEBUG)" MTRDEBUG="$(MTRDEBUG)" LDFLAGS="$(LDFLAGS)" PURE="$(PURE)" EXE="$(EXE)" )
-
- nanotrav: build
-
-@@ -318,4 +323,6 @@ distclean:
- echo Cleaning $$dir ...; \
- make -s EXE="$(EXE)" distclean ) \
- done
-+ rm -f libcudd* libdddmp*
-+ rm -fr .libs
- sh ./shutdown.sh
---- cudd-2.5.0.orig/mtr/Makefile
-+++ cudd-2.5.0/mtr/Makefile
-@@ -30,7 +30,7 @@ INCLUDE = $(WHERE)/include
- P = mtr
- PSRC = mtrBasic.c mtrGroup.c
- PHDR = mtr.h
--POBJ = $(PSRC:.c=.o)
-+POBJ = $(PSRC:.c=.lo)
- PUBJ = $(PSRC:.c=.u)
- SRC = test$(P).c
- HDR =
-@@ -49,12 +49,11 @@ LINTLIBS = llib-l$(P).ln
-
- #---------------------------
-
--lib$(P).a: $(POBJ)
-- ar rv $@ $?
-- $(RANLIB) $@
-+lib$(P).la: $(POBJ)
-+ libtool --mode=link gcc -o $@ $?
-
--.c.o: $(PSRC) $(PHDR)
-- $(CC) -c $< -I$(INCLUDE) $(CFLAGS) $(MTRDEBUG)
-+%.lo: %.c
-+ $(CC) -c -o $@ $< -I$(INCLUDE) $(CFLAGS) $(MTRDEBUG)
-
- optimize_dec: lib$(P).b
-
-@@ -88,9 +87,10 @@ $(TARGETu): $(SRC) $(PSRC) $(PHDR) $(UBJ
- cc -O3 $(XCFLAGS) $(LDFLAGS) -o $@ $(UBJ) $(BLIBS) -lm
-
- clean:
-- rm -f *.o *.u mon.out gmon.out *.pixie *.Addrs *.Counts mnem.* \
-+ rm -f *.o *.lo *.u mon.out gmon.out *.pixie *.Addrs *.Counts mnem.* \
- .pure core *.warnings
-
- distclean: clean
-- rm -f $(TARGET) $(TARGETu) lib*.a lib$(P).b llib-l$(P).ln \
-+ rm -f $(TARGET) $(TARGETu) lib*.a lib*.la lib$(P).b llib-l$(P).ln \
- *.bak *~ tags *.qv *.qx
-+ rm -fr .libs
---- cudd-2.5.0.orig/nanotrav/Makefile
-+++ cudd-2.5.0/nanotrav/Makefile
-@@ -19,9 +19,7 @@ WHERE = ..
-
- INCLUDE = $(WHERE)/include
-
--LIBS = $(WHERE)/dddmp/libdddmp.a $(WHERE)/cudd/libcudd.a \
-- $(WHERE)/mtr/libmtr.a $(WHERE)/st/libst.a $(WHERE)/util/libutil.a \
-- $(WHERE)/epd/libepd.a
-+LIBS = $(WHERE)/libcudd.la $(WHERE)/libdddmp.la
-
- MNEMLIB =
- #MNEMLIB = $(WHERE)/mnemosyne/libmnem.a
-@@ -39,7 +37,7 @@ SRC = main.c bnet.c ntr.c ntrHeap.c ntrB
- HDR = bnet.h ntr.h $(WHERE)/include/dddmp.h $(WHERE)/include/cudd.h \
- $(WHERE)/include/cuddInt.h
-
--OBJ = $(SRC:.c=.o)
-+OBJ = $(SRC:.c=.lo)
- UBJ = $(SRC:.c=.u)
-
- MFLAG =
-@@ -61,10 +59,10 @@ LINTFLAGS = -u -n -DDD_STATS -DDD_CACHE_
- #------------------------------------------------------
-
- $(TARGET): $(SRC) $(OBJ) $(HDR) $(LIBS) $(MNEMLIB)
-- $(PURE) $(CC) $(CFLAGS) $(LDFLAGS) -o $@ $(OBJ) $(LIBS) $(MNEMLIB) -lm
-+ libtool --mode=link gcc $(CFLAGS) $(LDFLAGS) -o $@ $(OBJ) $(LIBS) $(MNEMLIB) -lm
-
--.c.o: $(HDR)
-- $(CC) -c $< -I$(INCLUDE) $(CFLAGS) $(DDDEBUG)
-+%.lo: %.c
-+ $(CC) -c -o $@ $< -I$(INCLUDE) $(CFLAGS) $(DDDEBUG)
-
- # if the header files change, recompile
- $(OBJ): $(HDR)
-@@ -91,8 +89,9 @@ pixie: $(TARGETu)
- pixie $(TARGETu)
-
- clean:
-- rm -f *.o *.u mon.out gmon.out *.pixie *.Addrs *.Counts mnem.* \
-+ rm -f *.o *.lo *.u mon.out gmon.out *.pixie *.Addrs *.Counts mnem.* \
- .pure core *.warnings
-
- distclean: clean
- rm -f $(TARGET) $(TARGETu) *.bak *~ .gdb_history *.qv *.qx
-+ rm -fr .libs
---- cudd-2.5.0.orig/dddmp/Makefile
-+++ cudd-2.5.0/dddmp/Makefile
-@@ -148,7 +148,7 @@ PSRC = dddmpStoreBdd.c dddmpStoreAdd.
- dddmpStoreMisc.c dddmpUtil.c dddmpBinary.c dddmpConvert.c \
- dddmpDbg.c
- PHDR = dddmp.h dddmpInt.h $(INCLUDE)/cudd.h $(INCLUDE)/cuddInt.h
--POBJ = $(PSRC:.c=.o)
-+POBJ = $(PSRC:.c=.lo)
- PUBJ = $(PSRC:.c=.u)
- TARGET = test$(P)$(EXE)
- TARGETu = test$(P)-u
-@@ -182,12 +182,11 @@ LINTLIBS = ./llib-ldddmp.ln $(WHERE)/cud
- $(WHERE)/mtr/llib-lmtr.ln $(WHERE)/st/llib-lst.ln \
- $(WHERE)/util/llib-lutil.ln
-
--lib$(P).a: $(POBJ)
-- ar rv $@ $?
-- $(RANLIB) $@
-+lib$(P).la: $(POBJ)
-+ libtool --mode=link gcc -o $@ $?
-
--.c.o: $(PHDR)
-- $(CC) -c $< -I$(INCLUDE) $(ICFLAGS) $(XCFLAGS) $(DDDEBUG) $(MTRDEBUG) $(DDDMPDEBUG) $(LDFLAGS)
-+%.lo: %.c
-+ $(CC) -c -o $@ $< -I$(INCLUDE) $(ICFLAGS) $(XCFLAGS) $(DDDEBUG) $(MTRDEBUG) $(DDDMPDEBUG) $(LDFLAGS)
-
- optimize_dec: lib$(P).b
-
-@@ -231,12 +230,13 @@ programs: $(TARGET) $(TARGETu) lintpgm
- #----------------------------------------------------------------------------#
-
- clean:
-- rm -f *.o *.u mon.out gmon.out *.pixie *.Addrs *.Counts mnem.* \
-+ rm -f *.o *.lo *.u mon.out gmon.out *.pixie *.Addrs *.Counts mnem.* \
- .pure core *.warnings
-
- distclean: clean
-- rm -f $(TARGET) $(TARGETu) lib*.a lib$(P).b llib-l$(P).ln \
-+ rm -f $(TARGET) $(TARGETu) lib*.a lib*.la lib$(P).b llib-l$(P).ln \
- *.bak *~ tags .gdb_history *.qv *.qx
-+ rm -fr .libs
-
-
-
---- cudd-2.5.0.orig/util/Makefile
-+++ cudd-2.5.0/util/Makefile
-@@ -20,19 +20,18 @@ LINTSWITCH = -o
- P = util
- PSRC = cpu_time.c cpu_stats.c safe_mem.c strsav.c texpand.c \
- ptime.c prtime.c pipefork.c pathsearch.c stub.c datalimit.c
--POBJ = $(PSRC:.c=.o)
-+POBJ = $(PSRC:.c=.lo)
- PUBJ = $(PSRC:.c=.u)
- PHDR = util.h
-
- WHERE = ..
- INCLUDE = $(WHERE)/include
-
--lib$(P).a: $(POBJ)
-- ar rv $@ $?
-- $(RANLIB) $@
-+lib$(P).la: $(POBJ)
-+ libtool --mode=link gcc -o $@ $?
-
--.c.o: $(PHDR)
-- $(CC) -c $< -I$(INCLUDE) $(FLAGS) $(CFLAGS)
-+%.lo: %.c
-+ $(CC) -c -o $@ $< -I$(INCLUDE) $(FLAGS) $(CFLAGS)
-
- optimize_dec: lib$(P).b
-
-@@ -58,7 +57,8 @@ tags: $(PSRC) $(PHDR)
- all: lib$(P).a lib$(P).b llib-l$(P).ln tags
-
- clean:
-- rm -f *.o *.u core *.warnings
-+ rm -f *.o *.lo *.u core *.warnings
-
- distclean: clean
-- rm -f lib$(P).a lib$(P).b llib-l$(P).ln tags *.bak *~ .pure
-+ rm -f lib$(P).a lib$(P).la lib$(P).b llib-l$(P).ln tags *.bak *~ .pure
-+ rm -fr .libs
---- cudd-2.5.0.orig/epd/Makefile
-+++ cudd-2.5.0/epd/Makefile
-@@ -19,7 +19,7 @@ LINTSWITCH = -o
- P = epd
- PSRC = epd.c
- PHDR = epd.h
--POBJ = $(PSRC:.c=.o)
-+POBJ = $(PSRC:.c=.lo)
- PUBJ = $(PSRC:.c=.u)
-
- WHERE = ..
-@@ -27,12 +27,11 @@ INCLUDE = $(WHERE)/include
-
- #---------------------------
-
--lib$(P).a: $(POBJ)
-- ar rv $@ $?
-- $(RANLIB) $@
-+lib$(P).la: $(POBJ)
-+ libtool --mode=link gcc -o $@ $?
-
--.c.o: $(PSRC) $(PHDR)
-- $(CC) -c $< -I$(INCLUDE) $(CFLAGS)
-+%.lo: %.c
-+ $(CC) -c -o $@ $< -I$(INCLUDE) $(CFLAGS)
-
- optimize_dec: lib$(P).b
-
-@@ -58,7 +57,8 @@ tags: $(PSRC) $(PHDR)
- all: lib$(P).a lib$(P).b llib-l$(P).ln tags
-
- clean:
-- rm -f *.o *.u .pure *.warnings
-+ rm -f *.o *.lo *.u .pure *.warnings
-
- distclean: clean
-- rm -f lib*.a lib$(P).b llib-l$(P).ln tags *~ *.bak *.qv *.qx
-+ rm -f lib*.a lib*.la lib$(P).b llib-l$(P).ln tags *~ *.bak *.qv *.qx
-+ rm -fr .libs
---- cudd-2.5.0.orig/obj/Makefile
-+++ cudd-2.5.0/obj/Makefile
-@@ -45,7 +45,7 @@ LDFLAGS =
- P = obj
- PSRC = cuddObj.cc
- PHDR = cuddObj.hh $(INCLUDE)/cudd.h
--POBJ = $(PSRC:.cc=.o)
-+POBJ = $(PSRC:.cc=.lo)
- PUBJ = $(PSRC:.cc=.u)
- TARGET = test$(P)$(EXE)
- TARGETu = test$(P)-u
-@@ -57,12 +57,11 @@ UBJ = $(SRC:.cc=.u)
-
- #------------------------------------------------------
-
--lib$(P).a: $(POBJ)
-- ar rv $@ $?
-- $(RANLIB) $@
-+lib$(P).la: $(POBJ)
-+ libtool --mode=link g++ -o $@ $?
-
--.cc.o: $(PHDR)
-- $(CXX) -c $< -I$(INCLUDE) $(CFLAGS) $(DDDEBUG)
-+%.lo: %.cc
-+ libtool --mode=compile $(CXX) -c -o $@ $< -I$(INCLUDE) $(CFLAGS) $(DDDEBUG)
-
- optimize_dec: lib$(P).b
-
-@@ -80,7 +79,7 @@ $(OBJ): $(PHDR)
- $(UBJ): $(PHDR)
-
- $(TARGET): $(SRC) $(OBJ) $(HDR) $(LIBS) $(MNEMLIB)
-- $(PURE) $(CXX) $(CFLAGS) $(LDFLAGS) -o $@ $(OBJ) $(LIBS) $(MNEMLIB) -lm
-+ libtool --mode=compile $(PURE) $(CXX) $(CFLAGS) $(LDFLAGS) -o $@ $(OBJ) $(LIBS) $(MNEMLIB) -lm
-
- # optimize (DECstations and Alphas only: uses u-code)
- $(TARGETu): $(SRC) $(UBJ) $(HDR) $(LIBS:.a=.b)
-@@ -102,9 +101,10 @@ all: lib$(P).a lib$(P).b llib-l$(P).ln t
- programs: $(TARGET) $(TARGETu) lintpgm
-
- clean:
-- rm -f *.o *.u mon.out gmon.out *.pixie *.Addrs *.Counts mnem.* \
-+ rm -f *.o *.lo *.u mon.out gmon.out *.pixie *.Addrs *.Counts mnem.* \
- .pure core *.warnings
-
- distclean: clean
-- rm -f $(TARGET) $(TARGETu) lib*.a lib$(P).b llib-l$(P).ln \
-+ rm -f $(TARGET) $(TARGETu) lib*.a lib*.la lib$(P).b llib-l$(P).ln \
- *.bak *~ tags .gdb_history *.qv *.qx
-+ rm -fr .libs
---- cudd-2.5.0.orig/st/Makefile
-+++ cudd-2.5.0/st/Makefile
-@@ -19,7 +19,7 @@ LINTSWITCH = -o
- P = st
- PSRC = st.c
- PHDR = st.h
--POBJ = $(PSRC:.c=.o)
-+POBJ = $(PSRC:.c=.lo)
- PUBJ = $(PSRC:.c=.u)
-
- WHERE = ..
-@@ -27,12 +27,11 @@ INCLUDE = $(WHERE)/include
-
- #---------------------------
-
--lib$(P).a: $(POBJ)
-- ar rv $@ $?
-- $(RANLIB) $@
-+lib$(P).la: $(POBJ)
-+ libtool --mode=link gcc -o $@ $?
-
--.c.o: $(PHDR)
-- $(CC) -c $< -I$(INCLUDE) $(CFLAGS)
-+%.lo: %.c
-+ $(CC) -c -o $@ $< -I$(INCLUDE) $(CFLAGS)
-
- optimize_dec: lib$(P).b
-
-@@ -58,7 +57,8 @@ tags: $(PSRC) $(PHDR)
- all: lib$(P).a lib$(P).b llib-l$(P).ln tags
-
- clean:
-- rm -f *.o *.u .pure *.warnings
-+ rm -f *.o *.lo *.u .pure *.warnings
-
- distclean: clean
-- rm -f lib*.a lib$(P).b llib-l$(P).ln tags *~ *.bak *.qv *.qx
-+ rm -f lib*.a lib*.la lib$(P).b llib-l$(P).ln tags *~ *.bak *.qv *.qx
-+ rm -fr .libs
---- cudd-2.5.0.orig/cudd/Makefile
-+++ cudd-2.5.0/cudd/Makefile
-@@ -59,7 +59,7 @@ PSRC = cuddAPI.c cuddAddAbs.c cuddAddApp
- cuddZddPort.c cuddZddReord.c cuddZddSetop.c cuddZddSymm.c \
- cuddZddUtil.c
- PHDR = cudd.h cuddInt.h
--POBJ = $(PSRC:.c=.o)
-+POBJ = $(PSRC:.c=.lo)
- PUBJ = $(PSRC:.c=.u)
- TARGET = test$(P)$(EXE)
- TARGETu = test$(P)-u
-@@ -71,12 +71,11 @@ UBJ = $(SRC:.c=.u)
-
- #------------------------------------------------------
-
--lib$(P).a: $(POBJ)
-- ar rv $@ $?
-- $(RANLIB) $@
-+lib$(P).la: $(POBJ)
-+ libtool --mode=link gcc -o $@ $?
-
--.c.o: $(PSRC) $(PHDR)
-- $(CC) -c $< -I$(INCLUDE) $(CFLAGS) $(DDDEBUG)
-+%.lo: %.c
-+ $(CC) -c -o $@ $< -I$(INCLUDE) $(CFLAGS) $(DDDEBUG)
-
- optimize_dec: lib$(P).b
-
-@@ -116,9 +115,10 @@ all: lib$(P).a lib$(P).b llib-l$(P).ln t
- programs: $(TARGET) $(TARGETu) lintpgm
-
- clean:
-- rm -f *.o *.u mon.out gmon.out *.pixie *.Addrs *.Counts mnem.* \
-+ rm -f *.o *.lo *.u mon.out gmon.out *.pixie *.Addrs *.Counts mnem.* \
- .pure core *.warnings
-
- distclean: clean
-- rm -f $(TARGET) $(TARGETu) lib*.a lib$(P).b llib-l$(P).ln \
-+ rm -f $(TARGET) $(TARGETu) lib*.a lib*.la lib$(P).b llib-l$(P).ln \
- *.bak *~ tags .gdb_history *.qv *.qx
-+ rm -fr .libs
./autogen.sh || echo "autoconf failed; does library_versions have something to match $version?"; \
mkdir "release-$version"; \
cd "release-$version"; \
- ../configure production-staticbinary --disable-shared --enable-unit-testing --without-cudd --with-readline --with-portfolio; \
+ ../configure production-staticbinary --disable-shared --enable-unit-testing --with-readline --with-portfolio; \
make dist "$@"; \
tar xf "cvc4-$version.tar.gz"; \
cd "cvc4-$version"; \
- ./configure production-staticbinary --disable-shared --enable-unit-testing --without-cudd --with-readline --with-portfolio; \
+ ./configure production-staticbinary --disable-shared --enable-unit-testing --with-readline --with-portfolio; \
make check "$@"; \
make distcheck "$@"; \
'; then
-I@builddir@/.. -I@srcdir@/../include -I@srcdir@/..
AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
-noinst_LTLIBRARIES = libutil.la libutilcudd.la libstatistics.la
-
-# libutilcudd.la is a separate library so that we can pass separate
-# compiler flags
-libutilcudd_la_CPPFLAGS = $(CPPFLAGS) $(AM_CPPFLAGS) @CUDD_CPPFLAGS@
-libutilcudd_la_LIBADD = @CUDD_LDFLAGS@ @CUDD_LIBS@
+noinst_LTLIBRARIES = libutil.la libstatistics.la
libstatistics_la_CPPFLAGS = $(CPPFLAGS) $(AM_CPPFLAGS) -D__BUILDING_STATISTICS_FOR_EXPORT
sort_inference.h \
sort_inference.cpp
-libutil_la_LIBADD = \
- @builddir@/libutilcudd.la
-
libstatistics_la_SOURCES = \
statistics_registry.h \
statistics_registry.cpp
-libutilcudd_la_SOURCES = \
- propositional_query.h \
- propositional_query.cpp
-
BUILT_SOURCES = \
rational.h \
integer.h \
}
bool Configuration::isBuiltWithCudd() {
- return IS_CUDD_BUILD;
+ return false;
}
bool Configuration::isBuiltWithTlsSupport() {
# define IS_COMPETITION_BUILD false
#endif /* CVC4_COMPETITION_MODE */
-#ifdef CVC4_CUDD
-# define IS_CUDD_BUILD true
-#else /* CVC4_CUDD */
-# define IS_CUDD_BUILD false
-#endif /* CVC4_CUDD */
-
#ifdef CVC4_GMP_IMP
# define IS_GMP_BUILD true
#else /* CVC4_GMP_IMP */
+++ /dev/null
-/********************* */
-/*! \file propositional_query.cpp
- ** \verbatim
- ** Original author: taking
- ** Major contributors: mdeters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief A class for simple, quick, propositional
- ** satisfiability/validity checking
- **
- ** PropositionalQuery is a way for parts of CVC4 to do quick purely
- ** propositional satisfiability or validity checks on a Node. These
- ** checks do no theory reasoning, and handle atoms as propositional
- ** variables, but can sometimes be useful for subqueries.
- **/
-
-#include "util/propositional_query.h"
-
-#include <map>
-#include <algorithm>
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-
-#ifdef CVC4_CUDD
-
-#include <util.h>
-#include <cudd.h>
-#include <cuddObj.hh>
-
-namespace CVC4 {
-
-class BddInstance {
-private:
- Cudd d_mgr;
- typedef std::map<Node, BDD> AtomToIDMap;
- AtomToIDMap d_atomToBddMap;
-
- unsigned d_atomId;
-
- BDD encodeNode(TNode t);
- BDD encodeAtom(TNode t);
- BDD encodeCombinator(TNode t);
-
- bool isAnAtom(TNode t) {
- switch(t.getKind()) {
- case NOT:
- case XOR:
- case IFF:
- case IMPLIES:
- case OR:
- case AND:
- return false;
- case ITE:
- return t.getType().isBoolean();
- default:
- return true;
- }
- }
-
- void setupAtoms(TNode t);
-
- void clear() {
- d_atomId = 0;
- d_atomToBddMap.clear();
- }
-
- Result d_result;
-
-public:
- static const unsigned MAX_VARIABLES = 20;
-
- BddInstance(TNode t) : d_atomToBddMap(), d_atomId(0) {
- setupAtoms(t);
-
- Debug("bdd::sat") << t << endl;
- Debug("bdd::sat") << d_atomToBddMap.size() << endl;
-
-
- if(d_atomToBddMap.size() > MAX_VARIABLES) {
- d_result = Result(Result::SAT_UNKNOWN, Result::TIMEOUT);
- } else {
- BDD res = encodeNode(t);
- BDD falseBdd = d_mgr.bddZero();
- bool isUnsat = (res == falseBdd);
-
- clear();
-
- if(isUnsat) {
- d_result = Result::UNSAT;
- } else {
- d_result = Result::SAT;
- }
- }
- }
-
- Result getResult() const { return d_result; }
-
-};/* class BddInstance */
-
-}/* CVC4 namespace */
-
-BDD BddInstance::encodeNode(TNode t) {
- if(isAnAtom(t)) {
- return encodeAtom(t);
- } else {
- return encodeCombinator(t);
- }
-}
-
-BDD BddInstance::encodeCombinator(TNode t) {
- switch(t.getKind()) {
- case XOR: {
- Assert(t.getNumChildren() == 2);
- return encodeNode(t[0]).Xor(encodeNode(t[1]));
- }
-
- case IFF: {
- Assert(t.getNumChildren() == 2);
- BDD left = encodeNode(t[0]);
- BDD right = encodeNode(t[1]);
- return (!left | right) & (left | !right);
- }
-
- case IMPLIES: {
- Assert(t.getNumChildren() == 2);
- BDD left = encodeNode(t[0]);
- BDD right = encodeNode(t[1]);
- return (!left | right);
- }
-
- case AND:
- case OR: {
- Assert(t.getNumChildren() >= 2);
- TNode::iterator i = t.begin(), end = t.end();
- BDD tmp = encodeNode(*i);
- ++i;
- for(; i != end; ++i) {
- BDD curr = encodeNode(*i);
- if(t.getKind() == AND) {
- tmp = tmp & curr;
- } else {
- tmp = tmp | curr;
- }
- }
- return tmp;
- }
-
- case ITE: {
- Assert(t.getType().isBoolean());
- BDD cnd = encodeNode(t[0]);
- BDD thenBranch = encodeNode(t[1]);
- BDD elseBranch = encodeNode(t[2]);
- return cnd.Ite(thenBranch, elseBranch);
- }
-
- case NOT:
- return ! encodeNode(t[0]);
-
- default:
- Unhandled(t.getKind());
- }
-}
-
-BDD BddInstance::encodeAtom(TNode t) {
- if(t.getKind() == kind::CONST_BOOLEAN) {
- if(t.getConst<bool>()) {
- return d_mgr.bddOne();
- } else {
- return d_mgr.bddZero();
- }
- }
- Assert(t.getKind() != kind::CONST_BOOLEAN);
-
- AtomToIDMap::iterator findT = d_atomToBddMap.find(t);
-
- Assert(d_atomToBddMap.find(t) != d_atomToBddMap.end());
- return findT->second;
-}
-
-void BddInstance::setupAtoms(TNode t) {
- if(t.getKind() == kind::CONST_BOOLEAN) {
- // do nothing
- } else if(isAnAtom(t)) {
- AtomToIDMap::iterator findT = d_atomToBddMap.find(t);
- if(findT == d_atomToBddMap.end()) {
- BDD var = d_mgr.bddVar();
- d_atomToBddMap.insert(make_pair(t, var));
- d_atomId++;
- }
- } else {
- for(TNode::iterator i = t.begin(), end = t.end(); i != end; ++i) {
- setupAtoms(*i);
- }
- }
-}
-
-Result PropositionalQuery::isSatisfiable(TNode q) {
- BddInstance instance(q);
- return instance.getResult();
-}
-
-Result PropositionalQuery::isTautology(TNode q) {
- Node negQ = q.notNode();
- Result satResult = isSatisfiable(negQ);
- return satResult.asValidityResult();
-}
-
-#else /* CVC4_CUDD */
-
-// if CUDD wasn't available at build time, just return UNKNOWN everywhere.
-
-Result PropositionalQuery::isSatisfiable(TNode q) {
- return Result(Result::SAT_UNKNOWN, Result::UNSUPPORTED);
-}
-
-Result PropositionalQuery::isTautology(TNode q) {
- return Result(Result::VALIDITY_UNKNOWN, Result::UNSUPPORTED);
-}
-
-#endif /* CVC4_CUDD */
+++ /dev/null
-/********************* */
-/*! \file propositional_query.h
- ** \verbatim
- ** Original author: taking
- ** Major contributors: mdeters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief A class for simple, quick, propositional
- ** satisfiability/validity checking
- **
- ** PropositionalQuery is a way for parts of CVC4 to do quick purely
- ** propositional satisfiability or validity checks on a Node. These
- ** checks do no theory reasoning, and handle atoms as propositional
- ** variables, but can sometimes be useful for subqueries.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__PROPOSITIONAL_QUERY_H
-#define __CVC4__PROPOSITIONAL_QUERY_H
-
-#include "expr/node.h"
-#include "util/result.h"
-
-namespace CVC4 {
-
-/**
- * PropositionalQuery is a way for parts of CVC4 to do quick purely
- * propositional satisfiability or validity checks on a Node.
- */
-class PropositionalQuery {
-public:
-
- /**
- * Returns whether a node q is propositionally satisfiable.
- *
- * @param q Node to be checked for satisfiability.
- * @pre q is a ground formula.
- * @pre effort is between 0 and 1.
- */
- static Result isSatisfiable(TNode q);
-
- /**
- * Returns whether a node q is a propositional tautology.
- *
- * @param q Node to be checked for satisfiability.
- * @pre q is a ground formula.
- * @pre effort is between 0 and 1.
- */
- static Result isTautology(TNode q);
-
-};/* class PropositionalQuery */
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__PROPOSITIONAL_QUERY_H */
projects / cvc5.git / commitdiff