diff options
| -rw-r--r-- | src/base/output.h | 2 | ||||
| -rw-r--r-- | src/smt_util/dump.cpp | 6 |
2 files changed, 5 insertions, 3 deletions
diff --git a/src/base/output.h b/src/base/output.h index 4bffad85f..9d1ab03ae 100644 --- a/src/base/output.h +++ b/src/base/output.h @@ -110,6 +110,8 @@ public: bool isConnected() { return d_os != NULL; } operator std::ostream&() { return isConnected() ? *d_os : null_os; } + std::ostream* getStreamPointer() { return d_os; } + template <class T> CVC4ostream& operator<<(T const& t) CVC4_PUBLIC; diff --git a/src/smt_util/dump.cpp b/src/smt_util/dump.cpp index 218691bd0..66cb6e3d1 100644 --- a/src/smt_util/dump.cpp +++ b/src/smt_util/dump.cpp @@ -22,11 +22,11 @@ namespace CVC4 { DumpC DumpChannel CVC4_PUBLIC; std::ostream& DumpC::setStream(std::ostream* os) { - DumpOut.setStream(os); + ::CVC4::DumpOutChannel.setStream(os); return *os; } -std::ostream& DumpC::getStream() { return DumpOut.getStream(); } -std::ostream* DumpC::getStreamPointer() { return DumpOut.getStreamPointer(); } +std::ostream& DumpC::getStream() { return ::CVC4::DumpOutChannel.getStream(); } +std::ostream* DumpC::getStreamPointer() { return ::CVC4::DumpOutChannel.getStreamPointer(); } void DumpC::setDumpFromString(const std::string& optarg) { |