Skip to content

Commit

Permalink
More updates to NEWS for 1.6.
Browse files Browse the repository at this point in the history
  • Loading branch information
aniemetz committed Jun 25, 2018
1 parent 14b9dba commit 6ded58d
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions NEWS
Original file line number Diff line number Diff line change
Expand Up @@ -8,15 +8,15 @@ New Features:
* 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 transcendental functions (sin, cos, exp). In SMT2 input, this
can be enabled by adding T to the logic (e.g., QF_NRAT).
* 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
Expand Down

0 comments on commit 6ded58d

Please sign in to comment.