diff options
Diffstat (limited to 'src/util/output.h')
| -rw-r--r-- | src/util/output.h | 125 |
1 files changed, 49 insertions, 76 deletions
diff --git a/src/util/output.h b/src/util/output.h index f21fc39e7..b0e210c17 100644 --- a/src/util/output.h +++ b/src/util/output.h @@ -11,7 +11,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief Output utility classes and functions. + ** \brief Output utility classes and functions ** ** Output utility classes and functions. **/ @@ -58,8 +58,6 @@ extern null_streambuf null_sb; /** A null output stream singleton */ extern std::ostream null_os CVC4_PUBLIC; -#ifndef CVC4_MUZZLE - class CVC4_PUBLIC CVC4ostream { std::ostream* d_os; // Current indentation @@ -281,35 +279,57 @@ public: /** The debug output singleton */ extern DebugC DebugChannel CVC4_PUBLIC; -#ifdef CVC4_DEBUG -# define Debug ::CVC4::DebugChannel -#else /* CVC4_DEBUG */ -# define Debug ::CVC4::__cvc4_true() ? ::CVC4::debugNullCvc4Stream : ::CVC4::DebugChannel -#endif /* CVC4_DEBUG */ - /** The warning output singleton */ -extern WarningC Warning CVC4_PUBLIC; -#define Warning() (! ::CVC4::Warning.isOn()) ? ::CVC4::debugNullCvc4Stream : ::CVC4::Warning() - +extern WarningC WarningChannel CVC4_PUBLIC; /** The message output singleton */ -extern MessageC Message CVC4_PUBLIC; -#define Message() (! ::CVC4::Message.isOn()) ? ::CVC4::debugNullCvc4Stream : ::CVC4::Message() - +extern MessageC MessageChannel CVC4_PUBLIC; /** The notice output singleton */ -extern NoticeC Notice CVC4_PUBLIC; -#define Notice() (! ::CVC4::Notice.isOn()) ? ::CVC4::debugNullCvc4Stream : ::CVC4::Notice() - +extern NoticeC NoticeChannel CVC4_PUBLIC; /** The chat output singleton */ -extern ChatC Chat CVC4_PUBLIC; -#define Chat() (! ::CVC4::Chat.isOn()) ? ::CVC4::debugNullCvc4Stream : ::CVC4::Chat() - +extern ChatC ChatChannel CVC4_PUBLIC; /** The trace output singleton */ extern TraceC TraceChannel CVC4_PUBLIC; -#ifdef CVC4_TRACING -# define Trace ::CVC4::TraceChannel -#else /* CVC4_TRACING */ -# define Trace ::CVC4::__cvc4_true() ? ::CVC4::debugNullCvc4Stream : ::CVC4::TraceChannel -#endif /* CVC4_TRACING */ + +#ifdef CVC4_MUZZLE + +# define Debug ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::DebugChannel +# define Warning ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel +# define Message ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::MessageChannel +# define Notice ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::NoticeChannel +# define Chat ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::ChatChannel +# define Trace ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::TraceChannel + +inline int DebugC::printf(const char* tag, const char* fmt, ...) { return 0; } +inline int DebugC::printf(std::string tag, const char* fmt, ...) { return 0; } +inline int WarningC::printf(const char* fmt, ...) { return 0; } +inline int MessageC::printf(const char* fmt, ...) { return 0; } +inline int NoticeC::printf(const char* fmt, ...) { return 0; } +inline int ChatC::printf(const char* fmt, ...) { return 0; } +inline int TraceC::printf(const char* tag, const char* fmt, ...) { return 0; } +inline int TraceC::printf(std::string tag, const char* fmt, ...) { return 0; } + +#else /* CVC4_MUZZLE */ + +# ifdef CVC4_DEBUG +# define Debug ::CVC4::DebugChannel +# else /* CVC4_DEBUG */ +# define Debug ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::DebugChannel +inline int DebugC::printf(const char* tag, const char* fmt, ...) { return 0; } +inline int DebugC::printf(std::string tag, const char* fmt, ...) { return 0; } +# endif /* CVC4_DEBUG */ +# define Warning (! ::CVC4::WarningChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel +# define Message (! ::CVC4::MessageChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::MessageChannel +# define Notice (! ::CVC4::NoticeChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::NoticeChannel +# define Chat (! ::CVC4::ChatChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::ChatChannel +# ifdef CVC4_TRACING +# define Trace ::CVC4::TraceChannel +# else /* CVC4_TRACING */ +# define Trace ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::TraceChannel +inline int TraceC::printf(const char* tag, const char* fmt, ...) { return 0; } +inline int TraceC::printf(std::string tag, const char* fmt, ...) { return 0; } +# endif /* CVC4_TRACING */ + +#endif /* CVC4_MUZZLE */ // Disallow e.g. !Debug("foo").isOn() forms // because the ! will apply before the ? . @@ -418,65 +438,18 @@ public: #endif /* CVC4_TRACING */ -#else /* ! CVC4_MUZZLE */ - -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 */ - -extern NullDebugC Debug CVC4_PUBLIC; -extern NullC Warning CVC4_PUBLIC; -extern NullC Message CVC4_PUBLIC; -extern NullC Notice CVC4_PUBLIC; -extern NullC Chat CVC4_PUBLIC; -extern NullDebugC Trace CVC4_PUBLIC; - -#endif /* ! CVC4_MUZZLE */ - /** - * Same shape as DebugC/TraceC, but does nothing; designed for - * compilation of non-debug/non-trace builds. None of these should ever be called - * in such builds, but we offer this to the compiler so it doesn't complain. + * Does nothing; designed for compilation of non-debug/non-trace + * builds. None of these should ever be called in such builds, but we + * offer this to the compiler so it doesn't complain. */ -class CVC4_PUBLIC NullDebugC { -public: - operator bool() { return false; } - operator CVC4ostream() { return CVC4ostream(); } - operator std::ostream&() { return null_os; } -};/* class NullDebugC */ - -/** - * Same shape as WarningC/etc., but does nothing; designed for - * compilation of muzzled builds. None of these should ever be called - * in muzzled builds, but we offer this to the compiler so it doesn't - * complain. */ class CVC4_PUBLIC NullC { public: -/* - NullC() {} - NullC(std::ostream* os) {} - - int printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3))) { return 0; } - - std::ostream& operator()() { return null_os; } - - std::ostream& setStream(std::ostream& os) { return null_os; } - std::ostream& getStream() { return null_os; } -*/ operator bool() { return false; } operator CVC4ostream() { return CVC4ostream(); } operator std::ostream&() { return null_os; } };/* class NullC */ -extern NullDebugC debugNullCvc4Stream CVC4_PUBLIC; extern NullC nullCvc4Stream CVC4_PUBLIC; }/* CVC4 namespace */ |