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.

4 files changed, 71 insertions, 100 deletions

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 7b5319267..104992bd4 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -387,11 +387,11 @@ void TheoryDatatypes::addTester( Node assertion ){
         unsigned int testerIndex = -1;
         for( unsigned int i=0; i<possibleCons.size(); i++ ) {
           if( possibleCons[i] ){
-            Assert( testerIndex==-1 );
+            Assert( testerIndex==unsigned(-1) );
             testerIndex = i;
           }
         }
-        Assert( testerIndex!=-1 );
+        Assert( testerIndex!=unsigned(-1) );
         assertionRep = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[testerIndex].getTester() ), tRep );
         Node exp = ( nb.getNumChildren() == 1 ) ? nb.getChild( 0 ) : nb;
         d_em.addNode( assertionRep, exp, Reason::idt_texhaust );
@@ -862,7 +862,7 @@ void TheoryDatatypes::collectTerms( Node n ) {
   if( n.getKind() == APPLY_CONSTRUCTOR ){
     for( int i=0; i<(int)n.getNumChildren(); i++ ) {
       Debug("datatypes-cycles") << "Subterm " << n << " -> " << n[i] << endl;
-      bool result = d_cycle_check.addEdgeNode( n, n[i] );
+      bool result CVC4_UNUSED = d_cycle_check.addEdgeNode( n, n[i] );
       Assert( !result );    //this should not create any new cycles (relevant terms should have been recorded before)
     }
   }else{
diff --git a/src/theory/shared_term_manager.cpp b/src/theory/shared_term_manager.cpp
index 8103a149a..03afa984e 100644
--- a/src/theory/shared_term_manager.cpp
+++ b/src/theory/shared_term_manager.cpp
@@ -67,7 +67,7 @@ void SharedTermManager::addTerm(TNode n, Theory* parent, Theory* child) {
   uint64_t bothTags = parentTag | childTag;
 
   // Create or update the SharedData for n
-  SharedData* pData;
+  SharedData* pData = NULL;
   if(n.getAttribute(SharedAttr(), pData)) {
     // The attribute already exists, just update it if necessary
     uint64_t tags = pData->getTheories();
@@ -121,8 +121,8 @@ void SharedTermManager::addEq(TNode eq, Theory* thReason) {
   TNode x = eq[0];
   TNode y = eq[1];
 
-  SharedData* pDataX;
-  SharedData* pDataY;
+  SharedData* pDataX = NULL;
+  SharedData* pDataY = NULL;
 
   // Grab the SharedData for each side of the equality, create if necessary
   if(!x.getAttribute(SharedAttr(), pDataX)) {
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 */
 
diff --git a/src/util/output.h b/src/util/output.h
index f21fc39e7..b0e210c17 100644
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -11,7 +11,7 @@
  ** 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.
  **/
@@ -58,8 +58,6 @@ extern null_streambuf null_sb;
 /** A null output stream singleton */
 extern std::ostream null_os CVC4_PUBLIC;
 
-#ifndef CVC4_MUZZLE
-
 class CVC4_PUBLIC CVC4ostream {
   std::ostream* d_os;
   // Current indentation
@@ -281,35 +279,57 @@ public:
 
 /** The debug output singleton */
 extern DebugC DebugChannel CVC4_PUBLIC;
-#ifdef CVC4_DEBUG
-#  define Debug ::CVC4::DebugChannel
-#else /* CVC4_DEBUG */
-#  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()
-
+extern WarningC WarningChannel CVC4_PUBLIC;
 /** The message output singleton */
-extern MessageC Message CVC4_PUBLIC;
-#define Message() (! ::CVC4::Message.isOn()) ? ::CVC4::debugNullCvc4Stream : ::CVC4::Message()
-
+extern MessageC MessageChannel CVC4_PUBLIC;
 /** The notice output singleton */
-extern NoticeC Notice CVC4_PUBLIC;
-#define Notice() (! ::CVC4::Notice.isOn()) ? ::CVC4::debugNullCvc4Stream : ::CVC4::Notice()
-
+extern NoticeC NoticeChannel CVC4_PUBLIC;
 /** The chat output singleton */
-extern ChatC Chat CVC4_PUBLIC;
-#define Chat() (! ::CVC4::Chat.isOn()) ? ::CVC4::debugNullCvc4Stream : ::CVC4::Chat()
-
+extern ChatC ChatChannel CVC4_PUBLIC;
 /** The trace output singleton */
 extern TraceC TraceChannel CVC4_PUBLIC;
-#ifdef CVC4_TRACING
-#  define Trace ::CVC4::TraceChannel
-#else /* CVC4_TRACING */
-#  define Trace ::CVC4::__cvc4_true() ? ::CVC4::debugNullCvc4Stream : ::CVC4::TraceChannel
-#endif /* CVC4_TRACING */
+
+#ifdef CVC4_MUZZLE
+
+#  define Debug ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::DebugChannel
+#  define Warning ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel
+#  define Message ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::MessageChannel
+#  define Notice ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::NoticeChannel
+#  define Chat ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::ChatChannel
+#  define Trace ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::TraceChannel
+
+inline int DebugC::printf(const char* tag, const char* fmt, ...) { return 0; }
+inline int DebugC::printf(std::string tag, const char* fmt, ...) { return 0; }
+inline int WarningC::printf(const char* fmt, ...) { return 0; }
+inline int MessageC::printf(const char* fmt, ...) { return 0; }
+inline int NoticeC::printf(const char* fmt, ...) { return 0; }
+inline int ChatC::printf(const char* fmt, ...) { return 0; }
+inline int TraceC::printf(const char* tag, const char* fmt, ...) { return 0; }
+inline int TraceC::printf(std::string tag, const char* fmt, ...) { return 0; }
+
+#else /* CVC4_MUZZLE */
+
+#  ifdef CVC4_DEBUG
+#    define Debug ::CVC4::DebugChannel
+#  else /* CVC4_DEBUG */
+#    define Debug ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::DebugChannel
+inline int DebugC::printf(const char* tag, const char* fmt, ...) { return 0; }
+inline int DebugC::printf(std::string tag, const char* fmt, ...) { return 0; }
+#  endif /* CVC4_DEBUG */
+#  define Warning (! ::CVC4::WarningChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel
+#  define Message (! ::CVC4::MessageChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::MessageChannel
+#  define Notice (! ::CVC4::NoticeChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::NoticeChannel
+#  define Chat (! ::CVC4::ChatChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::ChatChannel
+#  ifdef CVC4_TRACING
+#    define Trace ::CVC4::TraceChannel
+#  else /* CVC4_TRACING */
+#    define Trace ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::TraceChannel
+inline int TraceC::printf(const char* tag, const char* fmt, ...) { return 0; }
+inline int TraceC::printf(std::string tag, const char* fmt, ...) { return 0; }
+#  endif /* CVC4_TRACING */
+
+#endif /* CVC4_MUZZLE */
 
 // Disallow e.g. !Debug("foo").isOn() forms
 // because the ! will apply before the ? .
@@ -418,65 +438,18 @@ public:
 
 #endif /* CVC4_TRACING */
 
-#else /* ! CVC4_MUZZLE */
-
-class CVC4_PUBLIC ScopedDebug {
-public:
-  ScopedDebug(std::string tag, bool newSetting = true) {}
-  ScopedDebug(const char* tag, bool newSetting = true) {}
-};/* class ScopedDebug */
-
-class CVC4_PUBLIC ScopedTrace {
-public:
-  ScopedTrace(std::string tag, bool newSetting = true) {}
-  ScopedTrace(const char* tag, bool newSetting = true) {}
-};/* class ScopedTrace */
-
-extern NullDebugC Debug 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;
-
-#endif /* ! CVC4_MUZZLE */
-
 /**
- * Same shape as DebugC/TraceC, but does nothing; designed for
- * compilation of non-debug/non-trace builds.  None of these should ever be called
- * in such builds, but we offer this to the compiler so it doesn't complain.
+ * Does nothing; designed for compilation of non-debug/non-trace
+ * builds.  None of these should ever be called in such builds, but we
+ * offer this to the compiler so it doesn't complain.
  */
-class CVC4_PUBLIC NullDebugC {
-public:
-  operator bool() { return false; }
-  operator CVC4ostream() { return CVC4ostream(); }
-  operator std::ostream&() { 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) {}
-
-  int printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3))) { return 0; }
-
-  std::ostream& operator()() { return null_os; }
-
-  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;
 extern NullC nullCvc4Stream CVC4_PUBLIC;
 
 }/* CVC4 namespace */