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.h | |
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.h')
-rw-r--r-- | src/theory/theory.h | 61 |
1 files changed, 46 insertions, 15 deletions
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); } /** |