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
|
This file contains a summary of important user-visible changes.
Changes since 1.3
=================
* Timed statistics are now properly updated even on process abort.
* The LFSC proof checker has been incorporated into CVC4 sources.
* By default, CVC4 builds in "production" mode (optimized, with fewer
internal checks on). The common alternative is a "debug" build, which
is much slower. CVC4 also builds with GPL dependences by default now
(if those libraries are available), as this is the best-performing
version of CVC4. However, the new configure option "--bsd" disables
these GPL dependences and builds the best-performing BSD-licenced version
of CVC4.
Changes since 1.2
=================
New features:
* SMT-LIB-compliant support for abs, to_real, to_int, is_int, which were
previously missing
* New bv2nat/int2bv operators for bitvector/integer inter-compatibility.
* Support in linear logics for /, div, and mod by constants (with the
--rewrite-divk command line option).
* Parsing support for TPTP's TFF and TFA formats.
* A new theory of strings: word (dis-)equations, length constraints,
regular expressions.
* Increased compliance to SMT-LIBv2, numerous bugs and usability issues
resolved.
* New :command-verbosity SMT option to silence success and error messages
on a per-command basis, and API changes to Command infrastructure to
support this.
Behavioral changes:
* It is no longer permitted to request model or proof generation if there's
been an intervening push/pop.
* User-defined symbols (define-funs) are no longer reported in the output
of get-model commands.
* Exit codes are now more standard for UNIX command-line tools. Exit code
zero means no error---but the result could be sat, unsat, or unknown---and
nonzero means error.
API changes:
* Expr::substitute() now capable of substituting operators (e.g.,
function symbols under an APPLY_UF)
* Numerous improvements to the Java language bindings
Changes since 1.1
=================
* Real arithmetic now has three simplex solvers for exact precision linear
arithmetic: the classical dual solver and two new solvers based on
techniques for minimizing the sum of infeasibilities. GLPK can now be used
as a heuristic backup to the exact precision solvers. GLPK must be enabled
at configure time. See --help for more information on enabling these solvers.
* added support for "bit0" and "bit1" bitvector constants in SMT-LIB v1.2
* support for theory "alternates": new ability to prototype new decision
procedures that are selectable at runtime
* various bugfixes
Changes since 1.0
=================
* bit-vector solver now has a specialized decision procedure for unsigned bit-
vector inequalities
* numerous important bug fixes, performance improvements, and usability
improvements
* support for multiline input in interactive mode
* Win32-building support via mingw
* SMT-LIB get-model output now is easier to machine-parse: contains (model...)
* user patterns for quantifier instantiation are now supported in the
SMT-LIBv1.2 parser
* --finite-model-find was incomplete when using --incremental, now fixed
* the E-matching procedure is slightly improved
* Boolean terms are now supported in datatypes
* tuple and record support have been added to the compatibility library
* driver verbosity change: for printing all commands as they're executed, you
now need verbosity level >= 3 (e.g., -vvv) instead of level 1 (-v). This
allows tracing the solver's activities (with -v and -vv) without having too
much output.
* to make CVC4 quieter in abnormal (e.g., "warning" conditions), you can
use -q. Previously, this would silence all output (including "sat" or
"unsat") as well. Now, single -q silences messages and warnings, and
double -qq silences all output (except on exception or signal).
-- Morgan Deters <mdeters@cs.nyu.edu> Thu, 05 Dec 2013 14:22:26 -0500
|
