-This is CVC4 release version 1.0. For build and installation notes,
+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
+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
+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
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
+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
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.
+in short order.
*** For more information
-More information about CVC4 is available at: http://cs.nyu.edu/acsys/cvc4
+More information about CVC4 is available at: http://cvc4.cs.nyu.edu/
projects / cvc5.git / blobdiff