diff options
Diffstat (limited to 'test/unit/parser/parser_black.h')
-rw-r--r-- | test/unit/parser/parser_black.h | 65 |
1 files changed, 0 insertions, 65 deletions
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index 13beedd63..bfaf8bda0 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -304,71 +304,6 @@ public: } };/* class Cvc4ParserTest */ -class Smt1ParserTest : public CxxTest::TestSuite, public ParserBlack { - typedef ParserBlack super; - -public: - Smt1ParserTest() : ParserBlack(LANG_SMTLIB_V1) { } - - void setUp() override { super::setUp(); } - - void tearDown() override { super::tearDown(); } - - void testGoodSmt1Inputs() { - tryGoodInput(""); // empty string is OK - tryGoodInput("(benchmark foo :assumption true)"); - tryGoodInput("(benchmark bar :formula true)"); - tryGoodInput("(benchmark qux :formula false)"); - tryGoodInput("(benchmark baz :extrapreds ( (a) (b) ) )"); - tryGoodInput("(benchmark zab :extrapreds ( (a) (b) ) :formula (implies (and (implies a b) a) b))"); - tryGoodInput("(benchmark zub :extrasorts (a) :extrafuns ( (f a a) (x a) ) :formula (= (f x) x))"); - tryGoodInput("(benchmark fuz :extrasorts (a) :extrafuns ((x a) (y a)) :formula (= (ite true x y) x))"); - tryGoodInput(";; nothing but a comment"); - tryGoodInput("; a comment\n(benchmark foo ; hello\n :formula true; goodbye\n)"); - } - - void testBadSmt1Inputs() { -// 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 testGoodSmt1Exprs() { - tryGoodExpr("(and a b)"); - tryGoodExpr("(or (and a b) c)"); - tryGoodExpr("(implies (and (implies a b) a) b)"); - tryGoodExpr("(and (iff a b) (not a))"); - tryGoodExpr("(iff (xor a b) (and (or a b) (not (and a b))))"); - tryGoodExpr("(ite a (f x) y)"); - tryGoodExpr("(if_then_else a (f x) y)"); - tryGoodExpr("1"); - tryGoodExpr("0"); - tryGoodExpr("1.5"); - } - - void testBadSmt1Exprs() { -// 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 - tryBadExpr("(OR (AND a b) c)"); // wrong case - tryBadExpr("(a IMPLIES b)"); // infix AND wrong case - tryBadExpr("(not a b)"); // wrong arity - tryBadExpr("not a"); // needs parens - tryBadExpr("(ite a x)"); // wrong arity - 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 Smt1ParserTest */ - class Smt2ParserTest : public CxxTest::TestSuite, public ParserBlack { typedef ParserBlack super; |