Difference between revisions of "CVC4"
From CVC4
| (45 intermediate revisions by 5 users not shown) | |||
| Line 1: | Line 1: | ||
| − | + | CVC4 is an automatic theorem prover for Satisfiability Modulo Theories (SMT) problems. It can be used to prove the validity (or, dually, the satisfiability) of first-order formulas in a large number of built-in logical theories and their combination. | |
| − | + | CVC4 is the most recent of a series of popular SMT provers, which originated at Stanford University with the SVC system. CVC4 is a from-scratch redesign and reimplementation of earlier solvers; it is designed for flexibility as a research tool and performance as an industrial SMT solver. | |
| − | + | ||
| − | + | ||
| − | + | ||
| − | + | CVC4 works with a version of first-order logic and has a wide variety of features including: | |
| − | + | ||
| − | + | ||
| − | + | ||
| − | + | ||
| − | + | * several built-in base theories: rational and integer linear arithmetic, arrays, tuples, records, inductive data types, bit vectors, and equality over uninterpreted function symbols; | |
| − | * [http:// | + | * support for quantifiers; |
| − | * [http:// | + | * 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/COPYING_source.html license]). | |
Latest revision as of 18:27, 30 November 2012
CVC4 is an automatic theorem prover for Satisfiability Modulo Theories (SMT) problems. It can be used to prove the validity (or, dually, the satisfiability) of first-order formulas in a large number of built-in logical theories and their combination.
CVC4 is the most recent of a series of popular SMT provers, which originated at Stanford University with the SVC system. CVC4 is a from-scratch redesign and reimplementation of earlier solvers; it is designed for flexibility as a research tool and performance as an industrial SMT solver.
CVC4 works with a version of first-order logic and has a wide variety of features including:
- several built-in base theories: rational and integer linear arithmetic, arrays, tuples, records, inductive data types, bit vectors, and equality over uninterpreted function symbols;
- support for quantifiers;
- 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).
