diff options
| -rw-r--r-- | src/theory/theory_engine.cpp | 4 | ||||
| -rw-r--r-- | src/util/output.h | 94 |
2 files changed, 61 insertions, 37 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 03678e30e..096c99c06 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -416,8 +416,8 @@ Node TheoryEngine::rewrite(TNode in, bool topLevel) { * 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")) { + if(debugTagIsOn("extra-checking") && + !debugTagIsOn("$extra-checking:inside-rewrite")) { ScopedDebug d("$extra-checking:inside-rewrite"); Node rewrittenAgain = rewrite(rse.d_node, rse.d_topLevel); Assert(rewrittenAgain == rse.d_node, diff --git a/src/util/output.h b/src/util/output.h index 87b7f69a6..851868c15 100644 --- a/src/util/output.h +++ b/src/util/output.h @@ -127,41 +127,6 @@ 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; @@ -321,6 +286,55 @@ extern TraceC TraceOut CVC4_PUBLIC; # define Trace if(0) debugNullCvc4Stream #endif /* CVC4_TRACING */ +#ifdef 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 = DebugOut.isOn(d_tag); + if(newSetting) { + DebugOut.on(d_tag); + } else { + DebugOut.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 */ + +#else /* CVC4_DEBUG */ + +class CVC4_PUBLIC ScopedDebug { +public: + ScopedDebug(std::string tag, bool newSetting = true) {} + ScopedDebug(const char* tag, bool newSetting = true) {} +};/* class ScopedDebug */ + +#endif /* CVC4_DEBUG */ + +#ifdef CVC4_TRACING + class CVC4_PUBLIC ScopedTrace { std::string d_tag; bool d_oldSetting; @@ -356,6 +370,16 @@ public: } };/* class ScopedTrace */ +#else /* CVC4_TRACING */ + +class CVC4_PUBLIC ScopedTrace { +public: + ScopedTrace(std::string tag, bool newSetting = true) {} + ScopedTrace(const char* tag, bool newSetting = true) {} +};/* class ScopedTrace */ + +#endif /* CVC4_TRACING */ + #else /* ! CVC4_MUZZLE */ # define Debug if(0) debugNullCvc4Stream |