From 691fbae1dad8689007686cf61b737da58a4c9427 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Wed, 4 May 2011 00:21:34 +0000
Subject: 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.
---
 src/util/output.cpp | 34 ++++++++++++++++------------------
 1 file changed, 16 insertions(+), 18 deletions(-)

(limited to 'src/util/output.cpp')

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 */
 
-- 
cgit v1.2.3