Refactoring Input/Parser code to support external manipulation of the parser state.

16 files changed, 526 insertions, 700 deletions

diff --git a/src/main/main.cpp b/src/main/main.cpp
index 819f7695e..bdf4f882b 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -23,6 +23,7 @@
 #include "main.h"
 #include "usage.h"
 #include "parser/input.h"
+#include "parser/parser.h"
 #include "expr/expr_manager.h"
 #include "smt/smt_engine.h"
 #include "expr/command.h"
@@ -152,17 +153,18 @@ int runCvc4(int argc, char* argv[]) {
 //  if(inputFromStdin) {
     //    parser = Parser::getNewParser(&exprMgr, options.lang, cin, "<stdin>");
 //  } else {
-    input = Input::newFileInput(&exprMgr, options.lang, argv[firstArgIndex],
-                                   options.memoryMap);
+    input = Input::newFileInput(options.lang, argv[firstArgIndex],
+                                     options.memoryMap);
 //  }
+  Parser parser(&exprMgr, input);
 
   if(!options.semanticChecks) {
-    input->disableChecks();
+    parser.disableChecks();
   }
 
   // Parse and execute commands until we are done
   Command* cmd;
-  while((cmd = input->parseNextCommand())) {
+  while((cmd = parser.nextCommand())) {
     if( !options.parseOnly ) {
       doCommand(smt, cmd);
     }
diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am
index 276266757..1464eeac0 100644
--- a/src/parser/Makefile.am
+++ b/src/parser/Makefile.am
@@ -34,20 +34,17 @@ libcvc4parser_noinst_la_LIBADD = \
 
 libcvc4parser_la_SOURCES =
 libcvc4parser_noinst_la_SOURCES = \
-	antlr_input.h \
-	antlr_input.cpp \
-	antlr_input_imports.cpp \
 	bounded_token_buffer.h \
 	bounded_token_buffer.cpp \
 	bounded_token_factory.h \
 	bounded_token_factory.cpp \
 	input.h \
 	input.cpp \
+	input_imports.cpp \
 	memory_mapped_input_buffer.h \
 	memory_mapped_input_buffer.cpp \
+    parser.h \
+    parser.cpp \
     parser_options.h \
-    parser_exception.h \
-    parser_state.h \
-    parser_state.cpp \
-	symbol_table.h
+    parser_exception.h
 
diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
deleted file mode 100644
index 47420a015..000000000
--- a/src/parser/antlr_input.cpp
+++ /dev/null
@@ -1,163 +0,0 @@
-/*********************                                                        */
-/** antlr_input.cpp
- ** Original author: cconway
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  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.
- **
- ** A super-class for ANTLR-generated input language parsers
- **/
-
-#include <limits.h>
-#include <antlr3.h>
-
-#include "antlr_input.h"
-#include "bounded_token_buffer.h"
-#include "bounded_token_factory.h"
-#include "memory_mapped_input_buffer.h"
-#include "parser_exception.h"
-#include "parser_state.h"
-
-#include "util/output.h"
-#include "util/Assert.h"
-#include "expr/command.h"
-#include "expr/type.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::parser;
-using namespace CVC4::kind;
-
-namespace CVC4 {
-namespace parser {
-
-AntlrInput::AntlrInput(ExprManager* exprManager, const std::string& filename, unsigned int lookahead, bool useMmap) :
-    Input(exprManager, filename),
-    d_lookahead(lookahead),
-    d_lexer(NULL),
-    d_parser(NULL),
-    d_tokenStream(NULL) {
-
-  if( useMmap ) {
-    d_input = MemoryMappedInputBufferNew(filename);
-  } else {
-    d_input = antlr3AsciiFileStreamNew((pANTLR3_UINT8) filename.c_str());
-  }
-  if( d_input == NULL ) {
-    throw ParserException("Couldn't open file: " + filename);
-  }
-}
-
-/*
-AntlrParser::AntlrParser(ExprManager* exprManager, std::istream& input, const std::string& name, unsigned int lookahead)
-  Parser(exprManager,name),
-  d_lookahead(lookahead) {
-
-}
-*/
-
-AntlrInput::AntlrInput(ExprManager* exprManager, const std::string& input, const std::string& name, unsigned int lookahead) :
-  Input(exprManager,name),
-  d_lookahead(lookahead),
-  d_lexer(NULL),
-  d_parser(NULL),
-  d_tokenStream(NULL) {
-  char* inputStr = strdup(input.c_str());
-  char* nameStr = strdup(name.c_str());
-  if( inputStr==NULL || nameStr==NULL ) {
-    throw ParserException("Couldn't initialize string input: '" + input + "'");
-  }
-  d_input = antlr3NewAsciiStringInPlaceStream((pANTLR3_UINT8)inputStr,input.size(),(pANTLR3_UINT8)nameStr);
-  if( d_input == NULL ) {
-    throw ParserException("Couldn't create input stream for string: '" + input + "'");
-  }
-}
-
-AntlrInput::~AntlrInput() {
-  d_tokenStream->free(d_tokenStream);
-  d_input->close(d_input);
-}
-
-pANTLR3_INPUT_STREAM AntlrInput::getInputStream() {
-  return d_input;
-}
-
-pANTLR3_COMMON_TOKEN_STREAM AntlrInput::getTokenStream() {
-  return d_tokenStream;
-}
-
-void AntlrInput::lexerError(pANTLR3_BASE_RECOGNIZER recognizer) {
-  pANTLR3_LEXER lexer = (pANTLR3_LEXER)(recognizer->super);
-  AlwaysAssert(lexer!=NULL);
-  ParserState *parserState = (ParserState*)(lexer->super);
-  AlwaysAssert(parserState!=NULL);
-
-  // Call the error display routine
-  parserState->parseError("Error finding next token.");
-}
-
-void AntlrInput::parseError(const std::string& message)
-    throw (ParserException) {
-  Debug("parser") << "Throwing exception: "
-      << getParserState()->getFilename() << ":"
-      << d_lexer->getLine(d_lexer) << "."
-      << d_lexer->getCharPositionInLine(d_lexer) << ": "
-      << message << endl;
-  throw ParserException(message, getParserState()->getFilename(),
-                        d_lexer->getLine(d_lexer),
-                        d_lexer->getCharPositionInLine(d_lexer));
-}
-
-
-void AntlrInput::setLexer(pANTLR3_LEXER pLexer) {
-  d_lexer = pLexer;
-
-  pANTLR3_TOKEN_FACTORY pTokenFactory = d_lexer->rec->state->tokFactory;
-  if( pTokenFactory != NULL ) {
-    pTokenFactory->close(pTokenFactory);
-  }
-
-  /* 2*lookahead should be sufficient, but we give ourselves some breathing room. */
-  pTokenFactory = BoundedTokenFactoryNew(d_input, 2*d_lookahead);
-  if( pTokenFactory == NULL ) {
-    throw ParserException("Couldn't create token factory.");
-  }
-  d_lexer->rec->state->tokFactory = pTokenFactory;
-
-  pBOUNDED_TOKEN_BUFFER buffer = BoundedTokenBufferSourceNew(d_lookahead, d_lexer->rec->state->tokSource);
-  if( buffer == NULL ) {
-    throw ParserException("Couldn't create token buffer.");
-  }
-
-  d_tokenStream = buffer->commonTstream;
-
-  // ANTLR isn't using super, AFAICT.
-  d_lexer->super = getParserState();
-  // Override default lexer error reporting
-  d_lexer->rec->reportError = &lexerError;
-}
-
-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 = getParserState();
-//  d_parser->rec->match = &match;
-  d_parser->rec->reportError = &reportError;
-  /* Don't try to recover from a parse error. */
-  // [chris 4/5/2010] Not clear on why this cast is necessary, but I get an error if I remove it.
-  d_parser->rec->recoverFromMismatchedToken =
-      (void* (*)(ANTLR3_BASE_RECOGNIZER_struct*, ANTLR3_UINT32, ANTLR3_BITSET_LIST_struct*))
-      d_parser->rec->mismatch;
-}
-
-
-}/* CVC4::parser namespace */
-}/* CVC4 namespace */
diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h
deleted file mode 100644
index a36853d7b..000000000
--- a/src/parser/antlr_input.h
+++ /dev/null
@@ -1,138 +0,0 @@
-/*********************                                                        */
-/** antlr_input.h
- ** Original author: cconway
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  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.
- **
- ** Base for ANTLR parser classes.
- **/
-
-#include "cvc4parser_private.h"
-
-#ifndef __CVC4__PARSER__ANTLR_PARSER_H
-#define __CVC4__PARSER__ANTLR_PARSER_H
-
-#include <vector>
-#include <string>
-#include <iostream>
-#include <antlr3.h>
-
-#include "expr/expr.h"
-#include "expr/expr_manager.h"
-#include "parser/input.h"
-#include "parser/symbol_table.h"
-#include "util/Assert.h"
-
-namespace CVC4 {
-
-class Command;
-class Type;
-class FunctionType;
-
-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);
-
-  /** Builds a message for a lexer error and calls <code>parseError</code>. */
-  static void lexerError(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 <code>ParserException</code> with the given message.
-   */
-  void parseError(const std::string& msg) throw (ParserException);
-
-  /** 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>. */
-  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);
-};
-
-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
-                        <<  "txt='" << txt << "'" << std::endl;
-  return txt;
-}
-
-}/* CVC4::parser namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__PARSER__ANTLR_PARSER_H */
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 3f4435966..94a8a6a32 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -48,7 +48,7 @@ options {
 
 @parser::includes {
 #include "expr/command.h"
-#include "parser/parser_state.h"
+#include "parser/parser.h"
 
 namespace CVC4 {
   class Expr;
@@ -59,8 +59,8 @@ namespace CVC4 {
 #include "expr/expr.h"
 #include "expr/kind.h"
 #include "expr/type.h"
-#include "parser/antlr_input.h"
-#include "parser/parser_state.h"
+#include "parser/input.h"
+#include "parser/parser.h"
 #include "util/output.h"
 #include <vector>
 
@@ -70,7 +70,7 @@ using namespace CVC4::parser;
 /* These need to be macros so they can refer to the PARSER macro, which will be defined
  * by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */
 #undef PARSER_STATE 
-#define PARSER_STATE ((ParserState*)PARSER->super)
+#define PARSER_STATE ((Parser*)PARSER->super)
 #undef EXPR_MANAGER
 #define EXPR_MANAGER PARSER_STATE->getExprManager()
 #undef MK_EXPR
@@ -104,7 +104,7 @@ parseCommand returns [CVC4::Command* cmd]
 command returns [CVC4::Command* cmd = 0]
 @init {
   Expr f;
-  Debug("parser-extra") << "command: " << AntlrInput::tokenText(LT(1)) << std::endl;
+  Debug("parser-extra") << "command: " << Input::tokenText(LT(1)) << std::endl;
 }
   : ASSERT_TOK formula[f] SEMICOLON { cmd = new AssertCommand(f);   }
   | QUERY_TOK formula[f] SEMICOLON { cmd = new QueryCommand(f);    }
@@ -124,7 +124,7 @@ declaration[CVC4::Command*& cmd]
 @init {
   std::vector<std::string> ids;
   Type t;
-  Debug("parser-extra") << "declaration: " << AntlrInput::tokenText(LT(1)) << std::endl;
+  Debug("parser-extra") << "declaration: " << Input::tokenText(LT(1)) << std::endl;
 }
   : // FIXME: These could be type or function declarations, if that matters.
     identifierList[ids, CHECK_UNDECLARED, SYM_VARIABLE] COLON declType[t,ids] SEMICOLON
@@ -134,7 +134,7 @@ declaration[CVC4::Command*& cmd]
 /** Match the right-hand side of a declaration. Returns the type. */
 declType[CVC4::Type& t, std::vector<std::string>& idList]
 @init {
-  Debug("parser-extra") << "declType: " << AntlrInput::tokenText(LT(1)) << std::endl;
+  Debug("parser-extra") << "declType: " << Input::tokenText(LT(1)) << std::endl;
 }
   : /* A sort declaration (e.g., "T : TYPE") */
     TYPE_TOK 
@@ -152,7 +152,7 @@ type[CVC4::Type& t]
 @init {
   Type t2;
   std::vector<Type> typeList;
-  Debug("parser-extra") << "type: " << AntlrInput::tokenText(LT(1)) << std::endl;
+  Debug("parser-extra") << "type: " << Input::tokenText(LT(1)) << std::endl;
 }
   : /* Simple type */
     baseType[t]
@@ -191,7 +191,7 @@ identifier[std::string& id,
            CVC4::parser::DeclarationCheck check,
            CVC4::parser::SymbolType type]
   : IDENTIFIER
-    { id = AntlrInput::tokenText($IDENTIFIER);
+    { id = Input::tokenText($IDENTIFIER);
       PARSER_STATE->checkDeclaration(id, check, type); }
   ;
 
@@ -202,7 +202,7 @@ identifier[std::string& id,
 baseType[CVC4::Type& t]
 @init {
   std::string id;
-  Debug("parser-extra") << "base type: " << AntlrInput::tokenText(LT(1)) << std::endl;
+  Debug("parser-extra") << "base type: " << Input::tokenText(LT(1)) << std::endl;
 }
   : BOOLEAN_TOK { t = EXPR_MANAGER->booleanType(); }
   | typeSymbol[t]
@@ -214,7 +214,7 @@ baseType[CVC4::Type& t]
 typeSymbol[CVC4::Type& t]
 @init {
   std::string id;
-  Debug("parser-extra") << "type symbol: " << AntlrInput::tokenText(LT(1)) << std::endl;
+  Debug("parser-extra") << "type symbol: " << Input::tokenText(LT(1)) << std::endl;
 }
   : identifier[id,CHECK_DECLARED,SYM_SORT]
     { t = PARSER_STATE->getSort(id); }
@@ -226,7 +226,7 @@ typeSymbol[CVC4::Type& t]
  */
 formula[CVC4::Expr& formula]
 @init {
-  Debug("parser-extra") << "formula: " << AntlrInput::tokenText(LT(1)) << std::endl;
+  Debug("parser-extra") << "formula: " << Input::tokenText(LT(1)) << std::endl;
 }
   :  iffFormula[formula]
   ;
@@ -250,7 +250,7 @@ formulaList[std::vector<CVC4::Expr>& formulas]
 iffFormula[CVC4::Expr& f]
 @init {
   Expr e;
-  Debug("parser-extra") << "<=> formula: " << AntlrInput::tokenText(LT(1)) << std::endl;
+  Debug("parser-extra") << "<=> formula: " << Input::tokenText(LT(1)) << std::endl;
 }
   : impliesFormula[f]
     ( IFF_TOK 
@@ -265,7 +265,7 @@ iffFormula[CVC4::Expr& f]
 impliesFormula[CVC4::Expr& f]
 @init {
   Expr e;
-  Debug("parser-extra") << "=> Formula: " << AntlrInput::tokenText(LT(1)) << std::endl;
+  Debug("parser-extra") << "=> Formula: " << Input::tokenText(LT(1)) << std::endl;
 }
   : orFormula[f]
     ( IMPLIES_TOK impliesFormula[e]
@@ -279,7 +279,7 @@ impliesFormula[CVC4::Expr& f]
 orFormula[CVC4::Expr& f]
 @init {
   std::vector<Expr> exprs;
-  Debug("parser-extra") << "OR Formula: " << AntlrInput::tokenText(LT(1)) << std::endl;
+  Debug("parser-extra") << "OR Formula: " << Input::tokenText(LT(1)) << std::endl;
 }
   : xorFormula[f]
       ( OR_TOK  { exprs.push_back(f); }
@@ -297,7 +297,7 @@ orFormula[CVC4::Expr& f]
 xorFormula[CVC4::Expr& f]
 @init {
   Expr e;
-  Debug("parser-extra") << "XOR formula: " << AntlrInput::tokenText(LT(1)) << std::endl;
+  Debug("parser-extra") << "XOR formula: " << Input::tokenText(LT(1)) << std::endl;
 }
   : andFormula[f]
     ( XOR_TOK andFormula[e]
@@ -311,7 +311,7 @@ xorFormula[CVC4::Expr& f]
 andFormula[CVC4::Expr& f]
 @init {
   std::vector<Expr> exprs;
-  Debug("parser-extra") << "AND Formula: " << AntlrInput::tokenText(LT(1)) << std::endl;
+  Debug("parser-extra") << "AND Formula: " << Input::tokenText(LT(1)) << std::endl;
 }
   : notFormula[f] 
     ( AND_TOK { exprs.push_back(f); }
@@ -329,7 +329,7 @@ andFormula[CVC4::Expr& f]
  */
 notFormula[CVC4::Expr& f]
 @init {
-  Debug("parser-extra") << "NOT formula: " << AntlrInput::tokenText(LT(1)) << std::endl;
+  Debug("parser-extra") << "NOT formula: " << Input::tokenText(LT(1)) << std::endl;
 }
   : /* negation */
     NOT_TOK notFormula[f]
@@ -341,7 +341,7 @@ notFormula[CVC4::Expr& f]
 predFormula[CVC4::Expr& f]
 @init {
   Expr e;
-  Debug("parser-extra") << "predicate formula: " << AntlrInput::tokenText(LT(1)) << std::endl;
+  Debug("parser-extra") << "predicate formula: " << Input::tokenText(LT(1)) << std::endl;
 }
   : term[f]
     (EQUAL_TOK term[e]
@@ -356,10 +356,10 @@ term[CVC4::Expr& f]
 @init {
   std::string name;
   std::vector<Expr> args;
-  Debug("parser-extra") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl;
+  Debug("parser-extra") << "term: " << Input::tokenText(LT(1)) << std::endl;
 }
   : /* function application */
-    // { isFunction(AntlrInput::tokenText(LT(1))) }?
+    // { isFunction(Input::tokenText(LT(1))) }?
     functionSymbol[f]
     { args.push_back( f ); }
     LPAREN formulaList[args] RPAREN
@@ -387,7 +387,7 @@ term[CVC4::Expr& f]
 iteTerm[CVC4::Expr& f]
 @init {
   std::vector<Expr> args;
-  Debug("parser-extra") << "ite: " << AntlrInput::tokenText(LT(1)) << std::endl;
+  Debug("parser-extra") << "ite: " << Input::tokenText(LT(1)) << std::endl;
 }
   : IF_TOK formula[f] { args.push_back(f); }
     THEN_TOK formula[f] { args.push_back(f); }
@@ -402,7 +402,7 @@ iteTerm[CVC4::Expr& f]
 iteElseTerm[CVC4::Expr& f]
 @init {
   std::vector<Expr> args;
-  Debug("parser-extra") << "else: " << AntlrInput::tokenText(LT(1)) << std::endl;
+  Debug("parser-extra") << "else: " << Input::tokenText(LT(1)) << std::endl;
 }
   : ELSE_TOK formula[f] 
   | ELSEIF_TOK iteCondition = formula[f] { args.push_back(f); }
@@ -418,7 +418,7 @@ iteElseTerm[CVC4::Expr& f]
  */
 functionSymbol[CVC4::Expr& f]
 @init {
-  Debug("parser-extra") << "function symbol: " << AntlrInput::tokenText(LT(1)) << std::endl;
+  Debug("parser-extra") << "function symbol: " << Input::tokenText(LT(1)) << std::endl;
   std::string name;
 }
   : identifier[name,CHECK_DECLARED,SYM_VARIABLE]
diff --git a/src/parser/cvc/cvc_input.cpp b/src/parser/cvc/cvc_input.cpp
index f247a651d..4595c52db 100644
--- a/src/parser/cvc/cvc_input.cpp
+++ b/src/parser/cvc/cvc_input.cpp
@@ -16,6 +16,7 @@
 #include <antlr3.h>
 
 #include "expr/expr_manager.h"
+#include "parser/input.h"
 #include "parser/parser_exception.h"
 #include "parser/cvc/cvc_input.h"
 #include "parser/cvc/generated/CvcLexer.h"
@@ -25,18 +26,9 @@ namespace CVC4 {
 namespace parser {
 
 /* Use lookahead=2 */
-CvcInput::CvcInput(ExprManager* exprManager, const std::string& filename, bool useMmap) :
-  AntlrInput(exprManager,filename,2,useMmap) {
-  init();
-}
-
-CvcInput::CvcInput(ExprManager* exprManager, const std::string& input, const std::string& name) :
-  AntlrInput(exprManager,input,name,2) {
-  init();
-}
-
-void CvcInput::init() {
-  pANTLR3_INPUT_STREAM input = getInputStream();
+CvcInput::CvcInput(AntlrInputStream *inputStream) :
+  Input(inputStream,2) {
+  pANTLR3_INPUT_STREAM input = inputStream->getAntlr3InputStream();
   AlwaysAssert( input != NULL );
 
   d_pCvcLexer = CvcLexerNew(input);
@@ -44,7 +36,7 @@ void CvcInput::init() {
     throw ParserException("Failed to create CVC lexer.");
   }
 
-  setLexer( d_pCvcLexer->pLexer );
+  setAntlr3Lexer( d_pCvcLexer->pLexer );
 
   pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream();
   AlwaysAssert( tokenStream != NULL );
@@ -54,7 +46,7 @@ void CvcInput::init() {
     throw ParserException("Failed to create CVC parser.");
   }
 
-  setParser(d_pCvcParser->pParser);
+  setAntlr3Parser(d_pCvcParser->pParser);
 }
 
 
@@ -63,11 +55,11 @@ CvcInput::~CvcInput() {
   d_pCvcParser->free(d_pCvcParser);
 }
 
-Command* CvcInput::doParseCommand() throw (ParserException) {
+Command* CvcInput::parseCommand() throw (ParserException) {
   return d_pCvcParser->parseCommand(d_pCvcParser);
 }
 
-Expr CvcInput::doParseExpr() throw (ParserException) {
+Expr CvcInput::parseExpr() throw (ParserException) {
   return d_pCvcParser->parseExpr(d_pCvcParser);
 }
 
diff --git a/src/parser/cvc/cvc_input.h b/src/parser/cvc/cvc_input.h
index 4878d015e..0d264f606 100644
--- a/src/parser/cvc/cvc_input.h
+++ b/src/parser/cvc/cvc_input.h
@@ -18,7 +18,7 @@
 #ifndef __CVC4__PARSER__CVC_INPUT_H
 #define __CVC4__PARSER__CVC_INPUT_H
 
-#include "parser/antlr_input.h"
+#include "parser/input.h"
 #include "parser/cvc/generated/CvcLexer.h"
 #include "parser/cvc/generated/CvcParser.h"
 
@@ -32,7 +32,7 @@ class ExprManager;
 
 namespace parser {
 
-class CvcInput : public AntlrInput {
+class CvcInput : public Input {
   /** The ANTLR3 CVC lexer for the input. */
   pCvcLexer d_pCvcLexer;
 
@@ -41,14 +41,11 @@ class CvcInput : public AntlrInput {
 
 public:
 
-  /** Create a file input.
+  /** Create an 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.
+   * @param inputStream the input to parse
    */
-  CvcInput(ExprManager* exprManager, const std::string& filename, bool useMmap);
+  CvcInput(AntlrInputStream *inputStream);
 
   /** Create a string input.
    *
@@ -56,8 +53,10 @@ public:
    * @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();
@@ -69,14 +68,14 @@ protected:
    *
    * @throws ParserException if an error is encountered during parsing.
    */
-  Command* doParseCommand() throw(ParserException);
+  Command* parseCommand() 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);
+  Expr parseExpr() throw(ParserException);
 
 private:
 
diff --git a/src/parser/input.cpp b/src/parser/input.cpp
index fd1a4cbd6..5df017f16 100644
--- a/src/parser/input.cpp
+++ b/src/parser/input.cpp
@@ -1,7 +1,7 @@
 /*********************                                                        */
 /** input.cpp
- ** Original author: dejan
- ** Major contributors: mdeters, cconway
+ ** Original author: cconway
+ ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
@@ -10,113 +10,176 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
- ** Parser implementation.
+ ** A super-class for ANTLR-generated input language parsers
  **/
 
-#include <stdint.h>
+#include <limits.h>
+#include <antlr3.h>
 
 #include "input.h"
+#include "bounded_token_buffer.h"
+#include "bounded_token_factory.h"
+#include "memory_mapped_input_buffer.h"
 #include "parser_exception.h"
-#include "parser_options.h"
-#include "parser_state.h"
+#include "parser.h"
+
 #include "expr/command.h"
-#include "expr/expr.h"
+#include "expr/type.h"
 #include "parser/cvc/cvc_input.h"
 #include "parser/smt/smt_input.h"
 #include "util/output.h"
 #include "util/Assert.h"
 
 using namespace std;
+using namespace CVC4;
+using namespace CVC4::parser;
+using namespace CVC4::kind;
 
 namespace CVC4 {
 namespace parser {
 
-bool Input::done() const {
-  return d_parserState->done();
+AntlrInputStream::AntlrInputStream(std::string name, pANTLR3_INPUT_STREAM input) :
+  d_name(name),
+  d_input(input) {
 }
 
-void Input::disableChecks() {
-  d_parserState->disableChecks();
+AntlrInputStream::~AntlrInputStream() {
+  d_input->free(d_input);
 }
 
-void Input::enableChecks() {
-  d_parserState->enableChecks();
+pANTLR3_INPUT_STREAM AntlrInputStream::getAntlr3InputStream() const {
+  return d_input;
 }
 
-Command* Input::parseNextCommand() throw(ParserException) {
-  Debug("parser") << "parseNextCommand()" << std::endl;
-  Command* cmd = NULL;
-  if(!done()) {
-    try {
-      cmd = doParseCommand();
-      if(cmd == NULL) {
-        d_parserState->setDone();
-      }
-    } catch(ParserException& e) {
-      d_parserState->setDone();
-      throw;
-    }
+const std::string AntlrInputStream::getName() const {
+  return d_name;
+}
+
+AntlrInputStream* AntlrInputStream::newFileInputStream(const std::string& name, bool useMmap) {
+  if( useMmap ) {
+    return new AntlrInputStream( name, MemoryMappedInputBufferNew(name) );
+  } else {
+    return new AntlrInputStream( name, antlr3AsciiFileStreamNew((pANTLR3_UINT8) name.c_str()) );
   }
-  Debug("parser") << "parseNextCommand() => " << cmd << std::endl;
-  return cmd;
-}
-
-Expr Input::parseNextExpression() throw(ParserException) {
-  Debug("parser") << "parseNextExpression()" << std::endl;
-  Expr result;
-  if(!done()) {
-    try {
-      result = doParseExpr();
-      if(result.isNull())
-        d_parserState->setDone();
-    } catch(ParserException& e) {
-      d_parserState->setDone();
-      throw;
+/*
+    if( d_inputStream == NULL ) {
+      throw ParserException("Couldn't open file: " + filename);
     }
+*/
+}
+
+AntlrInputStream* AntlrInputStream::newStringInputStream(const std::string& input, const std::string& name) /*throw (InputStreamException) */{
+  char* inputStr = strdup(input.c_str());
+  char* nameStr = strdup(name.c_str());
+/*
+  if( inputStr==NULL || nameStr==NULL ) {
+    throw InputStreamException("Couldn't initialize string input: '" + input + "'");
   }
-  Debug("parser") << "parseNextExpression() => " << result << std::endl;
-  return result;
+*/
+  return new AntlrInputStream( name,
+                               antlr3NewAsciiStringInPlaceStream(
+                                  (pANTLR3_UINT8)inputStr,input.size(),
+                                  (pANTLR3_UINT8)nameStr) );
+}
+
+
+Input::Input(AntlrInputStream *inputStream, unsigned int lookahead) :
+    d_lookahead(lookahead),
+    d_lexer(NULL),
+    d_parser(NULL),
+    d_tokenStream(NULL),
+    d_inputStream( inputStream ) {
+
+/*
+  if( useMmap ) {
+    d_inputStream = MemoryMappedInputBufferNew(filename);
+  } else {
+    d_inputStream = antlr3AsciiFileStreamNew((pANTLR3_UINT8) filename.c_str());
+  }
+*/
+/*
+  if( d_inputStream == NULL ) {
+    throw ParserException("Couldn't open file: " + filename);
+  }
+*/
+}
+
+/*
+AntlrParser::AntlrParser(ExprManager* exprManager, std::istream& input, const std::string& name, unsigned int lookahead)
+  Parser(exprManager,name),
+  d_lookahead(lookahead) {
+
 }
+*/
+
+/*
+Input::Input(ExprManager* exprManager, const std::string& input, const std::string& name, unsigned int lookahead) :
+  Input(exprManager,name),
+  d_lookahead(lookahead),
+  d_lexer(NULL),
+  d_parser(NULL),
+  d_tokenStream(NULL) {
+
+  char* inputStr = strdup(input.c_str());
+  char* nameStr = strdup(name.c_str());
+  if( inputStr==NULL || nameStr==NULL ) {
+    throw ParserException("Couldn't initialize string input: '" + input + "'");
+  }
+  d_inputStream = antlr3NewAsciiStringInPlaceStream((pANTLR3_UINT8)inputStr,input.size(),(pANTLR3_UINT8)nameStr);
+  if( d_inputStream == NULL ) {
+    throw ParserException("Couldn't create input stream for string: '" + input + "'");
+  }
 
-Input::Input(ExprManager* exprManager, const std::string& filename) {
-  d_parserState = new ParserState(exprManager,filename,this);
 }
+*/
 
 Input::~Input() {
-  delete d_parserState;
+  d_tokenStream->free(d_tokenStream);
+  delete d_inputStream;
 }
 
-Input* Input::newFileInput(ExprManager* em, InputLanguage lang,
-                           const std::string& filename, bool useMmap) {
+AntlrInputStream *Input::getInputStream() {
+  return d_inputStream;
+}
 
-  Input* input = 0;
+pANTLR3_COMMON_TOKEN_STREAM Input::getTokenStream() {
+  return d_tokenStream;
+}
 
-  switch(lang) {
-  case LANG_CVC4:
-    input = new CvcInput(em,filename,useMmap);
-    break;
-  case LANG_SMTLIB:
-    input = new SmtInput(em,filename,useMmap);
-    break;
+void Input::lexerError(pANTLR3_BASE_RECOGNIZER recognizer) {
+  pANTLR3_LEXER lexer = (pANTLR3_LEXER)(recognizer->super);
+  AlwaysAssert(lexer!=NULL);
+  Parser *parser = (Parser*)(lexer->super);
+  AlwaysAssert(parser!=NULL);
+  Input *input = parser->getInput();
+  AlwaysAssert(input!=NULL);
 
-  default:
-    Unhandled(lang);
-  }
+  // Call the error display routine
+  input->parseError("Error finding next token.");
+}
 
-  return input;
+Input* Input::newFileInput(InputLanguage lang,
+                           const std::string& filename, bool useMmap) {
+  AntlrInputStream *inputStream = AntlrInputStream::newFileInputStream(filename,useMmap);
+  return newInput(lang,inputStream);
 }
 
-Input* Input::newStringInput(ExprManager* em, InputLanguage lang,
+Input* Input::newStringInput(InputLanguage lang,
                              const std::string& str, const std::string& name) {
-  Input* input = 0;
+  AntlrInputStream *inputStream = AntlrInputStream::newStringInputStream(str,name);
+  return newInput(lang,inputStream);
+}
+
+Input* Input::newInput(InputLanguage lang, AntlrInputStream *inputStream) {
+  Input* input;
 
   switch(lang) {
   case LANG_CVC4: {
-    input = new CvcInput(em,str,name);
+    input = new CvcInput(inputStream);
     break;
   }
   case LANG_SMTLIB:
-    input = new SmtInput(em,str,name);
+    input = new SmtInput(inputStream);
     break;
 
   default:
@@ -125,5 +188,67 @@ Input* Input::newStringInput(ExprManager* em, InputLanguage lang,
   return input;
 }
 
+
+void Input::parseError(const std::string& message)
+    throw (ParserException) {
+  Debug("parser") << "Throwing exception: "
+      << d_inputStream->getName() << ":"
+      << d_lexer->getLine(d_lexer) << "."
+      << d_lexer->getCharPositionInLine(d_lexer) << ": "
+      << message << endl;
+  throw ParserException(message, d_inputStream->getName(),
+                        d_lexer->getLine(d_lexer),
+                        d_lexer->getCharPositionInLine(d_lexer));
+}
+
+
+void Input::setAntlr3Lexer(pANTLR3_LEXER pLexer) {
+  d_lexer = pLexer;
+
+  pANTLR3_TOKEN_FACTORY pTokenFactory = d_lexer->rec->state->tokFactory;
+  if( pTokenFactory != NULL ) {
+    pTokenFactory->close(pTokenFactory);
+  }
+
+  /* 2*lookahead should be sufficient, but we give ourselves some breathing room. */
+  pTokenFactory = BoundedTokenFactoryNew(d_inputStream->getAntlr3InputStream(), 2*d_lookahead);
+  if( pTokenFactory == NULL ) {
+    throw ParserException("Couldn't create token factory.");
+  }
+  d_lexer->rec->state->tokFactory = pTokenFactory;
+
+  pBOUNDED_TOKEN_BUFFER buffer = BoundedTokenBufferSourceNew(d_lookahead, d_lexer->rec->state->tokSource);
+  if( buffer == NULL ) {
+    throw ParserException("Couldn't create token buffer.");
+  }
+
+  d_tokenStream = buffer->commonTstream;
+
+  // Override default lexer error reporting
+  d_lexer->rec->reportError = &lexerError;
+}
+
+void Input::setParser(Parser *parser) {
+  // ANTLR isn't using super in the lexer or the parser, AFAICT.
+  // We could also use @lexer/parser::context to add a field to the generated
+  // objects, but then it would have to be declared separately in every
+  // language's grammar and we'd have to in the address of the field anyway.
+  d_lexer->super = parser;
+  d_parser->super = parser;
+
+}
+
+void Input::setAntlr3Parser(pANTLR3_PARSER pParser) {
+  d_parser = pParser;
+//  d_parser->rec->match = &match;
+  d_parser->rec->reportError = &reportError;
+  /* Don't try to recover from a parse error. */
+  // [chris 4/5/2010] Not clear on why this cast is necessary, but I get an error if I remove it.
+  d_parser->rec->recoverFromMismatchedToken =
+      (void* (*)(ANTLR3_BASE_RECOGNIZER_struct*, ANTLR3_UINT32, ANTLR3_BITSET_LIST_struct*))
+      d_parser->rec->mismatch;
+}
+
+
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
diff --git a/src/parser/input.h b/src/parser/input.h
index a32416305..21c5c4869 100644
--- a/src/parser/input.h
+++ b/src/parser/input.h
@@ -2,7 +2,7 @@
 /** input.h
  ** Original author: cconway
  ** Major contributors: none
- ** Minor contributors (to current version): mdeters
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -10,157 +10,228 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
- ** Parser abstraction.
+ ** Base for ANTLR parser classes.
  **/
 
-#include "cvc4parser_public.h"
+#include "cvc4parser_private.h"
 
-#ifndef __CVC4__PARSER__INPUT_H
-#define __CVC4__PARSER__INPUT_H
+#ifndef __CVC4__PARSER__ANTLR_INPUT_H
+#define __CVC4__PARSER__ANTLR_INPUT_H
 
+#include <antlr3.h>
+#include <iostream>
 #include <string>
+#include <vector>
 
 #include "expr/expr.h"
+#include "expr/expr_manager.h"
 #include "parser/parser_exception.h"
 #include "parser/parser_options.h"
+#include "util/Assert.h"
 
 namespace CVC4 {
 
-// Forward declarations
-class ExprManager;
 class Command;
 class Type;
+class FunctionType;
 
 namespace parser {
 
-class ParserState;
+/** Wrapper around an ANTLR3 input stream. */
+class AntlrInputStream {
+  std::string d_name;
+  pANTLR3_INPUT_STREAM d_input;
+
+  AntlrInputStream(std::string name,pANTLR3_INPUT_STREAM input);
+  /* This is private and throws an exception, because you should never use it. */
+  AntlrInputStream(const AntlrInputStream& inputStream) {
+    Unimplemented("copy constructor for AntlrInputStream");
+  }
+  /* This is private and throws an exception, because you should never use it. */
+  AntlrInputStream& operator=(const AntlrInputStream& inputStream) {
+    Unimplemented("operator= for AntlrInputStream");
+  }
+
+public:
+
+  virtual ~AntlrInputStream();
+
+  pANTLR3_INPUT_STREAM getAntlr3InputStream() const;
+  const std::string getName() const;
+
+  /** Create a file 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.
+   */
+  static AntlrInputStream* newFileInputStream(const std::string& name, bool useMmap = false);
+
+  /** Create an input from an istream. */
+  // AntlrInputStream newInputStream(std::istream& input, const std::string& name);
+
+  /** Create a string input.
+   *
+   * @param input the string to read
+   * @param name the "filename" to use when reporting errors
+   */
+  static AntlrInputStream* newStringInputStream(const std::string& input, const std::string& name);
+};
+
+class Parser;
 
 /**
- * An input to be parsed. This class serves two purposes: to the client, it provides
- * the methods <code>parseNextCommand</code> and <code>parseNextExpression</code> to
- * extract a stream of <code>Command</code>'s and <code>Expr</code>'s from the input;
- * to the parser, it provides a repository for state data, like the variable symbol
- * table, and a variety of convenience functions for updating and checking the state.
- *
- * An Input should be created using the static factory methods,
- * e.g., <code>newFileParser</code> and <code>newStringInput</code>, and
- * should be deleted when done.
+ * An input to be parsed. The static factory methods in this class (e.g.,
+ * <code>newFileInput</code>, <code>newStringInput</code>) create a parser
+ * for the given input language and attach it to an input source of the
+ * appropriate type.
  */
 class CVC4_PUBLIC Input {
-  friend class ParserState;
+  friend class Parser; // for parseError, parseCommand, parseExpr
 
-  /** Whether to de-allocate the input */
-  //  bool d_deleteInput;
+  /** The display name of the input (e.g., the filename). */
+  std::string d_name;
 
-  ParserState *d_parserState;
+  /** 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;
 
-public:
+  /** 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;
 
-  /**
-   * 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);
+  /** 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>Input::reportError</code>. */
+  pANTLR3_PARSER d_parser;
 
-  /**
-   * Destructor.
+  /** 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 input 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! */
+  AntlrInputStream *d_inputStream;
+
+  /** Turns an ANTLR3 exception into a message for the user and calls <code>parseError</code>. */
+  static void reportError(pANTLR3_BASE_RECOGNIZER recognizer);
+
+  /** Builds a message for a lexer error and calls <code>parseError</code>. */
+  static void lexerError(pANTLR3_BASE_RECOGNIZER recognizer);
+
+  /* Since we own d_tokenStream and it needs to be freed, we need to prevent
+   * copy construction and assignment.
    */
+  Input(const Input& input) { Unimplemented("Copy constructor for Input."); }
+  Input& operator=(const Input& input) { Unimplemented("operator= for Input."); }
+
+public:
+
+  /** Destructor. Frees the token stream and closes the input. */
   virtual ~Input();
 
   /** Create an input for the given file.
     *
-    * @param exprManager the ExprManager for creating expressions from the input
     * @param lang the input language
     * @param filename the input filename
     * @param useMmap true if the parser should use memory-mapped I/O (default: false)
     */
-   static Input* newFileInput(ExprManager* exprManager, InputLanguage lang, const std::string& filename, bool useMmap=false);
+  static Input* newFileInput(InputLanguage lang, const std::string& filename, bool useMmap=false);
+
+  /** Create an input for the given AntlrInputStream. NOTE: the new Input
+   * will take ownership of the input stream and delete it at destruction time.
+   *
+   * @param lang the input language
+   * @param inputStream the input stream
+   *
+   * */
+  static Input* newInput(InputLanguage lang, AntlrInputStream *inputStream);
 
   /** Create an input for the given stream.
    *
-   * @param exprManager the ExprManager for creating expressions from the input
    * @param lang the input language
    * @param input the input stream
    * @param name the name of the stream, for use in error messages
    */
-  //static Parser* getNewParser(ExprManager* exprManager, InputLanguage lang, std::istream& input, const std::string& name);
+  //static Parser* newStreamInput(InputLanguage lang, std::istream& input, const std::string& name);
 
   /** Create an input for the given string
    *
-   * @param exprManager the ExprManager for creating expressions from the input
    * @param lang the input language
    * @param input the input string
    * @param name the name of the stream, for use in error messages
    */
-  static Input* newStringInput(ExprManager* exprManager, InputLanguage lang, const std::string& input, const std::string& name);
+  static Input* newStringInput(InputLanguage lang, const std::string& input, const std::string& name);
 
-  /**
-   * Check if we are done -- either the end of input has been reached, or some
-   * error has been encountered.
-   * @return true if parser is done
-   */
-  bool done() const;
+  /** Retrieve the text associated with a token. */
+  inline static std::string tokenText(pANTLR3_COMMON_TOKEN token);
 
-  /** Enable semantic checks during parsing. */
-  void enableChecks();
 
-  /**
-   * Disable semantic checks during parsing. Disabling checks may lead
-   * to crashes on bad inputs.
-   */
-  void disableChecks();
-
-  /**
-   * Parse the next command of the input. If EOF is encountered a EmptyCommand
-   * is returned and done flag is set.
+protected:
+  /** Create an input. This input takes ownership of the given input stream,
+   * and will delete it at destruction time.
    *
-   * @throws ParserException if an error is encountered during parsing.
+   * @param inputStream the input stream to use
+   * @param lookahead the lookahead needed to parse the input (i.e., k for
+   * an LL(k) grammar)
    */
-  Command* parseNextCommand() throw(ParserException);
+  Input(AntlrInputStream *inputStream, unsigned int lookahead);
 
-  /**
-   * 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);
 
+  /** Retrieve the input stream for this parser. */
+  AntlrInputStream *getInputStream();
 
-protected:
+  /** Retrieve the token stream for this parser. Must not be called before
+   * <code>setLexer()</code>. */
+  pANTLR3_COMMON_TOKEN_STREAM getTokenStream();
 
-  /** Called by <code>parseNextCommand</code> to actually parse a command from
+  /** 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;
+  virtual Command* parseCommand() throw(ParserException) = 0;
+
+  /**
+   * Throws a <code>ParserException</code> with the given message.
+   */
+  void parseError(const std::string& msg) throw (ParserException);
 
-  /** Called by <code>parseNextExpression</code> to actually parse an
+  /** 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;
-
-  inline ParserState* getParserState() const {
-    return d_parserState;
-  }
-
-private:
-
-  /** 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;
-
-}; // end of class Input
+  virtual Expr parseExpr() throw(ParserException) = 0;
+
+  /** Set the ANTLR3 lexer for this input. */
+  void setAntlr3Lexer(pANTLR3_LEXER pLexer);
+
+  /** Set the ANTLR3 parser implementation for this input. */
+  void setAntlr3Parser(pANTLR3_PARSER pParser);
+
+  /** Set the Parser object for this input. */
+  void setParser(Parser *parser);
+};
+
+std::string Input::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
+                        <<  "txt='" << txt << "'" << std::endl;
+  return txt;
+}
 
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__PARSER__INPUT_H */
+#endif /* __CVC4__PARSER__ANTLR_INPUT_H */
diff --git a/src/parser/antlr_input_imports.cpp b/src/parser/input_imports.cpp
index 3555ed06b..73d804f95 100644
--- a/src/parser/antlr_input_imports.cpp
+++ b/src/parser/input_imports.cpp
@@ -35,8 +35,8 @@
 #include <antlr3.h>
 #include <sstream>
 
-#include "antlr_input.h"
-#include "parser_state.h"
+#include "input.h"
+#include "parser.h"
 #include "util/Assert.h"
 
 using namespace std;
@@ -62,10 +62,10 @@ namespace parser {
 /* *** CVC4 NOTE ***
  * This function is has been modified in not-completely-trivial ways from its
  * libantlr3c implementation to support more informative error messages and to
- * invoke the error reporting mechanism of the AntlrInput class instead of the
+ * invoke the error reporting mechanism of the Input class instead of the
  * default error printer.
  */
-void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) {
+void Input::reportError(pANTLR3_BASE_RECOGNIZER recognizer) {
   pANTLR3_EXCEPTION ex = recognizer->state->exception;
   pANTLR3_UINT8 * tokenNames = recognizer->state->tokenNames;
   stringstream ss;
@@ -230,13 +230,15 @@ void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) {
   }
 
   // Now get ready to throw an exception
-  pANTLR3_PARSER parser = (pANTLR3_PARSER)(recognizer->super);
+  pANTLR3_PARSER antlr3Parser = (pANTLR3_PARSER)(recognizer->super);
+  AlwaysAssert(antlr3Parser!=NULL);
+  Parser *parser = (Parser*)(antlr3Parser->super);
   AlwaysAssert(parser!=NULL);
-  ParserState *parserState = (ParserState*)(parser->super);
-  AlwaysAssert(parserState!=NULL);
+  Input *input = parser->getInput();
+  AlwaysAssert(input!=NULL);
 
   // Call the error display routine
-  parserState->parseError(ss.str());
+  input->parseError(ss.str());
 }
 
 } // namespace parser
diff --git a/src/parser/parser_state.cpp b/src/parser/parser.cpp
index 204dd3469..01cc99c3d 100644
--- a/src/parser/parser_state.cpp
+++ b/src/parser/parser.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/** parser_state.cpp
+/** parser.cpp
  ** Original author: cconway
  ** Major contributors: dejan, mdeters
  ** Minor contributors (to current version): none
@@ -18,14 +18,14 @@
 #include <stdint.h>
 
 #include "input.h"
+#include "parser.h"
+#include "parser_exception.h"
 #include "expr/command.h"
 #include "expr/expr.h"
 #include "expr/kind.h"
 #include "expr/type.h"
 #include "util/output.h"
 #include "util/Assert.h"
-#include "parser/parser_exception.h"
-#include "parser/symbol_table.h"
 #include "parser/cvc/cvc_input.h"
 #include "parser/smt/smt_input.h"
 
@@ -35,15 +35,15 @@ using namespace CVC4::kind;
 namespace CVC4 {
 namespace parser {
 
-ParserState::ParserState(ExprManager* exprManager, const std::string& filename, Input* input) :
+Parser::Parser(ExprManager* exprManager, Input* input) :
   d_exprManager(exprManager),
   d_input(input),
-  d_filename(filename),
   d_done(false),
   d_checksEnabled(true) {
+  d_input->setParser(this);
 }
 
-Expr ParserState::getSymbol(const std::string& name, SymbolType type) {
+Expr Parser::getSymbol(const std::string& name, SymbolType type) {
   Assert( isDeclared(name, type) );
 
   switch( type ) {
@@ -57,41 +57,41 @@ Expr ParserState::getSymbol(const std::string& name, SymbolType type) {
 }
 
 
-Expr ParserState::getVariable(const std::string& name) {
+Expr Parser::getVariable(const std::string& name) {
   return getSymbol(name, SYM_VARIABLE);
 }
 
 Type
-ParserState::getType(const std::string& var_name,
+Parser::getType(const std::string& var_name,
                      SymbolType type) {
   Assert( isDeclared(var_name, type) );
   Type t = getSymbol(var_name,type).getType();
   return t;
 }
 
-Type ParserState::getSort(const std::string& name) {
+Type Parser::getSort(const std::string& name) {
   Assert( isDeclared(name, SYM_SORT) );
   Type t = d_declScope.lookupType(name);
   return t;
 }
 
 /* Returns true if name is bound to a boolean variable. */
-bool ParserState::isBoolean(const std::string& name) {
+bool Parser::isBoolean(const std::string& name) {
   return isDeclared(name, SYM_VARIABLE) && getType(name).isBoolean();
 }
 
 /* Returns true if name is bound to a function. */
-bool ParserState::isFunction(const std::string& name) {
+bool Parser::isFunction(const std::string& name) {
   return isDeclared(name, SYM_VARIABLE) && getType(name).isFunction();
 }
 
 /* Returns true if name is bound to a function returning boolean. */
-bool ParserState::isPredicate(const std::string& name) {
+bool Parser::isPredicate(const std::string& name) {
   return isDeclared(name, SYM_VARIABLE) && getType(name).isPredicate();
 }
 
 Expr 
-ParserState::mkVar(const std::string& name, const Type& type) {
+Parser::mkVar(const std::string& name, const Type& type) {
   Debug("parser") << "mkVar(" << name << "," << type << ")" << std::endl;
   Expr expr = d_exprManager->mkVar(name, type);
   defineVar(name,expr);
@@ -99,7 +99,7 @@ ParserState::mkVar(const std::string& name, const Type& type) {
 }
 
 const std::vector<Expr>
-ParserState::mkVars(const std::vector<std::string> names,
+Parser::mkVars(const std::vector<std::string> names,
                     const Type& type) {
   std::vector<Expr> vars;
   for(unsigned i = 0; i < names.size(); ++i) {
@@ -109,24 +109,29 @@ ParserState::mkVars(const std::vector<std::string> names,
 }
 
 void
-ParserState::defineVar(const std::string& name, const Expr& val) {
+Parser::defineVar(const std::string& name, const Expr& val) {
   Assert(!isDeclared(name));
   d_declScope.bind(name,val);
   Assert(isDeclared(name));
 }
 
+void
+Parser::defineType(const std::string& name, const Type& type) {
+  Assert( !isDeclared(name, SYM_SORT) );
+  d_declScope.bindType(name,type);
+  Assert( isDeclared(name, SYM_SORT) ) ;
+}
+
 Type
-ParserState::mkSort(const std::string& name) {
+Parser::mkSort(const std::string& name) {
   Debug("parser") << "newSort(" << name << ")" << std::endl;
-  Assert( !isDeclared(name, SYM_SORT) ) ;
   Type type = d_exprManager->mkSort(name);
-  d_declScope.bindType(name, type);
-  Assert( isDeclared(name, SYM_SORT) ) ;
+  defineType(name,type);
   return type;
 }
 
 const std::vector<Type>
-ParserState::mkSorts(const std::vector<std::string>& names) {
+Parser::mkSorts(const std::vector<std::string>& names) {
   std::vector<Type> types;
   for(unsigned i = 0; i < names.size(); ++i) {
     types.push_back(mkSort(names[i]));
@@ -134,7 +139,7 @@ ParserState::mkSorts(const std::vector<std::string>& names) {
   return types;
 }
 
-bool ParserState::isDeclared(const std::string& name, SymbolType type) {
+bool Parser::isDeclared(const std::string& name, SymbolType type) {
   switch(type) {
   case SYM_VARIABLE:
     return d_declScope.isBound(name);
@@ -145,7 +150,7 @@ bool ParserState::isDeclared(const std::string& name, SymbolType type) {
   }
 }
 
-void ParserState::checkDeclaration(const std::string& varName,
+void Parser::checkDeclaration(const std::string& varName,
                                    DeclarationCheck check,
                                    SymbolType type)
     throw (ParserException) {
@@ -174,14 +179,14 @@ void ParserState::checkDeclaration(const std::string& varName,
   }
 }
 
-void ParserState::checkFunction(const std::string& name)
+void Parser::checkFunction(const std::string& name)
   throw (ParserException) {
   if( d_checksEnabled && !isFunction(name) ) {
     parseError("Expecting function symbol, found '" + name + "'");
   }
 }
 
-void ParserState::checkArity(Kind kind, unsigned int numArgs)
+void Parser::checkArity(Kind kind, unsigned int numArgs)
   throw (ParserException) {
   if(!d_checksEnabled) {
     return;
@@ -204,14 +209,49 @@ void ParserState::checkArity(Kind kind, unsigned int numArgs)
   }
 }
 
-void ParserState::enableChecks() {
+void Parser::enableChecks() {
   d_checksEnabled = true;
 }
 
-void ParserState::disableChecks() {
+void Parser::disableChecks() {
   d_checksEnabled = false;
 }
 
+Command* Parser::nextCommand() throw(ParserException) {
+  Debug("parser") << "nextCommand()" << std::endl;
+  Command* cmd = NULL;
+  if(!done()) {
+    try {
+      cmd = d_input->parseCommand();
+      if(cmd == NULL) {
+        setDone();
+      }
+    } catch(ParserException& e) {
+      setDone();
+      throw;
+    }
+  }
+  Debug("parser") << "nextCommand() => " << cmd << std::endl;
+  return cmd;
+}
+
+Expr Parser::nextExpression() throw(ParserException) {
+  Debug("parser") << "nextExpression()" << std::endl;
+  Expr result;
+  if(!done()) {
+    try {
+      result = d_input->parseExpr();
+      if(result.isNull())
+        setDone();
+    } catch(ParserException& e) {
+      setDone();
+      throw;
+    }
+  }
+  Debug("parser") << "nextExpression() => " << result << std::endl;
+  return result;
+}
+
 
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
diff --git a/src/parser/parser_state.h b/src/parser/parser.h
index 3ca9c2c0e..a84021c10 100644
--- a/src/parser/parser_state.h
+++ b/src/parser/parser.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/** parser_state.h
+/** parser.h
  ** Original author: cconway
  ** Major contributors: none
  ** Minor contributors (to current version): mdeters
@@ -20,13 +20,12 @@
 
 #include <string>
 
+#include "input.h"
+#include "parser_exception.h"
+#include "parser_options.h"
 #include "expr/declaration_scope.h"
 #include "expr/expr.h"
 #include "expr/kind.h"
-#include "parser/input.h"
-#include "parser/parser_exception.h"
-#include "parser/parser_options.h"
-#include "parser/symbol_table.h"
 #include "util/Assert.h"
 
 namespace CVC4 {
@@ -89,7 +88,12 @@ inline std::string toString(SymbolType type) {
   }
 }
 
-class ParserState {
+/**
+ * This class encapsulates all of the state of a parser, including the
+ * name of the file, line number and column information, and in-scope
+ * declarations.
+ */
+class CVC4_PUBLIC Parser {
 
   /** The expression manager */
   ExprManager *d_exprManager;
@@ -101,7 +105,7 @@ class ParserState {
   DeclarationScope d_declScope;
 
   /** The name of the input file. */
-  std::string d_filename;
+//  std::string d_filename;
 
   /** Are we done */
   bool d_done;
@@ -114,7 +118,14 @@ class ParserState {
   Expr getSymbol(const std::string& var_name, SymbolType type);
 
 public:
-  ParserState(ExprManager* exprManager, const std::string& filename, Input* input);
+  /** Create a parser state.
+   *
+   * @param exprManager the expression manager to use when creating expressions
+   * @param input the parser input
+   */
+  Parser(ExprManager* exprManager, Input* input);
+
+  virtual ~Parser() { }
 
   /** Get the associated <code>ExprManager</code>. */
   inline ExprManager* getExprManager() const {
@@ -153,9 +164,11 @@ public:
   void disableChecks();
 
   /** Get the name of the input file. */
+/*
   inline const std::string getFilename() {
     return d_filename;
   }
+*/
 
   /**
    * Sets the logic for the current benchmark. Declares any logic symbols.
@@ -228,8 +241,9 @@ public:
 
   /** Create a new variable definition (e.g., from a let binding). */
   void defineVar(const std::string& name, const Expr& val);
-  /** Remove a variable definition (e.g., from a let binding). */
-  void undefineVar(const std::string& name);
+
+  /** Create a new type definition. */
+  void defineType(const std::string& name, const Type& type);
 
   /**
    * Creates a new sort with the given name.
@@ -251,13 +265,16 @@ public:
   /** Is the symbol bound to a predicate? */
   bool isPredicate(const std::string& name);
 
+  Command* nextCommand() throw(ParserException);
+  Expr nextExpression() throw(ParserException);
+
   inline void parseError(const std::string& msg) throw (ParserException) {
     d_input->parseError(msg);
   }
 
   inline void pushScope() { d_declScope.pushScope(); }
   inline void popScope() { d_declScope.popScope(); }
-}; // class ParserState
+}; // class Parser
 
 } // namespace parser
 
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index 4539a6d43..cf22c5290 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -50,7 +50,7 @@ options {
 
 @parser::includes {
 #include "expr/command.h"
-#include "parser/parser_state.h"
+#include "parser/parser.h"
 
 namespace CVC4 {
   class Expr;
@@ -61,8 +61,8 @@ namespace CVC4 {
 #include "expr/expr.h"
 #include "expr/kind.h"
 #include "expr/type.h"
-#include "parser/antlr_input.h"
-#include "parser/parser_state.h"
+#include "parser/input.h"
+#include "parser/parser.h"
 #include "util/integer.h"
 #include "util/output.h"
 #include "util/rational.h"
@@ -74,7 +74,7 @@ using namespace CVC4::parser;
 /* These need to be macros so they can refer to the PARSER macro, which will be defined
  * by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */
 #undef PARSER_STATE 
-#define PARSER_STATE ((ParserState*)PARSER->super)
+#define PARSER_STATE ((Parser*)PARSER->super)
 #undef EXPR_MANAGER
 #define EXPR_MANAGER PARSER_STATE->getExprManager()
 #undef MK_EXPR
@@ -85,11 +85,11 @@ using namespace CVC4::parser;
 /**   
  * Sets the logic for the current benchmark. Declares any logic symbols.
  *
- * @param parserState pointer to the current parser state
+ * @param parser the CVC4 Parser object
  * @param name the name of the logic (e.g., QF_UF, AUFLIA)
  */
 void
-setLogic(ParserState *parserState, const std::string& name) {
+setLogic(Parser *parser, const std::string& name) {
   if( name == "QF_UF" ) {
     parserState->mkSort("U");
   } else if(name == "QF_LRA"){
@@ -174,7 +174,7 @@ benchAttribute returns [CVC4::Command* smt_command]
  */
 annotatedFormula[CVC4::Expr& expr]
 @init {
-  Debug("parser") << "annotated formula: " << AntlrInput::tokenText(LT(1)) << std::endl;
+  Debug("parser") << "annotated formula: " << Input::tokenText(LT(1)) << std::endl;
   Kind kind;
   std::string name;
   std::vector<Expr> args; /* = getExprVector(); */
@@ -236,11 +236,11 @@ annotatedFormula[CVC4::Expr& expr]
   | TRUE_TOK          { expr = MK_CONST(true); }
   | FALSE_TOK         { expr = MK_CONST(false); }
   | NUMERAL_TOK
-    { Integer num( AntlrInput::tokenText($NUMERAL_TOK) );
+    { Integer num( Input::tokenText($NUMERAL_TOK) );
       expr = MK_CONST(num); }
   | RATIONAL_TOK
     { // FIXME: This doesn't work because an SMT rational is not a valid GMP rational string
-      Rational rat( AntlrInput::tokenText($RATIONAL_TOK) );
+      Rational rat( Input::tokenText($RATIONAL_TOK) );
       expr = MK_CONST(rat); }
     // NOTE: Theory constants go here
     /* TODO: let, flet, quantifiers, arithmetic constants */
@@ -263,7 +263,7 @@ annotatedFormulas[std::vector<CVC4::Expr>& formulas, CVC4::Expr& expr]
 */
 builtinOp[CVC4::Kind& kind]
 @init {
-  Debug("parser") << "builtin: " << AntlrInput::tokenText(LT(1)) << std::endl;
+  Debug("parser") << "builtin: " << Input::tokenText(LT(1)) << std::endl;
 }
   : NOT_TOK      { $kind = CVC4::kind::NOT;     }
   | IMPLIES_TOK  { $kind = CVC4::kind::IMPLIES; }
@@ -417,7 +417,7 @@ identifier[std::string& id,
 		   CVC4::parser::DeclarationCheck check, 
            CVC4::parser::SymbolType type] 
   : IDENTIFIER
-    { id = AntlrInput::tokenText($IDENTIFIER);
+    { id = Input::tokenText($IDENTIFIER);
       Debug("parser") << "identifier: " << id
                       << " check? " << toString(check)
                       << " type? " << toString(type) << std::endl;
@@ -432,7 +432,7 @@ identifier[std::string& id,
 let_identifier[std::string& id,
     		   CVC4::parser::DeclarationCheck check] 
   : LET_IDENTIFIER
-    { id = AntlrInput::tokenText($LET_IDENTIFIER);
+    { id = Input::tokenText($LET_IDENTIFIER);
       Debug("parser") << "let_identifier: " << id
                       << " check? " << toString(check) << std::endl;
       PARSER_STATE->checkDeclaration(id, check, SYM_VARIABLE); }
@@ -446,7 +446,7 @@ let_identifier[std::string& id,
 flet_identifier[std::string& id,
     		    CVC4::parser::DeclarationCheck check] 
   : FLET_IDENTIFIER
-    { id = AntlrInput::tokenText($FLET_IDENTIFIER);
+    { id = Input::tokenText($FLET_IDENTIFIER);
       Debug("parser") << "flet_identifier: " << id
                       << " check? " << toString(check) << std::endl;
       PARSER_STATE->checkDeclaration(id, check); }
diff --git a/src/parser/smt/smt_input.cpp b/src/parser/smt/smt_input.cpp
index 1bff3d18f..451310cfd 100644
--- a/src/parser/smt/smt_input.cpp
+++ b/src/parser/smt/smt_input.cpp
@@ -15,9 +15,10 @@
 
 #include <antlr3.h>
 
+#include "smt_input.h"
 #include "expr/expr_manager.h"
+#include "parser/parser.h"
 #include "parser/parser_exception.h"
-#include "parser/smt/smt_input.h"
 #include "parser/smt/generated/SmtLexer.h"
 #include "parser/smt/generated/SmtParser.h"
 
@@ -25,20 +26,9 @@ namespace CVC4 {
 namespace parser {
 
 /* Use lookahead=2 */
-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) {
-  init();
-}
-
-void SmtInput::init() {
-  pANTLR3_INPUT_STREAM input = getInputStream();
+SmtInput::SmtInput(AntlrInputStream *inputStream) :
+  Input(inputStream, 2) {
+  pANTLR3_INPUT_STREAM input = inputStream->getAntlr3InputStream();
   AlwaysAssert( input != NULL );
 
   d_pSmtLexer = SmtLexerNew(input);
@@ -46,7 +36,7 @@ void SmtInput::init() {
     throw ParserException("Failed to create SMT lexer.");
   }
 
-  setLexer( d_pSmtLexer->pLexer );
+  setAntlr3Lexer( d_pSmtLexer->pLexer );
 
   pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream();
   AlwaysAssert( tokenStream != NULL );
@@ -56,7 +46,7 @@ void SmtInput::init() {
     throw ParserException("Failed to create SMT parser.");
   }
 
-  setParser(d_pSmtParser->pParser);
+  setAntlr3Parser(d_pSmtParser->pParser);
 }
 
 
@@ -65,11 +55,11 @@ SmtInput::~SmtInput() {
   d_pSmtParser->free(d_pSmtParser);
 }
 
-Command* SmtInput::doParseCommand() throw (ParserException) {
+Command* SmtInput::parseCommand() throw (ParserException) {
   return d_pSmtParser->parseCommand(d_pSmtParser);
 }
 
-Expr SmtInput::doParseExpr() throw (ParserException) {
+Expr SmtInput::parseExpr() throw (ParserException) {
   return d_pSmtParser->parseExpr(d_pSmtParser);
 }
 
diff --git a/src/parser/smt/smt_input.h b/src/parser/smt/smt_input.h
index f93a1bf0d..e9f4d2578 100644
--- a/src/parser/smt/smt_input.h
+++ b/src/parser/smt/smt_input.h
@@ -18,7 +18,7 @@
 #ifndef __CVC4__PARSER__SMT_INPUT_H
 #define __CVC4__PARSER__SMT_INPUT_H
 
-#include "parser/antlr_input.h"
+#include "parser/input.h"
 #include "parser/smt/generated/SmtLexer.h"
 #include "parser/smt/generated/SmtParser.h"
 
@@ -32,7 +32,7 @@ class ExprManager;
 
 namespace parser {
 
-class SmtInput : public AntlrInput {
+class SmtInput : public Input {
 
   /** The ANTLR3 SMT lexer for the input. */
   pSmtLexer d_pSmtLexer;
@@ -43,14 +43,11 @@ class SmtInput : public AntlrInput {
 public:
 
   /**
-   * Create a file input.
+   * Create an 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.
+   * @param inputStream the input stream to use
    */
-  SmtInput(ExprManager* exprManager, const std::string& filename, bool useMmap);
+  SmtInput(AntlrInputStream *inputStream);
 
   /**
    * Create a string input.
@@ -59,7 +56,7 @@ public:
    * @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);
+//  SmtInput(ExprManager* exprManager, const std::string& input, const std::string& name);
 
   /** Destructor. Frees the lexer and the parser. */
   ~SmtInput();
@@ -72,7 +69,7 @@ protected:
    *
    * @throws ParserException if an error is encountered during parsing.
    */
-  Command* doParseCommand() throw(ParserException);
+  Command* parseCommand() throw(ParserException);
 
   /**
    * Parse an expression from the input. Returns a null
@@ -80,7 +77,7 @@ protected:
    *
    * @throws ParserException if an error is encountered during parsing.
    */
-  Expr doParseExpr() throw(ParserException);
+  Expr parseExpr() throw(ParserException);
 
 private:
 
diff --git a/src/parser/symbol_table.h b/src/parser/symbol_table.h
deleted file mode 100644
index d6467f4e9..000000000
--- a/src/parser/symbol_table.h
+++ /dev/null
@@ -1,105 +0,0 @@
-/*********************                                                        */
-/** symbol_table.h
- ** Original author: cconway
- ** Major contributors: dejan, mdeters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  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.
- **
- ** A symbol table for the parsers' use.
- **/
-
-#include "cvc4parser_private.h"
-
-#ifndef __CVC4__PARSER__SYMBOL_TABLE_H
-#define __CVC4__PARSER__SYMBOL_TABLE_H
-
-#include <string>
-#include <stack>
-
-#include <ext/hash_map>
-
-#include "util/Assert.h"
-
-namespace CVC4 {
-namespace parser {
-
-struct StringHashFunction {
-  size_t operator()(const std::string& str) const {
-    return __gnu_cxx::hash<const char*>()(str.c_str());
-  }
-};
-
-/**
- * Generic symbol table for looking up variables by name.
- */
-template <class ObjectType>
-class SymbolTable {
-
-private:
-
-  /** The name to expression bindings */
-  typedef __gnu_cxx::hash_map<std::string, ObjectType, StringHashFunction>
-  LookupTable;
-
-  /** The table iterator */
-  typedef typename LookupTable::iterator table_iterator;
-  /** The table iterator */
-  typedef typename LookupTable::const_iterator const_table_iterator;
-
-  /** Bindings for the names */
-  LookupTable d_nameBindings;
-
-public:
-
-  /**
-   * Bind the name of the variable to the given expression. If the variable
-   * has been bind before, this will redefine it until its undefined.
-   */
-  void bindName(const std::string& name, const ObjectType& obj) throw () {
-    d_nameBindings[name] = obj;
-    Assert(isBound(name), "Expected name to be bound!");
-  }
-
-  /**
-   * Unbinds the last binding of the name to the expression.
-   */
-  void unbindName(const std::string& name) throw () {
-    table_iterator find = d_nameBindings.find(name);
-    if(find != d_nameBindings.end()) {
-/*
-      find->second.pop();
-      if(find->second.empty()) {
-*/
-        d_nameBindings.erase(find);
-/*      }*/
-    }
-  }
-
-  /**
-   * Returns the last binding expression of the name.
-   * Requires the name to have a binding in the table.
-   */
-  ObjectType getObject(const std::string& name) throw () {
-    table_iterator find = d_nameBindings.find(name);
-    Assert(find != d_nameBindings.end());
-    return find->second; /*.top()*/
-  }
-
-  /**
-   * Returns true is name is bound to an expression.
-   */
-  bool isBound(const std::string& name) const throw () {
-    const_table_iterator find = d_nameBindings.find(name);
-    return (find != d_nameBindings.end());
-  }
-};
-
-}/* CVC4::parser namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__PARSER__SYMBOL_TABLE_H */