From 05d29aa0de4c2d4d773a81375fb14584221595ea Mon Sep 17 00:00:00 2001 From: "Christopher L. Conway" Date: Wed, 12 May 2010 15:15:58 +0000 Subject: [PATCH] Refactoring parser tests --- test/unit/parser/parser_black.h | 433 +++++++++++++------------------- 1 file changed, 177 insertions(+), 256 deletions(-) diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index 37fac552e..e7df27083 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -21,6 +21,7 @@ #include "expr/expr_manager.h" #include "parser/input.h" #include "parser/parser.h" +#include "parser/smt2/smt2.h" #include "expr/command.h" #include "util/output.h" @@ -29,210 +30,14 @@ using namespace CVC4::parser; using namespace std; -/************************** CVC test inputs ********************************/ -const string goodCvc4Inputs[] = { - "", // empty string is OK - "ASSERT TRUE;", - "QUERY TRUE;", - "CHECKSAT FALSE;", - "a, b : BOOLEAN;", - "a, b : BOOLEAN; QUERY (a => b) AND a => b;", - "T, U : TYPE; f : T -> U; x : T; CHECKSAT f(x) = x;", - "T : TYPE; x, y : T; a : BOOLEAN; QUERY (IF a THEN x ELSE y ENDIF) = x;", - "%% nothing but a comment", - "% a comment\nASSERT TRUE; %a command\n% another comment", - }; - -const int numGoodCvc4Inputs = sizeof(goodCvc4Inputs) / sizeof(string); - - -/* The following expressions are valid after setupContext. */ -const string goodCvc4Exprs[] = { - "a AND b", - "a AND b OR c", - "(a => b) AND a => b", - "(a <=> b) AND (NOT a)", - "(a XOR b) <=> (a OR b) AND (NOT (a AND b))" -}; - -const int numGoodCvc4Exprs = sizeof(goodCvc4Exprs) / sizeof(string); - -const string badCvc4Inputs[] = { - ";", // no command - "ASSERT;", // no args - "QUERY", - "CHECKSAT", - "a, b : boolean;", // lowercase boolean isn't a type - "0x : INT;", // 0x isn't an identifier - "a, b : BOOLEAN\nQUERY (a => b) AND a => b;", // no semicolon after decl - "a : BOOLEAN; a: BOOLEAN;" // double decl - "a, b: BOOLEAN; QUERY a(b);" // non-function used as function - }; - -const int numBadCvc4Inputs = sizeof(badCvc4Inputs) / sizeof(string); - -/* The following expressions are invalid even after setupContext. */ -const string badCvc4Exprs[] = { - "a AND", // wrong arity - "AND(a,b)", // not infix - "(OR (AND a b) c)", // not infix - "a IMPLIES b", // should be => - "a NOT b", // wrong arity, not infix - "a and b" // wrong case -}; - -const int numBadCvc4Exprs = sizeof(badCvc4Exprs) / sizeof(string); - -/************************** SMT test inputs ********************************/ - -const string goodSmtInputs[] = { - "", // empty string is OK - "(benchmark foo :assumption true)", - "(benchmark bar :formula true)", - "(benchmark qux :formula false)", - "(benchmark baz :extrapreds ( (a) (b) ) )", - "(benchmark zab :extrapreds ( (a) (b) ) :formula (implies (and (implies a b) a) b))", - "(benchmark zub :extrasorts (a) :extrafuns ( (f a a) (x a) ) :formula (= (f x) x))", - "(benchmark fuz :extrasorts (a) :extrafuns ((x a) (y a)) :formula (= (ite true x y) x))", - ";; nothing but a comment", - "; a comment\n(benchmark foo ; hello\n :formula true; goodbye\n)" - }; - -const int numGoodSmtInputs = sizeof(goodSmtInputs) / sizeof(string); - -/* The following expressions are valid after setupContext. */ -const string goodSmtExprs[] = { - "(and a b)", - "(or (and a b) c)", - "(implies (and (implies a b) a) b)", - "(and (iff a b) (not a))", - "(iff (xor a b) (and (or a b) (not (and a b))))", - "(ite a (f x) y)", - "(if_then_else a (f x) y)", - "1", - "0"// , -// "1.5" -}; - -const int numGoodSmtExprs = sizeof(goodSmtExprs) / sizeof(string); - -const string badSmtInputs[] = { - "(benchmark foo)", // empty benchmark is not OK - "(benchmark bar :assumption)", // no args - "(benchmark bar :formula)", - "(benchmark baz :extrapreds ( (a) (a) ) )", // double decl - "(benchmark zub :extrasorts (a) :extrapreds (p a))" // (p a) needs parens - }; - -const int numBadSmtInputs = sizeof(badSmtInputs) / sizeof(string); - -/* The following expressions are invalid even after setupContext. */ -const string badSmtExprs[] = { - "(and)", // wrong arity - "(and a b", // no closing paren - "(a and b)", // infix - "(OR (AND a b) c)", // wrong case - "(a IMPLIES b)", // infix AND wrong case - "(not a b)", // wrong arity - "not a", // needs parens - "(ite a x)", // wrong arity - "(a b)", // using non-function as function - ".5", // rational constants must have integer prefix - "1." // rational constants must have fractional suffix -}; - -const int numBadSmtExprs = sizeof(badSmtExprs) / sizeof(string); - -/************************** SMT v2 test inputs ********************************/ - -const string goodSmt2Inputs[] = { - "", // empty string is OK - "(set-logic QF_UF)", - "(set-info :notes |This is a note, take note!|)", - "(assert true)", - "(check-sat)", - "(exit)", - "(assert false) (check-sat)", - "(declare-fun a () Bool) (declare-fun b () Bool)", - "(declare-fun a () Bool) (declare-fun b () Bool) (assert (=> (and (=> a b) a) b))", - "(declare-sort a 0) (declare-fun f (a) a) (declare-fun x () a) (assert (= (f x) x))", - "(declare-sort a 0) (declare-fun x () a) (declare-fun y () a) (assert (= (ite true x y) x))", - ";; nothing but a comment", - "; a comment\n(check-sat ; goodbye\n)" - }; - -const int numGoodSmt2Inputs = sizeof(goodSmt2Inputs) / sizeof(string); - -/* The following expressions are valid after setupContext. */ -const string goodSmt2Exprs[] = { - "(and a b)", - "(or (and a b) c)", - "(=> (and (=> a b) a) b)", - "(and (= a b) (not a))", - "(= (xor a b) (and (or a b) (not (and a b))))", - "(ite a (f x) y)", - "1", - "0", - "1.5", - "#xfab09c7", - "#b0001011", - "(* 5 01)" // '01' is OK in non-strict mode -}; - -const int numGoodSmt2Exprs = sizeof(goodSmt2Exprs) / sizeof(string); - -const string badSmt2Inputs[] = { - "(assert)", // no args - "(set-info :notes |Symbols can't contain the | character|)", - "(check-sat true)", // shouldn't have an arg - "(declare-sort a)", // no arg - "(declare-sort a 0) (declare-sort a 0)", // double decl - "(declare-fun p Bool)" // should be "p () Bool" - }; - -const int numBadSmt2Inputs = sizeof(badSmt2Inputs) / sizeof(string); - -/* The following expressions are invalid even after setupContext - * in non-strict mode. */ -const string badSmt2Exprs[] = { - "(and)", // wrong arity - "(and a b", // no closing paren - "(a and b)", // infix - "(implies a b)", // no implies in v2 - "(iff a b)", // no iff in v2 - "(OR (AND a b) c)", // wrong case - "(a IMPLIES b)", // infix AND wrong case - "(not a b)", // wrong arity - "not a", // needs parens - "(ite a x)", // wrong arity - "(if_then_else a (f x) y)", // no if_then_else in v2 - "(a b)", // using non-function as function - ".5", // rational constants must have integer prefix - "1.", // rational constants must have fractional suffix - "#x", // hex constants must have at least one digit - "#b", // ditto binary constants - "#xg0f", - "#b9" -}; - -const int numBadSmt2Exprs = sizeof(badSmt2Exprs) / sizeof(string); - -/* The following expressions are invalid in strict mode, even after setupContext. */ -const string badStrictSmt2Exprs[] = { - "(and a)", // no unary and's - "(or a)", // no unary or's - "(* 5 01)" // '01' is not a valid integer constant -}; - -const int numBadStrictSmt2Exprs = sizeof(badStrictSmt2Exprs) / sizeof(string); - -class ParserBlack : public CxxTest::TestSuite { +class ParserBlack { + InputLanguage d_lang; ExprManager *d_exprManager; +protected: /* Set up declaration context for expr inputs */ - - void setupContext(Parser& parser) { + virtual void setupContext(Parser& parser) { /* a, b, c: BOOLEAN */ parser.mkVar("a",d_exprManager->booleanType()); parser.mkVar("b",d_exprManager->booleanType()); @@ -251,60 +56,54 @@ class ParserBlack : public CxxTest::TestSuite { parser.mkVar("z",v); } - void tryGoodInputs(InputLanguage d_lang, const string goodInputs[], int numInputs) { - for(int i = 0; i < numInputs; ++i) { + void tryGoodInput(const string goodInput) { try { -// Debug.on("parser"); +// Debug.on("parser"); // Debug.on("parser-extra"); - Debug("test") << "Testing good input: '" << goodInputs[i] << "'\n"; +// cerr << "Testing good input: <<" << goodInput << ">>" << endl; // istringstream stream(goodInputs[i]); - Input* input = Input::newStringInput(d_lang, goodInputs[i], "test"); + Input* input = Input::newStringInput(d_lang, goodInput, "test"); Parser parser(d_exprManager, input); TS_ASSERT( !parser.done() ); Command* cmd; while((cmd = parser.nextCommand()) != NULL) { - // cout << "Parsed command: " << (*cmd) << endl; + Debug("parser") << "Parsed command: " << (*cmd) << endl; } - TS_ASSERT( parser.nextCommand() == NULL ); + TS_ASSERT( parser.done() ); delete input; -// Debug.off("parser"); + Debug.off("parser"); // Debug.off("parser-extra"); } catch (Exception& e) { - cout << "\nGood input failed:\n" << goodInputs[i] << endl + cout << "\nGood input failed:\n" << goodInput << endl << e << endl; -// Debug.off("parser-extra"); +// Debug.off("parser"); throw; } - } } - void tryBadInputs(InputLanguage d_lang, const string badInputs[], int numInputs) { - for(int i = 0; i < numInputs; ++i) { -// cerr << "Testing bad input: '" << badInputs[i] << "'\n"; + void tryBadInput(const string badInput) { +// cerr << "Testing bad input: '" << badInput << "'\n"; // Debug.on("parser"); - Input* input = Input::newStringInput(d_lang, badInputs[i], "test"); + Input* input = Input::newStringInput(d_lang, badInput, "test"); Parser parser(d_exprManager, input); TS_ASSERT_THROWS ( while(parser.nextCommand()); - cout << "\nBad input succeeded:\n" << badInputs[i] << endl;, + cout << "\nBad input succeeded:\n" << badInput << endl;, const ParserException& ); // Debug.off("parser"); delete input; - } } - void tryGoodExprs(InputLanguage d_lang, const string goodBooleanExprs[], int numExprs) { - // cout << "Using context: " << context << endl; + void tryGoodExpr(const string goodExpr) { // Debug.on("parser"); // Debug.on("parser-extra"); - for(int i = 0; i < numExprs; ++i) { try { - // cout << "Testing good expr: '" << goodBooleanExprs[i] << "'\n"; +// cerr << "Testing good expr: '" << goodExpr << "'\n"; // Debug.on("parser"); // istringstream stream(context + goodBooleanExprs[i]); Input* input = Input::newStringInput(d_lang, - goodBooleanExprs[i], "test"); + goodExpr, "test"); Parser parser(d_exprManager, input); TS_ASSERT( !parser.done() ); setupContext(parser); @@ -318,11 +117,10 @@ class ParserBlack : public CxxTest::TestSuite { } catch (Exception& e) { cout << endl << "Good expr failed." << endl - << "Input: <<" << goodBooleanExprs[i] << ">>" << endl + << "Input: <<" << goodExpr << ">>" << endl << "Output: <<" << e << ">>" << endl; throw; } - } } /* NOTE: The check implemented here may fail if a bad expression expression string @@ -331,14 +129,11 @@ class ParserBlack : public CxxTest::TestSuite { * input. It's more trouble than it's worth to check that the whole input was * consumed here, so just be careful to avoid valid prefixes in tests. */ - void tryBadExprs(InputLanguage d_lang, const string badBooleanExprs[], int numExprs, - bool strictMode = false) { + void tryBadExpr(const string badExpr, bool strictMode = false) { // Debug.on("parser"); // Debug.on("parser-extra"); - for(int i = 0; i < numExprs; ++i) { -// cout << "Testing bad expr: '" << badBooleanExprs[i] << "'\n"; - Input* input = Input::newStringInput(d_lang, - badBooleanExprs[i], "test"); +// cout << "Testing bad expr: '" << badExpr << "'\n"; + Input* input = Input::newStringInput(d_lang, badExpr, "test"); Parser parser(d_exprManager, input); if( strictMode ) { parser.enableStrictMode(); @@ -349,78 +144,204 @@ class ParserBlack : public CxxTest::TestSuite { ( Expr e = parser.nextExpression(); cout << endl << "Bad expr succeeded." << endl - << "Input: <<" << badBooleanExprs[i] << ">>" << endl + << "Input: <<" << badExpr << ">>" << endl << "Output: <<" << e << ">>" << endl;, const ParserException& ); delete input; - } // Debug.off("parser"); } -public: - void setUp() { - d_exprManager = new ExprManager(); + ParserBlack(InputLanguage lang) : + d_lang(lang), + d_exprManager(new ExprManager()) { } - void tearDown() { +public: + virtual ~ParserBlack() { delete d_exprManager; } +}; - void testBs() { - DeclarationScope declScope; - declScope.bind("foo", d_exprManager->mkVar("foo",d_exprManager->booleanType())); +class Cvc4ParserTest : public CxxTest::TestSuite, public ParserBlack { - } +public: + Cvc4ParserTest() : ParserBlack(LANG_CVC4) { } void testGoodCvc4Inputs() { - tryGoodInputs(LANG_CVC4,goodCvc4Inputs,numGoodCvc4Inputs); + tryGoodInput(""); // empty string is OK + tryGoodInput("ASSERT TRUE;"); + tryGoodInput("QUERY TRUE;"); + tryGoodInput("CHECKSAT FALSE;"); + tryGoodInput("a, b : BOOLEAN;"); + tryGoodInput("a, b : BOOLEAN; QUERY (a => b) AND a => b;"); + tryGoodInput("T, U : TYPE; f : T -> U; x : T; CHECKSAT f(x) = x;"); + tryGoodInput("T : TYPE; x, y : T; a : BOOLEAN; QUERY (IF a THEN x ELSE y ENDIF) = x;"); + tryGoodInput("%% nothing but a comment"); + tryGoodInput("% a comment\nASSERT TRUE; %a command\n% another comment"); } void testBadCvc4Inputs() { - tryBadInputs(LANG_CVC4,badCvc4Inputs,numBadCvc4Inputs); + tryBadInput(";"); // no command + tryBadInput("ASSERT;"); // no args + tryBadInput("QUERY"); + tryBadInput("CHECKSAT"); + tryBadInput("a, b : boolean;"); // lowercase boolean isn't a type + tryBadInput("0x : INT;"); // 0x isn't an identifier + tryBadInput("a, b : BOOLEAN\nQUERY (a => b) AND a => b;"); // no semicolon after decl + tryBadInput("a : BOOLEAN; a: BOOLEAN;"); // double decl + tryBadInput("a, b: BOOLEAN; QUERY a(b);"); // non-function used as function } void testGoodCvc4Exprs() { - tryGoodExprs(LANG_CVC4,goodCvc4Exprs,numGoodCvc4Exprs); + tryGoodExpr("a AND b"); + tryGoodExpr("a AND b OR c"); + tryGoodExpr("(a => b) AND a => b"); + tryGoodExpr("(a <=> b) AND (NOT a)"); + tryGoodExpr("(a XOR b) <=> (a OR b) AND (NOT (a AND b))"); } void testBadCvc4Exprs() { - tryBadExprs(LANG_CVC4,badCvc4Exprs,numBadCvc4Exprs); + 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 } +}; + +class SmtParserTest : public CxxTest::TestSuite, public ParserBlack { +public: + SmtParserTest() : ParserBlack(LANG_SMTLIB) { } void testGoodSmtInputs() { - tryGoodInputs(LANG_SMTLIB,goodSmtInputs,numGoodSmtInputs); + 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 testBadSmtInputs() { - tryBadInputs(LANG_SMTLIB,badSmtInputs,numBadSmtInputs); + 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 } void testGoodSmtExprs() { - tryGoodExprs(LANG_SMTLIB,goodSmtExprs,numGoodSmtExprs); + 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 testBadSmtExprs() { - tryBadExprs(LANG_SMTLIB,badSmtExprs,numBadSmtExprs); + 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 + } +}; + +class Smt2ParserTest : public CxxTest::TestSuite, public ParserBlack { + typedef ParserBlack super; + +public: + Smt2ParserTest() : ParserBlack(LANG_SMTLIB_V2) { } + + void setupContext(Parser& parser) { + Smt2::addTheory(parser,Smt2::THEORY_CORE); + super::setupContext(parser); } void testGoodSmt2Inputs() { - tryGoodInputs(LANG_SMTLIB_V2,goodSmt2Inputs,numGoodSmt2Inputs); + tryGoodInput(""); // empty string is OK + tryGoodInput("(set-logic QF_UF)"); + tryGoodInput("(set-info :notes |This is a note, take note!|)"); + tryGoodInput("(set-logic QF_UF)(assert true)"); + tryGoodInput("(check-sat)"); + tryGoodInput("(exit)"); + tryGoodInput("(assert false) (check-sat)"); + tryGoodInput("(set-logic QF_UF) (declare-fun a () Bool) " + "(declare-fun b () Bool)"); + tryGoodInput("(set-logic QF_UF) (declare-fun a () Bool) " + "(declare-fun b () Bool) (assert (=> (and (=> a b) a) b))"); + tryGoodInput("(set-logic QF_UF) (declare-sort a 0) " + "(declare-fun f (a) a) (declare-fun x () a) " + "(assert (= (f x) x))"); + tryGoodInput("(set-logic QF_UF) (declare-sort a 0) " + "(declare-fun x () a) (declare-fun y () a) " + "(assert (= (ite true x y) x))"); + tryGoodInput(";; nothing but a comment"); + tryGoodInput("; a comment\n(check-sat ; goodbye\n)"); } void testBadSmt2Inputs() { - tryBadInputs(LANG_SMTLIB_V2,badSmt2Inputs,numBadSmt2Inputs); + tryBadInput("(assert)"); // no args + tryBadInput("(set-info :notes |Symbols can't contain the | character|)"); + tryBadInput("(check-sat true)"); // shouldn't have an arg + tryBadInput("(declare-sort a)"); // no arg + tryBadInput("(declare-sort a 0) (declare-sort a 0)"); // double decl + tryBadInput("(declare-fun p Bool)"); // should be "p () Bool" } void testGoodSmt2Exprs() { - tryGoodExprs(LANG_SMTLIB_V2,goodSmt2Exprs,numGoodSmt2Exprs); + tryGoodExpr("(and a b)"); + tryGoodExpr("(or (and a b) c)"); + tryGoodExpr("(=> (and (=> a b) a) b)"); + tryGoodExpr("(and (= a b) (not a))"); + tryGoodExpr("(= (xor a b) (and (or a b) (not (and a b))))"); + tryGoodExpr("(ite a (f x) y)"); + tryGoodExpr("1"); + tryGoodExpr("0"); + tryGoodExpr("1.5"); + tryGoodExpr("#xfab09c7"); + tryGoodExpr("#b0001011"); + tryGoodExpr("(* 5 01)"); // '01' is OK in non-strict mode } void testBadSmt2Exprs() { - tryBadExprs(LANG_SMTLIB_V2,badSmt2Exprs,numBadSmt2Exprs); - } - - void testBadSmt2StrictExprs() { - tryBadExprs(LANG_SMTLIB_V2,badStrictSmt2Exprs,numBadStrictSmt2Exprs,true); + tryBadExpr("(and)"); // wrong arity + tryBadExpr("(and a b"); // no closing paren + tryBadExpr("(a and b)"); // infix + tryBadExpr("(implies a b)"); // no implies in v2 + tryBadExpr("(iff a b)"); // no iff in v2 + 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("(if_then_else a (f x) y)"); // no if_then_else in v2 + tryBadExpr("(a b)"); // using non-function as function + tryBadExpr(".5"); // rational constants must have integer prefix + tryBadExpr("1."); // rational constants must have fractional suffix + tryBadExpr("#x"); // hex constants must have at least one digit + tryBadExpr("#b"); // ditto binary constants + tryBadExpr("#xg0f"); + tryBadExpr("#b9"); + // Bad strict exprs + 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 } }; -- 2.30.2