-
Notifications
You must be signed in to change notification settings - Fork 0
/
NEWS
200 lines (180 loc) · 9.29 KB
/
NEWS
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
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
This file contains a summary of important user-visible changes.
Changes since 1.6
=================
New Features:
* Proofs:
* Support for bit-vector proofs with eager bitblasting (older versions only
supported proofs with lazy bitblasting).
* Strings:
* Support for `str.replaceall` operator.
* New option `--re-elim` to reduce regular expressions to extended string
operators, resulting in better performance on regular expression benchmarks
(enabled by default).
* SyGuS:
* Support for abduction (`--sygus-abduct`). Given a formula, this option uses
CVC4's SyGuS solver to find a sufficient condition such that the
conjunction of the condition and the formula is unsatisfiable.
* Support for two new term enumerator strategies: variable agnostic
(`--sygus-active-gen=var-agnostic`) and fast (`--sygus-active-gen=enum`).
By default, CVC4 tries to choose the best term enumerator strategy
automatically based on the input (`--sygus-active-gen=auto`).
* Support for streaming solutions of increasingly smaller size when using the
PBE solver (`--sygus-stream --sygus-pbe`). After the first solution is found
and printed, the solver will continue to look for new solutions and print
those, if any, that are smaller than previously printed solutions.
* Support for unification-based techniques in non-separable specifications
(`--sygus-unif`). For solving invariant problems a dedicate mode
(`--sygus-unif-boolean-heuristic-dt`) is available that builds candidate
solutions using heuristic decision tree learning.
Improvements:
* Strings:
* Significantly better performance on string benchmarks over the core theory
and those with extended string functions like substring, contains, and
replace.
Changes:
* API change: Expr::iffExpr() is renamed to Expr::eqExpr() to reflect its
actual behavior.
* Compiling the language bindings now requires SWIG 3 instead of SWIG 2.
* The CVC3 compatibility layer has been removed.
* The build system now uses CMake instead of Autotools. Please refer to
[INSTALL.md](https://github.com/CVC4/CVC4/blob/master/INSTALL.md) for
up-to-date instructions on how to build CVC4.
Changes since 1.5
=================
New Features:
* A new theory of floating points.
* Novel approach for solving quantified bit-vectors (BV).
* Eager bit-blasting: Support for SAT solver CaDiCaL.
* A new Gaussian Elimination preprocessing pass for the theory of bit-vectors.
* Support for transcendental functions (sin, cos, exp). In SMT2 input, this
can be enabled by adding T to the logic (e.g., QF_NRAT).
* Support for new operators in strings, including string inequality (str.<=)
and string code (str.code).
* Support for automated rewrite rule generation from sygus (*.sy) inputs using
syntax-guided enumeration (option --sygus-rr).
Improvements:
* Incremental unsat core support.
* Further development of rewrite rules for the theory of strings and regular
expressions.
* Many optimizations for syntax-guided synthesis, including improved symmetry
breaking for enumerative search and specialized algorithms for
programming-by-examples conjectures.
Changes:
* Eager bit-blasting: Removed support for SAT solver CryptoMinisat 4, added
support for CryptoMinisat 5.
* The LFSC proof checker now resides in its own repository on GitHub at
https://github.com/CVC4/LFSC. It is not distributed with CVC4 anymore.
Changes since 1.4
=================
* Improved heuristics for reasoning about non-linear arithmetic.
* Native support for syntax-guided synthesis (sygus).
* Support for many new heuristics for reasoning with quantifiers, including
finite model finding.
* Support for proofs for uninterpreted functions, arrays, bitvectors, and
their combinations.
* Performance improvements to existing theories.
* A new theory of sets with cardinality and relations.
* A new theory of strings.
* Support for unsat cores.
* Support for separation logic constraints.
* Simplification mode "incremental" no longer supported.
* Support for array constants in constraints.
* Syntax for array models has changed in some language front-ends.
* New input/output languages supported: "smt2.0" and "smtlib2.0" to
force SMT-LIB v2.0; "smt2.5" and "smtlib2.5" to force SMT-LIB v2.5;
"smt2.6" and "smtlib2.6" to force SMT-LIB v2.6;
"smt", "smtlib", "smt2", and "smtlib2" all refer to the current standard
version 2.6. If an :smt-lib-version is set in the input, that overrides
the command line.
* Abstract values in SMT-LIB models are now ascribed types (with "as").
* In SMT-LIB model output, real-sorted but integer-valued constants are
now printed in accordance with the standard (e.g. "1.0").
Changes since 1.3
=================
* CVC4 now supports libc++ in addition to libstdc++ (this especially
helps on Mac OS Mavericks).
* The LFSC proof checker has been incorporated into CVC4 sources.
* Theory of finite sets, handling the MLSS fragment (singleton, union,
intersection, set subtraction, membership and subset).
* By default, CVC4 builds in "production" mode (optimized, with fewer
internal checks on). The common alternative is a "debug" build, which
is much slower. By default, CVC4 builds with no GPL'ed dependences.
However, this is not the best-performing version; for that, you should
configure with "--enable-gpl --best", which links against GPL'ed
libraries that improve usability and performance. For details on
licensing and dependences, see the README file.
* Small API adjustments to Datatypes to even out the API and make it
function better in Java.
* Timed statistics are now properly updated even on process abort.
* Better automatic handling of output language setting when using CVC4
via API. Previously, the "automatic" language setting was sometimes
(though not always) defaulting to the internal "AST" language; it
should now (correctly) default to the same as the input language
(if the input language is supported as an output language), or the
"CVC4" native output language if no input language setting is applied.
* The SmtEngine cannot be safely copied with the copy constructor.
Previous versions inadvertently permitted clients to do this via the
API. This has been corrected, copy and assignment of the SmtEngine
is no longer permitted.
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).