diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-07-01 17:35:13 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-07-01 22:35:13 +0000 |
| commit | b4e98013a8e2572545ec3f637dd1caa06e3f7207 (patch) | |
| tree | 5d133f561aebe035a33c8f9256fb7097877be003 /test/regress/regress2/bv_to_int_inc1.smt2 | |
| parent | c2a5fcf1ae85d007bccd8fa294a7b66287972c65 (diff) | |
Add recursive function definitions to subsolver in sygus (#6824)
This passes recursive function definitions to the verification subsolver in sygus, with a default bounded limit of 3. This required improving the interface for setting up subsolvers by allowing custom options; the sygus solver statically computes an instance of the options that it uses in all calls.
This allows us to solve non-PBE sygus problems with recursive function definitions. The PR adds an example.
Diffstat (limited to 'test/regress/regress2/bv_to_int_inc1.smt2')
0 files changed, 0 insertions, 0 deletions