diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-06-25 13:51:11 -0700 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2018-06-25 14:11:54 -0700 |
commit | 14b9dbaa0c9e8dce52d1a28595dc1cc80756abed (patch) | |
tree | 0bb73ac56ff0e92d71152409aa0d3acd9547e235 /NEWS | |
parent | 8805781adbfb3f57c4765307c82267b1fabdf2b4 (diff) |
Update AUTHORS, NEWS, README, RELEASE-NOTES and THANKS file for 1.6.
Diffstat (limited to 'NEWS')
-rw-r--r-- | NEWS | 29 |
1 files changed, 29 insertions, 0 deletions
@@ -1,5 +1,34 @@ This file contains a summary of important user-visible changes. +Changes since 1.5 +================= + +New Features: +* A new theory of floating points. +* Novel approach for solving quantified bit-vectors (BV). +* Eager bit-blasting: Support for SAT solver CaDiCaL. +* A new Gaussian Elimination preprocessing pass for the theory of bit-vectors. +* Support for transcendental functions (sin, cos, exp). +* Support for new operators in strings, including string inequality (str.<=) + and string code (str.code). +* Support for automated rewrite rule generation from sygus (*.sy) inputs using + syntax-guided enumeration (option --sygus-rr). + +Improvements: +* Incremental unsat core support. +* Strings rewriter. +* Further development of rewrite rules for the theory of strings and regular + expressions. +* Many optimizations for syntax-guided synthesis, including improved symmetry + breaking for enumerative search and specialized algorithms for + programming-by-examples conjectures. + +Changes: +* Eager bit-blasting: Removed support for SAT solver CryptoMinisat 4, added + support for CryptoMinisat 5. +* The LFSC proof checker now resides in its own repository on GitHub at + https://github.com/CVC4/LFSC. It is not distributed with CVC4 anymore. + Changes since 1.4 ================= |