diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2019-04-04 13:30:27 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-04-04 13:30:27 -0500 |
| commit | 7de51f8f53db83ebbc871a4d437c382b6ef8d2ba (patch) | |
| tree | bd3fe0bc1b189175ef93a65bbb21c9e70bc27cd9 | |
| parent | a44c62c18a8380c089764decdd4c533268b4ef30 (diff) | |
adding sygus news (#2934)
| -rw-r--r-- | NEWS | 11 |
1 files changed, 9 insertions, 2 deletions
@@ -1,4 +1,4 @@ -This file contains a summary of important user-visible changes. +This file contains a summary of important user-visible changes. Changes since 1.6 ================= @@ -20,6 +20,14 @@ New Features: (`--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`). + * Support for streaming solutions of increasingly smaller size when using the + PBE solver (`--sygus-stream --sygus-pbe`). After the first solution is found + and printed, the solver will continue to look for new solutions and print + those, if any, that are smaller than previously printed solutions. + * Support for unification-based techniques in non-separable specifications + (`--sygus-unif`). For solving invariant problems a dedicate mode + (`--sygus-unif-boolean-heuristic-dt`) is available that builds candidate + solutions using heuristic decision tree learning. Improvements: * Strings: @@ -190,4 +198,3 @@ Changes since 1.0 use -q. Previously, this would silence all output (including "sat" or "unsat") as well. Now, single -q silences messages and warnings, and double -qq silences all output (except on exception or signal). - |