}
}
}
- return RewritingComplete(Node(n));
+ return RewriteComplete(Node(n));
}
Node TheoryArith::rewrite(TNode n){
* 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));
}
/**
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);
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);
}
}
/**
* 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) {}
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).
/**
* 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);
}
/**
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]));
}
if(somethingChanged) {
-
cachedRewrite = nodeManager->mkNode(node.getKind(), newChildren);
nodeManager->setAttribute(node, theory::IteRewriteAttr(), cachedRewrite);
return cachedRewrite;
/**
* 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) {
}
};
}/* 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);
// 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..
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
// 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);
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
// 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;
* 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.
* 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));
}
/**
# 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;
# 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
# 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 */
/**
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"
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) {
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() {
projects / cvc5.git / commitdiff