diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-05-04 00:21:34 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-05-04 00:21:34 +0000 |
commit | 691fbae1dad8689007686cf61b737da58a4c9427 (patch) | |
tree | e6dd40fc3bfd39d28e443d768106508226338452 /test/unit | |
parent | 12d31931b48b659b78f531e98dba9d449da0137b (diff) |
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.
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/parser/parser_black.h | 28 | ||||
-rw-r--r-- | test/unit/util/output_black.h | 83 | ||||
-rw-r--r-- | test/unit/util/stats_black.h | 3 |
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 */ } }; |