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.h | |
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.h')
-rw-r--r-- | src/util/output.h | 68 |
1 files changed, 43 insertions, 25 deletions
diff --git a/src/util/output.h b/src/util/output.h index f897fd1ca..94841a1f5 100644 --- a/src/util/output.h +++ b/src/util/output.h @@ -57,23 +57,46 @@ class CVC4_PUBLIC DebugC { public: DebugC(std::ostream* os) : d_os(os) {} - void operator()(const char* tag, const char*); - void operator()(const char* tag, std::string); - void operator()(std::string tag, const char*); - void operator()(std::string tag, std::string); + void operator()(const char* tag, const char* s) { + if(d_tags.find(std::string(tag)) != d_tags.end()) { + *d_os << s; + } + } - static void printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 2, 3))); - static void printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 2, 3))); + void operator()(const char* tag, const std::string& s) { + if(d_tags.find(std::string(tag)) != d_tags.end()) { + *d_os << s; + } + } + + void operator()(const std::string& tag, const char* s) { + if(d_tags.find(tag) != d_tags.end()) { + *d_os << s; + } + } + + void operator()(const std::string& tag, const std::string& s) { + if(d_tags.find(tag) != d_tags.end()) { + *d_os << s; + } + } + + void printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4))); + void printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4))); std::ostream& operator()(const char* tag) { - if(d_tags.find(std::string(tag)) != d_tags.end()) + if(d_tags.find(std::string(tag)) != d_tags.end()) { return *d_os; - else return null_os; + } else { + return null_os; + } } std::ostream& operator()(std::string tag) { - if(d_tags.find(tag) != d_tags.end()) + if(d_tags.find(tag) != d_tags.end()) { return *d_os; - else return null_os; + } else { + return null_os; + } } /** * The "Yeting option" - this allows use of Debug() without a tag @@ -190,28 +213,23 @@ public: void operator()(std::string tag, const char*); void operator()(std::string tag, std::string); - void printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4))) { - // 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 printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4))) { - } + void printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4))); + void printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4))); std::ostream& operator()(const char* tag) { - if(d_tags.find(tag) != d_tags.end()) + if(d_tags.find(tag) != d_tags.end()) { return *d_os; - else return null_os; + } else { + return null_os; + } } std::ostream& operator()(std::string tag) { - if(d_tags.find(tag) != d_tags.end()) + if(d_tags.find(tag) != d_tags.end()) { return *d_os; - else return null_os; + } else { + return null_os; + } } void on (const char* tag) { d_tags.insert(std::string(tag)); }; |