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/CMakeLists.txt | |
| 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/CMakeLists.txt')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index e2e216567..260b0d9b7 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2521,6 +2521,7 @@ set(regress_2_tests regress2/sygus/process-arg-invariance.sy regress2/sygus/real-grammar-neg.sy regress2/sygus/sets-fun-test.sy + regress2/sygus/sumn_recur_synth.sy regress2/sygus/strings-no-syntax-len.sy regress2/sygus/three.sy regress2/typed_v1l50016-simp.cvc |