Difference between revisions of "CVC4"

From CVC4
Jump to: navigation, search
m (CVC3 Developers Portal moved to CVC4 Developers Portal: New portal for CVC4)
 
(63 intermediate revisions by 5 users not shown)
Line 1: Line 1:
−
Welcome to [http://www.cs.nyu.edu/acsys/cvc3/ CVC4] developers documentation. This website and the service is only intended for the developers of CVC4 at NYU.  
+
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.
  
−
Two other pages important for developers:
+
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 Bugzilla located at [http://www.cs.nyu.edu/acsys/bugs/ http://www.cs.nyu.edu/acsys/bugs/]
+
−
* CVC4 User Documentation wiki [http://www.cs.nyu.edu/acsys/cvc4/wiki http://www.cs.nyu.edu/acsys/cvc4/wiki]
+
  
−
You can start by taking a look at the [[User's Guide]] to find out how to use the service. If you encounter any problems, you should first take a look at the [[Frequently Asked Questions]] or contact the [http://cs.nyu.edu/~dejan/ administrator].
+
CVC4 works with a version of first-order logic and has a wide variety of features including:
  
−
If you are a developer and you want to understand or change how the benchmarking service works, ou can also take a look at the [[How it's Made|developers documentation]].
+
* 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 [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 17: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).
Retrieved from "http://cvc4.cs.stanford.edu/w/index.php?title=CVC4&oldid=4020"