diff options
| author | Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> | 2020-03-28 12:39:47 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-28 12:39:47 -0500 |
| commit | 830c09d3cadc119845aff27684bd68c16e442692 (patch) | |
| tree | 4e0c15b4901d28202ca32cd7611810bf31ed78c9 /test/regress/regress0/sygus | |
| parent | 2c6b35d8ce7dcacd2f13bcdd5365629ee315dc8d (diff) | |
Convert the last few Sygus benchmarks to V2. (#4172)
Diffstat (limited to 'test/regress/regress0/sygus')
| -rw-r--r-- | test/regress/regress0/sygus/c100.sy | 4 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/check-generic-red.sy | 3 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/const-var-test.sy | 5 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/sygus-uf.sy | 7 |
4 files changed, 10 insertions, 9 deletions
diff --git a/test/regress/regress0/sygus/c100.sy b/test/regress/regress0/sygus/c100.sy index ef124c953..994fb6de3 100644 --- a/test/regress/regress0/sygus/c100.sy +++ b/test/regress/regress0/sygus/c100.sy @@ -1,9 +1,10 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status (set-logic LIA) (synth-fun constant ((x Int)) Int + ((Start Int)) ((Start Int (0 2 3 @@ -15,4 +16,3 @@ (declare-var x Int) (constraint (= (constant x) 100)) (check-synth) - diff --git a/test/regress/regress0/sygus/check-generic-red.sy b/test/regress/regress0/sygus/check-generic-red.sy index e169e1a5c..d593a7d9e 100644 --- a/test/regress/regress0/sygus/check-generic-red.sy +++ b/test/regress/regress0/sygus/check-generic-red.sy @@ -1,8 +1,9 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --sygus-out=status --decision=justification +; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status --decision=justification (set-logic LIA) (synth-fun P ((x Int) (y Int)) Bool + ((Start Bool) (StartIntC Int) (StartInt Int)) ((Start Bool ((and Start Start) (not Start) (<= StartInt StartIntC) diff --git a/test/regress/regress0/sygus/const-var-test.sy b/test/regress/regress0/sygus/const-var-test.sy index 305f5783a..31e88f523 100644 --- a/test/regress/regress0/sygus/const-var-test.sy +++ b/test/regress/regress0/sygus/const-var-test.sy @@ -1,9 +1,10 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status (set-logic LIA) (synth-fun max2 ((x Int) (y Int)) Int + ((Start Int) (StartBool Bool)) ((Start Int ((Variable Int) (Constant Int) (+ Start Start) @@ -21,6 +22,4 @@ (constraint (= (max2 x y) (+ x y 500))) - (check-synth) - diff --git a/test/regress/regress0/sygus/sygus-uf.sy b/test/regress/regress0/sygus/sygus-uf.sy index d506dd5b2..b08aa8929 100644 --- a/test/regress/regress0/sygus/sygus-uf.sy +++ b/test/regress/regress0/sygus/sygus-uf.sy @@ -1,10 +1,11 @@ -; COMMAND-LINE: --sygus-out=status --uf-ho +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --uf-ho ; EXPECT: unsat -(set-logic UFLIA) +(set-logic ALL) -(declare-fun uf (Int) Int) +(declare-var uf (-> Int Int)) (synth-fun f ((x Int) (y Int)) Bool + ((Start Bool) (IntExpr Int)) ((Start Bool (true false (<= IntExpr IntExpr) (= IntExpr IntExpr) |