diff options
Diffstat (limited to 'src/util/output.cpp')
-rw-r--r-- | src/util/output.cpp | 36 |
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 */ |