More fixes fot the parser tests.

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 << ")";
 }