Code cleanup in parser

9 files changed, 254 insertions, 138 deletions

diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index 02e07bc8f..0c0006031 100644
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -308,6 +308,9 @@ void AntlrInput::setLexer(pANTLR3_LEXER pLexer) {
 void AntlrInput::setParser(pANTLR3_PARSER pParser) {
   d_parser = pParser;
   // ANTLR isn't using super, AFAICT.
+  // We could also use @parser::context to add a field to the generated parser, but then
+  // it would have to be declared separately in every input's grammar and we'd have to
+  // pass it in as an address anyway.
   d_parser->super = this;
   d_parser->rec->reportError = &reportError;
 }
diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h
index 01ebe8339..05d785df3 100644
--- a/src/parser/antlr_input.h
+++ b/src/parser/antlr_input.h
@@ -41,38 +41,78 @@ namespace parser {
  * Wrapper for an ANTLR parser that includes convenience methods to set up input and token streams.
  */
 class AntlrInput : public Input {
-
+  /** The token lookahead used to lex and parse the input. This should usually be equal to
+   * <code>K</code> for an LL(k) grammar. */
   unsigned int d_lookahead;
+
+  /** The ANTLR3 lexer associated with this input. This will be <code>NULL</code> initially. It
+   *  must be set by a call to <code>setLexer</code>, preferably in the subclass constructor. */
   pANTLR3_LEXER d_lexer;
+
+  /** The ANTLR3 parser associated with this input. This will be <code>NULL</code> initially. It
+   *  must be set by a call to <code>setParser</code>, preferably in the subclass constructor.
+   *  The <code>super</code> field of <code>d_parser</code> will be set to <code>this</code> and
+   *  <code>reportError</code> will be set to <code>AntlrInput::reportError</code>. */
   pANTLR3_PARSER d_parser;
+
+  /** The ANTLR3 token stream associated with this input. We only need this so we can free it on exit.
+   *  This is set by <code>setLexer</code>.
+   *  NOTE: We assume that we <em>can</em> free it on exit. No sharing! */
   pANTLR3_COMMON_TOKEN_STREAM d_tokenStream;
+
+  /** The ANTLR3 token stream associated with this input. We only need this so we can free it on exit.
+   *  NOTE: We assume that we <em>can</em> free it on exit. No sharing! */
   pANTLR3_INPUT_STREAM d_input;
 
+  /** Turns an ANTLR3 exception into a message for the user and calls <code>parseError</code>. */
   static void reportError(pANTLR3_BASE_RECOGNIZER recognizer);
 
 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 lookahead the lookahead needed to parse the input (i.e., k for an LL(k) grammar)
+   * @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.
+   */
   AntlrInput(ExprManager* exprManager, const std::string& filename, unsigned int lookahead, bool useMmap);
+
+  /** Create an input from an istream. */
   // AntlrParser(ExprManager* em, std::istream& input, const std::string& name, unsigned int lookahead);
+
+  /** 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
+   * @param lookahead the lookahead needed to parse the input (i.e., k for an LL(k) grammar)
+   */
   AntlrInput(ExprManager* exprManager, const std::string& input, const std::string& name, unsigned int lookahead);
+
+  /** Destructor. Frees the token stream and closes the input. */
   ~AntlrInput();
 
+  /** Retrieve the text associated with a token. */
   inline static std::string tokenText(pANTLR3_COMMON_TOKEN token);
 
 protected:
 
   /**
-   * Throws a semantic exception with the given message.
+   * Throws a <code>ParserException</code> with the given message.
    */
   void parseError(const std::string& msg) throw (ParserException);
 
-  /** Get the lexer */
-  pANTLR3_LEXER getLexer();
   /** Retrieve the input stream for this parser. */
   pANTLR3_INPUT_STREAM getInputStream();
-  /** Retrieve the token stream for this parser. Must not be called before <code>setLexer()</code>. */
+  /** Retrieve the token stream for this parser. Must not be called before
+   * <code>setLexer()</code>. */
   pANTLR3_COMMON_TOKEN_STREAM getTokenStream();
+
   /** Set the ANTLR lexer for this parser. */
   void setLexer(pANTLR3_LEXER pLexer);
+
   /** Set the ANTLR parser implementation for this parser. */
   void setParser(pANTLR3_PARSER pParser);
 };
@@ -80,6 +120,8 @@ protected:
 std::string AntlrInput::tokenText(pANTLR3_COMMON_TOKEN token) {
   ANTLR3_MARKER start = token->getStartIndex(token);
   ANTLR3_MARKER end = token->getStopIndex(token);
+  /* start and end are boundary pointers. The text is a string
+   * of (end-start+1) bytes beginning at start. */
   std::string txt( (const char *)start, end-start+1 );
   Debug("parser-extra") << "tokenText: start=" << start << std::endl
                         <<  "end=" << end << std::endl
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
diff --git a/src/parser/input.h b/src/parser/input.h
index 68db0f5dd..af580d78e 100644
--- a/src/parser/input.h
+++ b/src/parser/input.h
@@ -92,7 +92,41 @@ inline std::string toString(SymbolType type) {
  */
 class CVC4_PUBLIC Input {
 
+  /** Whether to de-allocate the input */
+//  bool d_deleteInput;
+
+  /** The expression manager */
+  ExprManager* d_exprManager;
+
+  /** The symbol table lookup */
+  SymbolTable<Expr> d_varSymbolTable;
+
+  /** The sort table */
+  SymbolTable<Type*> d_sortTable;
+
+  /** The name of the input file. */
+  std::string d_filename;
+
+  /** Are we done */
+  bool d_done;
+
+  /** Are semantic checks enabled during parsing? */
+  bool d_checksEnabled;
+
 public:
+
+  /**
+   * Create a new parser for the given file.
+   * @param exprManager the ExprManager to use
+   * @param filename the path of the file to parse
+   */
+  Input(ExprManager* exprManager, const std::string& filename);
+
+  /**
+   * Destructor.
+   */
+  ~Input();
+
   /** Create a parser for the given file.
     *
     * @param exprManager the ExprManager for creating expressions from the input
@@ -120,13 +154,10 @@ public:
   static Input* newStringParser(ExprManager* exprManager, InputLanguage lang, const std::string& input, const std::string& name);
 
   /**
-   * Destructor.
-   */
-  ~Input();
-
-  /**
    * Parse the next command of the input. If EOF is encountered a EmptyCommand
    * is returned and done flag is set.
+   *
+   * @throws ParserException if an error is encountered during parsing.
    */
   Command* parseNextCommand() throw(ParserException);
 
@@ -134,6 +165,7 @@ public:
    * Parse the next expression of the stream. If EOF is encountered a null
    * expression is returned and done flag is set.
    * @return the parsed expression
+   * @throws ParserException if an error is encountered during parsing.
    */
   Expr parseNextExpression() throw(ParserException);
 
@@ -344,18 +376,29 @@ public:
     /** Returns the maximum arity of the given kind. */
     static unsigned int maxArity(Kind kind);
 
+    /** Throws a <code>ParserException</code> with the given error message.
+     * Implementations should fill in the <code>ParserException</code> with
+     * line number information, etc. */
     virtual void parseError(const std::string& msg) throw (ParserException) = 0;
 
 protected:
-    virtual Command* doParseCommand() throw(ParserException) = 0;
-    virtual Expr doParseExpr() throw(ParserException) = 0;
 
-    /**
-     * Create a new parser for the given file.
-     * @param exprManager the ExprManager to use
-     * @param filename the path of the file to parse
-     */
-    Input(ExprManager* exprManager, const std::string& filename);
+  /** Called by <code>parseNextCommand</code> to actually parse a command from
+   * the input by invoking the implementation-specific parsing method.  Returns
+   * <code>NULL</code> if there is no command there to parse.
+   *
+   * @throws ParserException if an error is encountered during parsing.
+   */
+  virtual Command* doParseCommand() throw(ParserException) = 0;
+
+  /** Called by <code>parseNextExpression</code> to actually parse an
+   * expression from the input by invoking the implementation-specific
+   * parsing method. Returns a null <code>Expr</code> if there is no
+   * expression there to parse.
+   *
+   * @throws ParserException if an error is encountered during parsing.
+   */
+  virtual Expr doParseExpr() throw(ParserException) = 0;
 
 private:
 
@@ -365,27 +408,6 @@ private:
   /** Lookup a symbol in the given namespace. */
   Expr getSymbol(const std::string& var_name, SymbolType type);
 
-  /** Whether to de-allocate the input */
-//  bool d_deleteInput;
-
-  /** The expression manager */
-  ExprManager* d_exprManager;
-
-  /** The symbol table lookup */
-  SymbolTable<Expr> d_varSymbolTable;
-
-  /** The sort table */
-  SymbolTable<Type*> d_sortTable;
-
-  /** The name of the input file. */
-  std::string d_filename;
-
-  /** Are we done */
-  bool d_done;
-
-  /** Are semantic checks enabled during parsing? */
-  bool d_checksEnabled;
-
 }; // end of class Parser
 
 }/* CVC4::parser namespace */
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