README

   1 This is CVC4 release version 1.3.  For build and installation notes,
   2 please see the INSTALL file included with this distribution.
   3
   4 This first official release of CVC4 is the result of more than three
   5 years of efforts by researchers at New York University and The
   6 University of Iowa.  The project leaders are Clark Barrett (New York
   7 University) and Cesare Tinelli (The University of Iowa).  For a full
   8 list of authors, please refer to the AUTHORS file in the source
   9 distribution.
  10
  11 CVC4 is a tool for determining the satisfiability of a first order
  12 formula modulo a first order theory (or a combination of such
  13 theories). It is the fourth in the Cooperating Validity Checker family
  14 of tools (CVC, CVC Lite, CVC3) but does not directly incorporate code
  15 from any previous version.
  16
  17 CVC4 is intended to be an open and extensible SMT engine.  It can be
  18 used as a stand-alone tool or as a library.  It has been designed to
  19 increase the performance and reduce the memory overhead of its
  20 predecessors.  It is written entirely in C++ and is released under an
  21 open-source software license (see the file COPYING in the source
  22 distribution).
  23
  24 *** Getting started with CVC4
  25
  26 For help installing CVC4, see the INSTALL file that comes with this
  27 distribution.
  28
  29 We recommend that you visit our CVC4 tutorials online at:
  30
  31   http://cvc4.cs.nyu.edu/wiki/Tutorials
  32
  33 for help getting started using CVC4.
  34
  35 *** Contributing to the CVC4 project
  36
  37 We are always happy to hear feedback from our users:
  38
  39 * if you need help with using CVC4, please write to the
  40   cvc-users@cs.nyu.edu mailing list.
  41
  42 * if you need to report a bug with CVC4, or make a feature request,
  43   please visit our bugtracker at http://cvc4.cs.nyu.edu/bugs/ or write
  44   to the cvc-bugs@cs.nyu.edu mailing list.  We are very grateful for
  45   bug reports, as they help us improve CVC4, and patches are generally
  46   reviewed and accepted quickly.
  47
  48 * if you are using CVC4 in your work, or incorporating it into
  49   software of your own, we'd like to invite you to leave a description
  50   and link to your project/software on our "Third Party Applications"
  51   page at http://cvc4.cs.nyu.edu/wiki/Public:Third_Party_Applications
  52
  53 * if you are interested in contributing code (for example, a new
  54   decision procedure implementation) to the CVC4 project, please
  55   contact us at cvc4-devel@cs.nyu.edu.  We'd be happy to point you to
  56   some internals documentation to help you out.
  57
  58 Thank you for using CVC4!
  59
  60 *** The History of CVC4
  61
  62 The Cooperating Validity Checker series has a long history.  The
  63 Stanford Validity Checker (SVC) came first in 1996, incorporating
  64 theories and its own SAT solver.  Its successor, the Cooperating
  65 Validity Checker (CVC), had a more optimized internal design, produced
  66 proofs, used the Chaff SAT solver, and featured a number of usability
  67 enhancements.  Its name comes from the cooperative nature of decision
  68 procedures in Nelson-Oppen theory combination, which share amongst
  69 each other equalities between shared terms.  CVC Lite, first made
  70 available in 2003, was a rewrite of CVC that attempted to make CVC
  71 more flexible (hence the "lite") while extending the feature set: CVC
  72 Lite supported quantifiers where its predecessors did not.  CVC3 was a
  73 major overhaul of portions of CVC Lite: it added better decision
  74 procedure implementations, added support for using MiniSat in the
  75 core, and had generally better performance.
  76
  77 CVC4 is the new version, the fifth generation of this validity checker
  78 line that is now celebrating sixteen years of heritage.  It represents
  79 a complete re-evaluation of the core architecture to be both
  80 performant and to serve as a cutting-edge research vehicle for the
  81 next several years.  Rather than taking CVC3 and redesigning problem
  82 parts, we've taken a clean-room approach, starting from scratch.
  83 Before using any designs from CVC3, we have thoroughly scrutinized,
  84 vetted, and updated them.  Many parts of CVC4 bear only a superficial
  85 resemblance, if any, to their correspondent in CVC3.
  86
  87 However, CVC4 is fundamentally similar to CVC3 and many other modern
  88 SMT solvers: it is a DPLL(T) solver, with a SAT solver at its core and
  89 a delegation path to different decision procedure implementations,
  90 each in charge of solving formulas in some background theory.
  91
  92 The re-evaluation and ground-up rewrite was necessitated, we felt, by
  93 the performance characteristics of CVC3.  CVC3 has many useful
  94 features, but some core aspects of the design led to high memory use,
  95 and the use of heavyweight computation (where more nimble engineering
  96 approaches could suffice) makes CVC3 a much slower prover than other
  97 tools.  As these designs are central to CVC3, a new version was
  98 preferable to a selective re-engineering, which would have ballooned
  99 in short order.
 100
 101 *** For more information
 102
 103 More information about CVC4 is available at: http://cvc4.cs.nyu.edu/