1 This file contains a summary of important user-visible changes.
8 * New unsat-core production modes based on the new proof infrastructure
9 (`--unsat-cores-mode=sat-proof`) and on the solving-under-assumption feature
10 of Minisat (`--unsat-cores-mode=assumptions`). The mode based on SAT
11 assumptions + preprocessing proofs is the new default.
12 * A new parametric theory of sequences whose syntax is compatible with the
13 syntax for sequences used by Z3.
14 * Arrays: Added support for an `eqrange` predicate. `(eqrange a b i j)` is true
15 if arrays `a` and `b` are equal on all indices within indices `i` and `j`.
16 * Support for an integer operator `(_ iand n)` that returns the bitwise `and`
17 of two integers, seen as integers modulo n.
20 * New API: Added functions to retrieve the heap/nil term when using separation
24 * SyGuS: Removed support for SyGuS-IF 1.0.
25 * Removed Java and Python bindings for the legacy API
26 * Interactive shell: the GPL-licensed Readline library has been replaced the
27 BSD-licensed Editline. Compiling with `--best` now enables Editline, instead
28 of Readline. Without selecting optional GPL components, Editline-enabled CVC4
29 builds will be BSD licensed.
30 * The semantics for division and remainder operators in the CVC language now
31 correspond to SMT-LIB 2.6 semantics (i.e. a division by zero or a zero
32 modulus results in a constant value, instead of an uninterpreted one).
33 Similarly, when no language is set, the API semantics now correspond to the
34 SMT-LIB 2.6 semantics.
35 * The `competition` build type includes the dependencies used for SMT-COMP by
36 default. Note that this makes this build type produce GPL-licensed binaries.
37 * Bit-vector operator bvxnor was previously mistakenly marked as
38 left-assoicative in SMT-LIB. This has recently been corrected in SMT-LIB. We
39 now restrict bvxnor to only allow two operands in order to avoid confusion
40 about the semantics, since the behavior of n-ary operands to bvxnor is now
42 * SMT-LIB output for `get-model` command now conforms with the standard,
43 and does *not* begin with the keyword `model`. The output
44 is the same as before, only with this word removed from the beginning.
45 * Building with Python 2 is now deprecated.
52 * New C++ and Python API: CVC4 has a new, more streamlined API. We plan to
53 make CVC4 1.8 the last version that ships with the legacy API.
54 * Strings: Full support of the new SMT-LIB standard for the theory of strings,
56 * Support for `str.replace_re`, `str.replace_re_all`, `str.is_digit`,
57 `str.from_code`, `re.diff`, and `re.comp`
58 * Support for new operator names (e.g. `str.in_re` instead of `str.in.re`),
59 new escape sequences. The new syntax is enabled by default for smt2 files.
60 * Support for syntax-guided synthesis (SyGuS) problems in the new API. C++
61 examples of the SyGuS API can be found in `./examples/api/sygus_*.cpp`.
62 * Support for higher-order constraints. This includes treating function sorts
63 (constructible by `->`) as first-class sorts and handling partially applied
64 function symbols. Support for higher-order constraints can be enabled by
66 * Support for set comprehension binders `comprehension`.
67 * Eager bit-blasting: Support for SAT solver Kissat.
70 * API: Function definitions can now be requested to be global. If the `global`
71 parameter is set to true, they persist after popping the user context.
72 * Java/Python bindings: The bindings now allow users to catch exceptions
73 * Arithmetic: Performance improvements
74 * Linear solver: New lemmas inspired by unit-cube tests
75 * Non-linear solver: Expanded set of axioms
76 * Ackermannization: The Ackermannization preprocessing pass now supports
77 uninterpreted sorts and as a result all QF_UFBV problems are supported in
78 combination with eager bit blasting.
81 * CVC language: Models printed in the CVC language now include an explicit end
82 marker to facilitate the communication over pipes with CVC4.
83 * API change: `SmtEngine::query()` has been renamed to
84 `SmtEngine::checkEntailed()` and `Result::Validity` has been renamed to
85 `Result::Entailment` along with corresponding changes to the enum values.
86 * Java API change: The name of CVC4's package is now `edu.stanford.CVC4`
87 instead of `edu.nyu.acsys.CVC4`.
88 * The default output language is changed from CVC to SMT-LIB 2.6. The
89 default output language is used when the problem language cannot be
90 easily inferred (for example when CVC4 is used from the API).
91 * Printing of BV constants: previously CVC4 would print BV constant
92 values as indexed symbols by default and in binary notation with the
93 option --bv-print-consts-in-binary. To be SMT-LIB compliant the
94 default behavior is now to print BV constant values in binary
95 notation and as indexed symbols with the new option
96 --bv-print-consts-as-indexed-symbols. The option
97 --bv-print-consts-in-binary has been removed.
98 * Updated to SyGuS language version 2.0 by default. This is the last release
99 that will support the SyGuS language version 1.0 (`--lang=sygus1`). A
100 script is provided to convert version 1.0 files to version 2.0, see
101 `./contrib/sygus-v1-to-v2.sh`.
102 * Support for user-provided rewrite rule quantifiers have been removed.
103 * Support for certain option aliases have been removed.
104 * Support for parallel portfolio builds has been removed.
111 * Support for bit-vector proofs with eager bitblasting (older versions only
112 supported proofs with lazy bitblasting).
114 * Support for `str.replaceall` operator.
115 * New option `--re-elim` to reduce regular expressions to extended string
116 operators, resulting in better performance on regular expression benchmarks
117 (enabled by default).
119 * Support for abduction (`--sygus-abduct`). Given a formula, this option uses
120 CVC4's SyGuS solver to find a sufficient condition such that the
121 conjunction of the condition and the formula is unsatisfiable.
122 * Support for two new term enumerator strategies: variable agnostic
123 (`--sygus-active-gen=var-agnostic`) and fast (`--sygus-active-gen=enum`).
124 By default, CVC4 tries to choose the best term enumerator strategy
125 automatically based on the input (`--sygus-active-gen=auto`).
126 * Support for streaming solutions of increasingly smaller size when using the
127 PBE solver (`--sygus-stream --sygus-pbe`). After the first solution is found
128 and printed, the solver will continue to look for new solutions and print
129 those, if any, that are smaller than previously printed solutions.
130 * Support for unification-based techniques in non-separable specifications
131 (`--sygus-unif`). For solving invariant problems a dedicate mode
132 (`--sygus-unif-boolean-heuristic-dt`) is available that builds candidate
133 solutions using heuristic decision tree learning.
137 * Significantly better performance on string benchmarks over the core theory
138 and those with extended string functions like substring, contains, and
142 * API change: Expr::iffExpr() is renamed to Expr::eqExpr() to reflect its
144 * Compiling the language bindings now requires SWIG 3 instead of SWIG 2.
145 * The CVC3 compatibility layer has been removed.
146 * The build system now uses CMake instead of Autotools. Please refer to
147 [INSTALL.md](https://github.com/CVC4/CVC4/blob/master/INSTALL.md) for
148 up-to-date instructions on how to build CVC4.
154 * A new theory of floating points.
155 * Novel approach for solving quantified bit-vectors (BV).
156 * Eager bit-blasting: Support for SAT solver CaDiCaL.
157 * A new Gaussian Elimination preprocessing pass for the theory of bit-vectors.
158 * Support for transcendental functions (sin, cos, exp). In SMT2 input, this
159 can be enabled by adding T to the logic (e.g., QF_NRAT).
160 * Support for new operators in strings, including string inequality (str.<=)
161 and string code (str.code).
162 * Support for automated rewrite rule generation from sygus (*.sy) inputs using
163 syntax-guided enumeration (option --sygus-rr).
166 * Incremental unsat core support.
167 * Further development of rewrite rules for the theory of strings and regular
169 * Many optimizations for syntax-guided synthesis, including improved symmetry
170 breaking for enumerative search and specialized algorithms for
171 programming-by-examples conjectures.
174 * Eager bit-blasting: Removed support for SAT solver CryptoMinisat 4, added
175 support for CryptoMinisat 5.
176 * The LFSC proof checker now resides in its own repository on GitHub at
177 https://github.com/CVC4/LFSC. It is not distributed with CVC4 anymore.
182 * Improved heuristics for reasoning about non-linear arithmetic.
183 * Native support for syntax-guided synthesis (sygus).
184 * Support for many new heuristics for reasoning with quantifiers, including
185 finite model finding.
186 * Support for proofs for uninterpreted functions, arrays, bitvectors, and
188 * Performance improvements to existing theories.
189 * A new theory of sets with cardinality and relations.
190 * A new theory of strings.
191 * Support for unsat cores.
192 * Support for separation logic constraints.
193 * Simplification mode "incremental" no longer supported.
194 * Support for array constants in constraints.
195 * Syntax for array models has changed in some language front-ends.
196 * New input/output languages supported: "smt2.0" and "smtlib2.0" to
197 force SMT-LIB v2.0; "smt2.5" and "smtlib2.5" to force SMT-LIB v2.5;
198 "smt2.6" and "smtlib2.6" to force SMT-LIB v2.6;
199 "smt", "smtlib", "smt2", and "smtlib2" all refer to the current standard
200 version 2.6. If an :smt-lib-version is set in the input, that overrides
202 * Abstract values in SMT-LIB models are now ascribed types (with "as").
203 * In SMT-LIB model output, real-sorted but integer-valued constants are
204 now printed in accordance with the standard (e.g. "1.0").
209 * CVC4 now supports libc++ in addition to libstdc++ (this especially
210 helps on Mac OS Mavericks).
211 * The LFSC proof checker has been incorporated into CVC4 sources.
212 * Theory of finite sets, handling the MLSS fragment (singleton, union,
213 intersection, set subtraction, membership and subset).
214 * By default, CVC4 builds in "production" mode (optimized, with fewer
215 internal checks on). The common alternative is a "debug" build, which
216 is much slower. By default, CVC4 builds with no GPL'ed dependences.
217 However, this is not the best-performing version; for that, you should
218 configure with "--enable-gpl --best", which links against GPL'ed
219 libraries that improve usability and performance. For details on
220 licensing and dependences, see the README file.
221 * Small API adjustments to Datatypes to even out the API and make it
222 function better in Java.
223 * Timed statistics are now properly updated even on process abort.
224 * Better automatic handling of output language setting when using CVC4
225 via API. Previously, the "automatic" language setting was sometimes
226 (though not always) defaulting to the internal "AST" language; it
227 should now (correctly) default to the same as the input language
228 (if the input language is supported as an output language), or the
229 "CVC4" native output language if no input language setting is applied.
230 * The SmtEngine cannot be safely copied with the copy constructor.
231 Previous versions inadvertently permitted clients to do this via the
232 API. This has been corrected, copy and assignment of the SmtEngine
233 is no longer permitted.
239 * SMT-LIB-compliant support for abs, to_real, to_int, is_int, which were
241 * New bv2nat/int2bv operators for bitvector/integer inter-compatibility.
242 * Support in linear logics for /, div, and mod by constants (with the
243 --rewrite-divk command line option).
244 * Parsing support for TPTP's TFF and TFA formats.
245 * A new theory of strings: word (dis-)equations, length constraints,
247 * Increased compliance to SMT-LIBv2, numerous bugs and usability issues
249 * New :command-verbosity SMT option to silence success and error messages
250 on a per-command basis, and API changes to Command infrastructure to
254 * It is no longer permitted to request model or proof generation if there's
255 been an intervening push/pop.
256 * User-defined symbols (define-funs) are no longer reported in the output
257 of get-model commands.
258 * Exit codes are now more standard for UNIX command-line tools. Exit code
259 zero means no error---but the result could be sat, unsat, or unknown---and
263 * Expr::substitute() now capable of substituting operators (e.g.,
264 function symbols under an APPLY_UF)
265 * Numerous improvements to the Java language bindings
270 * Real arithmetic now has three simplex solvers for exact precision linear
271 arithmetic: the classical dual solver and two new solvers based on
272 techniques for minimizing the sum of infeasibilities. GLPK can now be used
273 as a heuristic backup to the exact precision solvers. GLPK must be enabled
274 at configure time. See --help for more information on enabling these solvers.
275 * added support for "bit0" and "bit1" bitvector constants in SMT-LIB v1.2
276 * support for theory "alternates": new ability to prototype new decision
277 procedures that are selectable at runtime
283 * bit-vector solver now has a specialized decision procedure for unsigned bit-
285 * numerous important bug fixes, performance improvements, and usability
287 * support for multiline input in interactive mode
288 * Win32-building support via mingw
289 * SMT-LIB get-model output now is easier to machine-parse: contains (model...)
290 * user patterns for quantifier instantiation are now supported in the
292 * --finite-model-find was incomplete when using --incremental, now fixed
293 * the E-matching procedure is slightly improved
294 * Boolean terms are now supported in datatypes
295 * tuple and record support have been added to the compatibility library
296 * driver verbosity change: for printing all commands as they're executed, you
297 now need verbosity level >= 3 (e.g., -vvv) instead of level 1 (-v). This
298 allows tracing the solver's activities (with -v and -vv) without having too
300 * to make CVC4 quieter in abnormal (e.g., "warning" conditions), you can
301 use -q. Previously, this would silence all output (including "sat" or
302 "unsat") as well. Now, single -q silences messages and warnings, and
303 double -qq silences all output (except on exception or signal).