Code cleanup in parser

3 files changed, 73 insertions, 47 deletions

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index a9dff77bf..84713fc59 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -33,6 +33,11 @@ options {
 }
 
 @lexer::includes {
+/** This suppresses warnings about the redefinition of token symbols between different
+  * parsers. The redefinitions should be harmless as long as no client: (a) #include's 
+  * the lexer headers for two grammars AND (b) uses the token symbol definitions. */
+#pragma GCC system_header
+
 /* This improves performance by ~10 percent on big inputs.
  * This option is only valid if we know the input is ASCII (or some 8-bit encoding).
  * If we know the input is UTF-16, we can use ANTLR3_INLINE_INPUT_UTF16.
@@ -43,40 +48,25 @@ options {
 
 @parser::includes {
 #include "expr/command.h"
-#include "parser/input.h"
 
 namespace CVC4 {
   class Expr;
-namespace parser {
-  class CvcInput;
-}
 }
-
-extern
-void SetCvcInput(CVC4::parser::CvcInput* input);
-
 }
 
 @parser::postinclude {
 #include "expr/expr.h"
 #include "expr/kind.h"
 #include "expr/type.h"
-#include "parser/input.h"
 #include "parser/cvc/cvc_input.h"
 #include "util/output.h"
 #include <vector>
 
 using namespace CVC4;
 using namespace CVC4::parser;
-}
-
-@members {
-static CVC4::parser::CvcInput *input;
 
-extern
-void SetCvcInput(CVC4::parser::CvcInput* _input) {
-  input = _input;
-}
+#undef CVC_INPUT
+#define CVC_INPUT ((CvcInput*)(PARSER->super))
 }
 
 /**
@@ -108,7 +98,7 @@ command returns [CVC4::Command* cmd = 0]
   : ASSERT_TOK formula[f] SEMICOLON { cmd = new AssertCommand(f);   }
   | QUERY_TOK formula[f] SEMICOLON { cmd = new QueryCommand(f);    }
   | CHECKSAT_TOK formula[f] SEMICOLON { cmd = new CheckSatCommand(f); }
-  | CHECKSAT_TOK SEMICOLON { cmd = new CheckSatCommand(input->getTrueExpr()); }
+  | CHECKSAT_TOK SEMICOLON { cmd = new CheckSatCommand(CVC_INPUT->getTrueExpr()); }
   | PUSH_TOK SEMICOLON { cmd = new PushCommand(); }
   | POP_TOK SEMICOLON { cmd = new PopCommand(); }
   | declaration[cmd]
@@ -136,9 +126,9 @@ declType[CVC4::Type*& t, std::vector<std::string>& idList]
   Debug("parser-extra") << "declType: " << AntlrInput::tokenText(LT(1)) << std::endl;
 }
   : /* A sort declaration (e.g., "T : TYPE") */
-    TYPE_TOK { input->newSorts(idList); t = input->kindType(); }
+    TYPE_TOK { CVC_INPUT->newSorts(idList); t = CVC_INPUT->kindType(); }
   | /* A variable declaration */
-    type[t] { input->mkVars(idList,t); }
+    type[t] { CVC_INPUT->mkVars(idList,t); }
   ;
 
 /**
@@ -155,13 +145,13 @@ type[CVC4::Type*& t]
   | /* Single-parameter function type */
     baseType[t] { typeList.push_back(t); }
     ARROW_TOK baseType[t] 
-    { t = input->functionType(typeList,t); }
+    { t = CVC_INPUT->functionType(typeList,t); }
   | /* Multi-parameter function type */
     LPAREN baseType[t]
     { typeList.push_back(t); }
     (COMMA baseType[t] { typeList.push_back(t); } )+
     RPAREN ARROW_TOK baseType[t]
-    { t = input->functionType(typeList,t); }
+    { t = CVC_INPUT->functionType(typeList,t); }
   ;
 
 /**
@@ -189,7 +179,7 @@ identifier[std::string& id,
            CVC4::parser::SymbolType type]
   : IDENTIFIER
     { id = AntlrInput::tokenText($IDENTIFIER);
-      input->checkDeclaration(id, check, type); }
+      CVC_INPUT->checkDeclaration(id, check, type); }
   ;
 
 /**
@@ -201,7 +191,7 @@ baseType[CVC4::Type*& t]
   std::string id;
   Debug("parser-extra") << "base type: " << AntlrInput::tokenText(LT(1)) << std::endl;
 }
-  : BOOLEAN_TOK { t = input->booleanType(); }
+  : BOOLEAN_TOK { t = CVC_INPUT->booleanType(); }
   | typeSymbol[t]
   ;
 
@@ -214,7 +204,7 @@ typeSymbol[CVC4::Type*& t]
   Debug("parser-extra") << "type symbol: " << AntlrInput::tokenText(LT(1)) << std::endl;
 }
   : identifier[id,CHECK_DECLARED,SYM_SORT]
-    { t = input->getSort(id); }
+    { t = CVC_INPUT->getSort(id); }
   ;
 
 /**
@@ -252,7 +242,7 @@ iffFormula[CVC4::Expr& f]
   : impliesFormula[f]
     ( IFF_TOK 
     	iffFormula[e]
-        { f = input->mkExpr(CVC4::kind::IFF, f, e); }
+        { f = CVC_INPUT->mkExpr(CVC4::kind::IFF, f, e); }
     )?
   ;
 
@@ -266,7 +256,7 @@ impliesFormula[CVC4::Expr& f]
 }
   : orFormula[f]
     ( IMPLIES_TOK impliesFormula[e]
-        { f = input->mkExpr(CVC4::kind::IMPLIES, f, e); }
+        { f = CVC_INPUT->mkExpr(CVC4::kind::IMPLIES, f, e); }
     )?
   ;
 
@@ -283,7 +273,7 @@ orFormula[CVC4::Expr& f]
         xorFormula[f] { exprs.push_back(f); } )*
     {
       if( exprs.size() > 0 ) {
-        f = input->mkExpr(CVC4::kind::OR, exprs);
+        f = CVC_INPUT->mkExpr(CVC4::kind::OR, exprs);
       }
     }
   ;
@@ -298,7 +288,7 @@ xorFormula[CVC4::Expr& f]
 }
   : andFormula[f]
     ( XOR_TOK andFormula[e]
-      { f = input->mkExpr(CVC4::kind::XOR,f, e); }
+      { f = CVC_INPUT->mkExpr(CVC4::kind::XOR,f, e); }
     )*
   ;
 
@@ -315,7 +305,7 @@ andFormula[CVC4::Expr& f]
       notFormula[f] { exprs.push_back(f); } )*
     {
       if( exprs.size() > 0 ) {
-        f = input->mkExpr(CVC4::kind::AND, exprs);
+        f = CVC_INPUT->mkExpr(CVC4::kind::AND, exprs);
       }
     }
   ;
@@ -330,7 +320,7 @@ notFormula[CVC4::Expr& f]
 }
   : /* negation */
     NOT_TOK notFormula[f]
-    { f = input->mkExpr(CVC4::kind::NOT, f); }
+    { f = CVC_INPUT->mkExpr(CVC4::kind::NOT, f); }
   | /* a boolean atom */
     predFormula[f]
   ;
@@ -342,7 +332,7 @@ predFormula[CVC4::Expr& f]
 }
   : term[f]
     (EQUAL_TOK term[e]
-      { f = input->mkExpr(CVC4::kind::EQUAL, f, e); }
+      { f = CVC_INPUT->mkExpr(CVC4::kind::EQUAL, f, e); }
     )?
   ; // TODO: lt, gt, etc.
 
