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/util/output.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/util/output.h')
-rw-r--r-- | src/util/output.h | 82 |
1 files changed, 82 insertions, 0 deletions
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 */ /** |