diff options
Diffstat (limited to 'doc/cvc5.1_template.in')
-rw-r--r-- | doc/cvc5.1_template.in | 131 |
1 files changed, 131 insertions, 0 deletions
diff --git a/doc/cvc5.1_template.in b/doc/cvc5.1_template.in new file mode 100644 index 000000000..042d6cfc1 --- /dev/null +++ b/doc/cvc5.1_template.in @@ -0,0 +1,131 @@ +.\" Process this file with +.\" groff -man -Tascii cvc4.1 +.\" +.TH CVC4 1 "@MAN_DATE@" "CVC4 release @VERSION@" "User Manuals" +.SH NAME +cvc4, pcvc4 \- an automated theorem prover +.SH SYNOPSIS +.B cvc4 [ +.I options +.B ] [ +.I file +.B ] +.P +.B pcvc4 [ +.I options +.B ] [ +.I file +.B ] +.SH DESCRIPTION +.B cvc4 +is an automated theorem prover for first-order formulas with respect +to background theories of interest. +.B pcvc4 +is CVC4's "portfolio" variant, which is capable of running multiple +CVC4 instances in parallel, configured differently. + +With +.I file +, commands are read from +.I file +and executed. CVC4 supports the SMT-LIB (versions 1.2 and 2.0) input +format, as well as its own native \(lqpresentation language\(rq (see +.BR cvc4 (5) +), which is similar in many respects to CVC3's presentation language, +but not identical. + +If +.I file +is unspecified, standard input is read (and the +.B CVC4 +presentation language is assumed). If +.I file +is unspecified and +.B CVC4 +is connected to a terminal, interactive mode is assumed. + +.SH COMMON OPTIONS + +.IP "Each option marked with [*] has a \-\-no\-OPTIONNAME variant, which reverses the sense of the option." + +${man_common}$ + +${man_others}$ + +.IP "Each option marked with [*] has a \-\-no\-OPTIONNAME variant, which reverses the sense of the option." + +.\".SH FILES +.\".SH ENVIRONMENT +.SH DIAGNOSTICS +.B CVC4 +reports all syntactic and semantic errors on standard error. +.SH HISTORY +The +.B CVC4 +effort is the culmination of fifteen years of theorem proving +research, starting with the +.I Stanford Validity Checker (SVC) +in 1996. + +SVC's successor, the +.I Cooperating Validity Checker (CVC), +had a more optimized internal design, produced proofs, used the +.I 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 \(lqlite\(rq) 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( +.I 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. +.SH VERSION +This manual page refers to +.B CVC4 +version @VERSION@. +.SH BUGS +An issue tracker for the CVC4 project is maintained at +.BR https://github.com/CVC4/CVC4/issues . +.SH AUTHORS +.B 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. +.SH "SEE ALSO" +.BR libcvc4 (3), +.BR libcvc4parser (3) + +Additionally, the CVC4 wiki contains useful information about the +design and internals of CVC4. It is maintained at +.BR http://cvc4.cs.stanford.edu/wiki/ . |