Minor changes to parser files from code review.

diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp
index a50b1f18f69a563b778b05092174f1635b5c0ddb..2d3033a594f3d3e304f30afef274d913395c13f5 100644 (file)
--- 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 ad23d45f83c2b41cdcc825896f4e48059a6dd575..b2ef3f1818d26a81cb661240f83abf65760fcb49 100644 (file)
--- 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 8d706963f35ed9084222e224e60a8b093241759e..dd0d7c69c1022d134d380ca1cee523c6e1fca4e8 100644 (file)
--- 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 625f2c381e3714c64d30a6b47c0fd6a27dd23cf4..864719cfa7681e4fda812abe5a2fa5053dda380f 100644 (file)
--- 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 3d9a84f069d289427edf83af33d2ce5053e03781..70f60a0bcbebc66eaae4ef86d996c2b5c54e48ea 100644 (file)
--- 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 b1bb35e6fc993eb3633b3f980aa8c91ed50d8842..6e0051821c5628ef2aa3a0b2c8201074bbf5591a 100644 (file)
--- 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 a68f0e783cf72c02902c16c60ec0976e165627f9..6927888cfab7ce3cde4df72df7d58536338b7127 100644 (file)
--- 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)