diff options
Diffstat (limited to 'src/util/output.h')
-rw-r--r-- | src/util/output.h | 590 |
1 files changed, 0 insertions, 590 deletions
diff --git a/src/util/output.h b/src/util/output.h deleted file mode 100644 index 0974591db..000000000 --- a/src/util/output.h +++ /dev/null @@ -1,590 +0,0 @@ -/********************* */ -/*! \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 */ |