diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-21 19:38:40 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-08-21 19:38:40 -0500 |
commit | ab8d44b83e210ed38623a1440e3ef1d318f7d0d0 (patch) | |
tree | b241f69ddf7715eb1bfe0753e59ed02a12507da3 /test/regress | |
parent | 5b655946e1c73f511719d0264f92715b063e867f (diff) |
Fix processing of nested Variable construct in sygus let bodies (#2351)
Diffstat (limited to 'test/regress')
-rw-r--r-- | test/regress/Makefile.tests | 2 | ||||
-rw-r--r-- | test/regress/regress1/sygus/abv.sy | 61 | ||||
-rw-r--r-- | test/regress/regress1/sygus/let-bug-simp.sy | 22 |
3 files changed, 85 insertions, 0 deletions
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index e773bf698..f766396a1 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1513,6 +1513,7 @@ REG1_TESTS = \ regress1/strings/type003.smt2 \ regress1/strings/username_checker_min.smt2 \ regress1/sygus/VC22_a.sy \ + regress1/sygus/abv.sy \ regress1/sygus/array_search_2.sy \ regress1/sygus/array_search_5-Q-easy.sy \ regress1/sygus/array_sum_2_5.sy \ @@ -1546,6 +1547,7 @@ REG1_TESTS = \ regress1/sygus/inv-example.sy \ regress1/sygus/inv-unused.sy \ regress1/sygus/large-const-simp.sy \ + regress1/sygus/let-bug-simp.sy \ regress1/sygus/list-head-x.sy \ regress1/sygus/logiccell_help.sy \ regress1/sygus/max.sy \ diff --git a/test/regress/regress1/sygus/abv.sy b/test/regress/regress1/sygus/abv.sy new file mode 100644 index 000000000..6ce1a011a --- /dev/null +++ b/test/regress/regress1/sygus/abv.sy @@ -0,0 +1,61 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic ABV) + +(define-sort AddrSort () (BitVec 32)) +(define-sort ValSort () (BitVec 8)) +(define-sort MemSort () (Array AddrSort ValSort)) + +; Write the value y to index x +(define-fun WriteArr + ; Args + ((x AddrSort) (y ValSort) (arrIn MemSort)) + + ; Return value + MemSort + + ; Function Body + (store arrIn x y) +) + +; Read from index x +(define-fun ReadArr + ; Args + ((x AddrSort) (arrIn MemSort)) + + ; Return value + ValSort + + ; Function Body + (select arrIn x) +) + + +(synth-fun f + ; Args + ((x0 ValSort) (x1 ValSort) (idx0 AddrSort) (idx1 AddrSort) (mem MemSort)) + + ; Return value + ValSort + + ; Grammar + ( + (StartArray MemSort ( + (WriteArr (Variable AddrSort) (Variable ValSort) StartArray) + (WriteArr (Variable AddrSort) (Variable ValSort) mem))) + + (Start ValSort ( + (let + ((m MemSort StartArray)) + (bvadd + (ReadArr (Variable AddrSort) m) + (ReadArr (Variable AddrSort) m)))))) +) + +(declare-var a (BitVec 8)) +(declare-var b (BitVec 8)) +(declare-var c (BitVec 32)) +(declare-var d (BitVec 32)) +(declare-var e (Array (BitVec 32) (BitVec 8))) +(constraint (=> (not (= c d)) (= (bvadd a b) (f a b c d e)))) +(check-synth) diff --git a/test/regress/regress1/sygus/let-bug-simp.sy b/test/regress/regress1/sygus/let-bug-simp.sy new file mode 100644 index 000000000..d570d5a21 --- /dev/null +++ b/test/regress/regress1/sygus/let-bug-simp.sy @@ -0,0 +1,22 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic LIA) + +(synth-fun f ((x0 Int) (x1 Int)) Bool +( + (StartInt Int (5)) + + (Start Bool ( + (let + ((z Int StartInt)) + (or + (= (Variable Int) z) + (= (Variable Int) z))))) +) +) + +(declare-var a Int) +(declare-var b Int) +(constraint (=> (= a 5) (f a b))) +(constraint (=> (= b 5) (f a b))) +(check-synth) |