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.

3 files changed, 88 insertions, 26 deletions

diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index 3a9dd4418..91af11561 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -190,9 +190,9 @@ protected:
   void tearDown() {
     delete d_exprManager;
   }
-};
+};/* class ParserBlack */
 
-class Cvc4ParserTest : public CxxTest::TestSuite, public ParserBlack  {
+class Cvc4ParserTest : public CxxTest::TestSuite, public ParserBlack {
   typedef ParserBlack super;
 
 public:
@@ -236,6 +236,8 @@ public:
   }
 
   void testBadCvc4Inputs() {
+// competition builds don't do any checking
+#ifndef CVC4_COMPETITION_MODE
     tryBadInput("ASSERT;"); // no args
     tryBadInput("QUERY");
     tryBadInput("CHECKSAT");
@@ -256,6 +258,7 @@ public:
     tryBadInput("DATATYPE list = nil | cons(car:INT,cdr:list) END; DATATYPE list = nil | cons(car:INT,cdr:list) END;");
     tryBadInput("DATATYPE list = nil | cons(car:INT,cdr:list) END; DATATYPE list2 = nil END;");
     tryBadInput("DATATYPE tree = node(data:(list,list,ARRAY trex OF list)), list = cons(car:ARRAY list OF tree,cdr:BITVECTOR(32)) END;");
+#endif /* ! CVC4_COMPETITION_MODE */
   }
 
   void testGoodCvc4Exprs() {
@@ -267,14 +270,17 @@ public:
   }
 
   void testBadCvc4Exprs() {
+// competition builds don't do any checking
+#ifndef CVC4_COMPETITION_MODE
     tryBadInput("a AND"); // wrong arity
     tryBadInput("AND(a,b)"); // not infix
     tryBadInput("(OR (AND a b) c)"); // not infix
     tryBadInput("a IMPLIES b"); // should be =>
     tryBadInput("a NOT b"); // wrong arity, not infix
     tryBadInput("a and b"); // wrong case
+#endif /* ! CVC4_COMPETITION_MODE */
   }
-};
+};/* class Cvc4ParserTest */
 
 class SmtParserTest : public CxxTest::TestSuite, public ParserBlack {
   typedef ParserBlack super;
@@ -304,11 +310,14 @@ public:
   }
 
   void testBadSmtInputs() {
+// competition builds don't do any checking
+#ifndef CVC4_COMPETITION_MODE
     tryBadInput("(benchmark foo)"); // empty benchmark is not OK
     tryBadInput("(benchmark bar :assumption)"); // no args
     tryBadInput("(benchmark bar :formula)");
     tryBadInput("(benchmark baz :extrapreds ( (a) (a) ) )"); // double decl
     tryBadInput("(benchmark zub :extrasorts (a) :extrapreds (p a))"); // (p a) needs parens
+#endif /* ! CVC4_COMPETITION_MODE */
   }
 
   void testGoodSmtExprs() {
@@ -325,6 +334,8 @@ public:
   }
 
   void testBadSmtExprs() {
+// competition builds don't do any checking
+#ifndef CVC4_COMPETITION_MODE
     tryBadExpr("(and)"); // wrong arity
     tryBadExpr("(and a b"); // no closing paren
     tryBadExpr("(a and b)"); // infix
@@ -336,8 +347,9 @@ public:
     tryBadExpr("(a b)"); // using non-function as function
     tryBadExpr(".5"); // rational constants must have integer prefix
     tryBadExpr("1."); // rational constants must have fractional suffix
+#endif /* ! CVC4_COMPETITION_MODE */
   }
-};
+};/* class SmtParserTest */
 
 class Smt2ParserTest : public CxxTest::TestSuite, public ParserBlack {
   typedef ParserBlack super;
@@ -381,6 +393,8 @@ public:
   }
 
   void testBadSmt2Inputs() {
+// competition builds don't do any checking
+#ifndef CVC4_COMPETITION_MODE
     tryBadInput("(assert)"); // no args
     tryBadInput("(set-info :notes |Symbols can't contain the | character|)");
     tryBadInput("(set-logic QF_UF) (check-sat true)"); // shouldn't have an arg
@@ -390,6 +404,7 @@ public:
     // strict mode
     tryBadInput("(assert true)", true); // no set-logic, core theory symbol "true" undefined
     tryBadInput("(declare-fun p Bool)", true); // core theory symbol "Bool" undefined
+#endif /* ! CVC4_COMPETITION_MODE */
   }
 
   void testGoodSmt2Exprs() {
@@ -408,6 +423,8 @@ public:
   }
 
   void testBadSmt2Exprs() {
+// competition builds don't do any checking
+#ifndef CVC4_COMPETITION_MODE
     tryBadExpr("(and)"); // wrong arity
     tryBadExpr("(and a b"); // no closing paren
     tryBadExpr("(a and b)"); // infix
@@ -430,5 +447,6 @@ public:
     tryBadExpr("(and a)", true); // no unary and's
     tryBadExpr("(or a)", true);  // no unary or's
     tryBadExpr("(* 5 01)", true); // '01' is not a valid integer constant
+#endif /* ! CVC4_COMPETITION_MODE */
   }
-};
+};/* class Smt2ParserTest */
diff --git a/test/unit/util/output_black.h b/test/unit/util/output_black.h
index 183d8f7f1..61b1f40d2 100644
--- a/test/unit/util/output_black.h
+++ b/test/unit/util/output_black.h
@@ -219,29 +219,72 @@ public:
 
   }
 
