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.

1 files changed, 21 insertions, 0 deletions

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)