From: Dejan Jovanović Date: Fri, 18 Dec 2009 23:34:05 +0000 (+0000) Subject: More fixes fot the parser tests. X-Git-Tag: cvc5-1.0.0~9347 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1b3c2dc36df9d21a9eb7a536627ba37e13540c3a;p=cvc5.git More fixes fot the parser tests. --- diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp index ee9334f3c..6cbb41812 100644 --- a/src/expr/expr.cpp +++ b/src/expr/expr.cpp @@ -100,6 +100,10 @@ bool Expr::isNull() const { return d_node->isNull(); } +Expr::operator bool() const { + return !isNull(); +} + void Expr::toStream(std::ostream& out) const { d_node->toStream(out); } diff --git a/src/expr/expr.h b/src/expr/expr.h index 447c35f77..eb4d1ce03 100644 --- a/src/expr/expr.h +++ b/src/expr/expr.h @@ -83,6 +83,11 @@ public: */ bool operator<(const Expr& e) const; + /** + * Returns true if the expression is not the null expression. + */ + operator bool() const; + /** * Returns the hash value of the expression. Equal expression will have the * same hash value. diff --git a/src/parser/cvc/cvc_lexer.g b/src/parser/cvc/cvc_lexer.g index 863b15a95..52c58a38f 100644 --- a/src/parser/cvc/cvc_lexer.g +++ b/src/parser/cvc/cvc_lexer.g @@ -17,6 +17,10 @@ options { k = 2; } +/* + * The tokens that might match with the identifiers go here. Otherwise define + * them below. + */ tokens { // Types BOOLEAN = "BOOLEAN"; @@ -32,25 +36,28 @@ tokens { TRUE = "TRUE"; FALSE = "FALSE"; XOR = "XOR"; - IMPLIES = "=>"; - IFF = "<=>"; // Commands ASSERT = "ASSERT"; QUERY = "QUERY"; CHECKSAT = "CHECKSAT"; PRINT = "PRINT"; - EXHO = "ECHO"; + ECHO = "ECHO"; PUSH = "PUSH"; POP = "POP"; POPTO = "POPTO"; } +// Operators +COMMA : ','; +IMPLIES : "=>"; +IFF : "<=>"; + /** * Matches any letter ('a'-'z' and 'A'-'Z'). */ protected -ALPHA options{ paraphrase = "a letter"; } +ALPHA options { paraphrase = "a letter"; } : 'a'..'z' | 'A'..'Z' ; @@ -59,31 +66,24 @@ ALPHA options{ paraphrase = "a letter"; } * Matches the digits (0-9) */ protected -DIGIT options{ paraphrase = "a digit"; } +DIGIT options { paraphrase = "a digit"; } : '0'..'9' ; /** * Matches the ':' */ -COLON options{ paraphrase = "a colon"; } +COLON options { paraphrase = "a colon"; } : ':' ; /** * Matches the 'l' */ -SEMICOLON options{ paraphrase = "a semicolon"; } +SEMICOLON options { paraphrase = "a semicolon"; } : ';' ; -/** - * Matches the ',' - */ -COMMA options{ paraphrase = "a comma"; } - : ',' - ; - /** * Matches an identifier from the input. An identifier is a sequence of letters, * digits and "_", "'", "." symbols, starting with a letter. diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g index a22ce64e7..91864329e 100644 --- a/src/parser/cvc/cvc_parser.g +++ b/src/parser/cvc/cvc_parser.g @@ -77,8 +77,8 @@ identifierList[std::vector& idList, DeclarationCheck check = CHECK_ { string id; } - : id = identifier { idList.push_back(id); } - (COMMA id = identifier { idList.push_back(id); })* + : id = identifier[check] { idList.push_back(id); } + (COMMA id = identifier[check] { idList.push_back(id); })* ; @@ -126,11 +126,11 @@ boolFormula returns [CVC4::Expr formula] { vector formulas; vector kinds; - Expr f1, f2; + Expr f; Kind k; } - : f1 = primaryBoolFormula { formulas.push_back(f1); } - ( k = boolOperator { kinds.push_back(k); } f2 = primaryBoolFormula { formulas.push_back(f2); } )* + : f = primaryBoolFormula { formulas.push_back(f); } + ( k = boolOperator { kinds.push_back(k); } f = primaryBoolFormula { formulas.push_back(f); } )* { // Create the expression based on precedences formula = createPrecedenceExpr(formulas, kinds); diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 7b4810abb..96fe5f6a5 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -46,6 +46,7 @@ Command* Parser::parseNextCommand() throw(ParserException, AssertionException) { if(!done()) { try { cmd = d_antlrParser->parseCommand(); + if (cmd == NULL) setDone(); } catch(antlr::ANTLRException& e) { setDone(); throw ParserException(e.toString()); diff --git a/src/parser/symbol_table.h b/src/parser/symbol_table.h index 8c9582762..be2a958b8 100644 --- a/src/parser/symbol_table.h +++ b/src/parser/symbol_table.h @@ -59,6 +59,7 @@ public: */ void bindName(const std::string name, const ObjectType& obj) throw () { d_nameBindings[name].push(obj); + Assert(isBound(name), "Expected name to be bound!"); } /** diff --git a/src/util/command.cpp b/src/util/command.cpp index b80851233..334180967 100644 --- a/src/util/command.cpp +++ b/src/util/command.cpp @@ -129,11 +129,11 @@ void DeclarationCommand::toStream(std::ostream& out) const { out << "Declare("; bool first = true; for(unsigned i = 0; i < d_declaredSymbols.size(); ++i) { - if(first) { + if(!first) { out << ", "; - first = false; } out << d_declaredSymbols[i]; + first = false; } out << ")"; } diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index 1d4afbb7c..6db3b770b 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -35,11 +35,13 @@ const string goodCvc4Inputs[] = { "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", + "% a comment\nASSERT TRUE; %a command\n% another comment", }; const int numGoodCvc4Inputs = sizeof(goodCvc4Inputs) / sizeof(string); +const string cvc4ExprContext = "a,b,c:BOOLEAN;"; + /* The following expressions are good in a context where a, b, and c have been declared as BOOLEAN. */ const string goodCvc4Exprs[] = { "a AND b", @@ -55,7 +57,7 @@ const string badCvc4Inputs[] = { ";", // no command "ASSERT;", // no args "QUERY", - "CHECKSAT;", + "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 @@ -66,7 +68,6 @@ 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 @@ -92,6 +93,8 @@ const string goodSmtInputs[] = { const int numGoodSmtInputs = sizeof(goodSmtInputs) / sizeof(string); +const string smtExprContext = "(benchmark foo :extrapreds ((a) (b) (c)) )"; + /* The following expressions are good in a context where a, b, and c have been declared as BOOLEAN. */ const string goodSmtExprs[] = { "(and a b)", @@ -105,7 +108,7 @@ const int numGoodSmtExprs = sizeof(goodSmtExprs) / sizeof(string); const string badSmtInputs[] = { "(benchmark foo)", // empty benchmark is not OK - "(benchmark bar :assume)", // no args + "(benchmark bar :assumption)", // no args "(benchmark bar :formula)", "(benchmark baz :extrapreds ( (a) (a) ) )" // double decl }; @@ -114,7 +117,6 @@ 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 @@ -135,9 +137,12 @@ class SmtParserBlack : public CxxTest::TestSuite { 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 ); + Command* cmd; + while((cmd = smtParser->parseNextCommand())) { + cout << "Parsed command: " << *cmd << endl; } + TS_ASSERT( smtParser->parseNextCommand() == NULL ); + TS_ASSERT( smtParser->done() ); delete smtParser; } } @@ -147,21 +152,33 @@ class SmtParserBlack : public CxxTest::TestSuite { 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 ); + TS_ASSERT_THROWS( while(smtParser->parseNextCommand()); , ParserException ); delete smtParser; } } - void tryGoodExprs(Parser::InputLanguage d_lang,const string goodBooleanExprs[], int numExprs) { + void tryGoodExprs(Parser::InputLanguage d_lang,const string& context, const string goodBooleanExprs[], int numExprs) { + cout << "Using context: " << context << endl; 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() ); + try { + cout << "Testing expr: '" << goodBooleanExprs[i] << "'\n"; + istringstream stream(context + goodBooleanExprs[i]); + Parser* parser = Parser::getNewParser(d_exprManager, d_lang, stream); + TS_ASSERT( !parser->done() ); + Command* cmd = parser->parseNextCommand(); + TS_ASSERT( !parser->done() ); + Expr e; + while(e = parser->parseNextExpression()) { + cout << "Parsed expr: " << e << endl; + } + TS_ASSERT( parser->done() ); + TS_ASSERT( e.isNull() ); + delete cmd; + delete parser; + } catch (ParserException& e) { + cout << "Caught: " << e << endl; + TS_ASSERT( false ); } - delete smtParser; } } @@ -188,7 +205,7 @@ public: } void testGoodCvc4Exprs() { - tryGoodExprs(Parser::LANG_CVC4,goodCvc4Exprs,numGoodCvc4Exprs); + tryGoodExprs(Parser::LANG_CVC4,cvc4ExprContext,goodCvc4Exprs,numGoodCvc4Exprs); } void testBadCvc4Exprs() { @@ -204,7 +221,7 @@ public: } void testGoodSmtExprs() { - tryGoodExprs(Parser::LANG_SMTLIB,goodSmtExprs,numGoodSmtExprs); + tryGoodExprs(Parser::LANG_SMTLIB,smtExprContext,goodSmtExprs,numGoodSmtExprs); } void testBadSmtExprs() {