-  static int expensiveFunction() {
+  static int failure() {
     // this represents an expensive function that should NOT be called
     // when debugging/tracing is turned off
-    TS_FAIL("a function was evaluated under Debug() or Trace() when it should not have been");
+    TS_FAIL("a function was evaluated under an output operation when it should not have been");
     return 0;
   }
 
-  void testEvaluationOffWhenItsSupposedToBe() {
+  void testEvaluationOffWhenItIsSupposedToBe() {
+    Debug.on("foo");
+#ifndef CVC4_DEBUG
+    TS_ASSERT( !( Debug.isOn("foo") ) );
+    Debug("foo") << failure() << endl;
+    Debug.printf("foo", "%d\n", failure());
+#else /* ! CVC4_DEBUG */
+    TS_ASSERT( Debug.isOn("foo") );
+#endif /* ! CVC4_DEBUG */
+    Debug.off("foo");
+    //Debug("foo") << failure() << endl;
+    //Debug.printf("foo", "%d\n", failure());
+
     Trace.on("foo");
 #ifndef CVC4_TRACING
     TS_ASSERT( !( Trace.isOn("foo") ) );
-    Trace("foo") << expensiveFunction() << endl;
-#else /* CVC4_TRACING */
+    Trace("foo") << failure() << endl;
+    Trace.printf("foo", "%d\n", failure());
+#else /* ! CVC4_TRACING */
     TS_ASSERT( Trace.isOn("foo") );
-#endif /* CVC4_TRACING */
+#endif /* ! CVC4_TRACING */
+    Trace.off("foo");
+    //Trace("foo") << failure() << endl;
+    //Trace.printf("foo", "%d\n", failure());
 
-    Debug.on("foo");
-#ifndef CVC4_DEBUG
+#ifdef CVC4_MUZZLE
     TS_ASSERT( !( Debug.isOn("foo") ) );
-    Debug("foo") << expensiveFunction() << endl;
-#else /* CVC4_DEBUG */
-    TS_ASSERT( Debug.isOn("foo") );
-#endif /* CVC4_DEBUG */
+    TS_ASSERT( !( Trace.isOn("foo") ) );
+    TS_ASSERT( !( Warning.isOn() ) );
+    TS_ASSERT( !( Message.isOn() ) );
+    TS_ASSERT( !( Notice.isOn() ) );
+    TS_ASSERT( !( Chat.isOn() ) );
+
+    cout << "debug" << std::endl;
+    Debug("foo") << failure() << endl;
+    cout << "trace" << std::endl;
+    Trace("foo") << failure() << endl;
+    cout << "warning" << std::endl;
+    Warning() << failure() << endl;
+    cout << "message" << std::endl;
+    Message() << failure() << endl;
+    cout << "notice" << std::endl;
+    Notice() << failure() << endl;
+    cout << "chat" << std::endl;
+    Chat() << failure() << endl;
+
+    cout << "debug:printf" << std::endl;
+    Debug.printf("foo", "%d\n", failure());
+    cout << "trace:printf" << std::endl;
+    Trace.printf("foo", "%d\n", failure());
+    cout << "warning:printf" << std::endl;
+    Warning.printf("%d\n", failure());
+    cout << "message:printf" << std::endl;
+    Message.printf("%d\n", failure());
+    cout << "notice:printf" << std::endl;
+    Notice.printf("%d\n", failure());
+    cout << "chat:printf" << std::endl;
+    Chat.printf("%d\n", failure());
+#endif /* CVC4_MUZZLE */
   }
 
   void testSimplePrint() {
@@ -249,36 +292,36 @@ public:
 #ifdef CVC4_MUZZLE
 
     Debug.off("yo");
-    Debug("yo", "foobar");
+    Debug("yo") << "foobar";
     TS_ASSERT_EQUALS(d_debugStream.str(), string());
     d_debugStream.str("");
     Debug.on("yo");
-    Debug("yo", "baz foo");
+    Debug("yo") << "baz foo";
     TS_ASSERT_EQUALS(d_debugStream.str(), string());
     d_debugStream.str("");
 
     Trace.off("yo");
-    Trace("yo", "foobar");
+    Trace("yo") << "foobar";
     TS_ASSERT_EQUALS(d_traceStream.str(), string());
     d_traceStream.str("");
     Trace.on("yo");
-    Trace("yo", "baz foo");
+    Trace("yo") << "baz foo";
     TS_ASSERT_EQUALS(d_traceStream.str(), string());
     d_traceStream.str("");
 
-    Warning("baz foo");
+    Warning() << "baz foo";
     TS_ASSERT_EQUALS(d_warningStream.str(), string());
     d_warningStream.str("");
 
-    Chat("baz foo");
+    Chat() << "baz foo";
     TS_ASSERT_EQUALS(d_chatStream.str(), string());
     d_chatStream.str("");
 
-    Message("baz foo");
+    Message() << "baz foo";
     TS_ASSERT_EQUALS(d_messageStream.str(), string());
     d_messageStream.str("");
 
-    Notice("baz foo");
+    Notice() << "baz foo";
     TS_ASSERT_EQUALS(d_noticeStream.str(), string());
     d_noticeStream.str("");
 
diff --git a/test/unit/util/stats_black.h b/test/unit/util/stats_black.h
index e44a016e6..d32ef828c 100644
--- a/test/unit/util/stats_black.h
+++ b/test/unit/util/stats_black.h
@@ -30,7 +30,7 @@ class StatsBlack : public CxxTest::TestSuite {
 public:
 
   void testStats() {
-
+#ifdef CVC4_STATISTICS_ON
     // StatisticsRegistry
     //static void flushStatistics(std::ostream& out);
 
@@ -99,6 +99,7 @@ public:
     TS_ASSERT_EQUALS(zero, sTimer.getData());
     sTimer.stop();
     TS_ASSERT_LESS_THAN(zero, sTimer.getData());
+#endif /* CVC4_STATISTICS_ON */
   }
 
 };