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/arrays | |
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/arrays')
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 4 |
1 files changed, 2 insertions, 2 deletions
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); |