From 9697aa0761e798c95294bcaf291c648da0f1ba46 Mon Sep 17 00:00:00 2001 From: "Christopher L. Conway" Date: Fri, 18 Dec 2009 18:23:18 +0000 Subject: [PATCH] Updated parser tests, which are all kinds of FAIL --- test/unit/Makefile.am | 3 +- test/unit/Makefile.in | 3 +- test/unit/parser/cvc/cvc_parser_black.h | 127 -------------- test/unit/parser/parser_black.h | 213 ++++++++++++++++++++++++ test/unit/parser/smt/smt_parser_black.h | 121 -------------- 5 files changed, 215 insertions(+), 252 deletions(-) delete mode 100644 test/unit/parser/cvc/cvc_parser_black.h create mode 100644 test/unit/parser/parser_black.h delete mode 100644 test/unit/parser/smt/smt_parser_black.h diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index f05a74bcf..df85ba805 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -2,8 +2,7 @@ UNIT_TESTS = \ expr/node_white \ expr/node_black \ - parser/cvc/cvc_parser_black \ - parser/smt/smt_parser_black + parser/parser_black # things that aren't tests but that tests rely on and need to # go into the distribution diff --git a/test/unit/Makefile.in b/test/unit/Makefile.in index a3bb01929..4d20d59de 100644 --- a/test/unit/Makefile.in +++ b/test/unit/Makefile.in @@ -218,8 +218,7 @@ top_srcdir = @top_srcdir@ UNIT_TESTS = \ expr/node_white \ expr/node_black \ - parser/cvc/cvc_parser_black \ - parser/smt/smt_parser_black + parser/parser_black # things that aren't tests but that tests rely on and need to diff --git a/test/unit/parser/cvc/cvc_parser_black.h b/test/unit/parser/cvc/cvc_parser_black.h deleted file mode 100644 index 8c7dfb683..000000000 --- a/test/unit/parser/cvc/cvc_parser_black.h +++ /dev/null @@ -1,127 +0,0 @@ -/********************* -*- C++ -*- */ -/** cvc_parser_black.h - ** Original author: cconway - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information. - ** - ** Black box testing of CVC4::parser::CvcParser. - **/ - -#include -//#include -#include - -#include "expr/expr.h" -#include "expr/expr_manager.h" -#include "parser/parser.h" - -using namespace CVC4; -using namespace CVC4::parser; -using namespace std; - -const string goodInputs[] = { - "", // empty string is OK - "ASSERT TRUE;", - "QUERY TRUE;", - "CHECKSAT FALSE;", - "a, b : BOOLEAN;", - "x, y : INT;", - "a, b : BOOLEAN; QUERY (a => b) AND a => b;", - "%% nothing but a comment", - "% a comment\nASSERT TRUE %a command\n% another comment" - }; - -/* The following expressions are good in a context where a, b, and c have been declared as BOOLEAN. */ -const string goodBooleanExprs[] = { - "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 string badInputs[] = { - ";", // 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 - }; - -/* The following expressions are bad even in a context where a, b, and c have been declared as BOOLEAN. */ -const string badBooleanExprs[] = { - "", - "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 -}; - -class CvcParserBlack : public CxxTest::TestSuite { -private: - ExprManager *d_exprManager; - Parser::InputLanguage d_lang; - -public: - void setUp() { - d_exprManager = new ExprManager(); - d_lang = Parser::LANG_CVC4; - } - - void testGoodInputs() { - // cout << "In testGoodInputs()\n"; - for(int i = 0; i < sizeof(goodInputs); ++i) { - istringstream stream(goodInputs[i]); - Parser* cvcParser = Parser::getNewParser(d_exprManager, d_lang, stream); - TS_ASSERT( !cvcParser->done() ); - while(!cvcParser->done()) { - TS_ASSERT( cvcParser->parseNextCommand() != NULL ); - } - delete cvcParser; - } - } - - void testBadInputs() { - // cout << "In testGoodInputs()\n"; - for(int i = 0; i < sizeof(badInputs); ++i) { - istringstream stream(badInputs[i]); - Parser* cvcParser = Parser::getNewParser(d_exprManager, d_lang, stream); - TS_ASSERT_THROWS( cvcParser->parseNextCommand(), ParserException ); - delete cvcParser; - } - } - - void testGoodBooleanExprs() { - // cout << "In testGoodInputs()\n"; - for(int i = 0; i < sizeof(goodBooleanExprs); ++i) { - istringstream stream(goodBooleanExprs[i]); - Parser* cvcParser = Parser::getNewParser(d_exprManager, d_lang, stream); - TS_ASSERT( !cvcParser->done() ); - while(!cvcParser->done()) { - TS_ASSERT( !cvcParser->parseNextExpression().isNull() ); - } - delete cvcParser; - } - } - - void testBadBooleanExprs() { - // cout << "In testGoodInputs()\n"; - for(int i = 0; i < sizeof(badBooleanExprs); ++i) { - istringstream stream(badBooleanExprs[i]); - Parser* cvcParser = Parser::getNewParser(d_exprManager, d_lang, stream); - TS_ASSERT_THROWS( cvcParser->parseNextExpression(), ParserException ); - delete cvcParser; - } - } - -}; diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h new file mode 100644 index 000000000..645882724 --- /dev/null +++ b/test/unit/parser/parser_black.h @@ -0,0 +1,213 @@ +/********************* -*- C++ -*- */ +/** smt_parser_black.h + ** Original author: cconway + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** Black box testing of CVC4::parser::SmtParser. + **/ + +#include +//#include +#include + +#include "expr/expr.h" +#include "expr/expr_manager.h" +#include "parser/parser.h" + +using namespace CVC4; +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;", + "%% nothing but a comment", + "% a comment\nASSERT TRUE %a command\n% another comment", + }; + +const int numGoodCvc4Inputs = sizeof(goodCvc4Inputs) / sizeof(string); + +/* The following expressions are good in a context where a, b, and c have been declared as BOOLEAN. */ +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 + }; + +const int numBadCvc4Inputs = sizeof(badCvc4Inputs) / sizeof(string); + +/* The following expressions are bad even in a context where a, b, and c have been declared as BOOLEAN. */ +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 :assume 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))", + ";; 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 good in a context where a, b, and c have been declared as BOOLEAN. */ +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))))" +}; + +const int numGoodSmtExprs = sizeof(goodSmtExprs) / sizeof(string); + +const string badSmtInputs[] = { + "(benchmark foo)", // empty benchmark is not OK + "(benchmark bar :assume)", // no args + "(benchmark bar :formula)", + "(benchmark baz :extrapreds ( (a) (a) ) )" // double decl + }; + +const int numBadSmtInputs = sizeof(badSmtInputs) / sizeof(string); + +/* The following expressions are bad even in a context where a, b, and c have been declared as BOOLEAN. */ +const string badSmtExprs[] = { + "", + "(and a)", // 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 +}; + +const int numBadSmtExprs = sizeof(badSmtExprs) / sizeof(string); + +class SmtParserBlack : public CxxTest::TestSuite { + ExprManager *d_exprManager; + + void tryGoodInputs(Parser::InputLanguage d_lang, const string goodInputs[], int numInputs) { + for(int i = 0; i < numInputs; ++i) { + cout << "Testing input: '" << goodInputs[i] << "'\n"; + istringstream stream(goodInputs[i]); + Parser* smtParser = Parser::getNewParser(d_exprManager, d_lang, stream); + TS_ASSERT( !smtParser->done() ); + while(!smtParser->done()) { + TS_ASSERT( smtParser->parseNextCommand() != NULL ); + } + delete smtParser; + } + } + + void tryBadInputs(Parser::InputLanguage d_lang, const string badInputs[], int numInputs) { + for(int i = 0; i < numInputs; ++i) { + cout << "Testing input: '" << badInputs[i] << "'\n"; + istringstream stream(badInputs[i]); + Parser* smtParser = Parser::getNewParser(d_exprManager, d_lang, stream); + TS_ASSERT_THROWS( smtParser->parseNextCommand(), ParserException ); + delete smtParser; + } + } + + void tryGoodExprs(Parser::InputLanguage d_lang,const string goodBooleanExprs[], int numExprs) { + for(int i = 0; i < numExprs; ++i) { + cout << "Testing expr: '" << goodBooleanExprs[i] << "'\n"; + istringstream stream(goodBooleanExprs[i]); + Parser* smtParser = Parser::getNewParser(d_exprManager, d_lang, stream); + TS_ASSERT( !smtParser->done() ); + while(!smtParser->done()) { + TS_ASSERT( !smtParser->parseNextExpression().isNull() ); + } + delete smtParser; + } + } + + void tryBadExprs(Parser::InputLanguage d_lang,const string badBooleanExprs[], int numExprs) { + for(int i = 0; i < numExprs; ++i) { + cout << "Testing expr: '" << badBooleanExprs[i] << "'\n"; + istringstream stream(badBooleanExprs[i]); + Parser* smtParser = Parser::getNewParser(d_exprManager, d_lang, stream); + TS_ASSERT_THROWS( smtParser->parseNextExpression(), ParserException ); + } + } + +public: + void setUp() { + d_exprManager = new ExprManager(); + } + + void testGoodCvc4Inputs() { + tryGoodInputs(Parser::LANG_CVC4,goodCvc4Inputs,numGoodCvc4Inputs); + } + + void testBadCvc4Inputs() { + tryBadInputs(Parser::LANG_CVC4,badCvc4Inputs,numBadCvc4Inputs); + } + + void testGoodCvc4Exprs() { + tryGoodExprs(Parser::LANG_CVC4,goodCvc4Exprs,numGoodCvc4Exprs); + } + + void testBadCvc4Exprs() { + tryBadExprs(Parser::LANG_CVC4,badCvc4Exprs,numBadCvc4Exprs); + } + + void testGoodSmtInputs() { + tryGoodInputs(Parser::LANG_SMTLIB,goodSmtInputs,numGoodSmtInputs); + } + + void testBadSmtInputs() { + tryBadInputs(Parser::LANG_SMTLIB,badSmtInputs,numBadSmtInputs); + } + + void testGoodSmtExprs() { + tryGoodExprs(Parser::LANG_SMTLIB,goodSmtExprs,numGoodSmtExprs); + } + + void testBadSmtExprs() { + tryBadExprs(Parser::LANG_SMTLIB,badSmtExprs,numBadSmtExprs); + } +}; diff --git a/test/unit/parser/smt/smt_parser_black.h b/test/unit/parser/smt/smt_parser_black.h deleted file mode 100644 index 0f1e03f6c..000000000 --- a/test/unit/parser/smt/smt_parser_black.h +++ /dev/null @@ -1,121 +0,0 @@ -/********************* -*- C++ -*- */ -/** smt_parser_black.h - ** Original author: cconway - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information. - ** - ** Black box testing of CVC4::parser::SmtParser. - **/ - -#include -//#include -#include - -#include "expr/expr.h" -#include "expr/expr_manager.h" -#include "parser/parser.h" - -using namespace CVC4; -using namespace CVC4::parser; -using namespace std; - -const string goodInputs[] = { - "", // empty string is OK - "(benchmark foo :assume 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))", - ";; nothing but a comment", - "; a comment\n)(benchmark foo ; hello\n :formula true; goodbye\n)" - }; - -/* The following expressions are good in a context where a, b, and c have been declared as BOOLEAN. */ -const string goodBooleanExprs[] = { - "(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))))" -}; - -const string badInputs[] = { - "(benchmark foo)", // empty benchmark is not OK - "(benchmark bar :assume)", // no args - "(benchmark bar :formula)", - }; - -/* The following expressions are bad even in a context where a, b, and c have been declared as BOOLEAN. */ -const string badBooleanExprs[] = { - "", - "(and a)", // 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 -}; - -class SmtParserBlack : public CxxTest::TestSuite { -private: - ExprManager *d_exprManager; - Parser::InputLanguage d_lang; -public: - void setUp() { - d_exprManager = new ExprManager(); - d_lang = Parser::LANG_SMTLIB; - } - - void testGoodInputs() { - // cout << "In testGoodInputs()\n"; - for(int i = 0; i < sizeof(goodInputs); ++i) { - istringstream stream(goodInputs[i]); - Parser* smtParser = Parser::getNewParser(d_exprManager, d_lang, stream); - TS_ASSERT( !smtParser->done() ); - while(!smtParser->done()) { - TS_ASSERT( smtParser->parseNextCommand() != NULL ); - } - delete smtParser; - } - } - - void testBadInputs() { - // cout << "In testGoodInputs()\n"; - for(int i = 0; i < sizeof(badInputs); ++i) { - istringstream stream(badInputs[i]); - Parser* smtParser = Parser::getNewParser(d_exprManager, d_lang, stream); - TS_ASSERT_THROWS( smtParser->parseNextCommand(), ParserException ); - delete smtParser; - } - } - - void testGoodBooleanExprs() { - // cout << "In testGoodInputs()\n"; - for(int i = 0; i < sizeof(goodBooleanExprs); ++i) { - istringstream stream(goodBooleanExprs[i]); - Parser* smtParser = Parser::getNewParser(d_exprManager, d_lang, stream); - TS_ASSERT( !smtParser->done() ); - while(!smtParser->done()) { - TS_ASSERT( !smtParser->parseNextExpression().isNull() ); - } - delete smtParser; - } - } - - void testBadBooleanExprs() { - // cout << "In testGoodInputs()\n"; - for(int i = 0; i < sizeof(badBooleanExprs); ++i) { - istringstream stream(badBooleanExprs[i]); - SmtParser smtParser(d_exprManager, stream); - TS_ASSERT_THROWS( smtParser.parseNextExpression(), ParserException ); - } - } - -}; -- 2.30.2