diff options
Diffstat (limited to 'test')
-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 */ } }; |