diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-06 09:24:11 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-06 09:24:11 -0600 |
| commit | 210e6db5c6a76ee1e554426058ecf3397575f1e3 (patch) | |
| tree | 98140a04acd9eedc91e2d598224ac7005d0a3540 /test/regress/regress1/sygus | |
| parent | a727f6314c8f2ad72d8d83eb63c413bab68d1b08 (diff) | |
Support default sygus grammar construction for sets (#3842)
Fixes #3645.
Diffstat (limited to 'test/regress/regress1/sygus')
| -rw-r--r-- | test/regress/regress1/sygus/sets-pred-test.sy | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/test/regress/regress1/sygus/sets-pred-test.sy b/test/regress/regress1/sygus/sets-pred-test.sy new file mode 100644 index 000000000..284325712 --- /dev/null +++ b/test/regress/regress1/sygus/sets-pred-test.sy @@ -0,0 +1,12 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic ALL) +(synth-fun P ((x (Set Int))) Bool) + +(constraint (not (P (as emptyset (Set Int))))) +(constraint (not (P (insert 1 2 (as emptyset (Set Int)))))) +(constraint (P (insert 0 (as emptyset (Set Int))))) +(constraint (P (insert 0 4 5 (as emptyset (Set Int))))) +(constraint (not (P (singleton 45)))) + +(check-synth) |