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/regress0 | |
| parent | e69f6c3aa94e382d082d23f847709a97d9470f31 (diff) | |
Disallow let in sygus grammars, check for free variables in sygus constructors (#3259)
Diffstat (limited to 'test/regress/regress0')
| -rw-r--r-- | test/regress/regress0/sygus/let-ringer.sy | 4 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/let-simp.sy | 3 |
2 files changed, 5 insertions, 2 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) |