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.

1 files changed, 27 insertions, 7 deletions

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 */