Difference between revisions of "About CVC4"

From CVC4
Jump to: navigation, search
(Decision Procedures)
(31 intermediate revisions by 6 users not shown)
Line 1: Line 1:
CVC4 is an automatic theorem prover for [http://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories Satisifiability Modulo Theories (SMT) ] (for a more formal introduction to SMT see the following book chapter [https://cs.nyu.edu/~barrett/pubs/BSST09.pdf Satisfiability Modulo Theories] ). Technically, it is an automated validity checker for a many-sorted (i.e., typed) first-order logic with built-in theories.
+
CVC4 is an automatic theorem prover for [http://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories Satisifiability Modulo Theories (SMT)] (for a more formal introduction to SMT see the following book chapter [https://cs.stanford.edu/~barrett/pubs/BSST09.pdf Satisfiability Modulo Theories] ). Technically, it is an automated validity checker for a many-sorted (i.e., typed) first-order logic with built-in theories.
It can be used to prove the validity (or, dually, the satisfiability) of with respect to several built-in logical theories and their combination.
+
It can be used to prove the validity (or, dually, the satisfiability) of a formula with respect to several built-in logical theories and their combination.
  
 
CVC4 currently has support for the following theories:
 
CVC4 currently has support for the following theories:
Line 9: Line 9:
 
* tuples
 
* tuples
 
* records
 
* records
* user-defined inductive data types.
+
* user-defined inductive [[Datatypes|datatypes]]
 +
* [[Strings|strings]]
 +
* [[Sets|finite sets]]
 +
* [[Separation Logic|separation logic]]
  
 
CVC4 has a wide variety of features including:
 
CVC4 has a wide variety of features including:
  
* support for quantifiers through heuristic instantiaion;
+
* support for quantifiers through heuristic instantiation;
 
* an interactive text-based interface;
 
* an interactive text-based interface;
* a rich [http://church.cims.nyu.edu/cvc4-builds/documentation/public/latest/ C++ API] for embedding in other systems;
+
* a rich [http://cvc4.cs.stanford.edu/cvc4-builds/documentation/public/latest/ C++ API] for embedding in other systems;
 
* model generation abilities;
 
* model generation abilities;
 
* source compatibility with much of the CVC3 API via a "compatibility library";
 
* source compatibility with much of the CVC3 API via a "compatibility library";
* essentially no limit on its use for research or commercial purposes (see [http://church.cims.nyu.edu/cvc4-builds/documentation/public/latest/COPYING_source.html license]).
+
* essentially no limit on its use for research or commercial purposes (see [https://github.com/CVC4/CVC4/blob/master/COPYING license]).
  
 
=Web site=
 
=Web site=
  
For more information and the latest news about CVC4, visit the [http://cvc4.cs.nyu.edu CVC4 web site].
+
For more information and the latest news about CVC4, visit the [http://cvc4.cs.stanford.edu CVC4 web site].
  
 
=Decision Procedures=
 
=Decision Procedures=
Line 28: Line 31:
 
** See the [http://dl.acm.org/citation.cfm?id=2032319 CVC4 tool paper].
 
** See the [http://dl.acm.org/citation.cfm?id=2032319 CVC4 tool paper].
 
* Arithmetic
 
* Arithmetic
** Linear arithmetic is roughly an implementation of [yices.csl.sri.com/sri-csl-06-01.pdf Integrating Simplex with DPLL(T)]. A technical report is planned to explain our extensions.
+
** CVC4 solves linear real arithmetic using an implementation of [http://link.springer.com/chapter/10.1007%2F11817963_11? Simplex for DPLL(T)]. For a more complete introduction see the [http://yices.csl.sri.com/sri-csl-06-01.pdf tech report].
** Integers are currently handled in an equational solver based on [https://es.fbk.eu/people/griggio/papers/jsat12.pdf A Practical Approach to Satisfiability Modulo Linear Integer Arithmetic].
+
** The linear arithmetic module includes heuristics from [http://eprints-phd.biblio.unitn.it/166/2/thesis.pdf Section 2.5 of Alberto Griggio's thesis] and a few currently unpublished ones.
** Non-linear arithmetic support is rudimentary to non-existant. Currently, it is handled by abstracting monomials as unique new variables.  We plan on implementing [http://cs.nyu.edu/~dejan/papers/jovanovic-ijcar2012.pdf Solving Non-Linear Arithmetic] this spring.
+
** Integers are currently handled by first solving the real relaxation of the constraints, and then using a combination of [http://www.cs.wm.edu/~idillig/cav2009.pdf Cuts from Proofs] and branching to ensure integer solutions.  This approach and the equational solver used are described in [https://es.fbk.eu/people/griggio/papers/jsat12.pdf A Practical Approach to Satisfiability Modulo Linear Integer Arithmetic].
 +
** A technical report is planned to explain a number of small details and extensions including analysis to improve simplex's conflicts, handling disequalities, supporting model generation in CVC4's combination framework, heuristically propagating equalities over sharing terms, tableau row based propagation, and terminating simplex with unknown.
 +
** Non-linear arithmetic support is currently rudimentary to non-existent. In CVC4 v1.0, non-linearity is handled by abstracting monomials as unique new variables.  We plan on implementing [http://cs.nyu.edu/~dejan/papers/jovanovic-ijcar2012.pdf Solving Non-Linear Arithmetic] this spring.
 
* Arrays
 
* Arrays
 
** Arrays are implemented in a manner inspired by the [http://research.microsoft.com/en-us/um/people/leonardo/files/fmcad09.pdf Generalized, efficient array decision procedures] paper with a few major modifications.
 
** Arrays are implemented in a manner inspired by the [http://research.microsoft.com/en-us/um/people/leonardo/files/fmcad09.pdf Generalized, efficient array decision procedures] paper with a few major modifications.
 
* Bitvectors
 
* Bitvectors
** Bitvectors is implemented primarily via a lazy schema for bitblasting. See [http://eprints-phd.biblio.unitn.it/345/ Anders Franz�en's thesis] chapter 3.
+
** Bitvectors is implemented primarily via a lazy schema for bitblasting. See [http://eprints-phd.biblio.unitn.it/345/ Anders Franzen's thesis chapter 3].
 
* Combination
 
* Combination
 
** Theory combination is based on the care graph framework described in both [http://cs.nyu.edu/~dejan/papers/jovanovic-fmsd2012.pdf Being careful about theory combination] and [http://cs.nyu.edu/~dejan/papers/jovanovic-frocos2011.pdf Sharing is Caring: Combination of Theories].
 
** Theory combination is based on the care graph framework described in both [http://cs.nyu.edu/~dejan/papers/jovanovic-fmsd2012.pdf Being careful about theory combination] and [http://cs.nyu.edu/~dejan/papers/jovanovic-frocos2011.pdf Sharing is Caring: Combination of Theories].
 
* Datatypes
 
* Datatypes
** CVC4 implements [ftp://ftp.cs.uiowa.edu/pub/tinelli/papers/BarST-PDPAR-06.pdf An Abstract Decision Procedure for a Theory of Inductive Data Types].
+
** CVC4 implements [http://homepage.cs.uiowa.edu/~tinelli/papers/BarST-JSAT-07.pdf An Abstract Decision Procedure for a Theory of Inductive Data Types].
 +
** This procedure has been extended to incorporate coinductive datatypes [http://homepage.cs.uiowa.edu/~ajreynol/cade15.pdf].
 
* Quantifiers
 
* Quantifiers
** An overall description of the quantifier framework is given here [http://www.divms.uiowa.edu/~ajreynol/pres-comp12.pdf].
+
** E-matching and conflict-based quantifier instantiation [http://homepage.cs.uiowa.edu/~ajreynol/fmcad14.pdf].
** Rewrite rules [citation?]
+
** Finite model finding [http://homepage.cs.uiowa.edu/~ajreynol/thesis.pdf].
** Finite model finding is described in [http://www.divms.uiowa.edu/~ajreynol/pres-fmf12.pdf this presentation].
+
** Techniques for finding counterexamples for conjectures in the presence of recursive functions [http://homepage.cs.uiowa.edu/~ajreynol/ijcar16a.pdf].
 +
** Automated induction for datatypes [http://homepage.cs.uiowa.edu/~ajreynol/vmcai15.pdf].
 +
** A decision procedure for quantified linear arithmetic with one alternation [http://homepage.cs.uiowa.edu/~ajreynol/report-inst-la15.pdf].
 +
** Support for syntax-guided synthesis, as described in [http://homepage.cs.uiowa.edu/~ajreynol/cav15a.pdf].
 
* SAT Solver
 
* SAT Solver
 
** The main sat solver is based on [http://minisat.se/ minisat v2.2.0].
 
** The main sat solver is based on [http://minisat.se/ minisat v2.2.0].
** Additionally, we use justification and relevancy to limit what gets sent to each theory. [citation?]
+
** Additionally, we (optionally, and enabled by default for certain theories) use non-clausal analysis to cut down search space of minisat. For more details see the article [http://cs.nyu.edu/~kshitij/articles/cvc4-branching-heuristic.pdf A branching heuristic in CVC4].
 +
* Separation Logic
 +
** A decision procedure for a fragment quantifier-free separation logic containing negation, separation star and magic wand is implemented and can be composed with other decision procedures supported by CVC4.  For details see [http://homepage.divms.uiowa.edu/~ajreynol/atva16.pdf A Decision Procedure for Separation Logic in SMT].
 +
* Sets
 +
** Adaptation of tableau-based decision procedure described [http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.5176 here].
 +
* Strings
 +
** Original approach described in our [http://www.cs.stanford.edu/~barrett/pubs/LRT+14.pdf CAV 2014 paper: A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions].
 +
** Decision procedure for regular memberships with length [http://homepage.cs.uiowa.edu/~ajreynol/frocos15.pdf].
 
* Uninterpreted functions
 
* Uninterpreted functions
 
** UF (without cardinality) is handled in a manner inspired by [http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.70.1745 Simplify's tech report].
 
** UF (without cardinality) is handled in a manner inspired by [http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.70.1745 Simplify's tech report].

Revision as of 10:19, 27 January 2017

CVC4 is an automatic theorem prover for Satisifiability Modulo Theories (SMT) (for a more formal introduction to SMT see the following book chapter Satisfiability Modulo Theories ). Technically, it is an automated validity checker for a many-sorted (i.e., typed) first-order logic with built-in theories. It can be used to prove the validity (or, dually, the satisfiability) of a formula with respect to several built-in logical theories and their combination.

CVC4 currently has support for the following theories:

CVC4 has a wide variety of features including:

  • support for quantifiers through heuristic instantiation;
  • an interactive text-based interface;
  • a rich C++ API for embedding in other systems;
  • model generation abilities;
  • source compatibility with much of the CVC3 API via a "compatibility library";
  • essentially no limit on its use for research or commercial purposes (see license).

Web site

For more information and the latest news about CVC4, visit the CVC4 web site.

Decision Procedures

History of CVC

The SVC logo.
The CVC3 logo.
The CVC3 "by night" logo, used for nightly builds and regressions.
An early CVC4 logo.

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.

The CVC4 logo.

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.