cvc4(1) - f36

1CVC4(1)                          User Manuals                          CVC4(1)
2
3
4

NAME

6       cvc4, pcvc4 - an automated theorem prover
7

SYNOPSIS

9       cvc4 [ options ] [ file ]
10
11       pcvc4 [ options ] [ file ]
12

DESCRIPTION

14       cvc4  is  an automated theorem prover for first-order formulas with re‐
15       spect to background theories of interest.  pcvc4 is CVC4's  "portfolio"
16       variant,  which is capable of running multiple CVC4 instances in paral‐
17       lel, configured differently.
18
19       With file , commands are read from file and  executed.   CVC4  supports
20       the SMT-LIB (versions 1.2 and 2.0) input format, as well as its own na‐
21       tive “presentation language” (see cvc4(5) ), which is similar  in  many
22       respects to CVC3's presentation language, but not identical.
23
24       If  file is unspecified, standard input is read (and the CVC4 presenta‐
25       tion language is assumed).  If file is unspecified  and  CVC4  is  con‐
26       nected to a terminal, interactive mode is assumed.
27
28

COMMON OPTIONS

30       Each  option  marked  with [*] has a --no-OPTIONNAME variant, which re‐
31       verses the sense of the option.
32
33              $
34
35              $
36
37
38       Each option marked with [*] has a --no-OPTIONNAME  variant,  which  re‐
39       verses the sense of the option.
40
41

DIAGNOSTICS

43       CVC4 reports all syntactic and semantic errors on standard error.
44

HISTORY

46       The  CVC4 effort is the culmination of fifteen years of theorem proving
47       research, starting with the Stanford Validity Checker (SVC) in 1996.
48
49       SVC's successor, the Cooperating Validity Checker (CVC), had a more op‐
50       timized  internal  design,  produced proofs, used the Chaff SAT solver,
51       and featured a number of usability enhancements.  Its name  comes  from
52       the  cooperative  nature  of decision procedures in Nelson-Oppen theory
53       combination, which share amongst each other equalities  between  shared
54       terms.
55
56       CVC  Lite,  first made available in 2003, was a rewrite of CVC that at‐
57       tempted to make CVC more flexible (hence the  “lite”)  while  extending
58       the  feature  set: CVCLite supported quantifiers where its predecessors
59       did not.  CVC3 was a major overhaul of portions of CVC Lite:  it  added
60       better decision procedure implementations, added support for using Min‐
61       iSat in the core, and had generally better performance.
62
63       CVC4 is the new version, the fifth generation of this validity  checker
64       line  that is now celebrating fifteen years of heritage.  It represents
65       a complete re-evaluation of the core architecture to be both performant
66       and  to  serve  as a cutting-edge research vehicle for the next several
67       years.  Rather than taking CVC3 and redesigning  problem  parts,  we've
68       taken  a  clean-room approach, starting from scratch.  Before using any
69       designs from CVC3, we have thoroughly scrutinized, vetted, and  updated
70       them.   Many parts of CVC4 bear only a superficial resemblance, if any,
71       to their correspondent in CVC3.
72
73       However, CVC4 is fundamentally similar to CVC3 and  many  other  modern
74       SMT  solvers:  it  is a DPLL( T ) solver, with a SAT solver at its core
75       and a delegation path to different decision procedure  implementations,
76       each in charge of solving formulas in some background theory.
77
78       The  re-evaluation  and ground-up rewrite was necessitated, we felt, by
79       the performance characteristics of CVC3.  CVC3  has  many  useful  fea‐
80       tures,  but some core aspects of the design led to high memory use, and
81       the use of heavyweight computation (where more nimble  engineering  ap‐
82       proaches  could  suffice)  makes  CVC3  a much slower prover than other
83       tools.  As these designs are central to CVC3, a new version was prefer‐
84       able to a selective re-engineering, which would have ballooned in short
85       order.
86

VERSION

88       This manual page refers to CVC4 version CVC4_RELEASE_STRING.
89

BUGS

91       An  issue   tracker   for   the   CVC4   project   is   maintained   at
92       https://github.com/CVC4/CVC4/issues.
93

AUTHORS

95       CVC4  is  developed by a team of researchers at Stanford University and
96       the University of Iowa.  See the AUTHORS file in the distribution for a
97       full list of contributors.
98