diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-07-06 08:20:23 +0100 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-07-06 00:20:23 -0700 |
commit | a3a3c6f56ef1593076379e39ec478013d8a01ab8 (patch) | |
tree | 10e6a51dfdaeacd340be27eae425ad128f5e0052 /src/theory/uf | |
parent | ceba90a89f878cda01067042ca9a0dfee555b7cd (diff) |
sygusComp2018: simplify beta reduction in uf rewriter. (#2106)
This is PR 8/18 from the sygus comp 2018 branch (https://github.com/ajreynol/CVC4/tree/sygusComp2018-2).
I am not sure how it is possible in any circumstance that the complication in the comment I am deleting would ever happen, without doing something very strange. I think it is referring to some sort of inter-dependence between macro expansion + beta-reductions. This should not concern the rewriter. Here is the commit that introduced it: bdaa304.
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/theory_uf_rewriter.h | 50 |
1 files changed, 12 insertions, 38 deletions
diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h index 92bfd6647..3eb59e5fc 100644 --- a/src/theory/uf/theory_uf_rewriter.h +++ b/src/theory/uf/theory_uf_rewriter.h @@ -46,32 +46,20 @@ public: } if(node.getKind() == kind::APPLY_UF) { if( node.getOperator().getKind() == kind::LAMBDA ){ - // resolve away the lambda - context::Context fakeContext; - theory::SubstitutionMap substitutions(&fakeContext); TNode lambda = node.getOperator(); - for(TNode::iterator formal = lambda[0].begin(), arg = node.begin(); formal != lambda[0].end(); ++formal, ++arg) { - // typechecking should ensure that the APPLY_UF is well-typed, correct arity, etc. - Assert(formal != node.end()); - // This rewrite step is important: if we have (f (f 5)) for - // some lambda term f, we want to beta-reduce the inside (f 5) - // application first. Otherwise, we can end up in infinite - // recursion, because f's formal (say "x") gives the - // substitution "x |-> (f 5)". Fine, the body of the lambda - // gets (f 5) in place for x. But since the same lambda ("f") - // now occurs in the body, it's got the same bound var "x", so - // substitution continues and we replace that x by (f 5). And - // then again. :-( - // - // We need a better solution for distinguishing bound - // variables like this, but for now, handle it by going - // inside-out. (Quantifiers shouldn't ever have this problem, - // so long as the bound vars in different quantifiers are kept - // different.) - Node n = Rewriter::rewrite(*arg); - substitutions.addSubstitution(*formal, n); + std::vector<TNode> vars; + std::vector<TNode> subs; + for (const TNode& v : lambda[0]) + { + vars.push_back(v); } - return RewriteResponse(REWRITE_AGAIN_FULL, substitutions.apply(lambda[1])); + for (const TNode& s : node) + { + subs.push_back(s); + } + Node ret = lambda[1].substitute( + vars.begin(), vars.end(), subs.begin(), subs.end()); + return RewriteResponse(REWRITE_AGAIN_FULL, ret); }else if( !canUseAsApplyUfOperator( node.getOperator() ) ){ return RewriteResponse(REWRITE_AGAIN_FULL, getHoApplyForApplyUf(node)); } @@ -106,20 +94,6 @@ public: return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(false)); } } - if(node.getKind() == kind::APPLY_UF && node.getOperator().getKind() == kind::LAMBDA) { - // resolve away the lambda - context::Context fakeContext; - theory::SubstitutionMap substitutions(&fakeContext); - TNode lambda = node.getOperator(); - for(TNode::iterator formal = lambda[0].begin(), arg = node.begin(); formal != lambda[0].end(); ++formal, ++arg) { - // typechecking should ensure that the APPLY_UF is well-typed, correct arity, etc. - Assert(formal != node.end()); - // This rewrite step is important: see note in postRewrite(). - Node n = Rewriter::rewrite(*arg); - substitutions.addSubstitution(*formal, n); - } - return RewriteResponse(REWRITE_DONE, substitutions.apply(lambda[1])); - } return RewriteResponse(REWRITE_DONE, node); } |