From: Andres Noetzli Date: Thu, 21 Mar 2019 17:21:02 +0000 (+0000) Subject: Add more NEWS (#2859) X-Git-Tag: cvc5-1.0.0~4229 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=91f9355868d01999fd729544ea50ccd745e84d35;p=cvc5.git Add more NEWS (#2859) --- diff --git a/NEWS b/NEWS index f36460a27..7a7c9ba29 100644 --- a/NEWS +++ b/NEWS @@ -4,9 +4,28 @@ Changes since 1.6 ================= New Features: -* Strings: Support for `str.replaceall` operator. +* Proofs: + * Support for bit-vector proofs with eager bitblasting (older versions only + supported proofs with lazy bitblasting). +* Strings: + * Support for `str.replaceall` operator. + * New option `--re-elim` to reduce regular expressions to extended string + operators, resulting in better performance on regular expression benchmarks + (enabled by default). +* SyGuS: + * Support for abduction (`--sygus-abduct`). Given a formula, this option uses + CVC4's SyGuS solver to find a sufficient condition such that the + conjunction of the condition and the formula is unsatisfiable. + * Support for two new term enumerator strategies: variable agnostic + (`--sygus-active-gen=var-agnostic`) and fast (`--sygus-active-gen=enum`). + By default, CVC4 tries to choose the best term enumerator strategy + automatically based on the input (`--sygus-active-gen=auto`). Improvements: +* Strings: + * Significantly better performance on string benchmarks over the core theory + and those with extended string functions like substring, contains, and + replace. Changes: * API change: Expr::iffExpr() is renamed to Expr::eqExpr() to reflect its @@ -14,7 +33,7 @@ Changes: * Compiling the language bindings now requires SWIG 3 instead of SWIG 2. * The CVC3 compatibility layer has been removed. * The build system now uses CMake instead of Autotools. Please refer to -* [INSTALL.md](https://github.com/CVC4/CVC4/blob/master/INSTALL.md) for + [INSTALL.md](https://github.com/CVC4/CVC4/blob/master/INSTALL.md) for up-to-date instructions on how to build CVC4. Changes since 1.5