Lots of parser changes to make Chris happy. Yet more to come later.

5 files changed, 99 insertions, 190 deletions

diff --git a/src/parser/cvc/Makefile.am b/src/parser/cvc/Makefile.am
index 666c408cf..ad0eb70d8 100644
--- a/src/parser/cvc/Makefile.am
+++ b/src/parser/cvc/Makefile.am
@@ -24,8 +24,6 @@ ANTLR_STUFF = \
 libparsercvc_la_SOURCES = \
 	cvc_lexer.g \
 	cvc_parser.g \
-	cvc_parser.h \
-	cvc_parser.cpp \
 	$(ANTLR_STUFF)
 
 BUILT_SOURCES = $(ANTLR_STUFF)
diff --git a/src/parser/cvc/Makefile.in b/src/parser/cvc/Makefile.in
index 3fd1701c8..28b80800e 100644
--- a/src/parser/cvc/Makefile.in
+++ b/src/parser/cvc/Makefile.in
@@ -56,7 +56,7 @@ am__objects_1 =
 am__objects_2 = AntlrCvcLexer.lo $(am__objects_1)
 am__objects_3 = AntlrCvcParser.lo
 am__objects_4 = $(am__objects_2) $(am__objects_3)
-am_libparsercvc_la_OBJECTS = cvc_parser.lo $(am__objects_4)
+am_libparsercvc_la_OBJECTS = $(am__objects_4)
 libparsercvc_la_OBJECTS = $(am_libparsercvc_la_OBJECTS)
 DEFAULT_INCLUDES = -I.@am__isrc@ -I$(top_builddir)
 depcomp = $(SHELL) $(top_srcdir)/config/depcomp
@@ -249,8 +249,6 @@ ANTLR_STUFF = \
 libparsercvc_la_SOURCES = \
 	cvc_lexer.g \
 	cvc_parser.g \
-	cvc_parser.h \
-	cvc_parser.cpp \
 	$(ANTLR_STUFF)
 
 BUILT_SOURCES = $(ANTLR_STUFF)
@@ -310,7 +308,6 @@ distclean-compile:
 
 @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/AntlrCvcLexer.Plo@am__quote@
 @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/AntlrCvcParser.Plo@am__quote@