@@ -361,7 +351,7 @@ term[CVC4::Expr& f]
     { args.push_back( f ); }
     LPAREN formulaList[args] RPAREN
     // TODO: check arity
-    { f = input->mkExpr(CVC4::kind::APPLY_UF, args); }
+    { f = CVC_INPUT->mkExpr(CVC4::kind::APPLY_UF, args); }
 
   | /* if-then-else */
     iteTerm[f]
@@ -370,12 +360,12 @@ term[CVC4::Expr& f]
     LPAREN formula[f] RPAREN
 
     /* constants */
-  | TRUE_TOK  { f = input->getTrueExpr(); }
-  | FALSE_TOK { f = input->getFalseExpr(); }
+  | TRUE_TOK  { f = CVC_INPUT->getTrueExpr(); }
+  | FALSE_TOK { f = CVC_INPUT->getFalseExpr(); }
 
   | /* variable */
     identifier[name,CHECK_DECLARED,SYM_VARIABLE]
-    { f = input->getVariable(name); }
+    { f = CVC_INPUT->getVariable(name); }
   ;
 
 /**
@@ -390,7 +380,7 @@ iteTerm[CVC4::Expr& f]
     THEN_TOK formula[f] { args.push_back(f); }
     iteElseTerm[f] { args.push_back(f); }
     ENDIF_TOK
-    { f = input->mkExpr(CVC4::kind::ITE, args); }
+    { f = CVC_INPUT->mkExpr(CVC4::kind::ITE, args); }
   ;
 
 /**
@@ -405,7 +395,7 @@ iteElseTerm[CVC4::Expr& f]
   | ELSEIF_TOK iteCondition = formula[f] { args.push_back(f); }
     THEN_TOK iteThen = formula[f] { args.push_back(f); }
     iteElse = iteElseTerm[f] { args.push_back(f); }
-    { f = input->mkExpr(CVC4::kind::ITE, args); }
+    { f = CVC_INPUT->mkExpr(CVC4::kind::ITE, args); }
   ;
 
 /**
@@ -419,8 +409,8 @@ functionSymbol[CVC4::Expr& f]
   std::string name;
 }
   : identifier[name,CHECK_DECLARED,SYM_FUNCTION]
-    { input->checkFunction(name);
-      f = input->getFunction(name); }
+    { CVC_INPUT->checkFunction(name);
+      f = CVC_INPUT->getFunction(name); }
   ;
 
 
diff --git a/src/parser/cvc/cvc_input.cpp b/src/parser/cvc/cvc_input.cpp
index 9de608aae..1f1a602c5 100644
--- a/src/parser/cvc/cvc_input.cpp
+++ b/src/parser/cvc/cvc_input.cpp
@@ -47,7 +47,6 @@ void CvcInput::init() {
   }
 
   setParser(d_pCvcParser->pParser);
-  SetCvcInput(this);
 }
 
 
@@ -64,9 +63,11 @@ Expr CvcInput::doParseExpr() throw (ParserException) {
   return d_pCvcParser->parseExpr(d_pCvcParser);
 }
 
+/*
 pANTLR3_LEXER CvcInput::getLexer() {
   return d_pCvcLexer->pLexer;
 }
+*/
 
 } // namespace parser
 
