diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 2 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.h | 2 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 4 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin.cpp | 4 | ||||
-rw-r--r-- | src/theory/theory.h | 61 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 58 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 2 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.h | 2 | ||||
-rw-r--r-- | src/util/output.h | 82 |
9 files changed, 181 insertions, 36 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 5d719aa6f..4d6a95eff 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -340,7 +340,7 @@ RewriteResponse TheoryArith::preRewrite(TNode n, bool topLevel) { } } } - return RewritingComplete(Node(n)); + return RewriteComplete(Node(n)); } Node TheoryArith::rewrite(TNode n){ diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 465adacbc..7d9fd1136 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -116,7 +116,7 @@ public: * Plug in old rewrite to the new (pre,post)rewrite interface. */ RewriteResponse postRewrite(TNode n, bool topLevel) { - return RewritingComplete(topLevel ? rewrite(n) : Node(n)); + return RewriteComplete(topLevel ? rewrite(n) : Node(n)); } /** diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 7bc57bcfb..cf7f16f52 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -39,13 +39,13 @@ public: RewriteResponse preRewrite(TNode in, bool topLevel) { Debug("arrays-rewrite") << "pre-rewriting " << in << " topLevel==" << topLevel << std::endl; - return RewritingComplete(in); + return RewriteComplete(in); } RewriteResponse postRewrite(TNode in, bool topLevel) { Debug("arrays-rewrite") << "post-rewriting " << in << " topLevel==" << topLevel << std::endl; - return RewritingComplete(in); + return RewriteComplete(in); } void check(Effort e); diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp index 6cdcb4032..174e10d2f 100644 --- a/src/theory/builtin/theory_builtin.cpp +++ b/src/theory/builtin/theory_builtin.cpp @@ -54,14 +54,14 @@ Node TheoryBuiltin::blastDistinct(TNode in) { RewriteResponse TheoryBuiltin::preRewrite(TNode in, bool topLevel) { switch(in.getKind()) { case kind::DISTINCT: - return RewritingComplete(blastDistinct(in)); + return RewriteComplete(blastDistinct(in)); case kind::EQUAL: // EQUAL is a special case that should never end up here Unreachable("TheoryBuiltin can't rewrite EQUAL !"); default: - return RewritingComplete(in); + return RewriteComplete(in); } } diff --git a/src/theory/theory.h b/src/theory/theory.h index 8481aa5ff..ccc0a5f82 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -49,12 +49,13 @@ typedef expr::Attribute<PostRewriteCacheTag<false>, Node> PostRewriteCache; /** * Instances of this class serve as response codes from * Theory::preRewrite() and Theory::postRewrite(). Instances of - * derived classes RewritingComplete(n) and RewriteAgain(n) should - * be used for better self-documenting behavior. + * derived classes RewriteComplete(n), RewriteAgain(n), and + * FullRewriteNeeded(n) should be used, giving self-documenting + * rewrite behavior. */ class RewriteResponse { protected: - enum Status { DONE, REWRITE }; + enum Status { DONE, REWRITE, REWRITE_FULL }; RewriteResponse(Status s, Node n) : d_status(s), d_node(n) {} @@ -64,25 +65,55 @@ private: public: bool isDone() const { return d_status == DONE; } - bool needsMoreRewriting() const { return d_status == REWRITE; } + bool needsMoreRewriting() const { return d_status != DONE; } + bool needsFullRewriting() const { return d_status == REWRITE_FULL; } Node getNode() const { return d_node; } -}; +};/* class RewriteResponse */ /** - * Return n, but request additional (pre,post)rewriting of it. + * Signal that (pre,post)rewriting of the Node is complete at n. Note + * that if theory A returns this, and the Node is in another theory B, + * theory B will still be called on to pre- or postrewrite it. + */ +class RewriteComplete : public RewriteResponse { +public: + RewriteComplete(Node n) : RewriteResponse(DONE, n) {} +};/* class RewriteComplete */ + +/** + * Return n, but request additional rewriting of it; if this is + * returned from preRewrite(), this re-preRewrite()'s the Node. If + * this is returned from postRewrite(), this re-postRewrite()'s the + * Node, but does NOT re-preRewrite() it, nor does it rewrite the + * Node's children. + * + * Note that this is the behavior if a theory returns + * RewriteComplete() for a Node belonging to another theory. */ class RewriteAgain : public RewriteResponse { public: RewriteAgain(Node n) : RewriteResponse(REWRITE, n) {} -}; +};/* class RewriteAgain */ /** - * Signal that (pre,post)rewriting of the node is complete at n. + * Return n, but request an additional complete rewriting pass over + * it. This has the same behavior as RewriteAgain() for + * pre-rewriting. However, in post-rewriting, FullRewriteNeeded will + * _completely_ pre- and post-rewrite the term and the term's children + * (though it will use the cache to elide what calls it can). Use + * with caution; it has bad effects on performance. This might be + * useful if theory A rewrites a term into something quite different, + * and certain child nodes might belong to another theory whose normal + * form is unknown to theory A. For example, if the builtin theory + * post-rewrites (DISTINCT a b c) into pairwise NOT EQUAL expressions, + * the theories owning a, b, and c might need to rewrite that EQUAL. + * (This came up, but the fix was to rewrite DISTINCT in + * pre-rewriting, obviating the problem. See bug #168.) */ -class RewritingComplete : public RewriteResponse { +class FullRewriteNeeded : public RewriteResponse { public: - RewritingComplete(Node n) : RewriteResponse(DONE, n) {} -}; + FullRewriteNeeded(Node n) : RewriteResponse(REWRITE_FULL, n) {} +};/* class FullRewriteNeeded */ /** * Base class for T-solvers. Abstract DPLL(T). @@ -266,26 +297,26 @@ public: /** * Pre-rewrite a term. This default base-class implementation - * simply returns RewritingComplete(n). A theory should never + * simply returns RewriteComplete(n). A theory should never * 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). */ virtual RewriteResponse preRewrite(TNode n, bool topLevel) { Debug("theory-rewrite") << "no pre-rewriting to perform for " << n << std::endl; - return RewritingComplete(n); + return RewriteComplete(n); } /** * Post-rewrite a term. This default base-class implementation - * simply returns RewritingComplete(n). A theory should never + * simply returns RewriteComplete(n). A theory should never * 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). */ virtual RewriteResponse postRewrite(TNode n, bool topLevel) { Debug("theory-rewrite") << "no post-rewriting to perform for " << n << std::endl; - return RewritingComplete(n); + return RewriteComplete(n); } /** 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; diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 865fd83a9..92008cc99 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -172,7 +172,7 @@ class TheoryEngine { * This is the top rewrite entry point, called during preprocessing. * It dispatches to the proper theories to rewrite the given Node. */ - Node rewrite(TNode in); + Node rewrite(TNode in, bool topLevel = true); /** * Replace ITE forms in a node. diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 108102b9f..091fc5156 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -135,7 +135,7 @@ public: * Plug in old rewrite to the new (pre,post)rewrite interface. */ RewriteResponse postRewrite(TNode n, bool topLevel) { - return RewritingComplete(topLevel ? rewrite(n) : Node(n)); + return RewriteComplete(topLevel ? rewrite(n) : Node(n)); } /** diff --git a/src/util/output.h b/src/util/output.h index 651f6b607..87b7f69a6 100644 --- a/src/util/output.h +++ b/src/util/output.h @@ -127,6 +127,41 @@ extern DebugC DebugOut CVC4_PUBLIC; # define Debug if(0) debugNullCvc4Stream #endif /* CVC4_DEBUG */ +class CVC4_PUBLIC ScopedDebug { + std::string d_tag; + bool d_oldSetting; + +public: + + ScopedDebug(std::string tag, bool newSetting = true) : + d_tag(tag) { + d_oldSetting = Debug.isOn(d_tag); + if(newSetting) { + Debug.on(d_tag); + } else { + Debug.off(d_tag); + } + } + + ScopedDebug(const char* tag, bool newSetting = true) : + d_tag(tag) { + d_oldSetting = Debug.isOn(d_tag); + if(newSetting) { + Debug.on(d_tag); + } else { + Debug.off(d_tag); + } + } + + ~ScopedDebug() { + if(d_oldSetting) { + Debug.on(d_tag); + } else { + Debug.off(d_tag); + } + } +};/* class ScopedDebug */ + /** The warning output class */ class CVC4_PUBLIC WarningC { std::ostream *d_os; @@ -286,6 +321,41 @@ extern TraceC TraceOut CVC4_PUBLIC; # define Trace if(0) debugNullCvc4Stream #endif /* CVC4_TRACING */ +class CVC4_PUBLIC ScopedTrace { + std::string d_tag; + bool d_oldSetting; + +public: + + ScopedTrace(std::string tag, bool newSetting = true) : + d_tag(tag) { + d_oldSetting = Trace.isOn(d_tag); + if(newSetting) { + Trace.on(d_tag); + } else { + Trace.off(d_tag); + } + } + + ScopedTrace(const char* tag, bool newSetting = true) : + d_tag(tag) { + d_oldSetting = Trace.isOn(d_tag); + if(newSetting) { + Trace.on(d_tag); + } else { + Trace.off(d_tag); + } + } + + ~ScopedTrace() { + if(d_oldSetting) { + Trace.on(d_tag); + } else { + Trace.off(d_tag); + } + } +};/* class ScopedTrace */ + #else /* ! CVC4_MUZZLE */ # define Debug if(0) debugNullCvc4Stream @@ -295,6 +365,18 @@ extern TraceC TraceOut CVC4_PUBLIC; # define Chat if(0) nullCvc4Stream # define Trace if(0) debugNullCvc4Stream +class CVC4_PUBLIC ScopedDebug { +public: + ScopedDebug(std::string tag, bool newSetting = true) {} + ScopedDebug(const char* tag, bool newSetting = true) {} +};/* class ScopedDebug */ + +class CVC4_PUBLIC ScopedTrace { +public: + ScopedTrace(std::string tag, bool newSetting = true) {} + ScopedTrace(const char* tag, bool newSetting = true) {} +};/* class ScopedTrace */ + #endif /* ! CVC4_MUZZLE */ /** |