From badc9cb00c9086b9303fab1b494e9c5eb88265ec Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 3 Apr 2020 13:07:56 -0500 Subject: [PATCH] Only rewrite lambdas via array representations when constant (#4203) Fixes #4170. --- src/theory/builtin/theory_builtin_rewriter.cpp | 16 +++++++++++++++- test/regress/CMakeLists.txt | 1 + test/regress/regress3/issue4170.smt2 | 12 ++++++++++++ 3 files changed, 28 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress3/issue4170.smt2 diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp index 82952f9fd..a39d4231b 100644 --- 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 87bea4583..031dd297a 100644 --- 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 index 000000000..0dee146c0 --- /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) -- 2.30.2