Remove PropositionalQuery class and all CUDD-related build stuff (and references)

13 files changed, 7 insertions, 1329 deletions

diff --git a/INSTALL b/INSTALL
index d1e3d53a3..3dea1de7d 100644
--- a/INSTALL
+++ b/INSTALL
@@ -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.
diff --git a/Makefile b/Makefile
index 5bbd61b4c..667bb3f23 100644
--- a/Makefile
+++ b/Makefile
@@ -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 */