summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/arith/theory_arith.cpp2
-rw-r--r--src/theory/arith/theory_arith.h2
-rw-r--r--src/theory/arrays/theory_arrays.h4
-rw-r--r--src/theory/builtin/theory_builtin.cpp4
-rw-r--r--src/theory/theory.h61
-rw-r--r--src/theory/theory_engine.cpp58
-rw-r--r--src/theory/theory_engine.h2
-rw-r--r--src/theory/uf/theory_uf.h2
-rw-r--r--src/util/output.h82
-rwxr-xr-xtest/regress/run_regression2
-rw-r--r--test/unit/theory/theory_engine_white.h4
11 files changed, 184 insertions, 39 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 */
/**
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() {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback