diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-10-09 11:58:08 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-10-09 11:58:08 +0000 |
commit | bdaa3049467fd17d3fb95701f7946a4bf0f5206a (patch) | |
tree | 7b770e107d3a625f266381141d3489cc23fecafe /src | |
parent | 914dc99c1b89cf7203dc20296e8279786af202f9 (diff) |
fix beta reduction in both preRewrite() *and* postRewrite(), related to bug 417. oops. also fix spelling on "rewritting" test
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/uf/theory_uf_rewriter.h | 34 |
1 files changed, 18 insertions, 16 deletions
diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h index 50211f1ad..15ac0f605 100644 --- a/src/theory/uf/theory_uf_rewriter.h +++ b/src/theory/uf/theory_uf_rewriter.h @@ -53,7 +53,23 @@ public: 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()); - substitutions.addSubstitution(*formal, *arg); + // 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); } return RewriteResponse(REWRITE_DONE, substitutions.apply(lambda[1])); } @@ -77,21 +93,7 @@ public: 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.) + // This rewrite step is important: see note in postRewrite(). Node n = Rewriter::rewrite(*arg); substitutions.addSubstitution(*formal, n); } |