diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-02-19 23:10:02 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-02-19 23:10:02 +0000 |
commit | 7697b5218118d71800318472a7423a5b42bee469 (patch) | |
tree | 28f910c4cb5475a3bd70e5669420d55caee4f6d8 /src/util/output.cpp | |
parent | ce0e796ad92f040fb75435bd7880bc28a60b0374 (diff) |
specialized implementation for boolean node attributes ("flags"): they now share memory words properly; also, implementations of some output functionality
Diffstat (limited to 'src/util/output.cpp')
-rw-r--r-- | src/util/output.cpp | 106 |
1 files changed, 98 insertions, 8 deletions
diff --git a/src/util/output.cpp b/src/util/output.cpp index fdc54d9b5..278158ad1 100644 --- a/src/util/output.cpp +++ b/src/util/output.cpp @@ -18,18 +18,108 @@ #include <iostream> #include "util/output.h" +using namespace std; + namespace CVC4 { /* Definitions of the declared globals from output.h... */ null_streambuf null_sb; -std::ostream null_os(&null_sb); - -DebugC DebugOut (&std::cout); -WarningC Warning(&std::cerr); -MessageC Message(&std::cout); -NoticeC Notice (&std::cout); -ChatC Chat (&std::cout); -TraceC Trace (&std::cout); +ostream null_os(&null_sb); + +DebugC DebugOut(&cout); +WarningC Warning (&cerr); +MessageC Message (&cout); +NoticeC Notice (&cout); +ChatC Chat (&cout); +TraceC Trace (&cout); + +void DebugC::printf(const char* tag, const char* fmt, ...) { + if(d_tags.find(string(tag)) != d_tags.end()) { + // chop off output after 1024 bytes + char buf[1024]; + va_list vl; + va_start(vl, fmt); + vsnprintf(buf, sizeof(buf), fmt, vl); + va_end(vl); + *d_os << buf; + } +} + +void DebugC::printf(string tag, const char* fmt, ...) { + if(d_tags.find(tag) != d_tags.end()) { + // chop off output after 1024 bytes + char buf[1024]; + va_list vl; + va_start(vl, fmt); + vsnprintf(buf, sizeof(buf), fmt, vl); + va_end(vl); + *d_os << buf; + } +} + +void WarningC::printf(const char* fmt, ...) { + // chop off output after 1024 bytes + char buf[1024]; + va_list vl; + va_start(vl, fmt); + vsnprintf(buf, sizeof(buf), fmt, vl); + va_end(vl); + *d_os << buf; +} + +void MessageC::printf(const char* fmt, ...) { + // chop off output after 1024 bytes + char buf[1024]; + va_list vl; + va_start(vl, fmt); + vsnprintf(buf, sizeof(buf), fmt, vl); + va_end(vl); + *d_os << buf; +} + +void NoticeC::printf(const char* fmt, ...) { + // chop off output after 1024 bytes + char buf[1024]; + va_list vl; + va_start(vl, fmt); + vsnprintf(buf, sizeof(buf), fmt, vl); + va_end(vl); + *d_os << buf; +} + +void ChatC::printf(const char* fmt, ...) { + // chop off output after 1024 bytes + char buf[1024]; + va_list vl; + va_start(vl, fmt); + vsnprintf(buf, sizeof(buf), fmt, vl); + va_end(vl); + *d_os << buf; +} + +void TraceC::printf(const char* tag, const char* fmt, ...) { + if(d_tags.find(string(tag)) != d_tags.end()) { + // chop off output after 1024 bytes + char buf[1024]; + va_list vl; + va_start(vl, fmt); + vsnprintf(buf, sizeof(buf), fmt, vl); + va_end(vl); + *d_os << buf; + } +} + +void TraceC::printf(string tag, const char* fmt, ...) { + if(d_tags.find(tag) != d_tags.end()) { + // chop off output after 1024 bytes + char buf[1024]; + va_list vl; + va_start(vl, fmt); + vsnprintf(buf, sizeof(buf), fmt, vl); + va_end(vl); + *d_os << buf; + } +} }/* CVC4 namespace */ |