Code cleanup in parser

3 files changed, 75 insertions, 52 deletions

diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index 7095c7269..e97ced324 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.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 SmtInput;
-}
 }
-
-extern
-void SetSmtInput(CVC4::parser::SmtInput* smt);
-
 }
 
 @parser::postinclude {
 #include "expr/expr.h"
 #include "expr/kind.h"
 #include "expr/type.h"
-#include "parser/input.h"
 #include "parser/smt/smt_input.h"
 #include "util/output.h"
 #include <vector>
 
 using namespace CVC4;
 using namespace CVC4::parser;
-}
-
-@members {
-static CVC4::parser::SmtInput *input;
 
-extern
-void SetSmtInput(CVC4::parser::SmtInput* _input) {
-  input = _input;
-}
+#undef SMT_INPUT
+#define SMT_INPUT ((SmtInput*)(PARSER->super))
 }
 
 /**
@@ -130,7 +120,7 @@ benchAttribute returns [CVC4::Command* smt_command]
   Expr expr;
 }
   : LOGIC_TOK identifier[name,CHECK_NONE,SYM_VARIABLE]
-    { input->setLogic(name);
+    { SMT_INPUT->setLogic(name);
       smt_command = new SetBenchmarkLogicCommand(name);   }
   | ASSUMPTION_TOK annotatedFormula[expr]
     { smt_command = new AssertCommand(expr);   }
@@ -158,13 +148,13 @@ annotatedFormula[CVC4::Expr& expr]
 } 
   : /* a built-in operator application */
     LPAREN_TOK builtinOp[kind] annotatedFormulas[args,expr] RPAREN_TOK 
-    { input->checkArity(kind, args.size());
+    { SMT_INPUT->checkArity(kind, args.size());
       if((kind == CVC4::kind::AND || kind == CVC4::kind::OR) && args.size() == 1) {
         /* Unary AND/OR can be replaced with the argument.
 	       It just so happens expr should already by the only argument. */
         Assert( expr == args[0] );
       } else {
-        expr = input->mkExpr(kind, args);
+        expr = SMT_INPUT->mkExpr(kind, args);
       }
     }
 
@@ -179,7 +169,7 @@ annotatedFormula[CVC4::Expr& expr]
     { args.push_back(expr); }
     annotatedFormulas[args,expr] RPAREN_TOK
     // TODO: check arity
-    { expr = input->mkExpr(CVC4::kind::APPLY_UF,args); }
+    { expr = SMT_INPUT->mkExpr(CVC4::kind::APPLY_UF,args); }
 
   | /* An ite expression */
     LPAREN_TOK (ITE_TOK | IF_THEN_ELSE_TOK) 
@@ -190,27 +180,27 @@ annotatedFormula[CVC4::Expr& expr]
     annotatedFormula[expr]
     { args.push_back(expr); } 
     RPAREN_TOK
-    { expr = input->mkExpr(CVC4::kind::ITE, args); }
+    { expr = SMT_INPUT->mkExpr(CVC4::kind::ITE, args); }
 
   | /* a let/flet binding */
     LPAREN_TOK 
     (LET_TOK LPAREN_TOK var_identifier[name,CHECK_UNDECLARED]
       | FLET_TOK LPAREN_TOK fun_identifier[name,CHECK_UNDECLARED] )
     annotatedFormula[expr] RPAREN_TOK
-    { input->defineVar(name,expr); }
+    { SMT_INPUT->defineVar(name,expr); }
     annotatedFormula[expr]
     RPAREN_TOK
-    { input->undefineVar(name); }
+    { SMT_INPUT->undefineVar(name); }
 
   | /* a variable */
     ( identifier[name,CHECK_DECLARED,SYM_VARIABLE]
       | var_identifier[name,CHECK_DECLARED] 
       | fun_identifier[name,CHECK_DECLARED] )
-    { expr = input->getVariable(name); }
+    { expr = SMT_INPUT->getVariable(name); }
 
     /* constants */
-  | TRUE_TOK          { expr = input->getTrueExpr(); }
-  | FALSE_TOK         { expr = input->getFalseExpr(); }
+  | TRUE_TOK          { expr = SMT_INPUT->getTrueExpr(); }
+  | FALSE_TOK         { expr = SMT_INPUT->getFalseExpr(); }
     /* TODO: let, flet, quantifiers, arithmetic constants */
   ;
 
@@ -269,8 +259,8 @@ functionSymbol[CVC4::Expr& fun]
 	std::string name;
 }
   : functionName[name,CHECK_DECLARED]
