diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-07-04 06:31:05 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-07-04 06:31:05 +0000 |
commit | 18e073e53b49f24539f29a68e8ec905dd628e9d3 (patch) | |
tree | ac8d456f423a1952c52a194dcb2d2bdeb93d2933 /src/util/output.h | |
parent | 78f7f12f981982bc54435828aea224f785ec3f87 (diff) |
fix to production build
Diffstat (limited to 'src/util/output.h')
-rw-r--r-- | src/util/output.h | 94 |
1 files changed, 59 insertions, 35 deletions
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 |