specialized implementation for boolean node attributes ("flags"): they now share memory words properly; also, implementations of some output functionality

2 files changed, 141 insertions, 33 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 */
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)); };