Only rewrite lambdas via array representations when constant (#4203)

Fixes #4170.

diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp
index 82952f9fd23337ea4450199b8850ea835599d2da..a39d4231b6da00866616676bbd3823df0ac1b998 100644 (file)
--- a/src/theory/builtin/theory_builtin_rewriter.cpp
+++ b/src/theory/builtin/theory_builtin_rewriter.cpp
@@ -54,9 +54,23 @@ Node TheoryBuiltinRewriter::blastDistinct(TNode in) {
 
 RewriteResponse TheoryBuiltinRewriter::postRewrite(TNode node) {
   if( node.getKind()==kind::LAMBDA ){
+    // The following code ensures that if node is equivalent to a constant
+    // lambda, then we return the canonical representation for the lambda, which
+    // in turn ensures that two constant lambdas are equivalent if and only
+    // if they are the same node.
+    // We canonicalize lambdas by turning them into array constants, applying
+    // normalization on array constants, and then converting the array constant
+    // back to a lambda.
     Trace("builtin-rewrite") << "Rewriting lambda " << node << "..." << std::endl;
     Node anode = getArrayRepresentationForLambda( node );
-    if( !anode.isNull() ){
+    // Only rewrite constant array nodes, since these are the only cases
+    // where we require canonicalization of lambdas. Moreover, applying the
+    // below code is not correct if the arguments to the lambda occur
+    // in return values. For example, lambda x. ite( x=1, f(x), c ) would
+    // be converted to (store (storeall ... c) 1 f(x)), and then converted
+    // to lambda y. ite( y=1, f(x), c), losing the relation between x and y.
+    if (!anode.isNull() && anode.isConst())
+    {
       Assert(anode.getType().isArray());
       //must get the standard bound variable list
       Node varList = NodeManager::currentNM()->getBoundVarListForFunctionType( node.getType() );

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 87bea4583782a8e92751dba282ea60fc5da497f3..031dd297a32090ba436df1cfee4142dcc2eefa3d 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2087,6 +2087,7 @@ set(regress_3_tests
   regress3/hole9.cvc
   regress3/incorrect1.smtv1.smt2
   regress3/issue2429.smt2
+  regress3/issue4170.smt2
   regress3/pp-regfile.smtv1.smt2
   regress3/qwh.35.405.shuffled-as.sat03-1651.smtv1.smt2
   regress3/sixfuncs.sy

diff --git a/test/regress/regress3/issue4170.smt2 b/test/regress/regress3/issue4170.smt2
new file mode 100644 (file)
index 0000000..0dee146
--- /dev/null
+++ b/test/regress/regress3/issue4170.smt2
@@ -0,0 +1,12 @@
+(set-logic ALL)
+(set-option :sygus-inference true)
+(set-option :uf-ho true)
+(set-option :sygus-ext-rew false)
+(set-info :status sat)
+(declare-fun a (Int) Int)
+(declare-fun b (Int) Int)
+(declare-fun c (Int) Int)
+(declare-fun d () Int)
+(assert (distinct a (ite (= d 0) b c)))
+(assert (= (a 0) 4))
+(check-sat)