Considerably simplified the way output streams are used. This commit

should have no impact on production performance and speed up debug
performance considerably, while making the code much cleaner.  On some
benchmarks, debug builds now run _much_ faster.

We no longer have to sprinkle our code with things like:

  if(debugTagIsOn("context")) {
    Debug("context") << theContext << std::endl;
  }

which we had to do to get around performance problems previously.
Now just writing:

  Debug("context") << theContext << std::endl;

does the same in production and debug builds.  That is, if "context"
debugging is off, theContext isn't converted to a string, nor is it
output to a "/dev/null" ostream.  I've confirmed this.  In production
builds, the whole statement inlines to nothing.  I've confirmed this
too.

Also, "Debug" is no longer a #definition, so you can use it directly
in production builds where you couldn't previously, e.g.

  if(Debug.isOn("paranoid:check_tableau")) {
    checkTableau();
  }

I'm leaving debugTagIsOn() for now, but marking it as deprecated.

11 files changed, 273 insertions, 214 deletions

diff --git a/src/context/cdmap.h b/src/context/cdmap.h
index b981628c5..45ff68a23 100644
--- a/src/context/cdmap.h
+++ b/src/context/cdmap.h
@@ -106,11 +106,6 @@ namespace context {
 
 template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> > class CDMap;
 
-template <class T, class U>
-inline std::ostream& operator<<(std::ostream& out, const std::pair<T, U>& p) {
-  return out << "[" << p.first << "," << p.second << "]";
-}
-
 template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> >
 class CDOmap : public ContextObj {
   friend class CDMap<Key, Data, HashFcn>;
diff --git a/src/context/context.cpp b/src/context/context.cpp
index 994f644a7..0028aaad5 100644
--- a/src/context/context.cpp
+++ b/src/context/context.cpp
@@ -132,19 +132,15 @@ void Context::addNotifyObjPost(ContextNotifyObj* pCNO) {
 
 
 void ContextObj::update() throw(AssertionException) {
-  if(debugTagIsOn("context")) {
-    Debug("context") << "before update(" << this << "):" << std::endl
-                     << *getContext() << std::endl;
-  }
+  Debug("context") << "before update(" << this << "):" << std::endl
+                   << *getContext() << std::endl;
 
   // Call save() to save the information in the current object
   ContextObj* pContextObjSaved = save(d_pScope->getCMM());
 
-  if(debugTagIsOn("context")) {
-    Debug("context") << "in update(" << this << ") with restore "
-                     << pContextObjSaved << ": waypoint 1" << std::endl
-                     << *getContext() << std::endl;
-  }
+  Debug("context") << "in update(" << this << ") with restore "
+                   << pContextObjSaved << ": waypoint 1" << std::endl
+                   << *getContext() << std::endl;
 
   // Check that base class data was saved
   Assert( ( pContextObjSaved->d_pContextObjNext == d_pContextObjNext &&
@@ -173,11 +169,9 @@ void ContextObj::update() throw(AssertionException) {
   Debug("context") << "in update(" << this
                    << "): *prev() is now " << *prev() << std::endl;
 
-  if(debugTagIsOn("context")) {
-    Debug("context") << "in update(" << this << ") with restore "
-                     << pContextObjSaved << ": waypoint 3" << std::endl
-                     << *getContext() << std::endl;
-  }
+  Debug("context") << "in update(" << this << ") with restore "
+                   << pContextObjSaved << ": waypoint 3" << std::endl
+                   << *getContext() << std::endl;
 
   // Update Scope pointer to current top Scope
   d_pScope = d_pScope->getContext()->getTopScope();
@@ -189,11 +183,9 @@ void ContextObj::update() throw(AssertionException) {
   // Scope is popped.
   d_pScope->addToChain(this);
 
-  if(debugTagIsOn("context")) {
-    Debug("context") << "after update(" << this << ") with restore "
-                     << pContextObjSaved << ":" << std::endl
-                     << *getContext() << std::endl;
-  }
+  Debug("context") << "after update(" << this << ") with restore "
+                   << pContextObjSaved << ":" << std::endl
+                   << *getContext() << std::endl;
 }
 
 
@@ -238,12 +230,11 @@ ContextObj* ContextObj::restoreAndContinue() throw(AssertionException) {
 
 
 void ContextObj::destroy() throw(AssertionException) {
-  if(debugTagIsOn("context")) {
-    /* Context can be big and complicated, so we only want to process this output
-     * if we're really going to use it. (Same goes below.) */
-    Debug("context") << "before destroy " << this << " (level " << getLevel()
-          << "):" << std::endl << *getContext() << std::endl;
-  }
+  /* Context can be big and complicated, so we only want to process this output
+   * if we're really going to use it. (Same goes below.) */
+  Debug("context") << "before destroy " << this << " (level " << getLevel()
+                   << "):" << std::endl << *getContext() << std::endl;
+
   for(;;) {
     // If valgrind reports invalid writes on the next few lines,
     // here's a hint: make sure all classes derived from ContextObj in
@@ -256,18 +247,14 @@ void ContextObj::destroy() throw(AssertionException) {
     if(d_pContextObjRestore == NULL) {
       break;
     }
-    if(debugTagIsOn("context")) {
-      Debug("context") << "in destroy " << this << ", restore object is "
-            << d_pContextObjRestore << " at level "
-            << d_pContextObjRestore->getLevel() << ":" << std::endl
-            << *getContext() << std::endl;
-    }
+    Debug("context") << "in destroy " << this << ", restore object is "
+                     << d_pContextObjRestore << " at level "
+                     << d_pContextObjRestore->getLevel() << ":" << std::endl
+                     << *getContext() << std::endl;
     restoreAndContinue();
   }
-  if(debugTagIsOn("context")) {
-    Debug("context") << "after destroy " << this << ":" << std::endl
-          << *getContext() << std::endl;
-  }
+  Debug("context") << "after destroy " << this << ":" << std::endl
+                   << *getContext() << std::endl;
 }
 
 
@@ -318,7 +305,7 @@ ContextNotifyObj::~ContextNotifyObj() throw(AssertionException) {
 
 std::ostream& operator<<(std::ostream& out,
                          const Context& context) throw(AssertionException) {
-  const std::string separator(79, '-');
+  static const std::string separator(79, '-');
 
   int level = context.d_scopeList.size() - 1;
   typedef std::vector<Scope*>::const_reverse_iterator const_reverse_iterator;
diff --git a/src/context/context.h b/src/context/context.h
index 12d7c4673..1aa5fe44d 100644
--- a/src/context/context.h
+++ b/src/context/context.h
@@ -508,9 +508,7 @@ public:
    * ContextMemoryManager as an argument.
    */
   void deleteSelf() {
-    if(debugTagIsOn("context")) {
-      Debug("context") << "deleteSelf(" << this << ")" << std::endl;
-    }
+    Debug("context") << "deleteSelf(" << this << ")" << std::endl;
     this->~ContextObj();
     ::operator delete(this);
   }
diff --git a/src/context/context_mm.cpp b/src/context/context_mm.cpp
index 6a277245e..5a1e52d66 100644
--- a/src/context/context_mm.cpp
+++ b/src/context/context_mm.cpp
@@ -88,11 +88,9 @@ void* ContextMemoryManager::newData(size_t size) {
     AlwaysAssert(d_nextFree <= d_endChunk,
                  "Request is bigger than memory chunk size");
   }
-  if(debugTagIsOn("context")) {
-    Debug("context") << "ContextMemoryManager::newData(" << size
-                     << ") returning " << res << " at level "
-                     << d_chunkList.size() << std::endl;
-  }
+  Debug("context") << "ContextMemoryManager::newData(" << size
+                   << ") returning " << res << " at level "
+                   << d_chunkList.size() << std::endl;
   return res;
 }
 
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 7cccca177..c49d5f38a 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -122,7 +122,7 @@ Result PropEngine::checkSat() {
   // Check the problem
   bool result = d_satSolver->solve();
 
-  if( result && debugTagIsOn("prop") ) {
+  if( result && Debug.isOn("prop") ) {
     printSatisfyingAssignment();
   }
 
diff --git a/src/prop/sat.h b/src/prop/sat.h
index 9e09727e3..c58a198b3 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -237,7 +237,7 @@ inline SatSolver::SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine,
   d_minisat->polarity_mode = minisat::SimpSolver::polarity_user;
 
   // No random choices
-  if(debugTagIsOn("no_rnd_decisions")){
+  if(Debug.isOn("no_rnd_decisions")){
     d_minisat->random_var_freq = 0;
   }
 
@@ -271,13 +271,15 @@ SatSolver::SatLiteralHashFunction::operator()(const SatLiteral& literal) const {
   return hashSatLiteral(literal);
 }
 
-inline std::ostream& operator <<(std::ostream& out, SatLiteral lit) {
-  const char * s = (literalSign(lit)) ? "~" : " ";
-  out << s << literalToVariable(lit);
+}/* CVC4::prop namespace */
+
+inline std::ostream& operator <<(std::ostream& out, prop::SatLiteral lit) {
+  const char * s = (prop::literalSign(lit)) ? "~" : " ";
+  out << s << prop::literalToVariable(lit);
   return out;
 }
 
-inline std::ostream& operator <<(std::ostream& out, const SatClause& clause) {
+inline std::ostream& operator <<(std::ostream& out, const prop::SatClause& clause) {
   out << "clause:";
   for(int i = 0; i < clause.size(); ++i) {
     out << " " << clause[i];
@@ -286,12 +288,11 @@ inline std::ostream& operator <<(std::ostream& out, const SatClause& clause) {
   return out;
 }
 
-inline std::ostream& operator <<(std::ostream& out, const SatLiteralValue& val) {
-  out << stringOfLiteralValue(val);
+inline std::ostream& operator <<(std::ostream& out, prop::SatLiteralValue val) {
+  out << prop::stringOfLiteralValue(val);
   return out;
 }
 
-}/* CVC4::prop namespace */
 }/* CVC4 namespace */
 
 #endif /* __CVC4__PROP__SAT_H */
diff --git a/src/theory/arith/arith_propagator.cpp b/src/theory/arith/arith_propagator.cpp
index c5068c9fb..0f417bc41 100644
--- a/src/theory/arith/arith_propagator.cpp
+++ b/src/theory/arith/arith_propagator.cpp
@@ -122,7 +122,7 @@ std::vector<Node> ArithUnatePropagator::getImpliedLiterals(){
     enqueueImpliedLiterals(assertion, impliedButNotAsserted);
   }
 
-  if(debugTagIsOn("arith::propagator")){
+  if(Debug.isOn("arith::propagator")){
     for(std::vector<Node>::iterator i = impliedButNotAsserted.begin(),
           endIter = impliedButNotAsserted.end(); i != endIter; ++i){
       Node imp = *i;
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 4d6a95eff..f11f38ab4 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -517,7 +517,7 @@ void TheoryArith::update(TNode x_i, DeltaRational& v){
 
   d_partialModel.setAssignment(x_i, v);
 
-  if(debugTagIsOn("paranoid:check_tableau")){
+  if(Debug.isOn("paranoid:check_tableau")){
     checkTableau();
   }
 }
@@ -562,7 +562,7 @@ void TheoryArith::pivotAndUpdate(TNode x_i, TNode x_j, DeltaRational& v){
 
   checkBasicVariable(x_j);
 
-  if(debugTagIsOn("tableau")){
+  if(Debug.isOn("tableau")){
     d_tableau.printTableau();
   }
 }
@@ -583,7 +583,7 @@ TNode TheoryArith::selectSmallestInconsistentVar(){
     d_possiblyInconsistent.pop();
   }
 
-  if(debugTagIsOn("paranoid:variables")){
+  if(Debug.isOn("paranoid:variables")){
     for(Tableau::VarSet::iterator basicIter = d_tableau.begin();
         basicIter != d_tableau.end();
         ++basicIter){
@@ -631,7 +631,7 @@ Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06
   static int iteratationNum = 0;
   static const int EJECT_FREQUENCY = 10;
   while(true){
-    if(debugTagIsOn("paranoid:check_tableau")){ checkTableau(); }
+    if(Debug.isOn("paranoid:check_tableau")){ checkTableau(); }
 
     TNode x_i = selectSmallestInconsistentVar();
     Debug("arith_update") << "selectSmallestInconsistentVar()=" << x_i << endl;
@@ -824,14 +824,14 @@ void TheoryArith::check(Effort level){
   }
 
   //TODO This must be done everytime for the time being
-  if(debugTagIsOn("paranoid:check_tableau")){ checkTableau(); }
+  if(Debug.isOn("paranoid:check_tableau")){ checkTableau(); }
 
   Node possibleConflict = updateInconsistentVars();
   if(possibleConflict != Node::null()){
 
     d_partialModel.revertAssignmentChanges();
 
-    if(debugTagIsOn("arith::print-conflict"))
+    if(Debug.isOn("arith::print-conflict"))
       Debug("arith_conflict") << (possibleConflict) << std::endl;
 
     d_out->conflict(possibleConflict);
@@ -840,12 +840,12 @@ void TheoryArith::check(Effort level){
   }else{
     d_partialModel.commitAssignmentChanges();
   }
-  if(debugTagIsOn("paranoid:check_tableau")){ checkTableau(); }
+  if(Debug.isOn("paranoid:check_tableau")){ checkTableau(); }
 
 
   Debug("arith") << "TheoryArith::check end" << std::endl;
 
-  if(debugTagIsOn("arith::print_model")) {
+  if(Debug.isOn("arith::print_model")) {
     Debug("arith::print_model") << "Model:" << endl;
 
     for (unsigned i = 0; i < d_variables.size(); ++ i) {
@@ -856,7 +856,7 @@ void TheoryArith::check(Effort level){
       Debug("arith::print_model") << endl;
     }
   }
-  if(debugTagIsOn("arith::print_assertions")) {
+  if(Debug.isOn("arith::print_assertions")) {
     Debug("arith::print_assertions") << "Assertions:" << endl;
     for (unsigned i = 0; i < d_variables.size(); ++ i) {
       Node x = d_variables[i];
@@ -874,8 +874,8 @@ void TheoryArith::check(Effort level){
 
 /**
  * This check is quite expensive.
- * It should be wrapped in a debugTagIsOn guard.
- *   if(debugTagIsOn("paranoid:check_tableau")){
+ * It should be wrapped in a Debug.isOn() guard.
+ *   if(Debug.isOn("paranoid:check_tableau")){
  *      checkTableau();
  *   }
  */
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 096c99c06..c4dc1c508 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -154,12 +154,10 @@ Node TheoryEngine::removeITEs(TNode node) {
                             nodeManager->mkNode(kind::EQUAL, skolem, node[2]));
       nodeManager->setAttribute(node, theory::IteRewriteAttr(), skolem);
 
-      if(debugTagIsOn("ite")){
-        Debug("ite") << "removeITEs([" << node.getId() << "," << node << "])"
-                     << "->"
-                     << "["<<newAssertion.getId() << "," << newAssertion << "]"
-                     << endl;
-      }
+      Debug("ite") << "removeITEs([" << node.getId() << "," << node << "])"
+                   << "->"
+                   << "["<<newAssertion.getId() << "," << newAssertion << "]"
+                   << endl;
 
       Node preprocessed = preprocess(newAssertion);
       d_propEngine->assertFormula(preprocessed);
@@ -416,8 +414,8 @@ Node TheoryEngine::rewrite(TNode in, bool topLevel) {
        * in the cache to make sure they are the same.  This is
        * especially necessary if a theory post-rewrites something into
        * a term of another theory. */
-      if(debugTagIsOn("extra-checking") &&
-         !debugTagIsOn("$extra-checking:inside-rewrite")) {
+      if(Debug.isOn("extra-checking") &&
+         !Debug.isOn("$extra-checking:inside-rewrite")) {
         ScopedDebug d("$extra-checking:inside-rewrite");
         Node rewrittenAgain = rewrite(rse.d_node, rse.d_topLevel);
         Assert(rewrittenAgain == rse.d_node,
diff --git a/src/util/output.cpp b/src/util/output.cpp
index 501ef52fd..8a0bdd298 100644
--- a/src/util/output.cpp
+++ b/src/util/output.cpp
@@ -33,12 +33,22 @@ NullC nullCvc4Stream CVC4_PUBLIC;
 
 #ifndef CVC4_MUZZLE
 
-DebugC   DebugOut(&cout);
-WarningC WarningOut(&cerr);
-MessageC MessageOut(&cout);
-NoticeC  NoticeOut(&cout);
-ChatC    ChatOut(&cout);
-TraceC   TraceOut(&cout);
+#ifdef CVC4_DEBUG
+DebugC Debug CVC4_PUBLIC (&cout);
+#else /* CVC4_DEBUG */
+NullDebugC Debug CVC4_PUBLIC;
+#endif /* CVC4_DEBUG */
+
+WarningC Warning CVC4_PUBLIC (&cerr);
+MessageC Message CVC4_PUBLIC (&cout);
+NoticeC Notice CVC4_PUBLIC (&cout);
+ChatC Chat CVC4_PUBLIC (&cout);
+
+#ifdef CVC4_TRACING
+TraceC Trace CVC4_PUBLIC (&cout);
+#else /* CVC4_TRACING */
+NullDebugC Trace CVC4_PUBLIC;
+#endif /* CVC4_TRACING */
 
 void DebugC::printf(const char* tag, const char* fmt, ...) {
   if(d_tags.find(string(tag)) != d_tags.end()) {
@@ -128,6 +138,16 @@ void TraceC::printf(string tag, const char* fmt, ...) {
   }
 }
 
-#endif /* CVC4_MUZZLE */
+#else /* ! CVC4_MUZZLE */
+
+NullDebugC Debug CVC4_PUBLIC;
+NullC Warning CVC4_PUBLIC;
+NullC Warning CVC4_PUBLIC;
+NullC Message CVC4_PUBLIC;
+NullC Notice CVC4_PUBLIC;
+NullC Chat CVC4_PUBLIC;
+NullDebugC Trace CVC4_PUBLIC;
+
+#endif /* ! CVC4_MUZZLE */
 
 }/* CVC4 namespace */
diff --git a/src/util/output.h b/src/util/output.h
index 851868c15..355d15760 100644
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -29,6 +29,14 @@
 
 namespace CVC4 {
 
+template <class T, class U>
+std::ostream& operator<<(std::ostream& out, const std::pair<T, U>& p) CVC4_PUBLIC;
+
+template <class T, class U>
+std::ostream& operator<<(std::ostream& out, const std::pair<T, U>& p) {
+  return out << "[" << p.first << "," << p.second << "]";
+}
+
 /**
  * A utility class to provide (essentially) a "/dev/null" streambuf.
  * If debugging support is compiled in, but debugging for
@@ -36,7 +44,7 @@ namespace CVC4 {
  * attached to a null_streambuf instance so that output is directed to
  * the bit bucket.
  */
-class null_streambuf : public std::streambuf {
+class CVC4_PUBLIC null_streambuf : public std::streambuf {
 public:
   /* Overriding overflow() just ensures that EOF isn't returned on the
    * stream.  Perhaps this is not so critical, but recommended; this
@@ -50,12 +58,129 @@ extern null_streambuf null_sb;
 /** A null output stream singleton */
 extern std::ostream null_os CVC4_PUBLIC;
 
+class CVC4_PUBLIC NullCVC4ostream {
+public:
+  void flush() {}
+  bool isConnected() { return false; }
+  operator std::ostream&() { return null_os; }
+
+  template <class T>
+  NullCVC4ostream& operator<<(T const& t) { return *this; }
+
+  // support manipulators, endl, etc..
+  NullCVC4ostream& operator<<(std::ostream& (*pf)(std::ostream&)) { return *this; }
+  NullCVC4ostream& operator<<(std::ios& (*pf)(std::ios&)) { return *this; }
+  NullCVC4ostream& operator<<(std::ios_base& (*pf)(std::ios_base&)) { return *this; }
+};/* class NullCVC4ostream */
+
+/**
+ * Same shape as DebugC/TraceC, but does nothing; designed for
+ * compilation of muzzled builds.  None of these should ever be called
+ * in muzzled builds, but we offer this to the compiler so it doesn't complain.
+ */
+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) {}
+
+  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))) {}
+
+  NullCVC4ostream operator()(const char* tag) { return NullCVC4ostream(); }
+  NullCVC4ostream operator()(std::string tag) { return NullCVC4ostream(); }
+
+  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; }
+};/* class NullDebugC */
+
+/**
+ * Same shape as WarningC/etc., but does nothing; designed for
+ * compilation of muzzled builds.  None of these should ever be called
+ * in muzzled builds, but we offer this to the compiler so it doesn't
+ * complain. */
+class CVC4_PUBLIC NullC {
+public:
+  NullC() {}
+  NullC(std::ostream* os) {}
+
+  void operator()(const char*) {}
+  void operator()(std::string) {}
+
+  void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3))) {}
+
+  NullCVC4ostream operator()() { return NullCVC4ostream(); }
+
+  void setStream(std::ostream& os) {}
+  std::ostream& getStream() { return null_os; }
+};/* class NullC */
+
+extern NullDebugC debugNullCvc4Stream CVC4_PUBLIC;
+extern NullC nullCvc4Stream CVC4_PUBLIC;
+
 #ifndef CVC4_MUZZLE
 
+class CVC4_PUBLIC CVC4ostream {
+  std::ostream* d_os;
+public:
+  CVC4ostream() : d_os(NULL) {}
+  CVC4ostream(std::ostream* os) : d_os(os) {}
+
+  void flush() {
+    if(d_os != NULL) {
+      d_os->flush();
+    }
+  }
+
+  bool isConnected() { return d_os != NULL; }
+  operator std::ostream&() { return isConnected() ? *d_os : null_os; }
+
+  template <class T>
+  CVC4ostream& operator<<(T const& t) {
+    if(d_os != NULL) {
+      d_os = &(*d_os << t);
+    }
+    return *this;
+  }
+
+  // support manipulators, endl, etc..
+  CVC4ostream& operator<<(std::ostream& (*pf)(std::ostream&)) {
+    if(d_os != NULL) {
+      d_os = &(*d_os << pf);
+    }
+    return *this;
+  }
+  CVC4ostream& operator<<(std::ios& (*pf)(std::ios&)) {
+    if(d_os != NULL) {
+      d_os = &(*d_os << pf);
+    }
+    return *this;
+  }
+  CVC4ostream& operator<<(std::ios_base& (*pf)(std::ios_base&)) {
+    if(d_os != NULL) {
+      d_os = &(*d_os << pf);
+    }
+    return *this;
+  }
+
+};/* class CVC4ostream */
+
 /** The debug output class */
 class CVC4_PUBLIC DebugC {
   std::set<std::string> d_tags;
-  std::ostream *d_os;
+  std::ostream* d_os;
 
 public:
   DebugC(std::ostream* os) : d_os(os) {}
@@ -87,25 +212,25 @@ public:
   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) {
+  CVC4ostream operator()(const char* tag) {
     if(!d_tags.empty() && d_tags.find(std::string(tag)) != d_tags.end()) {
-      return *d_os;
+      return CVC4ostream(d_os);
     } else {
-      return null_os;
+      return CVC4ostream();
     }
   }
-  std::ostream& operator()(std::string tag) {
+  CVC4ostream operator()(std::string tag) {
     if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) {
-      return *d_os;
+      return CVC4ostream(d_os);
     } else {
-      return null_os;
+      return CVC4ostream();
     }
   }
   /**
    * The "Yeting option" - this allows use of Debug() without a tag
    * for temporary (file-only) debugging.
    */
-  std::ostream& operator()();
+  CVC4ostream operator()();
 
   void on (const char* tag) { d_tags.insert(std::string(tag)); }
   void on (std::string tag) { d_tags.insert(tag);              }
@@ -117,19 +242,11 @@ public:
 
   void setStream(std::ostream& os) { d_os = &os; }
   std::ostream& getStream() { return *d_os; }
-};/* class Debug */
-
-/** The debug output singleton */
-extern DebugC DebugOut CVC4_PUBLIC;
-#ifdef CVC4_DEBUG
-#  define Debug DebugOut
-#else /* CVC4_DEBUG */
-#  define Debug if(0) debugNullCvc4Stream
-#endif /* CVC4_DEBUG */
+};/* class DebugC */
 
 /** The warning output class */
 class CVC4_PUBLIC WarningC {
-  std::ostream *d_os;
+  std::ostream* d_os;
 
 public:
   WarningC(std::ostream* os) : d_os(os) {}
@@ -139,19 +256,15 @@ public:
 
   void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
 
-  std::ostream& operator()() { return *d_os; }
+  CVC4ostream operator()() { return CVC4ostream(d_os); }
 
   void setStream(std::ostream& os) { d_os = &os; }
   std::ostream& getStream() { return *d_os; }
-};/* class Warning */
-
-/** The warning output singleton */
-extern WarningC WarningOut CVC4_PUBLIC;
-#define Warning WarningOut
+};/* class WarningC */
 
 /** The message output class */
 class CVC4_PUBLIC MessageC {
-  std::ostream *d_os;
+  std::ostream* d_os;
 
 public:
   MessageC(std::ostream* os) : d_os(os) {}
@@ -161,19 +274,15 @@ public:
 
   void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
 
-  std::ostream& operator()() { return *d_os; }
+  CVC4ostream operator()() { return CVC4ostream(d_os); }
 
   void setStream(std::ostream& os) { d_os = &os; }
   std::ostream& getStream() { return *d_os; }
-};/* class Message */
-
-/** The message output singleton */
-extern MessageC MessageOut CVC4_PUBLIC;
-#define Message MessageOut
+};/* class MessageC */
 
 /** The notice output class */
 class CVC4_PUBLIC NoticeC {
-  std::ostream *d_os;
+  std::ostream* d_os;
 
 public:
   NoticeC(std::ostream* os) : d_os(os) {}
@@ -183,19 +292,15 @@ public:
 
   void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
 
-  std::ostream& operator()() { return *d_os; }
+  CVC4ostream operator()() { return CVC4ostream(d_os); }
 
   void setStream(std::ostream& os) { d_os = &os; }
   std::ostream& getStream() { return *d_os; }
-};/* class Notice */
-
-/** The notice output singleton */
-extern NoticeC NoticeOut CVC4_PUBLIC;
-#define Notice NoticeOut
+};/* class NoticeC */
 
 /** The chat output class */
 class CVC4_PUBLIC ChatC {
-  std::ostream *d_os;
+  std::ostream* d_os;
 
 public:
   ChatC(std::ostream* os) : d_os(os) {}
@@ -205,19 +310,15 @@ public:
 
   void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
 
-  std::ostream& operator()() { return *d_os; }
+  CVC4ostream operator()() { return CVC4ostream(d_os); }
 
   void setStream(std::ostream& os) { d_os = &os; }
   std::ostream& getStream() { return *d_os; }
-};/* class Chat */
-
-/** The chat output singleton */
-extern ChatC ChatOut CVC4_PUBLIC;
-#define Chat ChatOut
+};/* class ChatC */
 
 /** The trace output class */
 class CVC4_PUBLIC TraceC {
-  std::ostream *d_os;
+  std::ostream* d_os;
   std::set<std::string> d_tags;
 
 public:
@@ -250,19 +351,19 @@ public:
   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) {
+  CVC4ostream operator()(const char* tag) {
     if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) {
-      return *d_os;
+      return CVC4ostream(d_os);
     } else {
-      return null_os;
+      return CVC4ostream();
     }
   }
 
-  std::ostream& operator()(std::string tag) {
+  CVC4ostream operator()(std::string tag) {
     if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) {
-      return *d_os;
+      return CVC4ostream(d_os);
     } else {
-      return null_os;
+      return CVC4ostream();
     }
   }
 
@@ -276,14 +377,29 @@ public:
 
   void setStream(std::ostream& os) { d_os = &os; }
   std::ostream& getStream() { return *d_os; }
-};/* class Trace */
+};/* class TraceC */
+
+/** The debug output singleton */
+#ifdef CVC4_DEBUG
+extern DebugC Debug CVC4_PUBLIC;
+#else /* CVC4_DEBUG */
+extern NullDebugC Debug CVC4_PUBLIC;
+#endif /* CVC4_DEBUG */
+
+/** The warning output singleton */
+extern WarningC Warning CVC4_PUBLIC;
+/** The message output singleton */
+extern MessageC Message CVC4_PUBLIC;
+/** The notice output singleton */
+extern NoticeC Notice CVC4_PUBLIC;
+/** The chat output singleton */
+extern ChatC Chat CVC4_PUBLIC;
 
 /** The trace output singleton */
-extern TraceC TraceOut CVC4_PUBLIC;
 #ifdef CVC4_TRACING
-#  define Trace TraceOut
+extern TraceC Trace CVC4_PUBLIC;
 #else /* CVC4_TRACING */
-#  define Trace if(0) debugNullCvc4Stream
+extern NullDebugC Trace CVC4_PUBLIC;
 #endif /* CVC4_TRACING */
 
 #ifdef CVC4_DEBUG
@@ -296,11 +412,11 @@ public:
 
   ScopedDebug(std::string tag, bool newSetting = true) :
     d_tag(tag) {
-    d_oldSetting = DebugOut.isOn(d_tag);
+    d_oldSetting = Debug.isOn(d_tag);
     if(newSetting) {
-      DebugOut.on(d_tag);
+      Debug.on(d_tag);
     } else {
-      DebugOut.off(d_tag);
+      Debug.off(d_tag);
     }
   }
 
@@ -382,13 +498,6 @@ public:
 
 #else /* ! CVC4_MUZZLE */
 
-#  define Debug if(0) debugNullCvc4Stream
-#  define Warning if(0) nullCvc4Stream
-#  define Message if(0) nullCvc4Stream
-#  define Notice if(0) nullCvc4Stream
-#  define Chat if(0) nullCvc4Stream
-#  define Trace if(0) debugNullCvc4Stream
-
 class CVC4_PUBLIC ScopedDebug {
 public:
   ScopedDebug(std::string tag, bool newSetting = true) {}
@@ -401,72 +510,25 @@ public:
   ScopedTrace(const char* tag, bool newSetting = true) {}
 };/* class ScopedTrace */
 
-#endif /* ! CVC4_MUZZLE */
-
-/**
- * Same shape as DebugC/TraceC, but does nothing; designed for
- * compilation of muzzled builds.  None of these should ever be called
- * in muzzled builds, but we offer this to the compiler so it doesn't complain.
- */
-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) {}
+extern NullDebugC Debug CVC4_PUBLIC;
+extern NullC Warning CVC4_PUBLIC;
+extern NullC Warning CVC4_PUBLIC;
+extern NullC Message CVC4_PUBLIC;
+extern NullC Notice CVC4_PUBLIC;
+extern NullC Chat CVC4_PUBLIC;
+extern NullDebugC Trace CVC4_PUBLIC;
 
-  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) { 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; }
-};/* class NullDebugC */
-
-/**
- * Same shape as WarningC/etc., but does nothing; designed for
- * compilation of muzzled builds.  None of these should ever be called
- * in muzzled builds, but we offer this to the compiler so it doesn't
- * complain. */
-class CVC4_PUBLIC NullC {
-public:
-  NullC() {}
-  NullC(std::ostream* os) {}
-
-  void operator()(const char*) {}
-  void operator()(std::string) {}
-
-  void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3))) {}
-
-  std::ostream& operator()() { return null_os; }
-
-  void setStream(std::ostream& os) {}
-  std::ostream& getStream() { return null_os; }
-};/* class NullC */
-
-extern NullDebugC debugNullCvc4Stream CVC4_PUBLIC;
-extern NullC nullCvc4Stream CVC4_PUBLIC;
+#endif /* ! CVC4_MUZZLE */
 
+// don't use debugTagIsOn() anymore, use Debug.isOn()
+inline bool debugTagIsOn(std::string tag) __attribute__((__deprecated__));
 inline bool debugTagIsOn(std::string tag) {
-#ifdef CVC4_DEBUG
-  return DebugOut.isOn(tag);
-#else
+#if defined(CVC4_DEBUG) && !defined(CVC4_MUZZLE)
+  return Debug.isOn(tag);
+#else /* CVC4_DEBUG && !CVC4_MUZZLE */
   return false;
-#endif
-}
+#endif /* CVC4_DEBUG && !CVC4_MUZZLE */
+}/* debugTagIsOn() */
 
 }/* CVC4 namespace */