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
=================
New Features:
+* New C++ and Python API: CVC4 has a new, more streamlined API. We plan to
+ make CVC4 1.8 the last version that ships with the legacy API.
* Strings: Full support of the new SMT-LIB standard for the theory of strings,
including:
* Support for `str.replace_re`, `str.replace_re_all`, `str.is_digit`,
`str.from_code`, `re.diff`, and `re.comp`
* Support for new operator names (e.g. `str.in_re` instead of `str.in.re`),
new escape sequences. The new syntax is enabled by default for smt2 files.
+* Support for syntax-guided synthesis (SyGuS) problems in the new API. C++
+ examples of the SyGuS API can be found in `./examples/api/sygus_*.cpp`.
+* Support for higher-order constraints. This includes treating function sorts
+ (constructible by `->`) as first-class sorts and handling partially applied
+ function symbols. Support for higher-order constraints can be enabled by
+ the option `--uf-ho`.
+* Support for set comprehension binders `comprehension`.
+* Eager bit-blasting: Support for SAT solver Kissat.
Improvements:
* API: Function definitions can now be requested to be global. If the `global`
parameter is set to true, they persist after popping the user context.
+* Java/Python bindings: The bindings now allow users to catch exceptions
+* Arithmetic: Performance improvements
+ * Linear solver: New lemmas inspired by unit-cube tests
+ * Non-linear solver: Expanded set of axioms
+* Ackermannization: The Ackermannization preprocessing pass now supports
+ uninterpreted sorts and as a result all QF_UFBV problems are supported in
+ combination with eager bit blasting.
Changes:
+* CVC language: Models printed in the CVC language now include an explicit end
+ marker to facilitate the communication over pipes with CVC4.
* API change: `SmtEngine::query()` has been renamed to
`SmtEngine::checkEntailed()` and `Result::Validity` has been renamed to
`Result::Entailment` along with corresponding changes to the enum values.
notation and as indexed symbols with the new option
--bv-print-consts-as-indexed-symbols. The option
--bv-print-consts-in-binary has been removed.
+* Updated to SyGuS language version 2.0 by default. This is the last release
+ that will support the SyGuS language version 1.0 (`--lang=sygus1`). A
+ script is provided to convert version 1.0 files to version 2.0, see
+ `./contrib/sygus-v1-to-v2.sh`.
+* Support for user-provided rewrite rule quantifiers have been removed.
+* Support for certain option aliases have been removed.
+* Support for parallel portfolio builds has been removed.
Changes since 1.6
=================
projects / cvc5.git / blobdiff