diff options
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() ); |