From ad24cbdb3462b2b2dd312aab2f1f33d9bbcac00e Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 19 Aug 2010 23:49:58 +0000 Subject: UF theory bug fixes, code cleanup, and extra debugging output. Enabled new UF theory by default. Added some UF regressions. Some work on the whole equality-over-bool-removed-in-favor-of-IFF thing. (Congruence closure module and other things have to handle IFF as a special case of equality, etc..) Added pre-rewriting to TheoryBool which rewrites: * (IFF true x) => x * (IFF false x) => (NOT x) * (IFF x true) => x * (IFF x false) => (NOT x) * (IFF x x) => true * (IFF x (NOT x)) => false * (IFF (NOT x) x) => false * (ITE true x y) => x * (ITE false x y) => y * (ITE cond x x) => x Added post-rewriting that does all of the above, plus normalize IFF and ITE: * (IFF x y) => (IFF y x), if y < x * (ITE (NOT cond) x y) => (ITE cond y x) (Note: ITEs survive the removal-of-ITEs pass only if they are Boolean-valued.) A little more debugging output from CNF stream, context pushes/pops, ITE removal. Some more documentation. Fixed some typos. --- src/theory/theory.h | 13 +++++++++++++ 1 file changed, 13 insertions(+) (limited to 'src/theory/theory.h') diff --git a/src/theory/theory.h b/src/theory/theory.h index 64a3b8f06..1cce09439 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -313,6 +313,19 @@ public: * rewrite a term to a strictly larger term that contains itself, as * this will cause a loop of hard Node links in the cache (and thus * memory leakage). + * + * Be careful with the return value. If a preRewrite() can return a + * sub-expression, and that sub-expression can be a member of the + * same theory and could be rewritten, make sure to return + * RewriteAgain instead of RewriteComplete. This is an easy mistake + * to make, as preRewrite() is often a short-circuiting version of + * the same rewrites that occur in postRewrite(); however, in the + * postRewrite() case, the subexpressions have all been + * post-rewritten. In the preRewrite() case, they have NOT yet been + * pre-rewritten. For example, (ITE true (ITE true x y) z) should + * pre-rewrite to x; but if the outer preRewrite() returns + * RewriteComplete, the result of the pre-rewrite will be + * (ITE true x y). */ virtual RewriteResponse preRewrite(TNode n, bool topLevel) { Debug("theory-rewrite") << "no pre-rewriting to perform for " << n << std::endl; -- cgit v1.2.3