diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-07-04 03:59:36 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-07-04 03:59:36 +0000 |
commit | 9e15c81c673b2cb325cc21ace39f84b37d8b65c9 (patch) | |
tree | c50baf1f33a59cdac18f815465a35b61b2298ee7 /src/theory/theory_engine.cpp | |
parent | 994427c682dfe7323a0e806b18095b862508d454 (diff) |
With "-d extra-checking", rewrites are now checked (after
post-rewrite, another full rewrite is performed and the results
compared).
Also added another response code to rewriters. Theories return a
CVC4::theory::RewriteResponse from preRewrite() and postRewrite().
This class has nice subclasses to make the theory rewriters somewhat
self-documenting in termination behavior. They look like
tail-recursive rewriting calls, but they're not; they are
instantiations of the RewriteResponse result code, which carries the
Node being returned:
// Flags the node as DONE pre- or post-rewriting, though this is
// ignored if n belongs to another theory.
//
// NOTE this just changed name from RewritingComplete(), which
// didn't match RewriteAgain().
//
return RewriteComplete(n);
// Flags the node as needing another pre-rewrite (if returned from a
// preRewrite()) or post-rewrite (if returned from a postRewrite()).
//
return RewriteAgain(n);
// Flags the node as needing another FULL rewrite. This is the same
// as RewriteAgain() if returned from preRewrite(). If it's returned
// from postRewrite(), however, this causes a full preRewrite() and
// postRewrite() of the Node and all its children (though the cache is
// still in effect, which might elide some rewriting calls).
//
// This would have been another fix for bug #168. Its use should be
// discouraged in practice, but there are places where it will
// probably be necessary, where a theory rewrites a Node into
// something in another theory about which it knows nothing.
// A common case is where the returned Node is expressed as a
// conjuction or disjunction of EQUALs, or a negation of EQUAL,
// where the EQUAL is across terms in another theory, and that EQUAL
// subterm should be seen by the owning theory.
//
return FullRewriteNeeded(n);
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 58 |
1 files changed, 45 insertions, 13 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 86e808d66..03678e30e 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -146,11 +146,9 @@ Node TheoryEngine::removeITEs(TNode node) { Assert( node.getNumChildren() == 3 ); TypeNode nodeType = node[1].getType(); if(!nodeType.isBoolean()){ - Node skolem = nodeManager->mkVar(node.getType()); Node newAssertion = - nodeManager->mkNode( - kind::ITE, + nodeManager->mkNode(kind::ITE, node[0], nodeManager->mkNode(kind::EQUAL, skolem, node[1]), nodeManager->mkNode(kind::EQUAL, skolem, node[2])); @@ -180,7 +178,6 @@ Node TheoryEngine::removeITEs(TNode node) { } if(somethingChanged) { - cachedRewrite = nodeManager->mkNode(node.getKind(), newChildren); nodeManager->setAttribute(node, theory::IteRewriteAttr(), cachedRewrite); return cachedRewrite; @@ -246,10 +243,10 @@ struct RewriteStackElement { /** * Construct a fresh stack element. */ - RewriteStackElement(Node n, Theory* thy, bool top) : + RewriteStackElement(Node n, Theory* thy, bool topLevel) : d_node(n), d_theory(thy), - d_topLevel(top), + d_topLevel(topLevel), d_nextChild(0) { } }; @@ -257,7 +254,7 @@ struct RewriteStackElement { }/* CVC4::theory::rewrite namespace */ }/* CVC4::theory namespace */ -Node TheoryEngine::rewrite(TNode in) { +Node TheoryEngine::rewrite(TNode in, bool topLevel) { using theory::rewrite::RewriteStackElement; Node noItes = removeITEs(in); @@ -265,10 +262,11 @@ Node TheoryEngine::rewrite(TNode in) { // descend top-down into the theory rewriters vector<RewriteStackElement> stack; - stack.push_back(RewriteStackElement(noItes, theoryOf(noItes), true)); + stack.push_back(RewriteStackElement(noItes, theoryOf(noItes), topLevel)); Debug("theory-rewrite") << "TheoryEngine::rewrite() starting at" << endl << " " << noItes << " " << theoryOf(noItes) - << " TOP-LEVEL 0" << endl; + << " " << (topLevel ? "TOP-LEVEL " : "") + << "0" << endl; // This whole thing is essentially recursive, but we avoid actually // doing any recursion. do {// do until the stack is empty.. @@ -299,7 +297,9 @@ Node TheoryEngine::rewrite(TNode in) { Debug("theory-rewrite") << "got back " << rse.d_node << " " << thy2 << "[" << *thy2 << "]" << (response.needsMoreRewriting() ? - " MORE-REWRITING" : " DONE") + (response.needsFullRewriting() ? + " FULL-REWRITING" : " MORE-REWRITING") + : " DONE") << endl; if(rse.d_theory != thy2) { Debug("theory-rewrite") << "pre-rewritten from " << *rse.d_theory @@ -311,7 +311,7 @@ Node TheoryEngine::rewrite(TNode in) { // rewritten from theory T1 into T2, then back to T1 ? rse.d_topLevel = true; } else { - done = !response.needsMoreRewriting(); + done = response.isDone(); } } while(!done); setPreRewriteCache(original, wasTopLevel, rse.d_node); @@ -383,7 +383,9 @@ Node TheoryEngine::rewrite(TNode in) { Debug("theory-rewrite") << "got back " << rse.d_node << " " << thy2 << "[" << *thy2 << "]" << (response.needsMoreRewriting() ? - " MORE-REWRITING" : " DONE") + (response.needsFullRewriting() ? + " FULL-REWRITING" : " MORE-REWRITING") + : " DONE") << endl; if(rse.d_theory != thy2) { Debug("theory-rewrite") << "post-rewritten from " << *rse.d_theory @@ -395,10 +397,40 @@ Node TheoryEngine::rewrite(TNode in) { // rewritten from theory T1 into T2, then back to T1 ? rse.d_topLevel = true; } else { - done = !response.needsMoreRewriting(); + done = response.isDone(); + } + if(response.needsFullRewriting()) { + Debug("theory-rewrite") << "full-rewrite requested for node " + << rse.d_node.getId() << ", invoking..." + << endl; + Node n = rewrite(rse.d_node, rse.d_topLevel); + Debug("theory-rewrite") << "full-rewrite finished for node " + << rse.d_node.getId() << ", got node " + << n << " output." << endl; + rse.d_node = n; + done = true; } } while(!done); + /* If extra-checking is on, do _another_ rewrite before putting + * in the cache to make sure they are the same. This is + * especially necessary if a theory post-rewrites something into + * a term of another theory. */ + if(Debug.isOn("extra-checking") && + !Debug.isOn("$extra-checking:inside-rewrite")) { + ScopedDebug d("$extra-checking:inside-rewrite"); + Node rewrittenAgain = rewrite(rse.d_node, rse.d_topLevel); + Assert(rewrittenAgain == rse.d_node, + "\nExtra-checking assumption failed, " + "node is not completely rewritten.\n\n" + "Original : %s\n" + "Rewritten: %s\n" + "Again : %s\n", + original.toString().c_str(), + rse.d_node.toString().c_str(), + rewrittenAgain.toString().c_str()); + } + setPostRewriteCache(original, wasTopLevel, rse.d_node); out = rse.d_node; |