From: Christopher L. Conway Date: Thu, 17 Dec 2009 20:41:24 +0000 (+0000) Subject: Adding more parser tests X-Git-Tag: cvc5-1.0.0~9357 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fdc93191d331c6bd4a2934eb5cbeb18d78cb078d;p=cvc5.git Adding more parser tests --- diff --git a/test/unit/parser/smt/smt_parser_black.h b/test/unit/parser/smt/smt_parser_black.h new file mode 100644 index 000000000..3b4b81239 --- /dev/null +++ b/test/unit/parser/smt/smt_parser_black.h @@ -0,0 +1,104 @@ +/* Black box testing of smt4::parser:SmtParser. */ + +#include +//#include +#include + +#include "expr/expr.h" +#include "expr/expr_manager.h" +#include "parser/smt/smt_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; + +public: + void setUp() { + d_exprManager = new ExprManager(); + } + + void testGoodInputs() { + // cout << "In testGoodInputs()\n"; + for(int i = 0; i < sizeof(goodInputs); ++i) { + istringstream stream(goodInputs[i]); + SmtParser smtParser(d_exprManager, stream); + TS_ASSERT( !smtParser.done() ); + while(!smtParser.done()) { + TS_ASSERT( smtParser.parseNextCommand() != NULL ); + } + } + } + + void testBadInputs() { + // cout << "In testGoodInputs()\n"; + for(int i = 0; i < sizeof(badInputs); ++i) { + istringstream stream(badInputs[i]); + SmtParser smtParser(d_exprManager, stream); + TS_ASSERT_THROWS( smtParser.parseNextCommand(), ParserException ); + } + } + + void testGoodBooleanExprs() { + // cout << "In testGoodInputs()\n"; + for(int i = 0; i < sizeof(goodBooleanExprs); ++i) { + istringstream stream(goodBooleanExprs[i]); + SmtParser smtParser(d_exprManager, stream); + TS_ASSERT( !smtParser.done() ); + while(!smtParser.done()) { + TS_ASSERT( !smtParser.parseNextExpression().isNull() ); + } + } + } + + 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 ); + } + } + +};