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
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
|
Release Notes for CVC4 1.0, October 2012
** Getting started
If you run CVC4 without arguments, you will find yourself in an interactive
CVC4 session, which expects commands in CVC4's native language (the so-called
"presentation" language). To use SMT-LIB, use the "--lang smt" option on the
command line. For stricter adherence to the standard, use "--smtlib"
(see below regarding SMT-LIB compliance).
When a filename is given on the command line, the file's extension determines
the language parser that's used (e.g., file.smt is SMT-LIB 1.2, file.smt2
is SMT-LIB 2.0, and file.cvc is the presentation language). To override
this, you can use the --lang option.
** Type correctness
Type Correctness Conditions (TCCs), and the checking of such, are not
supported by CVC4 1.0. Thus, a function defined only on integers can be
applied to REAL (as INT is a subtype of REAL), and CVC4 will not complain,
but may produce strange results. For example:
f : INT -> INT;
ASSERT f(1/3) = 0;
ASSERT f(2/3) = 1;
CHECKSAT;
% sat
COUNTEREXAMPLE;
% f : (INT) -> INT = LAMBDA(x1:INT) : 0;
CVC3 can be used to produce TCCs for this input (with the +dump-tcc option).
The TCC can be checked by CVC3 or another solver. (CVC3 can also check
TCCs while solving with +tcc.)
** Changes in CVC's Presentation Language
The native language of all solvers in the CVC family, referred to as the
"presentation language," has undergone some revisions for CVC4. The
most notable is that CVC4 does _not_ add counterexample assertions to
the current assertion set after a SAT/INVALID result. For example:
x, y : INT;
ASSERT x = 1 OR x = 2;
ASSERT y = 1 OR y = 2;
ASSERT x /= y;
CHECKSAT;
% sat
QUERY x = 1;
% invalid
QUERY x = 2;
% invalid
Here, CVC4 responds "invalid" to the second and third queries, because
each has a counterexample (x=2 is a counterexample to the first, and
x=1 is a counterexample to the second). However, CVC3 will respond
with "valid" to one of these two, as the first query (the CHECKSAT)
had the side-effect of locking CVC3 into one of the two cases; the
later queries are effectively querying the counterexample that was
found by the first. CVC4 removes this side-effect of the CHECKSAT and
QUERY commands.
CVC4 supports rational literals (of type REAL) in decimal; CVC3 did not
support decimals.
CVC4 does not have support for the IS_INTEGER predicate, or for predicate
subtypes, although these are planned for future releases.
** SMT-LIB compliance
Every effort has been made to make CVC4 compliant with the SMT-LIB 2.0
standard (http://smtlib.org/). However, when parsing SMT-LIB input,
certain default settings don't match what is stated in the official
standard. To make CVC4 adhere more strictly to the standard, use the
"--smtlib" command-line option. Even with this setting, CVC4 is
somewhat lenient; some non-conforming input may still be parsed and
processed.
For the latest news on SMT-LIB compliance, please check:
http://church.cims.nyu.edu/wiki/SMT-LIB_Compliance
However, please note that that page may refer to a more recent version
(and possibly an unreleased, development version) than the one you are
looking at.
** Getting statistics
Statistics can be dumped on exit (both normal and abnormal exits) with
the --statistics command line option.
** Time and resource limits
CVC4 can be made to self-timeout after a given number of milliseconds.
Use the --tlimit command line option to limit the entire run of
CVC4, or use --tlimit-per to limit each individual query separately.
Preprocessing time is not counted by the time limit, so for some large
inputs which require aggressive preprocessing, you may notice that
--tlimit does not work very well. If you suspect this might be the
case, you can use "-vv" (double verbosity) to see what CVC4 is doing.
Time-limited runs are not deterministic; two consecutive runs with the
same time limit might produce different results (i.e., one may time out
and responds with "unknown", while the other completes and provides an
answer). To ensure that results are reproducible, use --rlimit or
--rlimit-per. These options take a "resource count" (presently, based on
the number of SAT conflicts) that limits the search time. A word of
caution, though: there is no guarantee that runs of different versions of
CVC4 or of different builds of CVC4 (e.g., two CVC4 binaries with different
features enabled, or for different architectures) will interpret the resource
count in the same manner.
CVC4 does not presently have a way to limit its memory use; you may opt
to run it from a shell after using "ulimit" to limit the size of the
heap.
** Proof support
CVC4 1.0 has limited support for proofs, and they are disabled by default.
(Run the configure script with --enable-proof to enable proofs). Proofs
are exported in LFSC format and are limited to the propositional backbone
of the discovered proof (theory lemmas are stated without proof in this
release).
** Nonlinear arithmetic
CVC4 1.0 has a state-of-the-art linear arithmetic solver. However, there
is extremely limited support for nonlinear arithmetic in this release.
** Portfolio solving
If enabled at configure-time (./configure --with-portfolio), a second
CVC4 binary will be produced ("pcvc4"). This binary has support for
running multiple instances of CVC4 in different threads. Use --threads=N
to specify the number of threads, and use --thread0="options for thread 0"
--thread1="options for thread 1", etc., to specify a configuration for the
threads. Lemmas are *not* shared between the threads by default; to adjust
this, use the --filter-lemma-length=N option to share lemmas of N literals
(or smaller). (Some lemmas are ineligible for sharing because they include
literals that are "local" to one thread.)
Currently, the portfolio **does not work** with quantifiers or with
the theory of inductive datatypes. These limitations will be addressed
in a future release.
** Questions ??
CVC4 and its predecessors have an active user base. You might want to
subscribe to the mailing list (http://cs.nyu.edu/mailman/listinfo/cvc-users)
and post a question there.
** Reporting bugs and making feature requests
CVC4 is under active development. Should you find a bug in CVC4's
documentation, behavior, API, or SMT-LIB compliance, or if you have
a feature request, please let us know on our bugtracker at
http://church.cims.nyu.edu/bugs/
or send an email to cvc-bugs@cims.nyu.edu.
|
