diff options
Diffstat (limited to 'src/base/output.h')
-rw-r--r-- | src/base/output.h | 590 |
1 files changed, 590 insertions, 0 deletions
diff --git a/src/base/output.h b/src/base/output.h new file mode 100644 index 000000000..0974591db --- /dev/null +++ b/src/base/output.h @@ -0,0 +1,590 @@ +/********************* */ +/*! \file output.h + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): Tim King, Dejan Jovanovic + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Output utility classes and functions + ** + ** Output utility classes and functions. + **/ + +#include "cvc4_private_library.h" + +#ifndef __CVC4__OUTPUT_H +#define __CVC4__OUTPUT_H + +#include <ios> +#include <iostream> +#include <streambuf> +#include <string> +#include <cstdio> +#include <cstdarg> +#include <set> +#include <utility> + +namespace CVC4 { + +template <class T, class U> +std::ostream& operator<<(std::ostream& out, const std::pair<T, U>& p) CVC4_PUBLIC; + +template <class T, class U> +std::ostream& operator<<(std::ostream& out, const std::pair<T, U>& p) { + return out << "[" << p.first << "," << p.second << "]"; +} + +/** + * A utility class to provide (essentially) a "/dev/null" streambuf. + * If debugging support is compiled in, but debugging for + * e.g. "parser" is off, then Debug("parser") returns a stream + * attached to a null_streambuf instance so that output is directed to + * the bit bucket. + */ +class CVC4_PUBLIC null_streambuf : public std::streambuf { +public: + /* Overriding overflow() just ensures that EOF isn't returned on the + * stream. Perhaps this is not so critical, but recommended; this + * way the output stream looks like it's functioning, in a non-error + * state. */ + int overflow(int c) { return c; } +};/* class null_streambuf */ + +/** A null stream-buffer singleton */ +extern null_streambuf null_sb; +/** A null output stream singleton */ +extern std::ostream null_os CVC4_PUBLIC; + +class CVC4_PUBLIC CVC4ostream { + static const std::string s_tab; + static const int s_indentIosIndex; + + /** The underlying ostream */ + std::ostream* d_os; + /** Are we in the first column? */ + bool d_firstColumn; + + /** The endl manipulator (why do we need to keep this?) */ + std::ostream& (*const d_endl)(std::ostream&); + + // do not allow use + CVC4ostream& operator=(const CVC4ostream&); + +public: + CVC4ostream() : + d_os(NULL), + d_firstColumn(false), + d_endl(&std::endl) { + } + explicit CVC4ostream(std::ostream* os) : + d_os(os), + d_firstColumn(true), + d_endl(&std::endl) { + } + + void pushIndent() { + if(d_os != NULL) { + ++d_os->iword(s_indentIosIndex); + } + } + void popIndent() { + if(d_os != NULL) { + long& indent = d_os->iword(s_indentIosIndex); + if(indent > 0) { + --indent; + } + } + } + + CVC4ostream& flush() { + if(d_os != NULL) { + d_os->flush(); + } + return *this; + } + + bool isConnected() { return d_os != NULL; } + operator std::ostream&() { return isConnected() ? *d_os : null_os; } + + template <class T> + CVC4ostream& operator<<(T const& t) CVC4_PUBLIC; + + // support manipulators, endl, etc.. + CVC4ostream& operator<<(std::ostream& (*pf)(std::ostream&)) { + if(d_os != NULL) { + d_os = &(*d_os << pf); + + if(pf == d_endl) { + d_firstColumn = true; + } + } + return *this; + } + CVC4ostream& operator<<(std::ios& (*pf)(std::ios&)) { + if(d_os != NULL) { + d_os = &(*d_os << pf); + } + return *this; + } + CVC4ostream& operator<<(std::ios_base& (*pf)(std::ios_base&)) { + if(d_os != NULL) { + d_os = &(*d_os << pf); + } + return *this; + } + CVC4ostream& operator<<(CVC4ostream& (*pf)(CVC4ostream&)) { + return pf(*this); + } +};/* class CVC4ostream */ + +inline CVC4ostream& push(CVC4ostream& stream) { + stream.pushIndent(); + return stream; +} + +inline CVC4ostream& pop(CVC4ostream& stream) { + stream.popIndent(); + return stream; +} + +template <class T> +CVC4ostream& CVC4ostream::operator<<(T const& t) { + if(d_os != NULL) { + if(d_firstColumn) { + d_firstColumn = false; + long indent = d_os->iword(s_indentIosIndex); + for(long i = 0; i < indent; ++i) { + d_os = &(*d_os << s_tab); + } + } + d_os = &(*d_os << t); + } + return *this; +} + +/** + * 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 NullC { +public: + operator bool() { return false; } + operator CVC4ostream() { return CVC4ostream(); } + operator std::ostream&() { return null_os; } +};/* class NullC */ + +extern NullC nullCvc4Stream CVC4_PUBLIC; + +/** The debug output class */ +class CVC4_PUBLIC DebugC { + std::set<std::string> d_tags; + std::ostream* d_os; + +public: + explicit DebugC(std::ostream* os) : d_os(os) {} + + int printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4))); + int printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4))); + + CVC4ostream operator()(const char* tag) { + if(!d_tags.empty() && d_tags.find(std::string(tag)) != d_tags.end()) { + return CVC4ostream(d_os); + } else { + return CVC4ostream(); + } + } + CVC4ostream operator()(std::string tag) { + if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) { + return CVC4ostream(d_os); + } else { + return CVC4ostream(); + } + } + + bool on (const char* tag) { d_tags.insert(std::string(tag)); return true; } + bool on (std::string tag) { d_tags.insert(tag); return true; } + bool off(const char* tag) { d_tags.erase (std::string(tag)); return false; } + bool off(std::string tag) { d_tags.erase (tag); return false; } + bool off() { d_tags.clear(); return false; } + + bool isOn(const char* tag) { return d_tags.find(std::string(tag)) != d_tags.end(); } + bool isOn(std::string tag) { return d_tags.find(tag) != d_tags.end(); } + + std::ostream& setStream(std::ostream& os) { d_os = &os; return os; } + std::ostream& getStream() { return *d_os; } +};/* class DebugC */ + +/** The warning output class */ +class CVC4_PUBLIC WarningC { + std::set< std::pair<const char*, size_t> > d_alreadyWarned; + std::ostream* d_os; + +public: + explicit WarningC(std::ostream* os) : d_os(os) {} + + int printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3))); + + CVC4ostream operator()() { return CVC4ostream(d_os); } + + std::ostream& setStream(std::ostream& os) { d_os = &os; return os; } + std::ostream& getStream() { return *d_os; } + + bool isOn() const { return d_os != &null_os; } + + // This function supports the WarningOnce() macro, which allows you + // to easily indicate that a warning should be emitted, but only + // once for a given run of CVC4. + bool warnOnce(const char* file, size_t line) { + std::pair<const char*, size_t> pr = std::make_pair(file, line); + if(d_alreadyWarned.find(pr) != d_alreadyWarned.end()) { + // signal caller not to warn again + return false; + } + + // okay warn this time, but don't do it again + d_alreadyWarned.insert(pr); + return true; + } + +};/* class WarningC */ + +/** The message output class */ +class CVC4_PUBLIC MessageC { + std::ostream* d_os; + +public: + explicit MessageC(std::ostream* os) : d_os(os) {} + + int printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3))); + + CVC4ostream operator()() { return CVC4ostream(d_os); } + + std::ostream& setStream(std::ostream& os) { d_os = &os; return os; } + std::ostream& getStream() { return *d_os; } + + bool isOn() const { return d_os != &null_os; } +};/* class MessageC */ + +/** The notice output class */ +class CVC4_PUBLIC NoticeC { + std::ostream* d_os; + +public: + explicit NoticeC(std::ostream* os) : d_os(os) {} + + int printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3))); + + CVC4ostream operator()() { return CVC4ostream(d_os); } + + std::ostream& setStream(std::ostream& os) { d_os = &os; return os; } + std::ostream& getStream() { return *d_os; } + + bool isOn() const { return d_os != &null_os; } +};/* class NoticeC */ + +/** The chat output class */ +class CVC4_PUBLIC ChatC { + std::ostream* d_os; + +public: + explicit ChatC(std::ostream* os) : d_os(os) {} + + int printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3))); + + CVC4ostream operator()() { return CVC4ostream(d_os); } + + std::ostream& setStream(std::ostream& os) { d_os = &os; return os; } + std::ostream& getStream() { return *d_os; } + + bool isOn() const { return d_os != &null_os; } +};/* class ChatC */ + +/** The trace output class */ +class CVC4_PUBLIC TraceC { + std::ostream* d_os; + std::set<std::string> d_tags; + +public: + explicit TraceC(std::ostream* os) : d_os(os) {} + + int printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4))); + int printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4))); + + CVC4ostream operator()(const char* tag) { + if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) { + return CVC4ostream(d_os); + } else { + return CVC4ostream(); + } + } + + CVC4ostream operator()(std::string tag) { + if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) { + return CVC4ostream(d_os); + } else { + return CVC4ostream(); + } + } + + bool on (const char* tag) { d_tags.insert(std::string(tag)); return true; } + bool on (std::string tag) { d_tags.insert(tag); return true; } + bool off(const char* tag) { d_tags.erase (std::string(tag)); return false; } + bool off(std::string tag) { d_tags.erase (tag); return false; } + bool off() { d_tags.clear(); return false; } + + bool isOn(const char* tag) { return d_tags.find(std::string(tag)) != d_tags.end(); } + bool isOn(std::string tag) { return d_tags.find(tag) != d_tags.end(); } + + std::ostream& setStream(std::ostream& os) { d_os = &os; return os; } + std::ostream& getStream() { return *d_os; } +};/* class TraceC */ + +/** The dump output class */ +class CVC4_PUBLIC DumpOutC { + std::set<std::string> d_tags; + std::ostream* d_os; + +public: + /** + * A copy of cout for use by the dumper. This is important because + * it has different settings (e.g., the expr printing depth is always + * unlimited). */ + static std::ostream dump_cout; + + explicit DumpOutC(std::ostream* os) : d_os(os) {} + + int printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4))); + int printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4))); + + CVC4ostream operator()(const char* tag) { + if(!d_tags.empty() && d_tags.find(std::string(tag)) != d_tags.end()) { + return CVC4ostream(d_os); + } else { + return CVC4ostream(); + } + } + CVC4ostream operator()(std::string tag) { + if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) { + return CVC4ostream(d_os); + } else { + return CVC4ostream(); + } + } + + bool on (const char* tag) { d_tags.insert(std::string(tag)); return true; } + bool on (std::string tag) { d_tags.insert(tag); return true; } + bool off(const char* tag) { d_tags.erase (std::string(tag)); return false; } + bool off(std::string tag) { d_tags.erase (tag); return false; } + bool off() { d_tags.clear(); return false; } + + bool isOn(const char* tag) { return d_tags.find(std::string(tag)) != d_tags.end(); } + bool isOn(std::string tag) { return d_tags.find(tag) != d_tags.end(); } + + std::ostream& setStream(std::ostream& os) { d_os = &os; return os; } + std::ostream& getStream() { return *d_os; } +};/* class DumpOutC */ + +/** The debug output singleton */ +extern DebugC DebugChannel CVC4_PUBLIC; +/** The warning output singleton */ +extern WarningC WarningChannel CVC4_PUBLIC; +/** The message output singleton */ +extern MessageC MessageChannel CVC4_PUBLIC; +/** The notice output singleton */ +extern NoticeC NoticeChannel CVC4_PUBLIC; +/** The chat output singleton */ +extern ChatC ChatChannel CVC4_PUBLIC; +/** The trace output singleton */ +extern TraceC TraceChannel CVC4_PUBLIC; +/** The dump output singleton */ +extern DumpOutC DumpOutChannel CVC4_PUBLIC; + +#ifdef CVC4_MUZZLE + +# define Debug ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::DebugChannel +# define Warning ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel +# define WarningOnce ::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 +# define DumpOut ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::DumpOutChannel + +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; } +inline int DumpOutC::printf(const char* tag, const char* fmt, ...) { return 0; } +inline int DumpOutC::printf(std::string tag, const char* fmt, ...) { return 0; } + +#else /* CVC4_MUZZLE */ + +# if defined(CVC4_DEBUG) && defined(CVC4_TRACING) +# define Debug ::CVC4::DebugChannel +# else /* CVC4_DEBUG && CVC4_TRACING */ +# 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 && CVC4_TRACING */ +# define Warning (! ::CVC4::WarningChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel +# define WarningOnce (! ::CVC4::WarningChannel.isOn() || ! ::CVC4::WarningChannel.warnOnce(__FILE__,__LINE__)) ? ::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 */ +# ifdef CVC4_DUMPING +# define DumpOut ::CVC4::DumpOutChannel +# else /* CVC4_DUMPING */ +# define DumpOut ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::DumpOutChannel +inline int DumpOutC::printf(const char* tag, const char* fmt, ...) { return 0; } +inline int DumpOutC::printf(std::string tag, const char* fmt, ...) { return 0; } +# endif /* CVC4_DUMPING */ + +#endif /* CVC4_MUZZLE */ + +// Disallow e.g. !Debug("foo").isOn() forms +// because the ! will apply before the ? . +// If a compiler error has directed you here, +// just parenthesize it e.g. !(Debug("foo").isOn()) +class __cvc4_true { + void operator!() CVC4_UNUSED; + void operator~() CVC4_UNUSED; + void operator-() CVC4_UNUSED; + void operator+() CVC4_UNUSED; +public: + inline operator bool() { return true; } +};/* __cvc4_true */ + +#if defined(CVC4_DEBUG) && defined(CVC4_TRACING) + +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 */ + +#else /* CVC4_DEBUG && CVC4_TRACING */ + +class CVC4_PUBLIC ScopedDebug { +public: + ScopedDebug(std::string tag, bool newSetting = true) {} + ScopedDebug(const char* tag, bool newSetting = true) {} +};/* class ScopedDebug */ + +#endif /* CVC4_DEBUG && CVC4_TRACING */ + +#ifdef 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_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 */ + +/** + * Pushes an indentation level on construction, pop on destruction. + * Useful for tracing recursive functions especially, but also can be + * used for clearly separating different phases of an algorithm, + * or iterations of a loop, or... etc. + */ +class CVC4_PUBLIC IndentedScope { + CVC4ostream d_out; +public: + inline IndentedScope(CVC4ostream out); + inline ~IndentedScope(); +};/* class IndentedScope */ + +#if defined(CVC4_DEBUG) && defined(CVC4_TRACING) +inline IndentedScope::IndentedScope(CVC4ostream out) : d_out(out) { d_out << push; } +inline IndentedScope::~IndentedScope() { d_out << pop; } +#else /* CVC4_DEBUG && CVC4_TRACING */ +inline IndentedScope::IndentedScope(CVC4ostream out) {} +inline IndentedScope::~IndentedScope() {} +#endif /* CVC4_DEBUG && CVC4_TRACING */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__OUTPUT_H */ |