diff options
author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2018-09-10 20:51:03 -0500 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-09-10 18:51:03 -0700 |
commit | 1a695dcbe3036ab0f1922c5655c082ec1f14db97 (patch) | |
tree | 96444e8dedeb0b98ba01a7f7b1a7a0c5b2349410 /src/expr/expr_template.cpp | |
parent | f5746ca4a24c1b9f05f5528bc66016668d9a7863 (diff) |
Using a single condition enumerator in sygus-unif (#2440)
This commit allows the use of unification techniques in which the search space for conditions in explored independently of the search space for return values (i.e. there is a single condition enumerator for which we always ask new values, similar to the PBE case).
In comparison with asking the ground solver to come up with a minimal number of condition values to resolve all my separation conflicts:
- _main advantage_: can quickly enumerate relevant condition values for solving the problem
- _main disadvantage_: there are many "spurious" values (as in not useful for actual solutions) that get in the way of "good" values when we build solutions from the lazy trie.
A follow-up PR will introduce an information-gain heuristic for building solutions, which ultimately greatly outperforms the other flavor of sygus-unif.
There is also small improvements for trace messages.
Diffstat (limited to 'src/expr/expr_template.cpp')
0 files changed, 0 insertions, 0 deletions