diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2018-05-31 11:52:06 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2018-05-31 11:52:06 -0500 |
commit | 39b40bbe2e0e4f8ce6c24a0c6b18b5bf7d07d94a (patch) | |
tree | 76e8a9f9beffe90056497d85fdfed2e157e3df7d /src | |
parent | 3a6cc7d746932fd38956725bb30b80e7b8b669fd (diff) |
Simplify beta reduction.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/uf/theory_uf_rewriter.h | 35 |
1 files changed, 11 insertions, 24 deletions
diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h index fe9247ae8..e60d51063 100644 --- a/src/theory/uf/theory_uf_rewriter.h +++ b/src/theory/uf/theory_uf_rewriter.h @@ -46,32 +46,19 @@ 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)); } |