From 8cb3a7b556e8b4b85745bffbd1f0246e6af29588 Mon Sep 17 00:00:00 2001 From: "Christopher L. Conway" Date: Tue, 15 Dec 2009 23:05:02 +0000 Subject: [PATCH] Minor changes to parser files from code review. --- src/parser/antlr_parser.cpp | 12 ++++++++++++ src/parser/antlr_parser.h | 23 +++++++++++++---------- src/parser/cvc/cvc_lexer.g | 4 ++-- src/parser/cvc/cvc_parser.g | 1 + src/parser/smt/smt_lexer.g | 4 ++-- src/parser/smt/smt_parser.g | 11 ++++++----- src/parser/smt/smt_parser.h | 3 +-- 7 files changed, 37 insertions(+), 21 deletions(-) diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp index a50b1f18f..2d3033a59 100644 --- a/src/parser/antlr_parser.cpp +++ b/src/parser/antlr_parser.cpp @@ -9,6 +9,7 @@ #include "antlr_parser.h" #include "util/output.h" +#include "util/Assert.h" using namespace std; using namespace CVC4; @@ -134,11 +135,16 @@ void AntlrParser::rethrow(antlr::SemanticException& e, string new_message) Expr AntlrParser::createPrecedenceExpr(const vector& exprs, const vector< Kind>& kinds) { + Assert( exprs.size() > 0, "Expected non-empty vector expr"); + Assert( vectors.size() + 1 == exprs.size(), "Expected kinds to match exprs"); return createPrecedenceExpr(exprs, kinds, 0, exprs.size() - 1); } unsigned AntlrParser::findPivot(const std::vector& kinds, unsigned start_index, unsigned end_index) const { + Assert( start_index >= 0, "Expected start_index >= 0. "); + Assert( end_index < kinds.size(), "Expected end_index < kinds.size(). "); + Assert( start_index <= end_index, "Expected start_index <= end_index. "); int pivot = start_index; unsigned pivot_precedence = getPrecedence(kinds[pivot]); @@ -157,6 +163,12 @@ unsigned AntlrParser::findPivot(const std::vector& kinds, Expr AntlrParser::createPrecedenceExpr(const std::vector& exprs, const std::vector& kinds, unsigned start_index, unsigned end_index) { + Assert( exprs.size() > 0, "Expected non-empty vector expr"); + Assert( kinds.size() + 1 == exprs.size(), "Expected kinds to match exprs."); + Assert( start_index >= 0, "Expected start_index >= 0. "); + Assert( end_index < exprs.size(), "Expected end_index < exprs.size. "); + Assert( start_index <= end_index, "Expected start_index <= end_index. "); + if(start_index == end_index) return exprs[start_index]; diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h index ad23d45f8..b2ef3f181 100644 --- a/src/parser/antlr_parser.h +++ b/src/parser/antlr_parser.h @@ -27,7 +27,7 @@ namespace parser { /** * Wrapper of the ANTLR parser that includes convenience methods that interacts * with the expression manager. The grammars should have as little C++ code as - * possible and all the state and actuall functionality (besides parsing) should + * possible and all the state and actual functionality (besides parsing) should * go into this class. */ class AntlrParser : public antlr::LLkParser { @@ -45,7 +45,7 @@ public: }; /** - * Set's the expression manager to use when creating/managing expression. + * Sets the expression manager to use when creating/managing expression. * @param expr_manager the expression manager */ void setExpressionManager(ExprManager* expr_manager); @@ -53,8 +53,7 @@ public: protected: /** - * Class constructor, just tunnels the construction to the antlr - * LLkParser class. + * Create a parser with the given input state and token lookahead. * * @param state the shared input state * @param k lookahead @@ -62,8 +61,7 @@ protected: AntlrParser(const antlr::ParserSharedInputState& state, int k); /** - * Class constructor, just tunnels the construction to the antlr - * LLkParser class. + * Create a parser with the given token buffer and lookahead. * * @param tokenBuf the token buffer to use in parsing * @param k lookahead @@ -71,8 +69,7 @@ protected: AntlrParser(antlr::TokenBuffer& tokenBuf, int k); /** - * Class constructor, just tunnels the construction to the antlr - * LLkParser class. + * Create a parser with the given token stream and lookahead. * * @param lexer the lexer to use in parsing * @param k lookahead @@ -143,8 +140,11 @@ protected: Expr newExpression(Kind kind, const std::vector& children); /** - * Creates a new expression based on the given string of expressions and kinds. + * Creates a new expression based on the given string of expressions and kinds, + * where kinds[i] is the operator to place between exprs[i] and exprs[i+1]. * The expression is created so that it respects the kinds precedence table. + * The exprs vector should be non-empty. If the length of exprs is N, then the + * length of kinds should be N-1 (kinds may be empty). */ Expr createPrecedenceExpr(const std::vector& exprs, const std::vector& kinds); @@ -190,8 +190,11 @@ private: unsigned findPivot(const std::vector& kinds, unsigned start_index, unsigned end_index) const; /** - * Creates a new expression based on the given string of expressions and kinds. + * Creates a new expression based on the given string of expressions and kinds * The expression is created so that it respects the kinds precedence table. + * The exprs vector should be non-empty. The kinds vector should have one less + * element than the exprs vector. start_index and end_index should be valid + * indices into exprs. */ Expr createPrecedenceExpr(const std::vector& exprs, const std::vector& kinds, unsigned start_index, unsigned end_index); diff --git a/src/parser/cvc/cvc_lexer.g b/src/parser/cvc/cvc_lexer.g index 8d706963f..dd0d7c69c 100644 --- a/src/parser/cvc/cvc_lexer.g +++ b/src/parser/cvc/cvc_lexer.g @@ -66,7 +66,7 @@ DIGIT options{ paraphrase = "a digit"; } /** * Matches the ':' */ -COLON options{ paraphrase = "a comma"; } +COLON options{ paraphrase = "a colon"; } : ':' ; @@ -115,7 +115,7 @@ NEWLINE options { paraphrase = "a newline"; } * Mathces the comments and ignores them */ COMMENT options { paraphrase = "comment"; } - : ';' (~('\n' | '\r'))* { $setType(antlr::Token::SKIP); } + : '%' (~('\n' | '\r'))* { $setType(antlr::Token::SKIP); } ; /** diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g index 625f2c381..864719cfa 100644 --- a/src/parser/cvc/cvc_parser.g +++ b/src/parser/cvc/cvc_parser.g @@ -42,6 +42,7 @@ command returns [CVC4::Command* cmd = 0] | CHECKSAT f = formula { cmd = new CheckSatCommand(f); } | CHECKSAT { cmd = new CheckSatCommand(); } | identifierList[ids] COLON type { + // [chris 12/15/2009] FIXME: decls may not be BOOLEAN newPredicates(ids); cmd = new EmptyCommand("Declaration"); } diff --git a/src/parser/smt/smt_lexer.g b/src/parser/smt/smt_lexer.g index 3d9a84f06..70f60a0bc 100644 --- a/src/parser/smt/smt_lexer.g +++ b/src/parser/smt/smt_lexer.g @@ -14,7 +14,7 @@ class AntlrSmtLexer extends Lexer; options { exportVocab = SmtVocabulary; // Name of the shared token vocabulary testLiterals = false; // Do not check for literals by default - defaultErrorHandler = false; // Skip the defaul error handling, just break with exceptions + defaultErrorHandler = false; // Skip the default error handling, just break with exceptions k = 2; } @@ -130,7 +130,7 @@ WHITESPACE options { paraphrase = "whitespace"; } ; /** - * Mathces and skips the newline symbols in the input. + * Matches and skips the newline symbols in the input. */ NEWLINE options { paraphrase = "a newline"; } : ('\r' '\n' | '\r' | '\n') { $setType(antlr::Token::SKIP); newline(); } diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g index b1bb35e6f..6e0051821 100644 --- a/src/parser/smt/smt_parser.g +++ b/src/parser/smt/smt_parser.g @@ -50,7 +50,7 @@ annotation ; /** - * Matches a predicate symbol from the input. + * Matches a predicate symbol. */ pred_symb returns [std::string p] : id:IDENTIFIER { p = id->getText(); } @@ -58,7 +58,7 @@ pred_symb returns [std::string p] /** - * Matches a propositional atom from the input. + * Matches a propositional atom. */ prop_atom returns [CVC4::Expr atom] { @@ -73,17 +73,18 @@ prop_atom returns [CVC4::Expr atom] ; /** - * Matches an annotated proposition atom which is either a propositional atom, + * Matches an annotated proposition atom, which is either a propositional atom * or built of other atoms using a predicate symbol. Annotation can be added if * enclosed in brackets. The prop_atom rule from the original SMT grammar is inlined - * here in order to get rid of the ugly antlr non-determinism warrnings. + * here in order to get rid of the ugly antlr non-determinism warnings. */ + // [chris 12/15/2009] FIXME: Where is the annotation? an_atom returns [CVC4::Expr atom] : atom = prop_atom ; /** - * Matches on of the unary Boolean conectives. + * Matches on of the unary Boolean connectives. */ bool_connective returns [CVC4::Kind kind] : NOT { kind = CVC4::NOT; } diff --git a/src/parser/smt/smt_parser.h b/src/parser/smt/smt_parser.h index a68f0e783..6927888cf 100644 --- a/src/parser/smt/smt_parser.h +++ b/src/parser/smt/smt_parser.h @@ -31,8 +31,7 @@ class CVC4_PUBLIC SmtParser : public Parser { public: /** - * Construct the parser that uses the given expression manager and parses - * from the given input stream. + * Construct the parser that uses the given expression manager and input stream. * @param em the expression manager to use * @param input the input stream to parse * @param file_name the name of the file (for diagnostic output) -- 2.30.2