diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-06-10 15:35:07 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-06-10 15:35:07 +0200 |
commit | 2f2b368448c3a5e50db46b3ec2cc364ae8959ac1 (patch) | |
tree | 91576c0fd2ed7fee5da14598f15138a18c2cc27a /test/regress/regress0/sygus | |
parent | 6417016a38e24b09bc062a4bd4b0a5945fbcc0ec (diff) |
Support for printing solutions involving LetGTerm sygus. Bug fix define-fun within LetGTerm sygus. Bug fix sygus argument generalization. Add regressions.
Diffstat (limited to 'test/regress/regress0/sygus')
-rw-r--r-- | test/regress/regress0/sygus/Makefile.am | 5 | ||||
-rw-r--r-- | test/regress/regress0/sygus/let-ringer.sy | 14 | ||||
-rw-r--r-- | test/regress/regress0/sygus/let-simp.sy | 15 | ||||
-rw-r--r-- | test/regress/regress0/sygus/twolets2-orig.sy | 28 |
4 files changed, 61 insertions, 1 deletions
diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am index 40f3fa4aa..dc6a1e0d1 100644 --- a/test/regress/regress0/sygus/Makefile.am +++ b/test/regress/regress0/sygus/Makefile.am @@ -32,7 +32,10 @@ TESTS = commutative.sy \ const-var-test.sy \ no-syntax-test.sy \ no-syntax-test-no-si.sy \ - no-flat-simp.sy + no-flat-simp.sy \ + twolets2-orig.sy \ + let-ringer.sy \ + let-simp.sy # sygus tests currently taking too long for make regress EXTRA_DIST = $(TESTS) \ diff --git a/test/regress/regress0/sygus/let-ringer.sy b/test/regress/regress0/sygus/let-ringer.sy new file mode 100644 index 000000000..046d074d9 --- /dev/null +++ b/test/regress/regress0/sygus/let-ringer.sy @@ -0,0 +1,14 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si +(set-logic LIA) +(define-fun g ((x Int)) Int (ite (= x 1) 15 19)) +(synth-fun f ((x Int)) Int + ((Start Int (x + 0 + 1 + (- Start Start) + (let ((z Int Start) (w Int Start)) (+ z (+ x (+ x (+ Start (+ 1 (+ (g w) z))))))))))) + +(declare-var x Int) +(constraint (= (f x) (+ (* 4 x) 15))) +(check-synth) diff --git a/test/regress/regress0/sygus/let-simp.sy b/test/regress/regress0/sygus/let-simp.sy new file mode 100644 index 000000000..daca906a2 --- /dev/null +++ b/test/regress/regress0/sygus/let-simp.sy @@ -0,0 +1,15 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si +(set-logic LIA) +(synth-fun f ((x Int) (y Int)) Int + ((Start Int (x + y + 0 + (- Start Start) + (let ((z Int Start)) (+ z z)))))) + +(declare-var x Int) +(declare-var y Int) +(constraint (= (f x y) (* 3 x))) +(check-synth) + diff --git a/test/regress/regress0/sygus/twolets2-orig.sy b/test/regress/regress0/sygus/twolets2-orig.sy new file mode 100644 index 000000000..c1066277e --- /dev/null +++ b/test/regress/regress0/sygus/twolets2-orig.sy @@ -0,0 +1,28 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si +(set-logic LIA) +(synth-fun f1 ((x Int)) Int + ( + (Start Int ( + (let ((y Int CInt) (z Int CInt)) (+ (+ y x) z)) + ) + ) + (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15)) + + ) +) +(synth-fun f2 ((x Int)) Int + ( + (Start Int (x + (let ((y Int Start) (z Int CInt)) (+ (+ y x) z)) + ) + ) + (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15)) + + ) +) +(declare-var x1 Int) +(declare-var x2 Int) +(constraint (= (+ (f1 x1)(f2 x2)) (+ (+ x2 x2) (+ x1 8)))) +(check-synth) + |