diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-09-02 20:41:08 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-09-02 20:41:08 +0000 |
commit | 1d18e5ebed9a5b20ed6a8fe21d11842acf6fa7ea (patch) | |
tree | 7074f04453914bc377ff6aeb307dd17b82b76ff3 /README | |
parent | 74770f1071e6102795393cf65dd0c651038db6b4 (diff) |
Merge from my post-smtcomp branch. Includes:
Dumping infrastructure. Can dump preprocessed queries and clauses. Can
also dump queries (for testing with another solver) to see if any conflicts
are missed, T-propagations are missed, all lemmas are T-valid, etc. For a
full list of options see --dump=help.
CUDD building much cleaner.
Documentation and assertion fixes.
Printer improvements, printing of commands in language-defined way, etc.
Typechecker stuff in expr package now autogenerated, no need to manually
edit the expr package when adding a new theory.
CVC3 compatibility layer (builds as libcompat).
SWIG detection and language binding support (infrastructure).
Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode
(when not in compliance mode).
Copyright and file headers regenerated.
Diffstat (limited to 'README')
-rw-r--r-- | README | 41 |
1 files changed, 29 insertions, 12 deletions
@@ -1,6 +1,6 @@ -This is a prerelease version of CVC4; distribution is restricted. +This is a prerelease version of CVC4. -For a suggestion of editing CVC4 code with emacs, see README.emacs. +*** Quick-start instructions To build, you'll need reasonably new automake, autoconf, and libtool installed (see below). Execute, @@ -33,19 +33,32 @@ Optional: CLN v1.3 (Class Library for Numbers) Optional: CUDD v2.4.2 (Colorado University Decision Diagram package) Optional: GNU Readline library (for an improved interactive experience) -CUDD, if desired, must be installed in a special manner. The default -distribution from vlsi.colorado.edu doesn't build shared objects, -and names things that make it difficult to compose software -dependences (e.g. a "libutil" is distributed). So we packaged our -own version of cudd that changes only its build process, making it -play nicely with libtool and packaging all the various cudd libraries -into just a few. This version must be used for cvc4, and is available -from the CVC4 apt repository by dropping the following line into your -/etc/apt/sources.list: +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 (remember, you need the C++ +development package for CVC4), 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-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 is here: deb http://goedel.cims.nyu.edu/cvc4-builds/debian unstable/ -The debian source package "cudd", available from the same repository, +The Debian source package "cudd", available from the same repository, includes a diff of all changes made to cudd makefiles. *** Build dependencies @@ -58,3 +71,7 @@ Autoconf v2.61 Libtool v2.2 ANTLR3 v3.2 +*** Emacs mode + +For a suggestion of editing CVC4 code with emacs, see README.emacs. + |