-@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/cvc_parser.Plo@am__quote@
 
 .cpp.o:
 @am__fastdepCXX_TRUE@	$(CXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ $<
diff --git a/src/parser/cvc/cvc_parser.cpp b/src/parser/cvc/cvc_parser.cpp
deleted file mode 100644
index 57d5e6c96..000000000
--- a/src/parser/cvc/cvc_parser.cpp
+++ /dev/null
@@ -1,82 +0,0 @@
-/*********************                                           -*- C++ -*-  */
-/** cvc_parser.cpp
- ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): dejan
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.
- **
- ** CVC presentation language parser implementation.
- **/
-
-#include <iostream>
-#include <fstream>
-
-#include "parser/parser.h"
-#include "util/command.h"
-#include "util/Assert.h"
-#include "parser/parser_exception.h"
-#include "parser/antlr_parser.h"
-#include "parser/cvc/cvc_parser.h"
-#include "parser/cvc/generated/AntlrCvcParser.hpp"
-#include "parser/cvc/generated/AntlrCvcLexer.hpp"
-
-using namespace std;
-
-namespace CVC4 {
-namespace parser {
-
-Command* CvcParser::parseNextCommand() throw(ParserException) {
-  Command* cmd = 0;
-  if(!done()) {
-    try {
-      cmd = d_antlr_parser->command();
-      if(cmd == 0) {
-        setDone();
-        cmd = new EmptyCommand("EOF");
-      }
-    } catch(antlr::ANTLRException& e) {
-      setDone();
-      throw ParserException(e.toString());
-    }
-  }
-  return cmd;
-}
-
-Expr CvcParser::parseNextExpression() throw(ParserException) {
-  Expr result;
-  if(!done()) {
-    try {
-      result = d_antlr_parser->formula();
-    } catch(antlr::ANTLRException& e) {
-      setDone();
-      throw ParserException(e.toString());
-    }
-  }
-  return result;
-}
-
-CvcParser::~CvcParser() {
-  delete d_antlr_parser;
-  delete d_antlr_lexer;
-}
-
-CvcParser::CvcParser(ExprManager*em, istream& input, const char* file_name) :
-  Parser(em), d_input(input) {
-  if(!d_input) {
-    throw ParserException(string("Read error") +
-                          ((file_name != NULL) ? (string(" on ") + file_name) : ""));
-  }
-  d_antlr_lexer = new AntlrCvcLexer(d_input);
-  d_antlr_lexer->setFilename(file_name);
-  d_antlr_parser = new AntlrCvcParser(*d_antlr_lexer);
-  d_antlr_parser->setExpressionManager(d_expr_manager);
-  d_antlr_parser->setFilename(file_name);
-}
-
-}/* CVC4::parser namespace */
-}/* CVC4 namespace */
diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g
index 864719cfa..c7f932a0c 100644
--- a/src/parser/cvc/cvc_parser.g
+++ b/src/parser/cvc/cvc_parser.g
@@ -29,6 +29,23 @@ options {
 }
  
 /**
+ * Parses the next command.
+ * @return command or 0 if EOF
+ */
+parseCommand returns [CVC4::Command* cmd]
+  : cmd = command
+  ;
+
+/**
+ * Parses the next expression.
+ * @return the parsed expression (null expression if EOF)
+ */
+parseExpr returns [CVC4::Expr expr]
+  : expr = formula
+  | EOF
+  ;
+  
+/**
  * Matches a command of the input. If a declaration, it will return an empty 
  * command.
  */
@@ -41,64 +58,118 @@ command returns [CVC4::Command* cmd = 0]
   | QUERY    f = formula  { cmd = new QueryCommand(f);    }
   | CHECKSAT f = formula  { cmd = new CheckSatCommand(f); }
   | CHECKSAT              { cmd = new CheckSatCommand();  }
-  | identifierList[ids] COLON type { 
+  | identifierList[ids, CHECK_UNDECLARED] COLON type { 
       // [chris 12/15/2009] FIXME: decls may not be BOOLEAN
       newPredicates(ids); 
-      cmd = new EmptyCommand("Declaration"); 
+      cmd = new DeclarationCommand(ids); 
     }
   | EOF 
   ;
 
-identifierList[std::vector<std::string>& id_list]
-  : id1:IDENTIFIER { id_list.push_back(id1->getText()); } 
-    (
-      COMMA 
-      id2:IDENTIFIER { id_list.push_back(id2->getText()); }
-    )*
+/**
+ * Mathches a list of identifiers separated by a comma and puts them in the 
+ * given list.
+ * @param idList the list to fill with identifiers.
+ * @param check what kinds of check to perform on the symbols 
+ */
+identifierList[std::vector<std::string>& idList, DeclarationCheck check = CHECK_NONE]
+{
+  string id;
+}
+  : id = identifier { idList.push_back(id); } 
+      (COMMA id = identifier { idList.push_back(id); })*
   ;
  
+
+/**
+ * Matches an identifier and returns a string.
+ */
+identifier[DeclarationCheck check = CHECK_NONE] returns [std::string id]
+  : x:IDENTIFIER { checkDeclation(x->getText(), check) }?
+    { 
+      id = x->getText(); 
+    } 
+    exception catch [antlr::SemanticException& ex] {
+      switch (check) {
+        case CHECK_DECLARED: rethrow(ex, "Symbol " + id + " not declared");
+        case CHECK_UNDECLARED: rethrow(ex, "Symbol " + id + " already declared");
+        default: throw ex;
+      }          
+    }    
+  ;
+  
+/** 
+ * Matches a type.
+ * TODO: parse more types
+ */
 type
   : BOOLEAN
   ;
 
+/** 
+ * Matches a CVC4 formula.
+ * @return the expression representing the formula
+ */ 
 formula returns [CVC4::Expr formula]
-  :  formula = bool_formula
+  :  formula = boolFormula
   ;
 
-bool_formula returns [CVC4::Expr formula] 
+/**
+ * Matches a CVC4 basic Boolean formula (AND, OR, NOT...). It parses the list of
+ * operands (primaryBoolFormulas) and operators (Kinds) and then calls the
+ * createPrecedenceExpr method to build the expression using the precedence
+ * and associativity of the operators.
+ * @return the expression representing the formula
+ */ 
+boolFormula returns [CVC4::Expr formula] 
 {
   vector<Expr> formulas;
   vector<Kind> kinds;
   Expr f1, f2;
   Kind k;
 }
-  : f1 = primary_bool_formula { formulas.push_back(f1); } 
-      ( k = bool_operator { kinds.push_back(k); } f2 = primary_bool_formula { formulas.push_back(f2); } )* 
+  : f1 = primaryBoolFormula { formulas.push_back(f1); } 
+      ( k = boolOperator { kinds.push_back(k); } f2 = primaryBoolFormula { formulas.push_back(f2); } )* 
     { 
       // Create the expression based on precedences
       formula = createPrecedenceExpr(formulas, kinds);
     }
   ;
   
-primary_bool_formula returns [CVC4::Expr formula]
-  : formula = bool_atom
-  | NOT formula = primary_bool_formula { formula = newExpression(CVC4::NOT, formula); }
-  | LPAREN formula = bool_formula RPAREN
+/**
+ * Parses a primary Boolean formula. A primary Boolean formula is either a 
+ * Boolean atom (variables and predicates) a negation of a primary Boolean 
+ * formula or a formula enclosed in parenthesis.
+ * @return the expression representing the formula
+ */
+primaryBoolFormula returns [CVC4::Expr formula]
+  : formula = boolAtom
+  | NOT formula = primaryBoolFormula { formula = mkExpr(CVC4::NOT, formula); }
+  | LPAREN formula = boolFormula RPAREN
   ;
 
-bool_operator returns [CVC4::Kind kind]
+/**
+ * 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;     }
   ;
-    
-bool_atom returns [CVC4::Expr atom]
+
+/**
+ * Parses the Boolean atoms (variables and predicates).
+ * @return the expression representing the atom.
+ */    
+boolAtom returns [CVC4::Expr atom]
 {
   string p;
 }
-  : p = predicate_sym {isDeclared(p, SYM_VARIABLE)}? { atom = getVariable(p); }
+  : p = predicateSymbol[CHECK_DECLARED] { atom = getVariable(p); }
       exception catch [antlr::SemanticException ex] {
         rethrow(ex, "Undeclared variable " + p);
       }
@@ -106,7 +177,12 @@ bool_atom returns [CVC4::Expr atom]
   | FALSE { atom = getFalseExpr(); }
   ;
  
-predicate_sym returns [std::string p]
-  : id:IDENTIFIER { p = id->getText(); }
+/**
+ * Parses a predicate symbol (an identifier).
+ * @param what kind of check to perform on the id 
+ * @return the predicate symol
+ */
+predicateSymbol[DeclarationCheck check = CHECK_NONE] returns [std::string pSymbol]
+  : pSymbol = identifier[check]
   ;
  
\ No newline at end of file
diff --git a/src/parser/cvc/cvc_parser.h b/src/parser/cvc/cvc_parser.h
deleted file mode 100644
index 82d659566..000000000
--- a/src/parser/cvc/cvc_parser.h
+++ /dev/null
@@ -1,80 +0,0 @@
-/*********************                                           -*- C++ -*-  */
-/** cvc_parser.h
- ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): dejan
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.
- **
- ** CVC presentation language parser abstraction.
- **/
-
-#ifndef __CVC4__PARSER__CVC_PARSER_H
-#define __CVC4__PARSER__CVC_PARSER_H
-
-#include <string>
-#include <iostream>
-#include <fstream>
-#include "cvc4_config.h"
-#include "parser/parser_exception.h"
-#include "parser/parser.h"
-
-namespace CVC4 {
-namespace parser {
-
-/**
- * The CVC parser.
- */
-class CVC4_PUBLIC CvcParser : public Parser {
-
-public:
-
-  /**
-   * Construct the parser that uses the given expression manager and parses
-   * from the given 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)
-   */
-  CvcParser(ExprManager* em, std::istream& input, const char* file_name = "");
-
-  /**
-   * Destructor.
-   */
-  ~CvcParser();
-
-  /**
-   * Parses the next command. By default, the CVC parser produces one
-   * CommandSequence command. If parsing is successful, we should be
-   * done after the first call to this command.
-   * @return the CommandSequence command that includes the whole
-   * benchmark
-   */
-  Command* parseNextCommand() throw(ParserException);
-
-  /**
-   * Parses the next complete expression of the stream.
-   * @return the expression parsed
-   */
-  Expr parseNextExpression() throw(ParserException);
-
-protected:
-
-  /** The ANTLR smt lexer */
-  AntlrCvcLexer* d_antlr_lexer;
-
-  /** The ANTLR smt parser */
-  AntlrCvcParser* d_antlr_parser;
-
-  /** The file stream we might be using */
-  std::istream& d_input;
-};
-
-}/* CVC4::parser namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__PARSER__CVC_PARSER_H */