1 files changed, 36 insertions, 0 deletions
diff --git a/src/util/output.cpp b/src/util/output.cpp
index 29de4c360..3823f7be6 100644
--- a/src/util/output.cpp
+++ b/src/util/output.cpp
@@ -40,6 +40,8 @@ MessageC MessageChannel CVC4_PUBLIC (&cout);
 NoticeC NoticeChannel CVC4_PUBLIC (&cout);
 ChatC ChatChannel CVC4_PUBLIC (&cout);
 TraceC TraceChannel CVC4_PUBLIC (&cout);
+std::ostream DumpC::dump_cout(cout.rdbuf());// copy cout stream buffer
+DumpC DumpChannel CVC4_PUBLIC (&DumpC::dump_cout);
 
 #ifndef CVC4_MUZZLE
 
@@ -155,6 +157,40 @@ int TraceC::printf(std::string tag, const char* fmt, ...) {
 
 #  endif /* CVC4_TRACING */
 
+#  ifdef CVC4_DUMPING
+
+int DumpC::printf(const char* tag, const char* fmt, ...) {
+  if(d_tags.find(string(tag)) == d_tags.end()) {
+    return 0;
+  }
+
+  // chop off output after 1024 bytes
+  char buf[1024];
+  va_list vl;
+  va_start(vl, fmt);
+  int retval = vsnprintf(buf, sizeof(buf), fmt, vl);
+  va_end(vl);
+  *d_os << buf;
+  return retval;
+}
+
+int DumpC::printf(std::string tag, const char* fmt, ...) {
+  if(d_tags.find(tag) == d_tags.end()) {
+    return 0;
+  }
+
+  // chop off output after 1024 bytes
+  char buf[1024];
+  va_list vl;
+  va_start(vl, fmt);
+  int retval = vsnprintf(buf, sizeof(buf), fmt, vl);
+  va_end(vl);
+  *d_os << buf;
+  return retval;
+}
+
+#  endif /* CVC4_DUMPING */
+
 #endif /* ! CVC4_MUZZLE */
 
 }/* CVC4 namespace */