diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-10-08 22:51:08 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-10-08 22:51:08 +0000 |
commit | e256e63588a867b9ea82e03cfc684c2ea2ca1738 (patch) | |
tree | 97583e7952f18934b2751574032b0a48ff8b866c /src/theory/uf | |
parent | ffda058e93ac699b1649a87f15418f645bb13312 (diff) |
* Models' SubstitutionMaps are now attached to the user context
(rather than SAT context)
* Enable part of CVC3 system test (resolves bug 375)
* Fix infinite recursion in beta reduction code (resolves bug 417)
* Some model-building assertions have been added
* Other minor changes
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/theory_uf_rewriter.h | 18 |
1 files changed, 17 insertions, 1 deletions
diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h index f70d89b30..50211f1ad 100644 --- a/src/theory/uf/theory_uf_rewriter.h +++ b/src/theory/uf/theory_uf_rewriter.h @@ -77,7 +77,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])); } |