Updates to NEWS. (#4628)

diff --git a/NEWS b/NEWS
index 8c6ec7bc97c6bc325c0895631d0d8f018d9b4e6e..d778540088bd8169ff69e86c2ceb2a755e82cf38 100644 (file)
--- 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
 =================