-    { input->checkFunction(name);
-      fun = input->getFunction(name); }
+    { SMT_INPUT->checkFunction(name);
+      fun = SMT_INPUT->getFunction(name); }
   ;
   
 /**
@@ -291,8 +281,8 @@ functionDeclaration
       t = sortSymbol // require at least one sort
     { sorts.push_back(t); }
       sortList[sorts] RPAREN_TOK
-    { t = input->functionType(sorts);
-      input->mkVar(name, t); } 
+    { t = SMT_INPUT->functionType(sorts);
+      SMT_INPUT->mkVar(name, t); } 
   ;
               
 /**
@@ -304,8 +294,8 @@ predicateDeclaration
   std::vector<Type*> p_sorts;
 }
   : LPAREN_TOK predicateName[name,CHECK_UNDECLARED] sortList[p_sorts] RPAREN_TOK
-    { Type *t = input->predicateType(p_sorts);
-      input->mkVar(name, t); } 
+    { Type *t = SMT_INPUT->predicateType(p_sorts);
+      SMT_INPUT->mkVar(name, t); } 
   ;
 
 sortDeclaration 
@@ -314,7 +304,7 @@ sortDeclaration
 }
   : sortName[name,CHECK_UNDECLARED]
     { Debug("parser") << "sort decl: '" << name << "'" << std::endl;
-      input->newSort(name); }
+      SMT_INPUT->newSort(name); }
   ;
   
 /**
@@ -337,7 +327,7 @@ sortSymbol returns [CVC4::Type* t]
   std::string name;
 }
   : sortName[name,CHECK_NONE] 
-  	{ $t = input->getSort(name); }
+  	{ $t = SMT_INPUT->getSort(name); }
   ;
 
 /**
@@ -370,7 +360,7 @@ identifier[std::string& id,
       Debug("parser") << "identifier: " << id
                       << " check? " << toString(check)
                       << " type? " << toString(type) << std::endl;
-      input->checkDeclaration(id, check, type); }
+      SMT_INPUT->checkDeclaration(id, check, type); }
   ;
 
 /**
@@ -384,7 +374,7 @@ var_identifier[std::string& id,
     { id = AntlrInput::tokenText($VAR_IDENTIFIER);
       Debug("parser") << "var_identifier: " << id
                       << " check? " << toString(check) << std::endl;
-      input->checkDeclaration(id, check, SYM_VARIABLE); }
+      SMT_INPUT->checkDeclaration(id, check, SYM_VARIABLE); }
   ;
 
 /**
@@ -398,7 +388,7 @@ fun_identifier[std::string& id,
     { id = AntlrInput::tokenText($FUN_IDENTIFIER);
       Debug("parser") << "fun_identifier: " << id
                       << " check? " << toString(check) << std::endl;
-      input->checkDeclaration(id, check, SYM_FUNCTION); }
+      SMT_INPUT->checkDeclaration(id, check, SYM_FUNCTION); }
   ;
 
 
diff --git a/src/parser/smt/smt_input.cpp b/src/parser/smt/smt_input.cpp
index 7a28c30f1..db4d89860 100644
--- a/src/parser/smt/smt_input.cpp
+++ b/src/parser/smt/smt_input.cpp
@@ -17,13 +17,15 @@ namespace CVC4 {
 namespace parser {
 
 /* Use lookahead=2 */
-SmtInput::SmtInput(ExprManager* exprManager, const std::string& filename, bool useMmap) :
-  AntlrInput(exprManager,filename,2,useMmap) {
+SmtInput::SmtInput(ExprManager* exprManager, const std::string& filename,
+                   bool useMmap) :
+  AntlrInput(exprManager, filename, 2, useMmap) {
   init();
 }
 
-SmtInput::SmtInput(ExprManager* exprManager, const std::string& input, const std::string& name) :
-  AntlrInput(exprManager,input,name,2) {
+SmtInput::SmtInput(ExprManager* exprManager, const std::string& input,
+                   const std::string& name) :
+  AntlrInput(exprManager, input, name, 2) {
   init();
 }
 
@@ -47,7 +49,6 @@ void SmtInput::init() {
   }
 
   setParser(d_pSmtParser->pParser);
-  SetSmtInput(this);
 }
 
 
@@ -64,10 +65,6 @@ Expr SmtInput::doParseExpr() throw (ParserException) {
   return d_pSmtParser->parseExpr(d_pSmtParser);
 }
 
-pANTLR3_LEXER SmtInput::getLexer() {
-  return d_pSmtLexer->pLexer;
-}
-
 } // namespace parser
 
 } // namespace CVC4
diff --git a/src/parser/smt/smt_input.h b/src/parser/smt/smt_input.h
index b3613d67b..4795edc91 100644
--- a/src/parser/smt/smt_input.h
+++ b/src/parser/smt/smt_input.h
@@ -23,23 +23,59 @@ class ExprManager;
 namespace parser {
 
 class SmtInput : public AntlrInput {
+
+  /** The ANTLR3 SMT lexer for the input. */
+  pSmtLexer d_pSmtLexer;
+
+  /** The ANTLR3 CVC parser for the input. */
+  pSmtParser d_pSmtParser;
+
 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.
+   */
   SmtInput(ExprManager* exprManager, const std::string& filename, bool useMmap);
+
+  /** 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
+   */
   SmtInput(ExprManager* exprManager, const std::string& input, const std::string& name);
+
+  /* Destructor. Frees the lexer and the parser. */
   ~SmtInput();
 
 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();
-  pSmtLexer d_pSmtLexer;
-  pSmtParser d_pSmtParser;
+
 }; // class SmtInput
+
 } // namespace parser
 
 } // namespace CVC4