NEWS

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