summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/parser/antlr_parser.cpp12
-rw-r--r--src/parser/antlr_parser.h23
-rw-r--r--src/parser/cvc/cvc_lexer.g4
-rw-r--r--src/parser/cvc/cvc_parser.g1
-rw-r--r--src/parser/smt/smt_lexer.g4
-rw-r--r--src/parser/smt/smt_parser.g11
-rw-r--r--src/parser/smt/smt_parser.h3
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<Expr>& 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<Kind>& 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<Kind>& kinds,
Expr AntlrParser::createPrecedenceExpr(const std::vector<Expr>& exprs,
const std::vector<Kind>& 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<Expr>& 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<Expr>& exprs, const std::vector<Kind>& kinds);
@@ -190,8 +190,11 @@ private:
unsigned findPivot(const std::vector<Kind>& 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<Expr>& exprs, const std::vector<Kind>& 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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback