1 .\" Process this file with
2 .\" groff -man -Tascii cvc4.1
4 .TH CVC4 1 "@MAN_DATE@" "CVC4 release @VERSION@" "User Manuals"
6 cvc4, pcvc4 \- an automated theorem prover
21 is an automated theorem prover for first-order formulas with respect
22 to background theories of interest.
24 is CVC4's "portfolio" variant, which is capable of running multiple
25 CVC4 instances in parallel, configured differently.
29 , commands are read from
31 and executed. CVC4 supports the SMT-LIB (versions 1.2 and 2.0) input
32 format, as well as its own native \(lqpresentation language\(rq (see
34 ), which is similar in many respects to CVC3's presentation language,
39 is unspecified, standard input is read (and the
41 presentation language is assumed). If
45 is connected to a terminal, interactive mode is assumed.
49 .IP "Each option marked with [*] has a \-\-no\-OPTIONNAME variant, which reverses the sense of the option."
55 .IP "Each option marked with [*] has a \-\-no\-OPTIONNAME variant, which reverses the sense of the option."
61 reports all syntactic and semantic errors on standard error.
65 effort is the culmination of fifteen years of theorem proving
66 research, starting with the
67 .I Stanford Validity Checker (SVC)
71 .I Cooperating Validity Checker (CVC),
72 had a more optimized internal design, produced proofs, used the
74 SAT solver, and featured a number of usability
75 enhancements. Its name comes from the cooperative nature of
76 decision procedures in Nelson-Oppen theory combination,
77 which share amongst each other equalities between shared terms.
79 CVC Lite, first made available in 2003, was a rewrite of CVC
80 that attempted to make CVC
81 more flexible (hence the \(lqlite\(rq) while extending the feature set:
82 CVCLite supported quantifiers where its predecessors did not.
83 CVC3 was a major overhaul of portions of CVC Lite: it added
84 better decision procedure implementations, added support for using
85 MiniSat in the core, and had generally better performance.
87 CVC4 is the new version, the fifth generation of this validity
88 checker line that is now celebrating fifteen years of heritage.
89 It represents a complete re-evaluation of
90 the core architecture to be both performant and to serve as a cutting-edge research vehicle
91 for the next several years. Rather than taking CVC3
92 and redesigning problem parts, we've taken a clean-room approach,
93 starting from scratch. Before using any designs from CVC3, we have
94 thoroughly scrutinized, vetted, and updated them. Many parts of CVC4
95 bear only a superficial resemblance, if any, to their correspondent in CVC3.
97 However, CVC4 is fundamentally similar to CVC3 and many other
98 modern SMT solvers: it is a DPLL(
101 with a SAT solver at its core and a delegation path to different decision
102 procedure implementations, each in charge of solving formulas in some
105 The re-evaluation and ground-up rewrite was necessitated, we felt, by
106 the performance characteristics of CVC3. CVC3 has many useful
107 features, but some core aspects of the design led to high memory use, and
108 the use of heavyweight computation (where more nimble engineering
109 approaches could suffice) makes CVC3 a much slower prover than other tools.
110 As these designs are central to CVC3, a new version was preferable to a
111 selective re-engineering, which would have ballooned in short order.
113 This manual page refers to
117 An issue tracker for the CVC4 project is maintained at
118 .BR https://github.com/CVC4/CVC4/issues .
121 is developed by a team of researchers at Stanford University
122 and the University of Iowa.
123 See the AUTHORS file in the distribution for a full list of
127 .BR libcvc4parser (3)
129 Additionally, the CVC4 wiki contains useful information about the
130 design and internals of CVC4. It is maintained at
131 .BR http://cvc4.cs.stanford.edu/wiki/ .