NEWS

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.