diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2009-12-15 23:05:02 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2009-12-15 23:05:02 +0000 |
commit | 8cb3a7b556e8b4b85745bffbd1f0246e6af29588 (patch) | |
tree | cdff09f0a4a274a402c05013013091c0c7966615 /src/parser/smt | |
parent | 7cc208713f373ee83946b9d53a9c405bfec9e107 (diff) |
Minor changes to parser files from code review.
Diffstat (limited to 'src/parser/smt')
-rw-r--r-- | src/parser/smt/smt_lexer.g | 4 | ||||
-rw-r--r-- | src/parser/smt/smt_parser.g | 11 | ||||
-rw-r--r-- | src/parser/smt/smt_parser.h | 3 |
3 files changed, 9 insertions, 9 deletions
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) |