More fixes fot the parser tests.

8 files changed, 67 insertions, 39 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 << ")";
 }
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index 1d4afbb7c..6db3b770b 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -35,11 +35,13 @@ const string goodCvc4Inputs[] = {
       "a, b : BOOLEAN;",
       "a, b : BOOLEAN; QUERY (a => b) AND a => b;",
       "%% nothing but a comment",
-      "% a comment\nASSERT TRUE %a command\n% another comment",
+      "% a comment\nASSERT TRUE; %a command\n% another comment",
   };
 
 const int numGoodCvc4Inputs = sizeof(goodCvc4Inputs) / sizeof(string);
 
+const string cvc4ExprContext = "a,b,c:BOOLEAN;";
+
 /* The following expressions are good in a context where a, b, and c have been declared as BOOLEAN. */
 const string goodCvc4Exprs[] = {
     "a AND b",
@@ -55,7 +57,7 @@ const string badCvc4Inputs[] = {
       ";", // no command
       "ASSERT;", // no args
       "QUERY",
-      "CHECKSAT;",
+      "CHECKSAT",
       "a, b : boolean;", // lowercase boolean isn't a type
       "0x : INT;", // 0x isn't an identifier
       "a, b : BOOLEAN\nQUERY (a => b) AND a => b;", // no semicolon after decl
@@ -66,7 +68,6 @@ const int numBadCvc4Inputs = sizeof(badCvc4Inputs) / sizeof(string);
 
 /* The following expressions are bad even in a context where a, b, and c have been declared as BOOLEAN. */
 const string badCvc4Exprs[] = {
-    "",
     "a AND", // wrong arity
     "AND(a,b)", // not infix
     "(OR (AND a b) c)", // not infix
@@ -92,6 +93,8 @@ const string goodSmtInputs[] = {
 
 const int numGoodSmtInputs = sizeof(goodSmtInputs) / sizeof(string);
 
+const string smtExprContext = "(benchmark foo :extrapreds ((a) (b) (c)) )";
+
 /* The following expressions are good in a context where a, b, and c have been declared as BOOLEAN. */
 const string goodSmtExprs[] = {
     "(and a b)",
@@ -105,7 +108,7 @@ const int numGoodSmtExprs = sizeof(goodSmtExprs) / sizeof(string);
 
 const string badSmtInputs[] = {
     "(benchmark foo)", // empty benchmark is not OK
-    "(benchmark bar :assume)", // no args
+    "(benchmark bar :assumption)", // no args
     "(benchmark bar :formula)",
     "(benchmark baz :extrapreds ( (a) (a) ) )" // double decl
   };
@@ -114,7 +117,6 @@ const int numBadSmtInputs = sizeof(badSmtInputs) / sizeof(string);
 
 /* The following expressions are bad even in a context where a, b, and c have been declared as BOOLEAN. */
 const string badSmtExprs[] = {
-    "",
     "(and a)", // wrong arity
     "(and a b", // no closing paren
     "(a and b)", // infix
@@ -135,9 +137,12 @@ class SmtParserBlack : public CxxTest::TestSuite {
       istringstream stream(goodInputs[i]);
       Parser* smtParser = Parser::getNewParser(d_exprManager, d_lang, stream);
       TS_ASSERT( !smtParser->done() );
-      while(!smtParser->done()) {
-        TS_ASSERT( smtParser->parseNextCommand() != NULL );
+      Command* cmd;
+      while((cmd = smtParser->parseNextCommand())) {
+        cout << "Parsed command: " << *cmd << endl;
       }
+      TS_ASSERT( smtParser->parseNextCommand() == NULL );
+      TS_ASSERT( smtParser->done() );
       delete smtParser;
     }
   }
@@ -147,21 +152,33 @@ class SmtParserBlack : public CxxTest::TestSuite {
       cout << "Testing input: '" << badInputs[i] << "'\n";
       istringstream stream(badInputs[i]);
       Parser* smtParser = Parser::getNewParser(d_exprManager, d_lang, stream);
-      TS_ASSERT_THROWS( smtParser->parseNextCommand(), ParserException );
+      TS_ASSERT_THROWS( while(smtParser->parseNextCommand()); , ParserException );
       delete smtParser;
     }
   }
 
-  void tryGoodExprs(Parser::InputLanguage d_lang,const string goodBooleanExprs[], int numExprs) {
+  void tryGoodExprs(Parser::InputLanguage d_lang,const string& context, const string goodBooleanExprs[], int numExprs) {
+    cout << "Using context: " << context << endl;
     for(int i = 0; i < numExprs; ++i) {
-      cout << "Testing expr: '" << goodBooleanExprs[i] << "'\n";
-      istringstream stream(goodBooleanExprs[i]);
-      Parser* smtParser = Parser::getNewParser(d_exprManager, d_lang, stream);
-      TS_ASSERT( !smtParser->done() );
-      while(!smtParser->done()) {
-        TS_ASSERT( !smtParser->parseNextExpression().isNull() );
+      try {
+        cout << "Testing expr: '" << goodBooleanExprs[i] << "'\n";
+        istringstream stream(context + goodBooleanExprs[i]);
+        Parser* parser = Parser::getNewParser(d_exprManager, d_lang, stream);
+        TS_ASSERT( !parser->done() );
+        Command* cmd = parser->parseNextCommand();
+        TS_ASSERT( !parser->done() );
+        Expr e;
+        while(e = parser->parseNextExpression()) {
+          cout << "Parsed expr: " << e << endl;
+        }
+        TS_ASSERT( parser->done() );
+        TS_ASSERT( e.isNull() );
+        delete cmd;
+        delete parser;
+      } catch (ParserException& e) {
+        cout << "Caught: " << e << endl;
+        TS_ASSERT( false );
       }
-      delete smtParser;
     }
   }
 
@@ -188,7 +205,7 @@ public:
   }
 
   void testGoodCvc4Exprs() {
-    tryGoodExprs(Parser::LANG_CVC4,goodCvc4Exprs,numGoodCvc4Exprs);
+    tryGoodExprs(Parser::LANG_CVC4,cvc4ExprContext,goodCvc4Exprs,numGoodCvc4Exprs);
   }
 
   void testBadCvc4Exprs() {
@@ -204,7 +221,7 @@ public:
   }
 
   void testGoodSmtExprs() {
-    tryGoodExprs(Parser::LANG_SMTLIB,goodSmtExprs,numGoodSmtExprs);
+    tryGoodExprs(Parser::LANG_SMTLIB,smtExprContext,goodSmtExprs,numGoodSmtExprs);
   }
 
   void testBadSmtExprs() {