diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-09-13 16:31:12 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-09-13 16:31:12 -0500 |
commit | a90b9e2b70be427d1380cb5e65dc33c86e4a63b2 (patch) | |
tree | a6cae3c98ec5c25b65c605dafd0d9e36e110245d /test/regress/regress1 | |
parent | e69f6c3aa94e382d082d23f847709a97d9470f31 (diff) |
Disallow let in sygus grammars, check for free variables in sygus constructors (#3259)
Diffstat (limited to 'test/regress/regress1')
-rw-r--r-- | test/regress/regress1/sygus/abv.sy | 12 | ||||
-rw-r--r-- | test/regress/regress1/sygus/let-bug-simp.sy | 12 | ||||
-rw-r--r-- | test/regress/regress1/sygus/tester.sy | 2 | ||||
-rw-r--r-- | test/regress/regress1/sygus/twolets2-orig.sy | 5 |
4 files changed, 15 insertions, 16 deletions
diff --git a/test/regress/regress1/sygus/abv.sy b/test/regress/regress1/sygus/abv.sy index 6ce1a011a..d9a8a019c 100644 --- a/test/regress/regress1/sygus/abv.sy +++ b/test/regress/regress1/sygus/abv.sy @@ -30,6 +30,10 @@ (select arrIn x) ) +(define-fun letf ((m MemSort) (v1 AddrSort) (v2 AddrSort)) ValSort + (bvadd + (ReadArr v1 m) + (ReadArr v2 m))) (synth-fun f ; Args @@ -45,12 +49,8 @@ (WriteArr (Variable AddrSort) (Variable ValSort) mem))) (Start ValSort ( - (let - ((m MemSort StartArray)) - (bvadd - (ReadArr (Variable AddrSort) m) - (ReadArr (Variable AddrSort) m)))))) -) + (letf StartArray (Variable AddrSort) (Variable AddrSort)))) +)) (declare-var a (BitVec 8)) (declare-var b (BitVec 8)) diff --git a/test/regress/regress1/sygus/let-bug-simp.sy b/test/regress/regress1/sygus/let-bug-simp.sy index d570d5a21..5c2dccff0 100644 --- a/test/regress/regress1/sygus/let-bug-simp.sy +++ b/test/regress/regress1/sygus/let-bug-simp.sy @@ -1,17 +1,15 @@ ; EXPECT: unsat ; COMMAND-LINE: --sygus-out=status (set-logic LIA) - +(define-fun letf ((z Int) (v1 Int) (v2 Int)) Bool + (or + (= v1 z) + (= v2 z))) (synth-fun f ((x0 Int) (x1 Int)) Bool ( (StartInt Int (5)) - (Start Bool ( - (let - ((z Int StartInt)) - (or - (= (Variable Int) z) - (= (Variable Int) z))))) + (Start Bool ( (letf StartInt (Variable Int) (Variable Int)) )) ) ) diff --git a/test/regress/regress1/sygus/tester.sy b/test/regress/regress1/sygus/tester.sy index 261666dd4..bf1cd1576 100644 --- a/test/regress/regress1/sygus/tester.sy +++ b/test/regress/regress1/sygus/tester.sy @@ -11,7 +11,7 @@ ( (Start DT (ntDT)) (ntDT DT - ( x1 x2 + ( x1 (JSBool ntBool) (A ntInt) (ite ntBool ntDT ntDT) diff --git a/test/regress/regress1/sygus/twolets2-orig.sy b/test/regress/regress1/sygus/twolets2-orig.sy index 50f7ad544..a92c0b014 100644 --- a/test/regress/regress1/sygus/twolets2-orig.sy +++ b/test/regress/regress1/sygus/twolets2-orig.sy @@ -1,10 +1,11 @@ ; EXPECT: unsat ; COMMAND-LINE: --cegqi-si=all --sygus-out=status (set-logic LIA) +(define-fun letf ((x Int) (y Int) (z Int)) Int (+ (+ y x) z)) (synth-fun f1 ((x Int)) Int ( (Start Int ( - (let ((y Int CInt) (z Int CInt)) (+ (+ y x) z)) + (letf x CInt CInt) ) ) (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15)) @@ -14,7 +15,7 @@ (synth-fun f2 ((x Int)) Int ( (Start Int (x - (let ((y Int Start) (z Int CInt)) (+ (+ y x) z)) + (letf x Start CInt) ) ) (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15)) |