summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rw-r--r--test/unit/parser/parser_black.h28
-rw-r--r--test/unit/util/output_black.h83
-rw-r--r--test/unit/util/stats_black.h3
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 */
}
};
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback