diff options
Diffstat (limited to 'test/regress')
-rw-r--r-- | test/regress/regress0/sygus/let-ringer.sy | 4 | ||||
-rw-r--r-- | test/regress/regress0/sygus/let-simp.sy | 3 | ||||
-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 |
6 files changed, 20 insertions, 18 deletions
diff --git a/test/regress/regress0/sygus/let-ringer.sy b/test/regress/regress0/sygus/let-ringer.sy index 0fe8dd05e..c02d2b31f 100644 --- a/test/regress/regress0/sygus/let-ringer.sy +++ b/test/regress/regress0/sygus/let-ringer.sy @@ -3,12 +3,14 @@ ; COMMAND-LINE: --cegqi-si=all --sygus-unif --sygus-out=status (set-logic LIA) (define-fun g ((x Int)) Int (ite (= x 1) 15 19)) +(define-fun letf ((z Int) (w Int) (s Int) (x Int)) Int (+ z (+ x (+ x (+ s (+ 1 (+ (g w) z))))))) + (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))))))))))) + (letf Start Start Start x))))) (declare-var x Int) (constraint (= (f x) (+ (* 4 x) 15))) diff --git a/test/regress/regress0/sygus/let-simp.sy b/test/regress/regress0/sygus/let-simp.sy index 6f9d9fff9..7e191e312 100644 --- a/test/regress/regress0/sygus/let-simp.sy +++ b/test/regress/regress0/sygus/let-simp.sy @@ -1,12 +1,13 @@ ; EXPECT: unsat ; COMMAND-LINE: --cegqi-si=all --sygus-out=status (set-logic LIA) +(define-fun letf ((z Int)) Int (+ z z)) (synth-fun f ((x Int) (y Int)) Int ((Start Int (x y 0 (- Start Start) - (let ((z Int Start)) (+ z z)))))) + (letf Start))))) (declare-var x Int) (declare-var y Int) 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)) |