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 /test/unit | |
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 'test/unit')
-rw-r--r-- | test/unit/theory/theory_engine_white.h | 4 |
1 files changed, 2 insertions, 2 deletions
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() { |