README.md

   1 [![License: BSD](
   2     https://img.shields.io/badge/License-BSD%203--Clause-blue.svg)](
   3         https://opensource.org/licenses/BSD-3-Clause)
   4 [![Build Status](
   5     https://travis-ci.org/CVC4/CVC4.svg?branch=master)](
   6         https://travis-ci.org/CVC4/CVC4)
   7
   8 CVC4
   9 ===============================================================================
  10
  11 CVC4 is a tool for determining the satisfiability of a first order formula
  12 modulo a first order theory (or a combination of such theories).  It is the
  13 fourth in the Cooperating Validity Checker family of tools (CVC, CVC Lite,
  14 CVC3) but does not directly incorporate code from any previous version.
  15
  16 CVC4 is intended to be an open and extensible SMT engine.  It can be used as a
  17 stand-alone tool or as a library.  It has been designed to increase the
  18 performance and reduce the memory overhead of its predecessors.  It is written
  19 entirely in C++ and is released under an open-source software license (see file
  20 [COPYING](https://github.com/CVC4/CVC4/blob/master/COPYING)).
  21
  22
  23 Website
  24 -------------------------------------------------------------------------------
  25
  26 More information about CVC4 is available at:
  27 http://cvc4.cs.stanford.edu/
  28
  29 Download
  30 -------------------------------------------------------------------------------
  31
  32 The latest version of CVC4 is available on GitHub:
  33 https://github.com/CVC4/CVC4
  34
  35 Source tar balls and binaries for releases and latest stable builds of the
  36 [master branch](https://github.com/CVC4/CVC4) on GitHub can be
  37 found [here](http://cvc4.cs.stanford.edu/downloads).
  38
  39
  40 Build and Dependencies
  41 -------------------------------------------------------------------------------
  42
  43 CVC4 can be built on Linux and macOS.  For Windows, CVC4 can be cross-compiled
  44 using Mingw-w64.
  45
  46 For detailed build and installation instructions on these platforms,
  47 see file [INSTALL.md](https://github.com/CVC4/CVC4/blob/master/INSTALL.md).
  48
  49
  50 Getting Started
  51 -------------------------------------------------------------------------------
  52
  53 We recommend that you visit our CVC4 tutorials online at:
  54
  55   http://cvc4.cs.stanford.edu/wiki/Tutorials
  56
  57 for help getting started using CVC4.
  58
  59
  60 Contributing
  61 -------------------------------------------------------------------------------
  62
  63 We are always happy to hear feedback from our users:
  64
  65 * if you need help with using CVC4, please refer to
  66   [http://cvc4.stanford.edu/#Technical_Support](http://cvc4.stanford.edu/#Technical_Support).
  67
  68 * if you need to report a bug with CVC4, or make a feature request, please
  69   visit our bugtracker at our
  70   [GitHub issues](https://github.com/CVC4/CVC4/issues) page or write to the
  71   cvc4-bugs@cs.stanford.edu mailing list.  We are very grateful for bug reports,
  72   as they help us improve CVC4, and patches are generally reviewed and accepted
  73   quickly.
  74
  75 * if you are using CVC4 in your work, or incorporating it into software of your
  76   own, we'd like to invite you to leave a description and link to your
  77   project/software on our [Third Party Applications](http://cvc4.cs.stanford.edu/wiki/Public:Third_Party_Applications).
  78
  79 * if you are interested in contributing code (for example, a new
  80   decision procedure implementation) to the CVC4 project, please
  81   contact one of the [project leaders](#project_leaders).
  82   We'd be happy to point you to some internal documentation to help you out.
  83
  84 Thank you for using CVC4!
  85
  86
  87 Project Leaders
  88 -------------------------------------------------------------------------------
  89
  90 * [Clark Barrett](http://theory.stanford.edu/~barrett/) (Stanford University)
  91 * [Cesare Tinelli](http://homepage.cs.uiowa.edu/~tinelli/) (The University of Iowa)
  92
  93
  94 Authors
  95 -------------------------------------------------------------------------------
  96
  97 For a full list of authors, please refer to the
  98 [AUTHORS](https://github.com/CVC4/CVC4/blob/master/AUTHORS) file.
  99
 100 History
 101 -------------------------------------------------------------------------------
 102
 103 The Cooperating Validity Checker series has a long history.  The Stanford
 104 Validity Checker (SVC) came first in 1996, incorporating theories and its own
 105 SAT solver.  Its successor, the Cooperating Validity Checker (CVC), had a more
 106 optimized internal design, produced proofs, used the Chaff SAT solver, and
 107 featured a number of usability enhancements.  Its name comes from the
 108 cooperative nature of decision procedures in Nelson-Oppen theory combination,
 109 which share amongst each other equalities between shared terms.
 110
 111 CVC Lite, first made available in 2003, was a rewrite of CVC that attempted to
 112 make CVC more flexible (hence the "lite") while extending the feature set: CVC
 113 Lite supported quantifiers where its predecessors did not.
 114
 115 CVC3 was a major overhaul of portions of CVC Lite: it added better decision
 116 procedure implementations, added support for using MiniSat in the core, and had
 117 generally better performance.
 118
 119 CVC4 is the fifth generation of this validity checker line.  It represents a
 120 complete re-evaluation of the core architecture to be both performant and to
 121 serve as a cutting-edge research vehicle for the next several years.  Rather
 122 than taking CVC3 and redesigning problem parts, we've taken a clean-room
 123 approach, starting from scratch.  Before using any designs from CVC3, we have
 124 thoroughly scrutinized, vetted, and updated them.  Many parts of CVC4 bear only
 125 a superficial resemblance, if any, to their correspondent in CVC3.
 126
 127 However, CVC4 is fundamentally similar to CVC3 and many other modern SMT
 128 solvers: it is a DPLL(T) solver, with a SAT solver at its core and a delegation
 129 path to different decision procedure implementations, each in charge of solving
 130 formulas in some background theory.
 131
 132 The re-evaluation and ground-up rewrite was necessitated, we felt, by the
 133 performance characteristics of CVC3.  CVC3 has many useful features, but some
 134 core aspects of the design led to high memory use, and the use of heavyweight
 135 computation (where more nimble engineering approaches could suffice) makes CVC3
 136 a much slower prover than other tools.  As these designs are central to CVC3, a
 137 new version was preferable to a selective re-engineering, which would have
 138 ballooned in short order.