| CVC4(1) | User Manuals | CVC4(1) |
cvc4, pcvc4 - an automated theorem prover
cvc4 [ options ] [ file ]
pcvc4 [ options ] [ file ]
cvc4 is an automated theorem prover for first-order formulas with respect to background theories of interest. pcvc4 is CVC4's "portfolio" variant, which is capable of running multiple CVC4 instances in parallel, configured differently.
With file , commands are read from file and executed. CVC4 supports the SMT-LIB (versions 1.2 and 2.0) input format, as well as its own native “presentation language” (see cvc4(5) ), which is similar in many respects to CVC3's presentation language, but not identical.
If file is unspecified, standard input is read (and the CVC4 presentation language is assumed). If file is unspecified and CVC4 is connected to a terminal, interactive mode is assumed.
CVC4 reports all syntactic and semantic errors on standard error.
The CVC4 effort is the culmination of fifteen years of theorem proving research, starting with the Stanford Validity Checker (SVC) in 1996.
SVC's 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: CVCLite 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.
CVC4 is the new version, the fifth generation of this validity checker line that is now celebrating fifteen 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.
This manual page refers to CVC4 version CVC4_RELEASE_STRING.
An issue tracker for the CVC4 project is maintained at https://github.com/CVC4/CVC4/issues.
CVC4 is developed by a team of researchers at Stanford University and the University of Iowa. See the AUTHORS file in the distribution for a full list of contributors.
Additionally, the CVC4 wiki contains useful information about the design and internals of CVC4. It is maintained at http://cvc4.cs.stanford.edu/wiki/.
| 2022-10-29 | CVC4 release CVC4_RELEASE_STRING |