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

1 files changed, 0 insertions, 41 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.