diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2009-12-18 23:34:05 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2009-12-18 23:34:05 +0000 |
commit | 1b3c2dc36df9d21a9eb7a536627ba37e13540c3a (patch) | |
tree | fe339ff256ac0acc3dcc21bb545bd33cc535cfab /src | |
parent | 9d57ed6b7e78373bec9db88adfb9878e377abb97 (diff) |
More fixes fot the parser tests.
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/expr.cpp | 4 | ||||
-rw-r--r-- | src/expr/expr.h | 5 | ||||
-rw-r--r-- | src/parser/cvc/cvc_lexer.g | 28 | ||||
-rw-r--r-- | src/parser/cvc/cvc_parser.g | 10 | ||||
-rw-r--r-- | src/parser/parser.cpp | 1 | ||||
-rw-r--r-- | src/parser/symbol_table.h | 1 | ||||
-rw-r--r-- | src/util/command.cpp | 4 |
7 files changed, 32 insertions, 21 deletions
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 @@ -84,6 +84,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,32 +66,25 @@ 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<std::string>& 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<Expr> formulas; vector<Kind> 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 << ")"; } |