diff options
-rw-r--r-- | NEWS | 23 |
1 files changed, 21 insertions, 2 deletions
@@ -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 |