diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-01-31 14:29:58 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-03-19 19:09:27 -0400 |
commit | 7dd316a13b796d02985be63b1b03975a756fb624 (patch) | |
tree | ab348129940e25c4dde47c19568aea40d31a51ea | |
parent | 89a1304db9208a366c10136e8dee722f634015e9 (diff) |
Remove PropositionalQuery class and all CUDD-related build stuff (and references)
-rw-r--r-- | INSTALL | 41 | ||||
-rw-r--r-- | Makefile | 6 | ||||
-rw-r--r-- | config/cudd.m4 | 120 | ||||
-rw-r--r-- | configure.ac | 4 | ||||
-rw-r--r-- | contrib/Makefile.am | 2 | ||||
-rwxr-xr-x | contrib/build-cudd-2.4.2-with-libtool.sh | 421 | ||||
-rwxr-xr-x | contrib/build-cudd-2.5.0-with-libtool.sh | 430 | ||||
-rwxr-xr-x | contrib/cut-release | 4 | ||||
-rw-r--r-- | src/util/Makefile.am | 14 | ||||
-rw-r--r-- | src/util/configuration.cpp | 2 | ||||
-rw-r--r-- | src/util/configuration_private.h | 6 | ||||
-rw-r--r-- | src/util/propositional_query.cpp | 226 | ||||
-rw-r--r-- | src/util/propositional_query.h | 60 |
13 files changed, 7 insertions, 1329 deletions
@@ -95,7 +95,6 @@ None of these is required, but can improve CVC4 as described below: 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 @@ -114,11 +113,6 @@ CVC4 with CLN support, you are licensing CVC4 under that same license. 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 @@ -136,41 +130,6 @@ and go on to run the extensive system- and regression-tests in the 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. @@ -47,7 +47,7 @@ submission submission-main: 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 @@ -67,7 +67,7 @@ submission-application: 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 @@ -88,7 +88,7 @@ submission-parallel: 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) diff --git a/config/cudd.m4 b/config/cudd.m4 deleted file mode 100644 index d905c1725..000000000 --- a/config/cudd.m4 +++ /dev/null @@ -1,120 +0,0 @@ -# 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 diff --git a/configure.ac b/configure.ac index bf5938e70..a4b8892ab 100644 --- a/configure.ac +++ b/configure.ac @@ -908,9 +908,6 @@ AC_CHECK_FUNC([ffs], [AC_DEFINE([HAVE_FFS], [1], [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 @@ -1298,7 +1295,6 @@ Unit tests : $support_unit_tests Proof tests : $support_proof_tests gcov support : $enable_coverage gprof support: $enable_profiling -CUDD : $cvc4cudd Readline : $with_readline Static libs : $enable_static diff --git a/contrib/Makefile.am b/contrib/Makefile.am index 6f977caec..b2147b19a 100644 --- a/contrib/Makefile.am +++ b/contrib/Makefile.am @@ -11,8 +11,6 @@ EXTRA_DIST = \ 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 \ diff --git a/contrib/build-cudd-2.4.2-with-libtool.sh b/contrib/build-cudd-2.4.2-with-libtool.sh deleted file mode 100755 index d55dd1385..000000000 --- a/contrib/build-cudd-2.4.2-with-libtool.sh +++ /dev/null @@ -1,421 +0,0 @@ -#!/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 diff --git a/contrib/build-cudd-2.5.0-with-libtool.sh b/contrib/build-cudd-2.5.0-with-libtool.sh deleted file mode 100755 index 39a51f0da..000000000 --- a/contrib/build-cudd-2.5.0-with-libtool.sh +++ /dev/null @@ -1,430 +0,0 @@ -#!/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 diff --git a/contrib/cut-release b/contrib/cut-release index 06fc12686..2b7f6f683 100755 --- a/contrib/cut-release +++ b/contrib/cut-release @@ -170,11 +170,11 @@ if ! $SHELL -c '\ ./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 diff --git a/src/util/Makefile.am b/src/util/Makefile.am index dffb22ea8..1952108f6 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -3,12 +3,7 @@ AM_CPPFLAGS = \ -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 @@ -91,17 +86,10 @@ libutil_la_SOURCES = \ 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 \ diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp index c6e951049..9be4e4104 100644 --- a/src/util/configuration.cpp +++ b/src/util/configuration.cpp @@ -122,7 +122,7 @@ bool Configuration::isBuiltWithCln() { } bool Configuration::isBuiltWithCudd() { - return IS_CUDD_BUILD; + return false; } bool Configuration::isBuiltWithTlsSupport() { diff --git a/src/util/configuration_private.h b/src/util/configuration_private.h index 4378badc8..7c94f4c18 100644 --- a/src/util/configuration_private.h +++ b/src/util/configuration_private.h @@ -89,12 +89,6 @@ namespace CVC4 { # 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 */ diff --git a/src/util/propositional_query.cpp b/src/util/propositional_query.cpp deleted file mode 100644 index f4ee3840b..000000000 --- a/src/util/propositional_query.cpp +++ /dev/null @@ -1,226 +0,0 @@ -/********************* */ -/*! \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 */ diff --git a/src/util/propositional_query.h b/src/util/propositional_query.h deleted file mode 100644 index b1dc58cee..000000000 --- a/src/util/propositional_query.h +++ /dev/null @@ -1,60 +0,0 @@ -/********************* */ -/*! \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 */ |