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 /INSTALL | |
parent | 89a1304db9208a366c10136e8dee722f634015e9 (diff) |
Remove PropositionalQuery class and all CUDD-related build stuff (and references)
Diffstat (limited to 'INSTALL')
-rw-r--r-- | INSTALL | 41 |
1 files changed, 0 insertions, 41 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. |