diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-07-26 14:48:40 -0500 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-07-26 12:48:40 -0700 |
commit | 8db4b7f5a0a7c3299313668e77bcf3944b8e5a01 (patch) | |
tree | 5e12ccdea4e9a9285de2b04fdfbc2c1f3ef22f05 /test/regress | |
parent | a131d4b4cf086f27c4c62d4b012862c75153033e (diff) |
Fix rewriter for lambda (#2211)
The rewriter for lambda is currently too aggressive, there are cases like:
lambda xy. x = y
that are converted into an array representation that when indexing based on x gives (store y true false), which is subsequently converted to:
lambda fv_1 fv_2. fv_1 = y
where fv_1 and fv_2 are canonical free variables. Here, y is used as index but was not substituted hence is incorrectly made free.
To make things simpler, this PR disables any rewriting for lambda unless the array representation of the lambda is a constant, which hardcodes/simplifies a previous argument (reqConst=true). This fixes a sygus issue I ran into yesterday (regression added in this PR).
Some parts of the code were formatted as a result.
Diffstat (limited to 'test/regress')
-rw-r--r-- | test/regress/Makefile.tests | 1 | ||||
-rw-r--r-- | test/regress/regress1/sygus/sygus-lambda-fv.sy | 21 |
2 files changed, 22 insertions, 0 deletions
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 48b290bfe..c43e083f3 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1547,6 +1547,7 @@ REG1_TESTS = \ regress1/sygus/strings-trivial-two-type.sy \ regress1/sygus/strings-trivial.sy \ regress1/sygus/sygus-dt.sy \ + regress1/sygus/sygus-lambda-fv.sy \ regress1/sygus/sygus-uf-ex.sy \ regress1/sygus/t8.sy \ regress1/sygus/tl-type-0.sy \ diff --git a/test/regress/regress1/sygus/sygus-lambda-fv.sy b/test/regress/regress1/sygus/sygus-lambda-fv.sy new file mode 100644 index 000000000..d2a3700ce --- /dev/null +++ b/test/regress/regress1/sygus/sygus-lambda-fv.sy @@ -0,0 +1,21 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic ALL) + +(synth-fun SC ((y (BitVec 32)) (w (BitVec 32)) ) (BitVec 32) + ( + (Start (BitVec 32) ( + y + w + #x00000000 + (bvadd Start Start) + (ite StartBool Start Start) + )) + (StartBool Bool ((= Start #x10000000) (= Start #x00000000))) +)) + +(constraint (= (SC #x00000000 #x00001000) #x00001000)) +(constraint (= (SC #x00001000 #x00001000) #x00001000)) +(constraint (= (SC #x01001000 #x00001000) #x01001000)) + +(check-synth) |