Stronger support for zero-performance-penalty output, and fixes and

simplifications for the "muzzled" (i.e. competition) design, which had
been broken.  Addition of some new unit test bits to ensure that
nothing is ever called in muzzled builds, e.g. things like

  Warning() << expensiveFunction();

Also, fix some compiler warnings.

1 files changed, 16 insertions, 18 deletions

diff --git a/src/util/output.cpp b/src/util/output.cpp
index 080409ed8..88628481f 100644
--- a/src/util/output.cpp
+++ b/src/util/output.cpp
@@ -11,15 +11,15 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief Output utility classes and functions.
+ ** \brief Output utility classes and functions
  **
  ** Output utility classes and functions.
  **/
 
-#include <iostream>
-
 #include "util/output.h"
 
+#include <iostream>
+
 using namespace std;
 
 namespace CVC4 {
@@ -29,18 +29,19 @@ namespace CVC4 {
 null_streambuf null_sb;
 ostream null_os(&null_sb);
 
-NullDebugC debugNullCvc4Stream CVC4_PUBLIC;
 NullC nullCvc4Stream CVC4_PUBLIC;
 
-#ifndef CVC4_MUZZLE
-
 DebugC DebugChannel CVC4_PUBLIC (&cout);
-WarningC Warning CVC4_PUBLIC (&cerr);
-MessageC Message CVC4_PUBLIC (&cout);
-NoticeC Notice CVC4_PUBLIC (&cout);
-ChatC Chat CVC4_PUBLIC (&cout);
+WarningC WarningChannel CVC4_PUBLIC (&cerr);
+MessageC MessageChannel CVC4_PUBLIC (&cout);
+NoticeC NoticeChannel CVC4_PUBLIC (&cout);
+ChatC ChatChannel CVC4_PUBLIC (&cout);
 TraceC TraceChannel CVC4_PUBLIC (&cout);
 
+#ifndef CVC4_MUZZLE
+
+#  ifdef CVC4_DEBUG
+
 int DebugC::printf(const char* tag, const char* fmt, ...) {
   if(d_tags.find(string(tag)) == d_tags.end()) {
     return 0;
@@ -71,6 +72,8 @@ int DebugC::printf(std::string tag, const char* fmt, ...) {
   return retval;
 }
 
+#  endif /* CVC4_DEBUG */
+
 int WarningC::printf(const char* fmt, ...) {
   // chop off output after 1024 bytes
   char buf[1024];
@@ -115,6 +118,8 @@ int ChatC::printf(const char* fmt, ...) {
   return retval;
 }
 
+#  ifdef CVC4_TRACING
+
 int TraceC::printf(const char* tag, const char* fmt, ...) {
   if(d_tags.find(string(tag)) == d_tags.end()) {
     return 0;
@@ -145,14 +150,7 @@ int TraceC::printf(std::string tag, const char* fmt, ...) {
   return retval;
 }
 
-#else /* ! CVC4_MUZZLE */
-
-NullDebugC Debug CVC4_PUBLIC;
-NullC Warning CVC4_PUBLIC;
-NullC Message CVC4_PUBLIC;
-NullC Notice CVC4_PUBLIC;
-NullC Chat CVC4_PUBLIC;
-NullDebugC Trace CVC4_PUBLIC;
+#  endif /* CVC4_TRACING */
 
 #endif /* ! CVC4_MUZZLE */