diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-06-19 09:59:27 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-19 09:59:27 -0700 |
commit | 5247901077efbc7b9016ba35fded7a6ab459a379 (patch) | |
tree | b0ffb77db20ef3cb5fde3210dbd866f3f5536063 /NEWS | |
parent | 039a642610f570f3367a73a3a29082152a2736f2 (diff) |
Update info for 1.8 release (#4633)
Diffstat (limited to 'NEWS')
-rw-r--r-- | NEWS | 13 |
1 files changed, 13 insertions, 0 deletions
@@ -4,6 +4,8 @@ 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`, @@ -17,12 +19,22 @@ New Features: 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. @@ -44,6 +56,7 @@ Changes: `./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 ================= |