diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-03 13:07:56 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-04-03 13:07:56 -0500 |
commit | badc9cb00c9086b9303fab1b494e9c5eb88265ec (patch) | |
tree | e9fc7debfae6c52eeae593b4b85653670e56a7b4 /src/theory/builtin | |
parent | d91b52085d7e3bbda65117c0cd88433aed383aff (diff) |
Only rewrite lambdas via array representations when constant (#4203)
Fixes #4170.
Diffstat (limited to 'src/theory/builtin')
-rw-r--r-- | src/theory/builtin/theory_builtin_rewriter.cpp | 16 |
1 files changed, 15 insertions, 1 deletions
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() ); |