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
|
This is CVC4 release version 1.0. For build and installation notes,
please see the INSTALL file included with this distribution.
This first official release of CVC4 is the result of more than three
years of efforts by researchers at New York University and the
University of Iowa. The project leaders are Clark Barrett (New York
University) and Cesare Tinelli (University of Iowa). For a full list
of authors, please refer to the AUTHORS file in the source
distribution.
CVC4 is a tool for determining the satisfiability of a first order
formula modulo a first order theory (or a combination of such
theories). It is the fourth in the Cooperating Validity Checker family
of tools (CVC, CVC Lite, CVC3) but does not directly incorporate code
from any previous version.
CVC4 is intended to be an open and extensible SMT engine. It can be
used as a stand-alone tool or as a library. It has been designed to
increase the performance and reduce the memory overhead of its
predecessors. It is written entirely in C++ and is released under a
free software license (see the file COPYING in the source
distribution).
*** Getting started with CVC4
For help installing CVC4, see the INSTALL file that comes with this
distribution.
We recommend that you visit our CVC4 tutorials online at:
http://cvc4.cs.nyu.edu/wiki/Tutorials
for help getting started using CVC4.
*** The History of CVC4
The Cooperating Validity Checker series has a long history. The
Stanford Validity Checker (SVC) came first in 1996, incorporating
theories and its own SAT solver. Its 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: CVC
Lite 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 sixteen 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. Some specific deficiencies of CVC3 are mentioned in
this article.
*** For more information
More information about CVC4 is available at: http://cs.nyu.edu/acsys/cvc4
|
