Fixing the CVC grammar for parsing Boolean expressions. All the associativity stufff is now in the grammar. All the parser tests pass now.

8 files changed, 84 insertions, 127 deletions

diff --git a/src/context/context.h b/src/context/context.h
index 114c8ed69..3bac70cb6 100644
--- a/src/context/context.h
+++ b/src/context/context.h
@@ -51,7 +51,7 @@ class ContextNotifyObj;
 class Context {
 
   /**
-   * Pointer to the ContextMemoryManager fot this Context.
+   * Pointer to the ContextMemoryManager for this Context.
    */
   ContextMemoryManager* d_pCMM;
 
@@ -67,13 +67,13 @@ class Context {
 
   /**
    * Doubly-linked list of objects to notify before every pop.  See
-   * ContextNotifyObj for sturcture of linked list.
+   * ContextNotifyObj for structure of linked list.
    */
   ContextNotifyObj* d_pCNOpre;
 
   /**
    * Doubly-linked list of objects to notify after every pop.  See
-   * ContextNotifyObj for sturcture of linked list.
+   * ContextNotifyObj for structure of linked list.
    */
   ContextNotifyObj* d_pCNOpost;
 
@@ -189,7 +189,7 @@ public:
     { if (pScopePrev != NULL) d_level = pScopePrev->getLevel() + 1; }
 
   /**
-   * Destructor: Restore all of the objects in CotextObjList.  Defined inline
+   * Destructor: Restore all of the objects in ContextObjList.  Defined inline
    * below.
    */
   ~Scope();
diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp
index b7361eb0f..e7169a02b 100644
--- a/src/parser/antlr_parser.cpp
+++ b/src/parser/antlr_parser.cpp
@@ -33,25 +33,6 @@ using namespace CVC4::parser;
 namespace CVC4 {
 namespace parser {
 
-unsigned AntlrParser::getPrecedence(Kind kind) {
-  switch(kind) {
-  // Boolean operators
-  case IFF:
-    return 1;
-  case IMPLIES:
-    return 2;
-  case OR:
-    return 3;
-  case XOR:
-    return 4;
-  case AND:
-    return 5;
-  default:
-    Unhandled("Undefined precedence - necessary for proper parsing of CVC files!");
-  }
-  return 0;
-}
-
 AntlrParser::AntlrParser(const antlr::ParserSharedInputState& state, int k) :
   antlr::LLkParser(state, k) {
 }
@@ -127,64 +108,6 @@ void AntlrParser::rethrow(antlr::SemanticException& e, string new_message)
                                  LT(0).get()->getColumn());
 }
 
-Expr AntlrParser::createPrecedenceExpr(const vector<Expr>& exprs, const vector<
-    Kind>& kinds) {
-  Assert( exprs.size() > 0, "Expected non-empty vector expr");
-  Assert( kinds.size() + 1 == exprs.size(), "Expected kinds to match exprs");
-  return createPrecedenceExpr(exprs, kinds, 0, exprs.size() - 1);
-}
-
-  /* Find the index of the kind with the lowest precedence. */
-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]);
-
-  for(unsigned i = start_index + 1; i <= end_index; ++i) {
-    unsigned current_precedence = getPrecedence(kinds[i]);
-    if(current_precedence < pivot_precedence) {
-      pivot = i;
-      pivot_precedence = current_precedence;
-    }
-  }
-
-  return pivot;
-}
-
-  /* "Tree-ify" an unparenthesized expression:
-         e_1 op_1 e_2 op_2 ... e_(n-1) op_(n-1) e_n
-     represented as a vector of exprs <e_1,e_2,...,e_n> and 
-     kinds <k_1,k_2,...,k_(n-1)>.
-
-     This works by finding the lowest precedence operator op_i,
-     then recursively tree-ifying lhs = (e1 op_1 ... op_(i-1) e_i),
-     rhs = (e_(i+1) op_(i+1) ... op_(n-1) e_N), and forming the
-     expression (lhs op_i rhs).
- */
-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];
-  }
-
-  unsigned pivot = findPivot(kinds, start_index, end_index - 1);
-
-  Expr child_1 = createPrecedenceExpr(exprs, kinds, start_index, pivot);
-  Expr child_2 = createPrecedenceExpr(exprs, kinds, pivot + 1, end_index);
-  return d_exprManager->mkExpr(kinds[pivot], child_1, child_2);
-}
-
 bool AntlrParser::checkDeclation(string varName, DeclarationCheck check) {
   switch(check) {
   case CHECK_DECLARED:
diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h
index 271171281..f83ccd5f2 100644
--- a/src/parser/antlr_parser.h
+++ b/src/parser/antlr_parser.h
@@ -168,15 +168,6 @@ protected:
   Expr mkExpr(Kind kind, const std::vector<Expr>& children);
 
   /**
-   * 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);
-
-  /**
    * Creates a new predicated over the given sorts.
    * @param p_name the name of the predicate
    * @param p_sorts the arity sorts
@@ -196,18 +187,6 @@ protected:
 
 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
-   * 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);
-
   /** The expression manager */
   ExprManager* d_exprManager;
 
diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g
index 91864329e..51473312e 100644
--- a/src/parser/cvc/cvc_parser.g
+++ b/src/parser/cvc/cvc_parser.g
@@ -122,20 +122,86 @@ formula returns [CVC4::Expr formula]
  * and associativity of the operators.
  * @return the expression representing the formula
  */ 
-boolFormula returns [CVC4::Expr formula] 
+boolFormula returns [CVC4::Expr formula]
+  : formula = boolAndFormula 
+  ;
+
+/**
+ * Matches a Boolean AND formula of a given kind by doing a recursive descent. 
+ */
+boolAndFormula returns [CVC4::Expr andFormula]
 {
-  vector<Expr> formulas;
-  vector<Kind> kinds;
-  Expr f;
-  Kind k;
+  Expr e;
+  vector<Expr> exprs;
+}
+  : e = boolXorFormula { exprs.push_back(e); } 
+      ( AND e = boolXorFormula { exprs.push_back(e); } )*
+    { 
+      andFormula = (exprs.size() > 1 ? mkExpr(CVC4::AND, exprs) : exprs[0]); 
+    }  
+  ;
+
+/**
+ * Matches a Boolean XOR formula of a given kind by doing a recursive descent. 
+ */
+boolXorFormula returns [CVC4::Expr xorFormula]
+{
+  Expr e;
+  vector<Expr> exprs;
+}
+  : e = boolOrFormula { exprs.push_back(e); } 
+      ( XOR e = boolOrFormula { exprs.push_back(e); } )*
+    { 
+      xorFormula = (exprs.size() > 1 ? mkExpr(CVC4::XOR, exprs) : exprs[0]); 
+    }  
+  ;
+
+/**
+ * Matches a Boolean OR formula of a given kind by doing a recursive descent. 
+ */
+boolOrFormula returns [CVC4::Expr orFormula]
+{
+  Expr e;
+  vector<Expr> exprs;
 }
-  : f = primaryBoolFormula { formulas.push_back(f); } 
-      ( k = boolOperator { kinds.push_back(k); } f = primaryBoolFormula { formulas.push_back(f); } )* 
+  : e = boolImpliesFormula { exprs.push_back(e); } 
+      ( OR e = boolImpliesFormula { exprs.push_back(e); } )*
     { 
-      // Create the expression based on precedences
-      formula = createPrecedenceExpr(formulas, kinds);
+      orFormula = (exprs.size() > 1 ? mkExpr(CVC4::OR, exprs) : exprs[0]); 
+    }  
+  ;
+
+/**
+ * Matches a Boolean IMPLIES formula of a given kind by doing a recursive descent. 
+ */
+boolImpliesFormula returns [CVC4::Expr impliesFormula]
+{
+  vector<Expr> exprs;
+  Expr e;
+}
+  : e = boolIffFormula { exprs.push_back(e); } 
+    ( IMPLIES e = boolIffFormula { exprs.push_back(e); } 
+    )*
+    {
+      impliesFormula = exprs.back(); 
+      for (int i = exprs.size() - 2; i >= 0; -- i) {
+        impliesFormula = mkExpr(CVC4::IMPLIES, exprs[i], impliesFormula);
+      }
     }
   ;
+
+/**
+ * Matches a Boolean IFF formula of a given kind by doing a recursive descent. 
+ */
+boolIffFormula returns [CVC4::Expr iffFormula]
+{
+  Expr e;
+}
+  : iffFormula = primaryBoolFormula  
+    ( IFF e = primaryBoolFormula 
+        { iffFormula = mkExpr(CVC4::IFF, iffFormula, e); } 
+    )*
+  ;
   
 /**
  * Parses a primary Boolean formula. A primary Boolean formula is either a 
@@ -150,19 +216,6 @@ primaryBoolFormula returns [CVC4::Expr formula]
   ;
 
 /**
- * Parses the Boolean operators and returns the corresponding CVC4 expression 
- * kind. 
- * @param the kind of the Boolean operator
- */
-boolOperator returns [CVC4::Kind kind]
-  : IMPLIES  { kind = CVC4::IMPLIES; }
-  | AND      { kind = CVC4::AND;     }
-  | OR       { kind = CVC4::OR;      }
-  | XOR      { kind = CVC4::XOR;     }
-  | IFF      { kind = CVC4::IFF;     }
-  ;
-
-/**
  * Parses the Boolean atoms (variables and predicates).
  * @return the expression representing the atom.
  */    
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 96fe5f6a5..a38868d3b 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -79,7 +79,7 @@ Parser::~Parser() {
 }
 
 Parser::Parser(istream* input, AntlrParser* antlrParser, CharScanner* antlrLexer, bool deleteInput) :
-  d_done(false), d_input(input), d_antlrParser(antlrParser), d_antlrLexer(antlrLexer), d_deleteInput(deleteInput) {
+  d_done(false), d_antlrParser(antlrParser), d_antlrLexer(antlrLexer), d_input(input), d_deleteInput(deleteInput) {
 }
 
 Parser* Parser::getNewParser(ExprManager* em, InputLanguage lang,
diff --git a/src/parser/parser.h b/src/parser/parser.h
index b099a8142..618b1c8ab 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -117,7 +117,8 @@ private:
   std::istream* d_input;
 
   /** Wherther to de-allocate the input */
-  bool d_deleteInput;}; // end of class Parser
+  bool d_deleteInput;
+}; // end of class Parser
 
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g
index 56e1f9f17..88216336d 100644
--- a/src/parser/smt/smt_parser.g
+++ b/src/parser/smt/smt_parser.g
@@ -34,6 +34,7 @@ options {
  */
 parseExpr returns [CVC4::Expr expr]
   : expr = annotatedFormula
+  | EOF
   ;
 
 /**
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index 6db3b770b..8a1f781dc 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -99,7 +99,7 @@ const string smtExprContext = "(benchmark foo :extrapreds ((a) (b) (c)) )";
 const string goodSmtExprs[] = {
     "(and a b)",
     "(or (and a b) c)",
-    "(implies (and (implies a b) a) b))",
+    "(implies (and (implies a b) a) b)",
     "(and (iff a b) (not a))",
     "(iff (xor a b) (and (or a b) (not (and a b))))"
 };