diff --git a/src/parser/cvc/cvc_input.h b/src/parser/cvc/cvc_input.h
index 659123401..a6117b4a9 100644
--- a/src/parser/cvc/cvc_input.h
+++ b/src/parser/cvc/cvc_input.h
@@ -23,22 +23,57 @@ class ExprManager;
 namespace parser {
 
 class CvcInput : public AntlrInput {
+  /** The ANTLR3 CVC lexer for the input. */
+  pCvcLexer d_pCvcLexer;
+
+  /** The ANTLR3 CVC parser for the input. */
+  pCvcParser d_pCvcParser;
+
 public:
+
+  /** Create a file input.
+   *
+   * @param exprManager the manager to use when building expressions from the input
+   * @param filename the path of the file to read
+   * @param useMmap <code>true</code> if the input should use memory-mapped
+   * I/O; otherwise, the input will use the standard ANTLR3 I/O implementation.
+   */
   CvcInput(ExprManager* exprManager, const std::string& filename, bool useMmap);
-  CvcInput(ExprManager* exprManager, const std::string& input, const std::string& name);
+
+  /** Create a string input.
+   *
+   * @param exprManager the manager to use when building expressions from the input
+   * @param input the string to read
+   * @param name the "filename" to use when reporting errors
+   */
+  CvcInput(ExprManager* exprManager, const std::string& input,
+           const std::string& name);
+
+  /* Destructor. Frees the lexer and the parser. */
   ~CvcInput();
 
 protected:
+
+  /** Parse a command from the input. Returns <code>NULL</code> if there is
+   * no command there to parse.
+   *
+   * @throws ParserException if an error is encountered during parsing.
+   */
   Command* doParseCommand() throw(ParserException);
+
+  /** Parse an expression from the input. Returns a null <code>Expr</code>
+   * if there is no expression there to parse.
+   *
+   * @throws ParserException if an error is encountered during parsing.
+   */
   Expr doParseExpr() throw(ParserException);
-  pANTLR3_LEXER getLexer();
-  pANTLR3_LEXER createLexer(pANTLR3_INPUT_STREAM input);
-  pANTLR3_PARSER createParser(pANTLR3_COMMON_TOKEN_STREAM tokenStream);
 
 private:
+
+  /** Initialize the class. Called from the constructors once the input stream
+   * is initialized. */
   void init();
-  pCvcLexer d_pCvcLexer;
-  pCvcParser d_pCvcParser;
+
 }; // class CvcInput
 
 } // namespace parser