CVC4 - User contributions [en]

About CVC4

2014-12-02T19:46:15Z

Mdeters: /* Decision Procedures */

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.
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:
* equality over free (aka uninterpreted) function and predicate symbols
* real and integer linear arithmetic
* bit-vectors
* arrays
* tuples
* records
* user-defined inductive data types
* [[Strings|strings]]
* [[Sets|finite sets]]

CVC4 has a wide variety of features including:

* support for quantifiers through heuristic instantiation;
* an interactive text-based interface;
* a rich [http://church.cims.nyu.edu/cvc4-builds/documentation/public/latest/ 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 [http://church.cims.nyu.edu/cvc4-builds/documentation/public/latest-unstable/copying.html license]).

=Web site=

For more information and the latest news about CVC4, visit the [http://cvc4.cs.nyu.edu CVC4 web site].

=Decision Procedures=
* Architecture
** See the [http://dl.acm.org/citation.cfm?id=2032319 CVC4 tool paper].
* Arithmetic
** 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].
** 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.
** 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 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 is implemented primarily via a lazy schema for bitblasting. See [http://eprints-phd.biblio.unitn.it/345/ Anders Franzen's thesis chapter 3].
* 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].
* Datatypes
** CVC4 implements [http://cs.nyu.edu/acsys/pubs/BST07.ps An Abstract Decision Procedure for a Theory of Inductive Data Types].
* Quantifiers
** An overall description of the quantifier framework is given here [http://www.divms.uiowa.edu/~ajreynol/pres-comp12.pdf].
** Rewrite rules [citation?]
** Finite model finding is described in [http://www.divms.uiowa.edu/~ajreynol/pres-fmf12.pdf this presentation].
* SAT Solver
** The main sat solver is based on [http://minisat.se/ minisat v2.2.0].
** 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].
* 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.nyu.edu/~barrett/pubs/LRT+14.pdf CAV 2014 paper]
* 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 + cardinality is described [http://www.divms.uiowa.edu/~ajreynol/pres-fmf12.pdf this presentation] and is used for finite model finding.

=History of CVC=

[[File:svc.gif|thumb|border|100px|The SVC logo.]]
[[File:cvc3_logo.jpg|thumb|border|100px|The CVC3 logo.]]
[[File:cvc3_night_logo.png|thumb|border|100px|The CVC3 "by night" logo, used for nightly builds and regressions.]]
[[File:cvc3cvc4.png|thumb|border|100px|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.

[[File:cvc4-logo.png|thumb|border|100px|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.

About CVC4

2014-11-19T19:06:56Z

Mdeters: /* Decision Procedures */

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.
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:
* equality over free (aka uninterpreted) function and predicate symbols
* real and integer linear arithmetic
* bit-vectors
* arrays
* tuples
* records
* user-defined inductive data types
* [[Strings|strings]]
* [[Sets|finite sets]]

CVC4 has a wide variety of features including:

* support for quantifiers through heuristic instantiation;
* an interactive text-based interface;
* a rich [http://church.cims.nyu.edu/cvc4-builds/documentation/public/latest/ 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 [http://church.cims.nyu.edu/cvc4-builds/documentation/public/latest-unstable/copying.html license]).

=Web site=

For more information and the latest news about CVC4, visit the [http://cvc4.cs.nyu.edu CVC4 web site].

=Decision Procedures=
* Architecture
** See the [http://dl.acm.org/citation.cfm?id=2032319 CVC4 tool paper].
* Arithmetic
** 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].
** 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.
** 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 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 is implemented primarily via a lazy schema for bitblasting. See [http://eprints-phd.biblio.unitn.it/345/ Anders Franzen's thesis chapter 3].
* 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].
* Datatypes
** CVC4 implements [http://cs.nyu.edu/acsys/pubs/BST07.ps An Abstract Decision Procedure for a Theory of Inductive Data Types].
* Quantifiers
** An overall description of the quantifier framework is given here [http://www.divms.uiowa.edu/~ajreynol/pres-comp12.pdf].
** Rewrite rules [citation?]
** Finite model finding is described in [http://www.divms.uiowa.edu/~ajreynol/pres-fmf12.pdf this presentation].
* SAT Solver
** The main sat solver is based on [http://minisat.se/ minisat v2.2.0].
** 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].
* Sets
** Adaptation of tableau-based decision procedure described [http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.5176 here].
* 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 + cardinality is described [http://www.divms.uiowa.edu/~ajreynol/pres-fmf12.pdf this presentation] and is used for finite model finding.

=History of CVC=

[[File:svc.gif|thumb|border|100px|The SVC logo.]]
[[File:cvc3_logo.jpg|thumb|border|100px|The CVC3 logo.]]
[[File:cvc3_night_logo.png|thumb|border|100px|The CVC3 "by night" logo, used for nightly builds and regressions.]]
[[File:cvc3cvc4.png|thumb|border|100px|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.

[[File:cvc4-logo.png|thumb|border|100px|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.

Publications

2014-11-13T22:00:23Z

Mdeters:

Papers about the tool
* Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanović, Tim King, Andrew Reynolds, and Cesare Tinelli. [http://cs.nyu.edu/~barrett/pubs/BCD+11.pdf CVC4]. Lecture Notes in Computer Science, 2011, Volume 6806, Computer Aided Verification, pages 171-177.

Papers describing original research that was incorporated into CVC4
* Theory Combination
** Dejan Jovanović and Clark Barrett. [http://cs.nyu.edu/~barrett/pubs/JB10-SMT.pdf Sharing is Caring]. In Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (SMT '10), July 2010.
** Dejan Jovanović and Clark Barrett. [http://cs.nyu.edu/~barrett/pubs/JB10-TR.pdf Polite Theories Revisited]. In Proceedings of the Seventeenth International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '10), volume 6397 of Lecture Notes in Computer Science, pages 402-416. Springer, October 2010. Yogyakarta, Indonesia.
** Dejan Jovanović and Clark Barrett. [http://cs.nyu.edu/~barrett/pubs/JB13.pdf Being careful about theory combination]. In Formal Methods in System Design, vol. 42, no. 1, Feb. 2013, pp. 67-90, Springer US.
* Bitvectors
** Liana Hadarean, Clark Barrett, Dejan Jovanović, Cesare Tinelli, and Kshitij Bansal. [http://www.cs.nyu.edu/~barrett/pubs/HBJ+14.pdf A tale of two solvers: Eager and lazy approaches to bit-vectors]. In Proceedings of the Twenty-Sixth International Conference on Computer Aided Verification (CAV '14), July 2014, pages 646-662. Vienna, Austria.
* Arithmetic
** Tim King, Clark Barrett, and Bruno Dutertre. [http://www.cs.nyu.edu/~barrett/pubs/KBD13.pdf Simplex with sum of infeasibilities for SMT]. In Formal Methods in Computer-Aided Design (FMCAD), 2013.
** Tim King, Clark Barrett, and Cesare Tinelli. [http://www.cs.nyu.edu/~barrett/pubs/KBT14.pdf Leveraging linear and mixed integer programming for SMT]. In FMCAD, 2014.
* Strings
** Tianyi Liang, Andrew Reynolds, Cesare Tinelli, Clark Barrett, and Morgan Deters. [http://www.cs.nyu.edu/~barrett/pubs/LRT+14.pdf A DPLL(T) theory solver for a theory of strings and regular expressions]. In Computer Aided Verification (CAV), 2014.
* Quantifiers and finite model finding
** Andrew Reynolds, Cesare Tinelli, and Leonardo de Moura. [http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD14/proceedings/31_reynolds.pdf Finding conflicting instances of quantified formulas in SMT]. In FMCAD, 2014.
** Andrew Reynolds, Cesare Tinelli, Amit Goel, and Sava Krstić. [http://lara.epfl.ch/~reynolds/cav13.pdf Finite model finding in SMT]. In Computer Aided Verification (CAV), 2013.
** Andrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krstić, Morgan Deters, and Clark Barrett. [http://www.cs.nyu.edu/~barrett/pubs/RTG+13.pdf Quantifier instantiation techniques for finite model finding in SMT]. In CADE, 2013.

Applications of CVC4
* Tim King and Clark Barrett. [http://cs.nyu.edu/~barrett/pubs/KB11.pdf Exploring and Categorizing Error Spaces using BMC and SMT]. In Proceedings of the 9th International Workshop on Satisfiability Modulo Theories (SMT '11), July 2011.
* Wei Wang, Clark Barrett, and Thomas Wies. [http://www.cs.nyu.edu/~barrett/pubs/WBW14.pdf Cascade 2.0]. In Verification, Model Checking, and Abstract Interpretation (VMCAI), 2014.

Publications

2014-11-13T22:00:05Z

Mdeters:

Papers about the tool
* Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanović, Tim King, Andrew Reynolds, and Cesare Tinelli. [http://cs.nyu.edu/~barrett/pubs/BCD+11.pdf CVC4]. Lecture Notes in Computer Science, 2011, Volume 6806, Computer Aided Verification, Pages 171-177.

Papers describing original research that was incorporated into CVC4
* Theory Combination
** Dejan Jovanović and Clark Barrett. [http://cs.nyu.edu/~barrett/pubs/JB10-SMT.pdf Sharing is Caring]. In Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (SMT '10), July 2010.
** Dejan Jovanović and Clark Barrett. [http://cs.nyu.edu/~barrett/pubs/JB10-TR.pdf Polite Theories Revisited]. In Proceedings of the Seventeenth International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '10), volume 6397 of Lecture Notes in Computer Science, pages 402-416. Springer, October 2010. Yogyakarta, Indonesia.
** Dejan Jovanović and Clark Barrett. [http://cs.nyu.edu/~barrett/pubs/JB13.pdf Being careful about theory combination]. In Formal Methods in System Design, vol. 42, no. 1, Feb. 2013, pp. 67-90, Springer US.
* Bitvectors
** Liana Hadarean, Clark Barrett, Dejan Jovanović, Cesare Tinelli, and Kshitij Bansal. [http://www.cs.nyu.edu/~barrett/pubs/HBJ+14.pdf A tale of two solvers: Eager and lazy approaches to bit-vectors]. In Proceedings of the Twenty-Sixth International Conference on Computer Aided Verification (CAV '14), July 2014, pages 646-662. Vienna, Austria.
* Arithmetic
** Tim King, Clark Barrett, and Bruno Dutertre. [http://www.cs.nyu.edu/~barrett/pubs/KBD13.pdf Simplex with sum of infeasibilities for SMT]. In Formal Methods in Computer-Aided Design (FMCAD), 2013.
** Tim King, Clark Barrett, and Cesare Tinelli. [http://www.cs.nyu.edu/~barrett/pubs/KBT14.pdf Leveraging linear and mixed integer programming for SMT]. In FMCAD, 2014.
* Strings
** Tianyi Liang, Andrew Reynolds, Cesare Tinelli, Clark Barrett, and Morgan Deters. [http://www.cs.nyu.edu/~barrett/pubs/LRT+14.pdf A DPLL(T) theory solver for a theory of strings and regular expressions]. In Computer Aided Verification (CAV), 2014.
* Quantifiers and finite model finding
** Andrew Reynolds, Cesare Tinelli, and Leonardo de Moura. [http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD14/proceedings/31_reynolds.pdf Finding conflicting instances of quantified formulas in SMT]. In FMCAD, 2014.
** Andrew Reynolds, Cesare Tinelli, Amit Goel, and Sava Krstić. [http://lara.epfl.ch/~reynolds/cav13.pdf Finite model finding in SMT]. In Computer Aided Verification (CAV), 2013.
** Andrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krstić, Morgan Deters, and Clark Barrett. [http://www.cs.nyu.edu/~barrett/pubs/RTG+13.pdf Quantifier instantiation techniques for finite model finding in SMT]. In CADE, 2013.

Applications of CVC4
* Tim King and Clark Barrett. [http://cs.nyu.edu/~barrett/pubs/KB11.pdf Exploring and Categorizing Error Spaces using BMC and SMT]. In Proceedings of the 9th International Workshop on Satisfiability Modulo Theories (SMT '11), July 2011.
* Wei Wang, Clark Barrett, and Thomas Wies. [http://www.cs.nyu.edu/~barrett/pubs/WBW14.pdf Cascade 2.0]. In Verification, Model Checking, and Abstract Interpretation (VMCAI), 2014.

About CVC4

2014-11-13T21:47:01Z

Mdeters:

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.
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:
* equality over free (aka uninterpreted) function and predicate symbols
* real and integer linear arithmetic
* bit-vectors
* arrays
* tuples
* records
* user-defined inductive data types
* [[Strings|strings]]
* [[Sets|finite sets]]

CVC4 has a wide variety of features including:

* support for quantifiers through heuristic instantiation;
* an interactive text-based interface;
* a rich [http://church.cims.nyu.edu/cvc4-builds/documentation/public/latest/ 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 [http://church.cims.nyu.edu/cvc4-builds/documentation/public/latest-unstable/copying.html license]).

=Web site=

For more information and the latest news about CVC4, visit the [http://cvc4.cs.nyu.edu CVC4 web site].

=Decision Procedures=
* Architecture
** See the [http://dl.acm.org/citation.cfm?id=2032319 CVC4 tool paper].
* Arithmetic
** 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].
** 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.
** 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-existant. 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 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 is implemented primarily via a lazy schema for bitblasting. See [http://eprints-phd.biblio.unitn.it/345/ Anders Franzen's thesis chapter 3].
* 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].
* Datatypes
** CVC4 implements [http://cs.nyu.edu/acsys/pubs/BST07.ps An Abstract Decision Procedure for a Theory of Inductive Data Types].
* Quantifiers
** An overall description of the quantifier framework is given here [http://www.divms.uiowa.edu/~ajreynol/pres-comp12.pdf].
** Rewrite rules [citation?]
** Finite model finding is described in [http://www.divms.uiowa.edu/~ajreynol/pres-fmf12.pdf this presentation].
* SAT Solver
** The main sat solver is based on [http://minisat.se/ minisat v2.2.0].
** 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].
* Sets
** Adaptation of tableau-based decision procedure described [http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.5176 here].
* 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 + cardinality is described [http://www.divms.uiowa.edu/~ajreynol/pres-fmf12.pdf this presentation] and is used for finite model finding.

=History of CVC=

[[File:svc.gif|thumb|border|100px|The SVC logo.]]
[[File:cvc3_logo.jpg|thumb|border|100px|The CVC3 logo.]]
[[File:cvc3_night_logo.png|thumb|border|100px|The CVC3 "by night" logo, used for nightly builds and regressions.]]
[[File:cvc3cvc4.png|thumb|border|100px|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.

[[File:cvc4-logo.png|thumb|border|100px|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.

SMT-LIB Compliance

2014-09-27T17:47:16Z

Mdeters:

CVC4 is mostly SMT-LIB-conforming with ''--lang smt''. With the ''--smtlib-strict'' command line option, though, you get additional strictness and standards conformance.

There are areas where we don't support full functionality, or where we are not compliant:

* We do not yet adequately support nonlinear-arithmetic (the QF_NIA, QF_NRA, QF_UFNRA, UFNRA, and AUFNIRA logics)
* We do not yet support all the features of the recent (September 2014) draft of SMT-LIB 2.5

Also, please note that CVC4 is not intended as a compliance-checker for SMT-LIB input. That is, it is a bit lenient in accepting non-conforming input.