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
|
This file contains a summary of important user-visible changes.
Changes since CVC4 1.8
======================
New Features:
* CaDiCaL is now a required dependency.
* SymFPU is now a required dependency.
* New unsat-core production modes based on the new proof infrastructure
(`--unsat-cores-mode=sat-proof`) and on the solving-under-assumption feature
of Minisat (`--unsat-cores-mode=assumptions`). The mode based on SAT
assumptions + preprocessing proofs is the new default.
* A new parametric theory of sequences whose syntax is compatible with the
syntax for sequences used by Z3.
* Arrays: Added support for an `eqrange` predicate. `(eqrange a b i j)` is true
if arrays `a` and `b` are equal on all indices within indices `i` and `j`.
* Integers:
* Support for an integer operator `(_ iand n)` that returns the bitwise `and`
of two integers, seen as integers modulo n.
* Support for an integer operator `int.pow2`, used as `(int.pow2 x)` which
represents 2 to the power of x.
* Strings:
* Support for `str.indexof_re(s, r, n)`, which returns the index of the first
occurrence of a regular expression `r` in a string `s` after index `n` or
-1 if `r` does not match a substring after `n`.
* A new option to compute minimal unsat cores (`--minimal-unsat-cores`).
Improvements:
* New API: Added functions to retrieve the heap/nil term when using separation
logic.
Changes:
* SyGuS: Removed support for SyGuS-IF 1.0.
* Removed support for the (non-standard) `define` command.
* Removed Java and Python bindings for the legacy API.
* Interactive shell: the GPL-licensed Readline library has been replaced the
BSD-licensed Editline. Compiling with `--best` now enables Editline, instead
of Readline. Without selecting optional GPL components, Editline-enabled CVC4
builds will be BSD licensed.
* The semantics for division and remainder operators in the CVC language now
correspond to SMT-LIB 2.6 semantics (i.e. a division by zero or a zero
modulus results in a constant value, instead of an uninterpreted one). As a
result the option `--bv-div-zero-const` has been removed. Similarly, when no
language is set, the API semantics now correspond to the SMT-LIB 2.6
semantics.
* The `competition` build type includes the dependencies used for SMT-COMP by
default. Note that this makes this build type produce GPL-licensed binaries.
* Bit-vector operator bvxnor was previously mistakenly marked as
left-assoicative in SMT-LIB. This has recently been corrected in SMT-LIB. We
now restrict bvxnor to only allow two operands in order to avoid confusion
about the semantics, since the behavior of n-ary operands to bvxnor is now
undefined in SMT-LIB.
* SMT-LIB output for `get-model` command now conforms with the standard,
and does *not* begin with the keyword `model`. The output
is the same as before, only with this word removed from the beginning.
* Building with Python 2 is now deprecated.
* Removed the option `--rewrite-divk` (now effectively enabled by default).
* Removed support for redundant logics ALL_SUPPORTED and QF_ALL_SUPPORTED,
use ALL and QF_ALL instead.
|
