From 12d31931b48b659b78f531e98dba9d449da0137b Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Tue, 3 May 2011 04:33:09 +0000
Subject: [PATCH] output fixes for performance

---
 src/parser/cvc/Cvc.g |  4 +--
 src/util/output.h    | 58 ++++++++++++++++++++------------------------
 2 files changed, 28 insertions(+), 34 deletions(-)

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index af0024156..fce785cc7 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -688,8 +688,8 @@ mainCommand[CVC4::Command*& cmd]
 
   | ECHO_TOK
     ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } )
-      { CVC4::Message() << s << std::endl; }
-    | { CVC4::Message() << std::endl; }
+      { Message() << s << std::endl; }
+    | { Message() << std::endl; }
     )
 
   | INCLUDE_TOK
diff --git a/src/util/output.h b/src/util/output.h
index d3eb3a831..f21fc39e7 100644
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -76,10 +76,11 @@ public:
   void pushIndent() { d_indent ++; }
   void popIndent()  { if (d_indent > 0) -- d_indent; }
 
-  void flush() {
+  CVC4ostream& flush() {
     if(d_os != NULL) {
       d_os->flush();
     }
+    return *this;
   }
 
   bool isConnected() { return d_os != NULL; }
@@ -184,6 +185,8 @@ public:
 
   std::ostream& setStream(std::ostream& os) { d_os = &os; return os; }
   std::ostream& getStream() { return *d_os; }
+
+  bool isOn() const { return d_os != &null_os; }
 };/* class WarningC */
 
 /** The message output class */
@@ -199,6 +202,8 @@ public:
 
   std::ostream& setStream(std::ostream& os) { d_os = &os; return os; }
   std::ostream& getStream() { return *d_os; }
+
+  bool isOn() const { return d_os != &null_os; }
 };/* class MessageC */
 
 /** The notice output class */
@@ -214,6 +219,8 @@ public:
 
   std::ostream& setStream(std::ostream& os) { d_os = &os; return os; }
   std::ostream& getStream() { return *d_os; }
+
+  bool isOn() const { return d_os != &null_os; }
 };/* class NoticeC */
 
 /** The chat output class */
@@ -229,6 +236,8 @@ public:
 
   std::ostream& setStream(std::ostream& os) { d_os = &os; return os; }
   std::ostream& getStream() { return *d_os; }
+
+  bool isOn() const { return d_os != &null_os; }
 };/* class ChatC */
 
 /** The trace output class */
@@ -273,26 +282,33 @@ public:
 /** The debug output singleton */
 extern DebugC DebugChannel CVC4_PUBLIC;
 #ifdef CVC4_DEBUG
-#  define Debug CVC4::DebugChannel
+#  define Debug ::CVC4::DebugChannel
 #else /* CVC4_DEBUG */
-#  define Debug CVC4::__cvc4_true() ? CVC4::debugNullCvc4Stream : CVC4::DebugChannel
+#  define Debug ::CVC4::__cvc4_true() ? ::CVC4::debugNullCvc4Stream : ::CVC4::DebugChannel
 #endif /* CVC4_DEBUG */
 
 /** The warning output singleton */
 extern WarningC Warning CVC4_PUBLIC;
+#define Warning() (! ::CVC4::Warning.isOn()) ? ::CVC4::debugNullCvc4Stream : ::CVC4::Warning()
+
 /** The message output singleton */
 extern MessageC Message CVC4_PUBLIC;
+#define Message() (! ::CVC4::Message.isOn()) ? ::CVC4::debugNullCvc4Stream : ::CVC4::Message()
+
 /** The notice output singleton */
 extern NoticeC Notice CVC4_PUBLIC;
+#define Notice() (! ::CVC4::Notice.isOn()) ? ::CVC4::debugNullCvc4Stream : ::CVC4::Notice()
+
 /** The chat output singleton */
 extern ChatC Chat CVC4_PUBLIC;
+#define Chat() (! ::CVC4::Chat.isOn()) ? ::CVC4::debugNullCvc4Stream : ::CVC4::Chat()
 
 /** The trace output singleton */
 extern TraceC TraceChannel CVC4_PUBLIC;
 #ifdef CVC4_TRACING
-#  define Trace CVC4::TraceChannel
+#  define Trace ::CVC4::TraceChannel
 #else /* CVC4_TRACING */
-#  define Trace CVC4::__cvc4_true() ? CVC4::debugNullCvc4Stream : CVC4::TraceChannel
+#  define Trace ::CVC4::__cvc4_true() ? ::CVC4::debugNullCvc4Stream : ::CVC4::TraceChannel
 #endif /* CVC4_TRACING */
 
 // Disallow e.g. !Debug("foo").isOn() forms
@@ -432,33 +448,6 @@ extern NullDebugC Trace CVC4_PUBLIC;
  */
 class CVC4_PUBLIC NullDebugC {
 public:
-/*
-  NullDebugC() {}
-  NullDebugC(std::ostream* 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) {}
-
-  int printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4))) {}
-  int printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4))) {}
-
-  std::ostream& operator()(const char* tag) { return null_os; }
-  std::ostream& operator()(std::string tag) { return null_os; }
-
-  void on (const char* tag) {}
-  void on (std::string tag) {}
-  void off(const char* tag) {}
-  void off(std::string tag) {}
-
-  bool isOn(const char* tag) { return false; }
-  bool isOn(std::string tag) { return false; }
-
-  void setStream(std::ostream& os) {}
-  std::ostream& getStream() { return null_os; }
-
-*/
   operator bool() { return false; }
   operator CVC4ostream() { return CVC4ostream(); }
   operator std::ostream&() { return null_os; }
@@ -471,6 +460,7 @@ public:
  * complain. */
 class CVC4_PUBLIC NullC {
 public:
+/*
   NullC() {}
   NullC(std::ostream* os) {}
 
@@ -480,6 +470,10 @@ public:
 
   std::ostream& setStream(std::ostream& os) { return null_os; }
   std::ostream& getStream() { return null_os; }
+*/
+  operator bool() { return false; }
+  operator CVC4ostream() { return CVC4ostream(); }
+  operator std::ostream&() { return null_os; }
 };/* class NullC */
 
 extern NullDebugC debugNullCvc4Stream CVC4_PUBLIC;
-- 
2.30.2