diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-04-15 13:04:55 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-15 20:04:55 +0000 |
commit | 77bca094a140b35341257f125a55212ff0108250 (patch) | |
tree | 1d3369b9be5fc4c3e8cb279ae5ea662e59cbcb3e /src/base/output.h | |
parent | 63647b1d79df6f287ea6599958b16fce44b8271d (diff) |
Rename occurrences of CVC4 to CVC5. (#6351)
This renames everything but GitHub links and build system related
macros. Switching the build system to cvc5 will be the last step in the
renaming process.
Diffstat (limited to 'src/base/output.h')
-rw-r--r-- | src/base/output.h | 96 |
1 files changed, 52 insertions, 44 deletions
diff --git a/src/base/output.h b/src/base/output.h index 9a7fc3f36..9d4b4389f 100644 --- a/src/base/output.h +++ b/src/base/output.h @@ -60,7 +60,7 @@ extern null_streambuf null_sb; /** A null output stream singleton */ extern std::ostream null_os CVC4_EXPORT; -class CVC4_EXPORT CVC4ostream +class CVC4_EXPORT CVC5ostream { static const std::string s_tab; static const int s_indentIosIndex; @@ -74,18 +74,13 @@ class CVC4_EXPORT CVC4ostream std::ostream& (*const d_endl)(std::ostream&); // do not allow use - CVC4ostream& operator=(const CVC4ostream&); + CVC5ostream& operator=(const CVC5ostream&); -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) { + public: + CVC5ostream() : d_os(NULL), d_firstColumn(false), d_endl(&std::endl) {} + explicit CVC5ostream(std::ostream* os) + : d_os(os), d_firstColumn(true), d_endl(&std::endl) + { } void pushIndent() { @@ -102,7 +97,8 @@ public: } } - CVC4ostream& flush() { + CVC5ostream& flush() + { if(d_os != NULL) { d_os->flush(); } @@ -115,10 +111,11 @@ public: std::ostream* getStreamPointer() const { return d_os; } template <class T> - CVC4ostream& operator<<(T const& t) CVC4_EXPORT; + CVC5ostream& operator<<(T const& t) CVC4_EXPORT; // support manipulators, endl, etc.. - CVC4ostream& operator<<(std::ostream& (*pf)(std::ostream&)) { + CVC5ostream& operator<<(std::ostream& (*pf)(std::ostream&)) + { if(d_os != NULL) { d_os = &(*d_os << pf); @@ -128,35 +125,41 @@ public: } return *this; } - CVC4ostream& operator<<(std::ios& (*pf)(std::ios&)) { + CVC5ostream& 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&)) { + CVC5ostream& operator<<(std::ios_base& (*pf)(std::ios_base&)) + { if(d_os != NULL) { d_os = &(*d_os << pf); } return *this; } - CVC4ostream& operator<<(CVC4ostream& (*pf)(CVC4ostream&)) { + CVC5ostream& operator<<(CVC5ostream& (*pf)(CVC5ostream&)) + { return pf(*this); } -}; /* class CVC4ostream */ +}; /* class CVC5ostream */ -inline CVC4ostream& push(CVC4ostream& stream) { +inline CVC5ostream& push(CVC5ostream& stream) +{ stream.pushIndent(); return stream; } -inline CVC4ostream& pop(CVC4ostream& stream) { +inline CVC5ostream& pop(CVC5ostream& stream) +{ stream.popIndent(); return stream; } template <class T> -CVC4ostream& CVC4ostream::operator<<(T const& t) { +CVC5ostream& CVC5ostream::operator<<(T const& t) +{ if(d_os != NULL) { if(d_firstColumn) { d_firstColumn = false; @@ -179,7 +182,7 @@ class NullC { public: operator bool() const { return false; } - operator CVC4ostream() const { return CVC4ostream(); } + operator CVC5ostream() const { return CVC5ostream(); } operator std::ostream&() const { return null_os; } }; /* class NullC */ @@ -194,12 +197,12 @@ class DebugC public: explicit DebugC(std::ostream* os) : d_os(os) {} - CVC4ostream operator()(const std::string& tag) const + CVC5ostream operator()(const std::string& tag) const { if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) { - return CVC4ostream(d_os); + return CVC5ostream(d_os); } else { - return CVC4ostream(); + return CVC5ostream(); } } @@ -234,7 +237,7 @@ class WarningC public: explicit WarningC(std::ostream* os) : d_os(os) {} - CVC4ostream operator()() const { return CVC4ostream(d_os); } + CVC5ostream operator()() const { return CVC5ostream(d_os); } std::ostream& setStream(std::ostream* os) { d_os = os; return *d_os; } std::ostream& getStream() const { return *d_os; } @@ -244,7 +247,7 @@ public: // 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. + // once for a given run of cvc5. bool warnOnce(const std::string& file, size_t line) { std::pair<std::string, size_t> pr = std::make_pair(file, line); @@ -268,7 +271,7 @@ class MessageC public: explicit MessageC(std::ostream* os) : d_os(os) {} - CVC4ostream operator()() const { return CVC4ostream(d_os); } + CVC5ostream operator()() const { return CVC5ostream(d_os); } std::ostream& setStream(std::ostream* os) { d_os = os; return *d_os; } std::ostream& getStream() const { return *d_os; } @@ -285,7 +288,7 @@ class NoticeC public: explicit NoticeC(std::ostream* os) : d_os(os) {} - CVC4ostream operator()() const { return CVC4ostream(d_os); } + CVC5ostream operator()() const { return CVC5ostream(d_os); } std::ostream& setStream(std::ostream* os) { d_os = os; return *d_os; } std::ostream& getStream() const { return *d_os; } @@ -302,7 +305,7 @@ class ChatC public: explicit ChatC(std::ostream* os) : d_os(os) {} - CVC4ostream operator()() const { return CVC4ostream(d_os); } + CVC5ostream operator()() const { return CVC5ostream(d_os); } std::ostream& setStream(std::ostream* os) { d_os = os; return *d_os; } std::ostream& getStream() const { return *d_os; } @@ -320,12 +323,12 @@ class TraceC public: explicit TraceC(std::ostream* os) : d_os(os) {} - CVC4ostream operator()(std::string tag) const + CVC5ostream operator()(std::string tag) const { if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) { - return CVC4ostream(d_os); + return CVC5ostream(d_os); } else { - return CVC4ostream(); + return CVC5ostream(); } } @@ -367,11 +370,12 @@ public: explicit DumpOutC(std::ostream* os) : d_os(os) {} - CVC4ostream operator()(std::string tag) { + CVC5ostream operator()(std::string tag) + { if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) { - return CVC4ostream(d_os); + return CVC5ostream(d_os); } else { - return CVC4ostream(); + return CVC5ostream(); } } @@ -417,7 +421,7 @@ extern DumpOutC DumpOutChannel CVC4_EXPORT; ::cvc5::__cvc4_true() ? ::cvc5::nullCvc4Stream : ::cvc5::WarningChannel #define WarningOnce \ ::cvc5::__cvc4_true() ? ::cvc5::nullCvc4Stream : ::cvc5::WarningChannel -#define CVC4Message \ +#define CVC5Message \ ::cvc5::__cvc4_true() ? ::cvc5::nullCvc4Stream : ::cvc5::MessageChannel #define Notice \ ::cvc5::__cvc4_true() ? ::cvc5::nullCvc4Stream : ::cvc5::NoticeChannel @@ -444,7 +448,7 @@ extern DumpOutC DumpOutChannel CVC4_EXPORT; || !::cvc5::WarningChannel.warnOnce(__FILE__, __LINE__)) \ ? ::cvc5::nullCvc4Stream \ : ::cvc5::WarningChannel -#define CVC4Message \ +#define CVC5Message \ (!::cvc5::MessageChannel.isOn()) ? ::cvc5::nullCvc4Stream \ : ::cvc5::MessageChannel #define Notice \ @@ -565,17 +569,21 @@ class ScopedTrace */ class IndentedScope { - CVC4ostream d_out; -public: - inline IndentedScope(CVC4ostream out); + CVC5ostream d_out; + + public: + inline IndentedScope(CVC5ostream out); inline ~IndentedScope(); }; /* class IndentedScope */ #if defined(CVC5_DEBUG) && defined(CVC5_TRACING) -inline IndentedScope::IndentedScope(CVC4ostream out) : d_out(out) { d_out << push; } +inline IndentedScope::IndentedScope(CVC5ostream out) : d_out(out) +{ + d_out << push; +} inline IndentedScope::~IndentedScope() { d_out << pop; } #else /* CVC5_DEBUG && CVC5_TRACING */ -inline IndentedScope::IndentedScope(CVC4ostream out) {} +inline IndentedScope::IndentedScope(CVC5ostream out) {} inline IndentedScope::~IndentedScope() {} #endif /* CVC5_DEBUG && CVC5_TRACING */ |