From: Andrew Reynolds Date: Tue, 16 Jun 2020 23:51:10 +0000 (-0500) Subject: Updates to NEWS. (#4628) X-Git-Tag: cvc5-1.0.0~3207 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2e4d33f5ec1b097075fe0ad334e4f4f354e30679;p=cvc5.git Updates to NEWS. (#4628) --- diff --git a/NEWS b/NEWS index 8c6ec7bc9..d77854008 100644 --- a/NEWS +++ b/NEWS @@ -10,6 +10,13 @@ New Features: `str.from_code`, `re.diff`, and `re.comp` * Support for new operator names (e.g. `str.in_re` instead of `str.in.re`), new escape sequences. The new syntax is enabled by default for smt2 files. +* Support for syntax-guided synthesis (SyGuS) problems in the new API. C++ + examples of the SyGuS API can be found in `./examples/api/sygus_*.cpp`. +* Support for higher-order constraints. This includes treating function sorts + (constructible by `->`) as first-class sorts and handling partially applied + function symbols. Support for higher-order constraints can be enabled by + the option `--uf-ho`. +* Support for set comprehension binders `comprehension`. Improvements: * API: Function definitions can now be requested to be global. If the `global` @@ -31,6 +38,12 @@ Changes: notation and as indexed symbols with the new option --bv-print-consts-as-indexed-symbols. The option --bv-print-consts-in-binary has been removed. +* Updated to SyGuS language version 2.0 by default. This is the last release + that will support the SyGuS language version 1.0 (`--lang=sygus1`). A + script is provided to convert version 1.0 files to version 2.0, see + `./contrib/sygus-v1-to-v2.sh`. +* Support for user-provided rewrite rule quantifiers have been removed. +* Support for certain option aliases have been removed. Changes since 1.6 =================