diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-10-01 01:56:57 -0500 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-09-30 23:56:57 -0700 |
commit | 2e1b546811778f2c95f07b70f42e458b0552fab0 (patch) | |
tree | e819e393153d339128914477b9bbf0e458bcf4ed /contrib | |
parent | 8182ab9f7d8d6c732202371c24bafd721ef6cfcc (diff) |
Trivial solve method for single invocation sygus (#3328)
This short circuits CEGQI when the conjecture is solvable by simple equality reasoning. It adds two examples where we previously would have fallen back on enumeration due to not having an instantiation technique for strings, despite the conjectures being trivially solvable.
Diffstat (limited to 'contrib')
0 files changed, 0 insertions, 0 deletions