-This is a prerelease version of CVC4; distribution is restricted.
-
-For a suggestion of editing CVC4 code with emacs, see README.emacs.
-
-To build, you'll need reasonably new automake, autoconf, and libtool
-installed (see below). Execute,
-
- ./autogen.sh
- ./configure
- make
-
-You can then "make install" to install in the prefix you gave to
-the configure script (/usr/local by default).
-
-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.
-
-To build documentation, use "make doc". Documentation is produced
-under doc/ but is not installed by "make install".
-
-*** 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
-GMP v4.2 (GNU Multi-Precision arithmetic library)
-libantlr3c v3.2 (ANTLR parser generator)
-Optional: CLN v1.3 (Class Library for Numbers)
-Optional: CUDD v2.4.2 (Colorado University Decision Diagram package)
-
-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:
-
- 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.
-
-Automake v1.11
-Autoconf v2.61
-Libtool v2.2
-ANTLR3 v3.2
-
+This is CVC4 release version 1.4. 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 (The 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 an
+open-source software license (see the file COPYING in the source
+distribution).
+
+*** Getting started with CVC4
+
+For help installing CVC4, see the INSTALL file that comes with this
+distribution.
+
+We recommend that you visit our CVC4 tutorials online at:
+
+ http://cvc4.cs.nyu.edu/wiki/Tutorials
+
+for help getting started using CVC4.
+
+*** Contributing to the CVC4 project
+
+We are always happy to hear feedback from our users:
+
+* if you need help with using CVC4, please write to the
+ cvc-users@cs.nyu.edu mailing list.
+
+* if you need to report a bug with CVC4, or make a feature request,
+ please visit our bugtracker at http://cvc4.cs.nyu.edu/bugs/ or write
+ to the cvc-bugs@cs.nyu.edu mailing list. We are very grateful for
+ bug reports, as they help us improve CVC4, and patches are generally
+ reviewed and accepted quickly.
+
+* if you are using CVC4 in your work, or incorporating it into
+ software of your own, we'd like to invite you to leave a description
+ and link to your project/software on our "Third Party Applications"
+ page at http://cvc4.cs.nyu.edu/wiki/Public:Third_Party_Applications
+
+* if you are interested in contributing code (for example, a new
+ decision procedure implementation) to the CVC4 project, please
+ contact us at cvc4-devel@cs.nyu.edu. We'd be happy to point you to
+ some internals documentation to help you out.
+
+Thank you for using CVC4!
+
+*** 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.
+
+*** For more information
+
+More information about CVC4 is available at: http://cvc4.cs.nyu.edu/
projects / cvc5.git / blobdiff