From: Morgan Deters Date: Sun, 4 Jul 2010 03:59:36 +0000 (+0000) Subject: With "-d extra-checking", rewrites are now checked (after X-Git-Tag: cvc5-1.0.0~8955 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9e15c81c673b2cb325cc21ace39f84b37d8b65c9;p=cvc5.git 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); --- 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, 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 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 */ /** diff --git a/test/regress/run_regression b/test/regress/run_regression index b26792a78..a6ea0797b 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -132,7 +132,7 @@ cvc4base=`basename "$cvc4"` cvc4full="$cvc4dirfull/$cvc4base" echo running $cvc4full `basename "$benchmark"` from `dirname "$benchmark"` ( cd `dirname "$benchmark"`; - "$cvc4full" --segv-nospin `basename "$benchmark"`; + "$cvc4full" -d extra-checking --segv-nospin `basename "$benchmark"`; echo $? >"$exitstatusfile" ) > "$outfile" 2> "$errfile" diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index 715799435..addf15af3 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -119,7 +119,7 @@ public: TS_ASSERT_EQUALS(expected.d_node, n); TS_ASSERT_EQUALS(expected.d_topLevel, topLevel); - return RewritingComplete(n); + return RewriteComplete(n); } RewriteResponse postRewrite(TNode n, bool topLevel) { @@ -147,7 +147,7 @@ public: TS_ASSERT_EQUALS(expected.d_node, n); TS_ASSERT_EQUALS(expected.d_topLevel, topLevel); - return RewritingComplete(n); + return RewriteComplete(n); } std::string identify() const throw() {