From c33c9d3699597abe2fbeaacb6799ba05f11f8e93 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 3 Oct 2012 21:27:11 +0000 Subject: [PATCH] new README and INSTALL files --- INSTALL | 161 +++++++++++++++++++++++++++++++++++++++++++++++++++ README | 174 ++++++++++++++++++++++---------------------------------- 2 files changed, 229 insertions(+), 106 deletions(-) create mode 100644 INSTALL diff --git a/INSTALL b/INSTALL new file mode 100644 index 000000000..96e9cbd60 --- /dev/null +++ b/INSTALL @@ -0,0 +1,161 @@ +This is CVC4 release version 1.0. + +*** Quick-start instructions + + ./configure + make + make check [optional but a good idea!] + +(To build from a repository checkout, see below.) + +You can then "make install" to install in the prefix you gave to +the configure script (/usr/local by default). ** You should run +"make check" ** before installation to ensure that CVC4 has been +built correctly. In particular, GCC version 4.5.1 seems to have a +bug in the optimizer that results in incorrect behavior (and wrong +results) in many builds. This is a known problem for Minisat, and +since Minisat is at the core of CVC4, a problem for CVC4. "make check" +easily detects this problem (by showing a number of FAILed test cases). +It is ok if the unit tests aren't run as part of "make check", but all +system tests and regression tests should pass without incident. + +To build API documentation, use "make doc". Documentation is produced +under doc/ but is not installed by "make install". + +Examples/tutorials are not installed with "make install." See below. + +*** Build dependences + +The following tools and libraries are required to run CVC4. Versions +given are minimum versions; more recent versions should be compatible. + + GNU C and C++ (gcc and g++), reasonably recent versions + GNU Make + GNU Bash + GMP v4.2 (GNU Multi-Precision arithmetic library) + MacPorts [only if on a Mac; see below] + libantlr3c v3.2 or v3.4 (ANTLR parser generator C support library) + The Boost C++ base libraries + +The hardest to obtain and install is the libantlr3c requirement, so +that one is explained next. + +On a Mac, you need to additionally install MacPorts (see +http://www.macports.org/). Doing so is easy. Then, simply run the +script contrib/mac-build, which installs a few ports from the MacPorts +repository, then compiles and installs antlr3c using the get-antlr-3.4 +script (as described next). The mac-build script should set you up +with all requirements, and will tell you how to configure CVC4 when it +completes successfully. + +If "make" is non-GNU on your system, make sure to invoke "gmake" (or +whatever GNU Make is installed as). If your usual shell is not Bash, +the configure script should auto-correct this. If it does not, you'll +see strange shell syntax errors, and you may need to explicitly set +SHELL or CONFIG_SHELL to the location of bash on your system. + +*** Installing libantlr3c: ANTLR parser generator C support library + +For libantlr3c, you can use the convenience script in +contrib/get-antlr-3.4 --this will download, patch, and install +libantlr3c. On a 32-bit machine, or if you have difficulty building +libantlr3c (or difficulty getting CVC4 to link against it later), you +may need to remove the --enable-64bit part in the script. (If you're +curious, the manual instructions are at +http://church.cims.nyu.edu/wiki/Developer%27s_Guide#ANTLR3 .) + +*** Installing the Boost C++ base libraries + +A Boost package is available on most Linux distributions; check yours +for a package named something like libboost-dev or boost-devel. There +are a number of additional Boost packages in some distributions, but +this "basic" one should be sufficient for building CVC4. + +Should you want to install Boost manually, or to learn more about the +Boost project, please visit http://www.boost.org/. + +*** Optional requirements + +None of these is required, but can improve CVC4 as described below: + + 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) + +CLN is an alternative multiprecision arithmetic package that can offer +better performance and memory footprint than GMP. CLN is covered by +the GNU General Public License, version 3; so if you choose to use +CVC4 with CLN support, you are licensing CVC4 under that same license. +(Usually CVC4's license is more permissive than GPL is; see the file +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 +package named "libreadline-dev" or "readline-devel" or similar. + +The Boost C++ threading library (often packaged independently of the +Boost base library) is needed to run CVC4 in "portfolio" +(multithreaded) mode. Check your distribution for a package named +"libboost-thread-dev" or similar. + +*** 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-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: + + deb http://goedel.cims.nyu.edu/cvc4-builds/debian unstable/ + +The Debian source package "cudd", available from the same repository, +includes a diff of all changes made to cudd makefiles. + +*** Building CVC4 from a repository checkout + +The following tools and libraries are additionally required to build +CVC4 from from a repository checkout rather than from a prepared +source tarball. + + Automake v1.11 + Autoconf v2.61 + Libtool v2.2 + ANTLR3 v3.2 or v3.4 + +First, use "./autogen.sh" to create the configure script. Then +proceed as normal for any distribution tarball. The parsers are +pre-generated for the tarballs; hence the extra ANTLR3 requirement to +generate the source code for the parsers, when building from the +repository. + +*** Examples/tutorials are not built or installed + +Examples are not built by "make" or "make install". See +examples/README for information on what to find in the examples/ +directory, as well as information about building and installing them. diff --git a/README b/README index 65c2d6fec..ad9c8eb7e 100644 --- a/README +++ b/README @@ -1,106 +1,68 @@ -This is a prerelease version of CVC4. - -*** Quick-start instructions - - ./configure - make - -(To build from a Subversion checkout, you'll need reasonably new -automake, autoconf, and libtool installed (see below). The -"configure" script isn't in the repository, so run "./autogen.sh" -first to produce it. Then proceed as above.) - -You can then "make install" to install in the prefix you gave to -the configure script (/usr/local by default). ** You should run -"make check" ** before installation to ensure that CVC4 has been -built correctly. In particular, GCC version 4.5.1 seems to have a -bug in the optimizer that results in incorrect behavior (and wrong -results) in many builds. This is a known problem for Minisat, and -since Minisat is at the core of CVC4, a problem for CVC4. "make check" -easily detects this problem (by showing a number of FAILed test cases). -It is ok if the unit tests aren't run as part of "make check", but all -system tests and regression tests should pass without incident. - -To build API documentation, use "make doc". Documentation is produced -under doc/ but is not installed by "make install". - -To build a source release, use "make dist"; this will include the -configure script and all the bits of automake/autoconf/libtool that -are necessary for an independent install. You'll find the resulting -tarball in builds/cvc4-${VERSION}.tar.gz. - -*** Dependencies - -The following tools and libraries are required to run CVC4. Versions -given are minimum versions; more recent versions should be compatible. - -GNU C and C++ (gcc and g++), reasonably recent versions -GNU Make -GNU Bash -GMP v4.2 (GNU Multi-Precision arithmetic library) -libantlr3c v3.2 or v3.4 (ANTLR parser generator) -The Boost C++ base libraries - -For libantlr3c, you can use the convenience script in -contrib/get-antlr-3.4 --this will download, patch, and install -libantlr3c. On a 32-bit machine, or if you have difficulty -building libantlr3c (or difficulty getting CVC4 to link against -it later), you may need to remove the --enable-64bit part in the -script. (If you're curious, the manual instructions are at -http://church.cims.nyu.edu/wiki/Developer%27s_Guide#ANTLR3 .) - -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) -Optional: The Boost C++ threading library (libboost_thread) - -If "make" is non-GNU on your system, make sure to invoke "gmake" (or -whatever GNU Make is installed as). If your usual shell is not -Bash, the configure script should auto-correct this. If it does not, -you'll see strange shell syntax errors, and you may need to explicitly -set SHELL or CONFIG_SHELL to the location of bash on your system. - -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, -includes a diff of all changes made to cudd makefiles. - -*** Build dependencies - -The following tools and libraries are required to build CVC4 from -scratch (i.e., from the repository rather than from a source tarball). - -Automake v1.11 -Autoconf v2.61 -Libtool v2.2 -ANTLR3 v3.2 - -*** Emacs support - -For a suggestion of editing CVC4 source code with emacs, see the file -contrib/editing-with-emacs. For a CVC language mode (the native input -language for CVC4), see contrib/cvc-mode.el. - +This is CVC4 release version 1.0. For build and installation notes, +please see the INSTALL file included with this distribution. + +This first official release of CVC4 is the result of more than three +years of efforts by researchers at New York University and the +University of Iowa. The project leaders are Clark Barrett (New York +University) and Cesare Tinelli (University of Iowa). For a full list +of authors, please refer to the AUTHORS file in the source +distribution. + +CVC4 is a tool for determining the satisfiability of a first order +formula modulo a first order theory (or a combination of such +theories). It is the fourth in the Cooperating Validity Checker family +of tools (CVC, CVC Lite, CVC3) but does not directly incorporate code +from any previous version. + +CVC4 is intended to be an open and extensible SMT engine. It can be +used as a stand-alone tool or as a library. It has been designed to +increase the performance and reduce the memory overhead of its +predecessors. It is written entirely in C++ and is released under a +free software license (see the file COPYING in the source +distribution). + +*** The History of CVC4 + +The Cooperating Validity Checker series has a long history. The +Stanford Validity Checker (SVC) came first in 1996, incorporating +theories and its own SAT solver. Its successor, the Cooperating +Validity Checker (CVC), had a more optimized internal design, produced +proofs, used the Chaff SAT solver, and featured a number of usability +enhancements. Its name comes from the cooperative nature of decision +procedures in Nelson-Oppen theory combination, which share amongst +each other equalities between shared terms. CVC Lite, first made +available in 2003, was a rewrite of CVC that attempted to make CVC +more flexible (hence the "lite") while extending the feature set: CVC +Lite supported quantifiers where its predecessors did not. CVC3 was a +major overhaul of portions of CVC Lite: it added better decision +procedure implementations, added support for using MiniSat in the +core, and had generally better performance. + +CVC4 is the new version, the fifth generation of this validity checker +line that is now celebrating sixteen years of heritage. It represents +a complete re-evaluation of the core architecture to be both +performant and to serve as a cutting-edge research vehicle for the +next several years. Rather than taking CVC3 and redesigning problem +parts, we've taken a clean-room approach, starting from scratch. +Before using any designs from CVC3, we have thoroughly scrutinized, +vetted, and updated them. Many parts of CVC4 bear only a superficial +resemblance, if any, to their correspondent in CVC3. + +However, CVC4 is fundamentally similar to CVC3 and many other modern +SMT solvers: it is a DPLL(T) solver, with a SAT solver at its core and +a delegation path to different decision procedure implementations, +each in charge of solving formulas in some background theory. + +The re-evaluation and ground-up rewrite was necessitated, we felt, by +the performance characteristics of CVC3. CVC3 has many useful +features, but some core aspects of the design led to high memory use, +and the use of heavyweight computation (where more nimble engineering +approaches could suffice) makes CVC3 a much slower prover than other +tools. As these designs are central to CVC3, a new version was +preferable to a selective re-engineering, which would have ballooned +in short order. Some specific deficiencies of CVC3 are mentioned in +this article. + +*** For more information + +More information about CVC4 is available at: http://cs.nyu.edu/acsys/cvc4 -- 2.30.2