1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
|
.\" 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."
${common_manpage_documentation}
${remaining_manpage_documentation}
.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
A Bugzilla for the CVC4 project is maintained at
.BR http://goedel.cs.nyu.edu/bugzilla3/ .
.SH AUTHORS
.B CVC4
is developed by a team of researchers at New York 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),
.BR libcvc4compat (3)
Additionally, the CVC4 wiki contains useful information about the
design and internals of CVC4. It is maintained at
.BR http://goedel.cs.nyu.edu/wiki/ .
|
