diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-03-21 17:21:02 +0000 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-03-21 17:21:02 +0000 |
commit | 91f9355868d01999fd729544ea50ccd745e84d35 (patch) | |
tree | e0c2eec04e631fb56dba59afdbb8ada8ad5b6cef /NEWS | |
parent | 7dfd55085c60affdc4523c330ea2d2daa69ae66a (diff) |
Add more NEWS (#2859)
Diffstat (limited to 'NEWS')
-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 |