Eliminate equality query dependence on quantifiers engine (#5831)

[cvc5.git] / NEWS

diff --git a/NEWS b/NEWS
index 60ff9dbc8e8fda5f42e6f9082247d026f0fdebe8..d915ef44fa010782482da4a431bc7e9f5d16e79c 100644 (file)
--- a/NEWS
+++ b/NEWS
@@ -1,5 +1,44 @@
 This file contains a summary of important user-visible changes.
 
+Changes since 1.8
+=================
+
+New Features:
+* 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`.
+* Support for an integer operator `(_ iand n)` that returns the bitwise `and`
+  of two integers, seen as integers modulo n.
+
+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 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).
+  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.
+
+
 Changes since 1.7
 =================