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`.
-* Support for an integer operator `(_ iand n)` that returns the bitwise `and`
- of two integers, seen as integers modulo n.
+* 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
Changes:
* SyGuS: Removed support for SyGuS-IF 1.0.
-* Removed Java and Python bindings for the legacy API
+* 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
projects / cvc5.git / blobdiff