summaryrefslogtreecommitdiff
path: root/src/base/output.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/base/output.h')
-rw-r--r--src/base/output.h96
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback