Parser tweaks to address review

Private members of Input moved to new class ParserState

11 files changed, 918 insertions, 508 deletions

diff --git a/src/main/main.cpp b/src/main/main.cpp
index 174ab4b7f..5e1f4be93 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -146,23 +146,23 @@ int runCvc4(int argc, char* argv[]) {
   }
 
   // Create the parser
-  Input* parser;
-  istream* input = NULL;
+  Input* input;
 
+  /* TODO: Hack ANTLR3 to support input from streams */
 //  if(inputFromStdin) {
     //    parser = Parser::getNewParser(&exprMgr, options.lang, cin, "<stdin>");
 //  } else {
-    parser = Input::newFileParser(&exprMgr, options.lang, argv[firstArgIndex],
+    input = Input::newFileInput(&exprMgr, options.lang, argv[firstArgIndex],
                                    options.memoryMap);
 //  }
 
   if(!options.semanticChecks) {
-    parser->disableChecks();
+    input->disableChecks();
   }
 
   // Parse and execute commands until we are done
   Command* cmd;
-  while((cmd = parser->parseNextCommand())) {
+  while((cmd = input->parseNextCommand())) {
     if( !options.parseOnly ) {
       doCommand(smt, cmd);
     }
@@ -170,7 +170,7 @@ int runCvc4(int argc, char* argv[]) {
   }
 
   // Remove the parser
-  delete parser;
+  delete input;
   delete input;
 
   switch(lastResult.asSatisfiabilityResult().isSAT()) {
diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am
index 5d8b75f38..1aaf7ab69 100644
--- a/src/parser/Makefile.am
+++ b/src/parser/Makefile.am
@@ -46,5 +46,7 @@ libcvc4parser_noinst_la_SOURCES = \
 	memory_mapped_input_buffer.cpp \
     parser_options.h \
     parser_exception.h \
+    parser_state.h \
+    parser_state.cpp \
 	symbol_table.h
 
diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index 16f10cd93..0d6f63812 100644
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -17,15 +17,17 @@
 #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"
-#include "parser/antlr_input.h"
-#include "parser/bounded_token_buffer.h"
-#include "parser/bounded_token_factory.h"
-#include "parser/memory_mapped_input_buffer.h"
-#include "parser/parser_exception.h"
 
 using namespace std;
 using namespace CVC4;
@@ -92,12 +94,14 @@ pANTLR3_COMMON_TOKEN_STREAM AntlrInput::getTokenStream() {
 
 void AntlrInput::parseError(const std::string& message)
     throw (ParserException) {
-  Debug("parser") << "Throwing exception: " << getFilename() << ":"
+  Debug("parser") << "Throwing exception: "
+      << getParserState()->getFilename() << ":"
       << d_lexer->getLine(d_lexer) << "."
       << d_lexer->getCharPositionInLine(d_lexer) << ": "
       << message << endl;
-  throw ParserException(message, getFilename(), d_lexer->getLine(d_lexer),
-                          d_lexer->getCharPositionInLine(d_lexer));
+  throw ParserException(message, getParserState()->getFilename(),
+                        d_lexer->getLine(d_lexer),
+                        d_lexer->getCharPositionInLine(d_lexer));
 }
 
 void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) {
@@ -268,11 +272,11 @@ void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) {
   // Now get ready to throw an exception
   pANTLR3_PARSER parser = (pANTLR3_PARSER)(recognizer->super);
   AlwaysAssert(parser!=NULL);
-  AntlrInput *input = (AntlrInput*)(parser->super);
-  AlwaysAssert(input!=NULL);
+  ParserState *parserState = (ParserState*)(parser->super);
+  AlwaysAssert(parserState!=NULL);
 
   // Call the error display routine
-  input->parseError(ss.str());
+  parserState->parseError(ss.str());
 }
 
 void AntlrInput::setLexer(pANTLR3_LEXER pLexer) {
@@ -304,7 +308,7 @@ void AntlrInput::setParser(pANTLR3_PARSER pParser) {
   // 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->super = getParserState();
   d_parser->rec->reportError = &reportError;
 }
 
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index feb2e6d35..8b8f251ae 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/input.h"
+#include "parser/parser_state.h"
 
 namespace CVC4 {
   class Expr;
@@ -60,6 +60,7 @@ namespace CVC4 {
 #include "expr/kind.h"
 #include "expr/type.h"
 #include "parser/antlr_input.h"
+#include "parser/parser_state.h"
 #include "util/output.h"
 #include <vector>
 
@@ -68,10 +69,10 @@ 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 ANTLR_INPUT 
-#define ANTLR_INPUT ((Input*)PARSER->super)
+#undef PARSER_STATE 
+#define PARSER_STATE ((ParserState*)PARSER->super)
 #undef EXPR_MANAGER
-#define EXPR_MANAGER ANTLR_INPUT->getExprManager()
+#define EXPR_MANAGER PARSER_STATE->getExprManager()
 #undef MK_EXPR
 #define MK_EXPR EXPR_MANAGER->mkExpr
 #undef MK_CONST
@@ -136,10 +137,10 @@ declType[CVC4::Type*& t, std::vector<std::string>& idList]
 }
   : /* A sort declaration (e.g., "T : TYPE") */
     TYPE_TOK 
-    { ANTLR_INPUT->newSorts(idList); 
+    { PARSER_STATE->newSorts(idList); 
       t = EXPR_MANAGER->kindType(); }
   | /* A variable declaration */
-    type[t] { ANTLR_INPUT->mkVars(idList,t); }
+    type[t] { PARSER_STATE->mkVars(idList,t); }
   ;
 
 /**
@@ -190,7 +191,7 @@ identifier[std::string& id,
            CVC4::parser::SymbolType type]
   : IDENTIFIER
     { id = AntlrInput::tokenText($IDENTIFIER);
-      ANTLR_INPUT->checkDeclaration(id, check, type); }
+      PARSER_STATE->checkDeclaration(id, check, type); }
   ;
 
 /**
@@ -215,7 +216,7 @@ typeSymbol[CVC4::Type*& t]
   Debug("parser-extra") << "type symbol: " << AntlrInput::tokenText(LT(1)) << std::endl;
 }
   : identifier[id,CHECK_DECLARED,SYM_SORT]
-    { t = ANTLR_INPUT->getSort(id); }
+    { t = PARSER_STATE->getSort(id); }
   ;
 
 /**
@@ -376,7 +377,7 @@ term[CVC4::Expr& f]
 
   | /* variable */
     identifier[name,CHECK_DECLARED,SYM_VARIABLE]
-    { f = ANTLR_INPUT->getVariable(name); }
+    { f = PARSER_STATE->getVariable(name); }
   ;
 
 /**
@@ -420,8 +421,8 @@ functionSymbol[CVC4::Expr& f]
   std::string name;
 }
   : identifier[name,CHECK_DECLARED,SYM_VARIABLE]
-    { ANTLR_INPUT->checkFunction(name);
-      f = ANTLR_INPUT->getVariable(name); }
+    { PARSER_STATE->checkFunction(name);
+      f = PARSER_STATE->getVariable(name); }
   ;
 
 
diff --git a/src/parser/input.cpp b/src/parser/input.cpp
index 3b7b322ca..4d5f348d8 100644
--- a/src/parser/input.cpp
+++ b/src/parser/input.cpp
@@ -13,33 +13,34 @@
  ** Parser implementation.
  **/
 
-#include <iostream>
-#include <fstream>
 #include <stdint.h>
 
 #include "input.h"
+#include "parser_exception.h"
+#include "parser_options.h"
+#include "parser_state.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/cvc/cvc_input.h"
 #include "parser/smt/smt_input.h"
+#include "util/output.h"
+#include "util/Assert.h"
 
 using namespace std;
-using namespace CVC4::kind;
 
 namespace CVC4 {
 namespace parser {
 
-void Input::setDone(bool done) {
-  d_done = done;
+bool Input::done() const {
+  return d_parserState->done();
 }
 
-bool Input::done() const {
-  return d_done;
+void Input::disableChecks() {
+  d_parserState->disableChecks();
+}
+
+void Input::enableChecks() {
+  d_parserState->enableChecks();
 }
 
 Command* Input::parseNextCommand() throw (ParserException) {
@@ -49,10 +50,10 @@ Command* Input::parseNextCommand() throw (ParserException) {
     try {
       cmd = doParseCommand();
       if(cmd == NULL) {
-        setDone();
+        d_parserState->setDone();
       }
     } catch(ParserException& e) {
-      setDone();
+      d_parserState->setDone();
       throw ParserException(e.toString());
     }
   }
@@ -67,9 +68,9 @@ Expr Input::parseNextExpression() throw (ParserException) {
     try {
       result = doParseExpr();
       if(result.isNull())
-        setDone();
+        d_parserState->setDone();
     } catch(ParserException& e) {
-      setDone();
+      d_parserState->setDone();
       throw ParserException(e.toString());
     }
   }
@@ -77,271 +78,52 @@ Expr Input::parseNextExpression() throw (ParserException) {
   return result;
 }
 
-Input::~Input() {
+Input::Input(ExprManager* exprManager, const std::string& filename) {
+  d_parserState = new ParserState(exprManager,filename,this);
 }
 
-Input::Input(ExprManager* exprManager, const std::string& filename) :
-  d_exprManager(exprManager),
-  d_filename(filename),
-  d_done(false),
-  d_checksEnabled(true) {
+Input::~Input() {
+  delete d_parserState;
 }
 
-Input* Input::newFileParser(ExprManager* em, InputLanguage lang,
-                              const std::string& filename, bool useMmap) {
+Input* Input::newFileInput(ExprManager* em, InputLanguage lang,
+                           const std::string& filename, bool useMmap) {
 
-  Input* parser = 0;
+  Input* input = 0;
 
   switch(lang) {
   case LANG_CVC4:
-    parser = new CvcInput(em,filename,useMmap);
+    input = new CvcInput(em,filename,useMmap);
     break;
   case LANG_SMTLIB:
-    parser = new SmtInput(em,filename,useMmap);
+    input = new SmtInput(em,filename,useMmap);
     break;
 
   default:
     Unhandled(lang);
   }
 
-  return parser;
-}
-
-/*
-Parser* Parser::getNewParser(ExprManager* em, InputLanguage lang,
-                             istream& input, string filename) {
-  antlr::CharBuffer* inputBuffer = new CharBuffer(input);
-  return getNewParser(em, lang, inputBuffer, filename);
-}
-*/
-
-/*
-Parser* Parser::getNewParser(ExprManager* em, InputLanguage lang,
-                             std::istream& input, const std::string& name) {
-  Parser* parser = 0;
-
-  switch(lang) {
-  case LANG_CVC4: {
-    antlrLexer = new AntlrCvcLexer(*inputBuffer);
-    antlrParser = new AntlrCvcParser(*antlrLexer);
-    break;
-  }
-  case LANG_SMTLIB:
-    parser = new Smt(em,input,name);
-    break;
-
-  default:
-    Unhandled("Unknown Input language!");
-  }
-  return parser;
+  return input;
 }
-*/
 
-Input* Input::newStringParser(ExprManager* em, InputLanguage lang,
-                             const std::string& input, const std::string& name) {
-  Input* parser = 0;
+Input* Input::newStringInput(ExprManager* em, InputLanguage lang,
+                             const std::string& str, const std::string& name) {
+  Input* input = 0;
 
   switch(lang) {
   case LANG_CVC4: {
-    parser = new CvcInput(em,input,name);
+    input = new CvcInput(em,str,name);
     break;
   }
   case LANG_SMTLIB:
-    parser = new SmtInput(em,input,name);
+    input = new SmtInput(em,str,name);
     break;
 
   default:
     Unhandled(lang);
   }
-  return parser;
+  return input;
 }
 
-Expr Input::getSymbol(const std::string& name, SymbolType type) {
-  Assert( isDeclared(name, type) );
-
-
-  switch( type ) {
-
-  case SYM_VARIABLE: // Functions share var namespace
-    return d_varSymbolTable.getObject(name);
-
-  default:
-    Unhandled(type);
-  }
-}
-
-
-Expr Input::getVariable(const std::string& name) {
-  return getSymbol(name, SYM_VARIABLE);
-}
-
-Type*
-Input::getType(const std::string& var_name,
-                     SymbolType type) {
-  Assert( isDeclared(var_name, type) );
-  Type* t = getSymbol(var_name,type).getType();
-  return t;
-}
-
-Type* Input::getSort(const std::string& name) {
-  Assert( isDeclared(name, SYM_SORT) );
-  Type* t = d_sortTable.getObject(name);
-  return t;
-}
-
-/* Returns true if name is bound to a boolean variable. */
-bool Input::isBoolean(const std::string& name) {
-  return isDeclared(name, SYM_VARIABLE) && getType(name)->isBoolean();
-}
-
-/* Returns true if name is bound to a function. */
-bool Input::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 Input::isPredicate(const std::string& name) {
-  return isDeclared(name, SYM_VARIABLE) && getType(name)->isPredicate();
-}
-
-Expr 
-Input::mkVar(const std::string& name, Type* type) {
-  Debug("parser") << "mkVar(" << name << "," << *type << ")" << std::endl;
-  Expr expr = d_exprManager->mkVar(type, name);
-  defineVar(name,expr);
-  return expr;
-}
-
-const std::vector<Expr>
-Input::mkVars(const std::vector<std::string> names,
-                    Type* type) {
-  std::vector<Expr> vars;
-  for(unsigned i = 0; i < names.size(); ++i) {
-    vars.push_back(mkVar(names[i], type));
-  }
-  return vars;
-}
-
-void
-Input::defineVar(const std::string& name, const Expr& val) {
-  Assert(!isDeclared(name));
-  d_varSymbolTable.bindName(name,val);
-  Assert(isDeclared(name));
-}
-
-void
-Input::undefineVar(const std::string& name) {
-  Assert(isDeclared(name));
-  d_varSymbolTable.unbindName(name);
-  Assert(!isDeclared(name));
-}
-
-void
-Input::setLogic(const std::string& name) {
-  if( name == "QF_UF" ) {
-    newSort("U");
-  } else {
-    Unhandled(name);
-  }
-}
-
-Type*
-Input::newSort(const std::string& name) {
-  Debug("parser") << "newSort(" << name << ")" << std::endl;
-  Assert( !isDeclared(name, SYM_SORT) ) ;
-  Type* type = d_exprManager->mkSort(name);
-  d_sortTable.bindName(name, type);
-  Assert( isDeclared(name, SYM_SORT) ) ;
-  return type;
-}
-
-const std::vector<Type*>
-Input::newSorts(const std::vector<std::string>& names) {
-  std::vector<Type*> types;
-  for(unsigned i = 0; i < names.size(); ++i) {
-    types.push_back(newSort(names[i]));
-  }
-  return types;
-}
-
-bool Input::isDeclared(const std::string& name, SymbolType type) {
-  switch(type) {
-  case SYM_VARIABLE:
-    return d_varSymbolTable.isBound(name);
-  case SYM_SORT:
-    return d_sortTable.isBound(name);
-  default:
-    Unhandled(type);
-  }
-}
-
-void Input::checkDeclaration(const std::string& varName,
-                                   DeclarationCheck check,
-                                   SymbolType type)
-    throw (ParserException) {
-  if(!d_checksEnabled) {
-    return;
-  }
-
-  switch(check) {
-  case CHECK_DECLARED:
-    if( !isDeclared(varName, type) ) {
-      parseError("Symbol " + varName + " not declared");
-    }
-    break;
-
-  case CHECK_UNDECLARED:
-    if( isDeclared(varName, type) ) {
-      parseError("Symbol " + varName + " previously declared");
-    }
-    break;
-
-  case CHECK_NONE:
-    break;
-
-  default:
-    Unhandled(check);
-  }
-}
-
-void Input::checkFunction(const std::string& name)
-  throw (ParserException) {
-  if( d_checksEnabled && !isFunction(name) ) {
-    parseError("Expecting function symbol, found '" + name + "'");
-  }
-}
-
-void Input::checkArity(Kind kind, unsigned int numArgs)
-  throw (ParserException) {
-  if(!d_checksEnabled) {
-    return;
-  }
-
-  unsigned int min = d_exprManager->minArity(kind);
-  unsigned int max = d_exprManager->maxArity(kind);
-
-  if( numArgs < min || numArgs > max ) {
-    stringstream ss;
-    ss << "Expecting ";
-    if( numArgs < min ) {
-      ss << "at least " << min << " ";
-    } else {
-      ss << "at most " << max << " ";
-    }
-    ss << "arguments for operator '" << kind << "', ";
-    ss << "found " << numArgs;
-    parseError(ss.str());
-  }
-}
-
-void Input::enableChecks() {
-  d_checksEnabled = true;
-}
-
-void Input::disableChecks() {
-  d_checksEnabled = false;
-}
-
-
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
diff --git a/src/parser/input.h b/src/parser/input.h
index ad888c6cc..0e924364d 100644
--- a/src/parser/input.h
+++ b/src/parser/input.h
@@ -15,101 +15,44 @@
 
 #include "cvc4parser_public.h"
 
-#ifndef __CVC4__PARSER__PARSER_H
-#define __CVC4__PARSER__PARSER_H
+#ifndef __CVC4__PARSER__INPUT_H
+#define __CVC4__PARSER__INPUT_H
 
 #include <string>
-#include <iostream>
 
 #include "expr/expr.h"
-#include "expr/kind.h"
 #include "parser/parser_exception.h"
 #include "parser/parser_options.h"
-#include "parser/symbol_table.h"
-#include "util/Assert.h"
 
 namespace CVC4 {
 
 // Forward declarations
-class BooleanType;
 class ExprManager;
 class Command;
-class FunctionType;
-class KindType;
 class Type;
 
 namespace parser {
 
-/** Types of check for the symols */
-enum DeclarationCheck {
-  /** Enforce that the symbol has been declared */
-  CHECK_DECLARED,
-  /** Enforce that the symbol has not been declared */
-  CHECK_UNDECLARED,
-  /** Don't check anything */
-  CHECK_NONE
-};
-
-/** Returns a string representation of the given object (for
-    debugging). */
-inline std::string toString(DeclarationCheck check) {
-  switch(check) {
-  case CHECK_NONE: return "CHECK_NONE";
-  case CHECK_DECLARED:  return "CHECK_DECLARED";
-  case CHECK_UNDECLARED: return "CHECK_UNDECLARED";
-  default: Unreachable();
-  }
-}
-
-/**
- * Types of symbols. Used to define namespaces.
- */
-enum SymbolType {
-  /** Variables */
-  SYM_VARIABLE,
-  /** Sorts */
-  SYM_SORT
-};
-
-/** Returns a string representation of the given object (for
-    debugging). */
-inline std::string toString(SymbolType type) {
-  switch(type) {
-  case SYM_VARIABLE: return "SYM_VARIABLE";
-  case SYM_SORT: return "SYM_SORT";
-  default: Unreachable();
-  }
-}
+class ParserState;
 
 /**
- * The parser. The parser should be obtained by calling the static methods
- * getNewParser, and should be deleted when done.
+ * 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.
  *
- * This class includes convenience methods for interacting with the ExprManager
- * from within a grammar.
+ * 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.
  */
 class CVC4_PUBLIC Input {
+  friend class ParserState;
 
   /** 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;
+  //  bool d_deleteInput;
 
-  /** Are semantic checks enabled during parsing? */
-  bool d_checksEnabled;
+  ParserState *d_parserState;
 
 public:
 
@@ -123,17 +66,17 @@ public:
   /**
    * Destructor.
    */
-  ~Input();
+  virtual ~Input();
 
-  /** Create a parser for the given file.
+  /** 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
     */
-   static Input* newFileParser(ExprManager* exprManager, InputLanguage lang, const std::string& filename, bool useMmap=false);
+   static Input* newFileInput(ExprManager* exprManager, InputLanguage lang, const std::string& filename, bool useMmap=false);
 
-  /** Create a parser for the given input stream.
+  /** Create an input for the given stream.
    *
    * @param exprManager the ExprManager for creating expressions from the input
    * @param lang the input language
@@ -142,19 +85,27 @@ public:
    */
   //static Parser* getNewParser(ExprManager* exprManager, InputLanguage lang, std::istream& input, const std::string& name);
 
-  /** Create a parser for the given input string
+  /** 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* newStringParser(ExprManager* exprManager, InputLanguage lang, const std::string& input, const std::string& name);
+  static Input* newStringInput(ExprManager* exprManager, InputLanguage lang, const std::string& input, const std::string& name);
 
-  /** Get the <code>ExprManager</code> associated with this input. */
-  inline ExprManager* getExprManager() const {
-    return d_exprManager;
-  }
+  /**
+    * 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;
+
+  /** 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
@@ -172,127 +123,6 @@ public:
    */
   Expr parseNextExpression() throw(ParserException);
 
-  /**
-   * 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;
-
-  /** Enable semantic checks during parsing. */
-  void enableChecks();
-
-  /** Disable semantic checks during parsing. Disabling checks may lead to crashes on bad inputs. */
-  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.
-   *
-   * @param name the name of the logic (e.g., QF_UF, AUFLIA)
-   */
-  void setLogic(const std::string& name);
-
-  /**
-     * Returns a variable, given a name and a type.
-     * @param var_name the name of the variable
-     * @return the variable expression
-     */
-    Expr getVariable(const std::string& var_name);
-
-    /**
-     * Returns a sort, given a name
-     */
-    Type* getSort(const std::string& sort_name);
-
-    /**
-     * Checks if a symbol has been declared.
-     * @param name the symbol name
-     * @param type the symbol type
-     * @return true iff the symbol has been declared with the given type
-     */
-    bool isDeclared(const std::string& name, SymbolType type = SYM_VARIABLE);
-
-    /**
-     * Checks if the declaration policy we want to enforce holds
-     * for the given symbol.
-     * @param name the symbol to check
-     * @param check the kind of check to perform
-     * @param type the type of the symbol
-     * @throws ParserException if checks are enabled and the check fails
-     */
-    void checkDeclaration(const std::string& name,
-                          DeclarationCheck check,
-                          SymbolType type = SYM_VARIABLE)
-      throw (ParserException);
-
-    /**
-     * Checks whether the given name is bound to a function.
-     * @param name the name to check
-     * @throws ParserException if checks are enabled and name is not bound to a function
-     */
-    void checkFunction(const std::string& name) throw (ParserException);
-
-    /**
-     * Check that <code>kind</code> can accept <code>numArgs</codes> arguments.
-     * @param kind the built-in operator to check
-     * @param numArgs the number of actual arguments
-     * @throws ParserException if checks are enabled and the operator <code>kind</code> cannot be
-     * applied to <code>numArgs</code> arguments.
-     */
-    void checkArity(Kind kind, unsigned int numArgs) throw (ParserException);
-
-    /**
-     * Returns the type for the variable with the given name.
-     * @param name the symbol to lookup
-     * @param type the (namespace) type of the symbol
-     */
-    Type* getType(const std::string& var_name,
-                        SymbolType type = SYM_VARIABLE);
-
-    /** Create a new CVC4 variable expression of the given type. */
-    Expr mkVar(const std::string& name, Type* type);
-
-    /** Create a set of new CVC4 variable expressions of the given
-        type. */
-    const std::vector<Expr>
-    mkVars(const std::vector<std::string> names,
-           Type* type);
-
-
-    /** 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);
-
-    /**
-     * Creates a new sort with the given name.
-     */
-    Type* newSort(const std::string& name);
-
-    /**
-     * Creates a new sorts with the given names.
-     */
-    const std::vector<Type*>
-    newSorts(const std::vector<std::string>& names);
-
-    /** Is the symbol bound to a boolean variable? */
-    bool isBoolean(const std::string& name);
-
-    /** Is the symbol bound to a function? */
-    bool isFunction(const std::string& name);
-
-    /** Is the symbol bound to a predicate? */
-    bool isPredicate(const std::string& name);
-
-    /** 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:
 
@@ -313,17 +143,20 @@ protected:
    */
   virtual Expr doParseExpr() throw(ParserException) = 0;
 
-private:
+  inline ParserState* getParserState() const {
+    return d_parserState;
+  }
 
-  /** Sets the done flag */
-  void setDone(bool done = true);
+private:
 
-  /** Lookup a symbol in the given namespace. */
-  Expr getSymbol(const std::string& var_name, SymbolType type);
+  /** 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 Parser
+}; // end of class Input
 
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__PARSER__PARSER_H */
+#endif /* __CVC4__PARSER__INPUT_H */
diff --git a/src/parser/parser_state.cpp b/src/parser/parser_state.cpp
new file mode 100644
index 000000000..9e8ff577e
--- /dev/null
+++ b/src/parser/parser_state.cpp
@@ -0,0 +1,234 @@
+/*********************                                                        */
+/** parser_state.cpp
+ ** 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.
+ **
+ ** Parser state implementation.
+ **/
+
+#include <iostream>
+#include <fstream>
+#include <stdint.h>
+
+#include "input.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"
+
+using namespace std;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace parser {
+
+ParserState::ParserState(ExprManager* exprManager, const std::string& filename, Input* input) :
+  d_exprManager(exprManager),
+  d_input(input),
+  d_filename(filename),
+  d_done(false),
+  d_checksEnabled(true) {
+}
+
+Expr ParserState::getSymbol(const std::string& name, SymbolType type) {
+  Assert( isDeclared(name, type) );
+
+
+  switch( type ) {
+
+  case SYM_VARIABLE: // Functions share var namespace
+    return d_varTable.getObject(name);
+
+  default:
+    Unhandled(type);
+  }
+}
+
+
+Expr ParserState::getVariable(const std::string& name) {
+  return getSymbol(name, SYM_VARIABLE);
+}
+
+Type*
+ParserState::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) {
+  Assert( isDeclared(name, SYM_SORT) );
+  Type* t = d_sortTable.getObject(name);
+  return t;
+}
+
+/* Returns true if name is bound to a boolean variable. */
+bool ParserState::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) {
+  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) {
+  return isDeclared(name, SYM_VARIABLE) && getType(name)->isPredicate();
+}
+
+Expr 
+ParserState::mkVar(const std::string& name, Type* type) {
+  Debug("parser") << "mkVar(" << name << "," << *type << ")" << std::endl;
+  Expr expr = d_exprManager->mkVar(type, name);
+  defineVar(name,expr);
+  return expr;
+}
+
+const std::vector<Expr>
+ParserState::mkVars(const std::vector<std::string> names,
+                    Type* type) {
+  std::vector<Expr> vars;
+  for(unsigned i = 0; i < names.size(); ++i) {
+    vars.push_back(mkVar(names[i], type));
+  }
+  return vars;
+}
+
+void
+ParserState::defineVar(const std::string& name, const Expr& val) {
+  Assert(!isDeclared(name));
+  d_varTable.bindName(name,val);
+  Assert(isDeclared(name));
+}
+
+void
+ParserState::undefineVar(const std::string& name) {
+  Assert(isDeclared(name));
+  d_varTable.unbindName(name);
+  Assert(!isDeclared(name));
+}
+
+void
+ParserState::setLogic(const std::string& name) {
+  if( name == "QF_UF" ) {
+    newSort("U");
+  } else {
+    Unhandled(name);
+  }
+}
+
+Type*
+ParserState::newSort(const std::string& name) {
+  Debug("parser") << "newSort(" << name << ")" << std::endl;
+  Assert( !isDeclared(name, SYM_SORT) ) ;
+  Type* type = d_exprManager->mkSort(name);
+  d_sortTable.bindName(name, type);
+  Assert( isDeclared(name, SYM_SORT) ) ;
+  return type;
+}
+
+const std::vector<Type*>
+ParserState::newSorts(const std::vector<std::string>& names) {
+  std::vector<Type*> types;
+  for(unsigned i = 0; i < names.size(); ++i) {
+    types.push_back(newSort(names[i]));
+  }
+  return types;
+}
+
+bool ParserState::isDeclared(const std::string& name, SymbolType type) {
+  switch(type) {
+  case SYM_VARIABLE:
+    return d_varTable.isBound(name);
+  case SYM_SORT:
+    return d_sortTable.isBound(name);
+  default:
+    Unhandled(type);
+  }
+}
+
+void ParserState::checkDeclaration(const std::string& varName,
+                                   DeclarationCheck check,
+                                   SymbolType type)
+    throw (ParserException) {
+  if(!d_checksEnabled) {
+    return;
+  }
+
+  switch(check) {
+  case CHECK_DECLARED:
+    if( !isDeclared(varName, type) ) {
+      parseError("Symbol " + varName + " not declared");
+    }
+    break;
+
+  case CHECK_UNDECLARED:
+    if( isDeclared(varName, type) ) {
+      parseError("Symbol " + varName + " previously declared");
+    }
+    break;
+
+  case CHECK_NONE:
+    break;
+
+  default:
+    Unhandled(check);
+  }
+}
+
+void ParserState::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)
+  throw (ParserException) {
+  if(!d_checksEnabled) {
+    return;
+  }
+
+  unsigned int min = d_exprManager->minArity(kind);
+  unsigned int max = d_exprManager->maxArity(kind);
+
+  if( numArgs < min || numArgs > max ) {
+    stringstream ss;
+    ss << "Expecting ";
+    if( numArgs < min ) {
+      ss << "at least " << min << " ";
+    } else {
+      ss << "at most " << max << " ";
+    }
+    ss << "arguments for operator '" << kind << "', ";
+    ss << "found " << numArgs;
+    parseError(ss.str());
+  }
+}
+
+void ParserState::enableChecks() {
+  d_checksEnabled = true;
+}
+
+void ParserState::disableChecks() {
+  d_checksEnabled = false;
+}
+
+
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
diff --git a/src/parser/parser_state.h b/src/parser/parser_state.h
new file mode 100644
index 000000000..3130e1f46
--- /dev/null
+++ b/src/parser/parser_state.h
@@ -0,0 +1,258 @@
+/*********************                                                        */
+/** parser_state.h
+ ** Original author: cconway
+ ** Major contributors: none
+ ** Minor contributors (to current version): mdeters
+ ** 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 collection of state for use by parser implementations.
+ **/
+
+#ifndef __CVC4__PARSER__PARSER_STATE_H_
+#define __CVC4__PARSER__PARSER_STATE_H_
+
+#include <string>
+
+#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 {
+
+// Forward declarations
+class BooleanType;
+class ExprManager;
+class Command;
+class FunctionType;
+class KindType;
+class Type;
+
+namespace parser {
+
+/** Types of check for the symols */
+enum DeclarationCheck {
+  /** Enforce that the symbol has been declared */
+  CHECK_DECLARED,
+  /** Enforce that the symbol has not been declared */
+  CHECK_UNDECLARED,
+  /** Don't check anything */
+  CHECK_NONE
+};
+
+/** Returns a string representation of the given object (for
+ debugging). */
+inline std::string toString(DeclarationCheck check) {
+  switch(check) {
+  case CHECK_NONE:
+    return "CHECK_NONE";
+  case CHECK_DECLARED:
+    return "CHECK_DECLARED";
+  case CHECK_UNDECLARED:
+    return "CHECK_UNDECLARED";
+  default:
+    Unreachable();
+  }
+}
+
+/**
+ * Types of symbols. Used to define namespaces.
+ */
+enum SymbolType {
+  /** Variables */
+  SYM_VARIABLE,
+  /** Sorts */
+  SYM_SORT
+};
+
+/** Returns a string representation of the given object (for
+ debugging). */
+inline std::string toString(SymbolType type) {
+  switch(type) {
+  case SYM_VARIABLE:
+    return "SYM_VARIABLE";
+  case SYM_SORT:
+    return "SYM_SORT";
+  default:
+    Unreachable();
+  }
+}
+
+class ParserState {
+
+  /** The expression manager */
+  ExprManager *d_exprManager;
+
+  /** The input that we're parsing. */
+  Input *d_input;
+
+  /** The symbol table lookup */
+  SymbolTable<Expr> d_varTable;
+
+  /** 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;
+
+
+  /** Lookup a symbol in the given namespace. */
+  Expr getSymbol(const std::string& var_name, SymbolType type);
+
+public:
+  ParserState(ExprManager* exprManager, const std::string& filename, Input* input);
+
+  /** Get the associated <code>ExprManager</code>. */
+  inline ExprManager* getExprManager() const {
+    return d_exprManager;
+  }
+
+  /** Get the associated input. */
+  inline Input* getInput() const {
+    return d_input;
+  }
+
+  /**
+   * 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
+   */
+  inline bool done() const {
+    return d_done;
+  }
+
+  /** Sets the done flag */
+  inline void setDone(bool done = true) {
+    d_done = done;
+  }
+
+  /** Enable semantic checks during parsing. */
+  void enableChecks();
+
+  /** Disable semantic checks during parsing. Disabling checks may lead to crashes on bad inputs. */
+  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.
+   *
+   * @param name the name of the logic (e.g., QF_UF, AUFLIA)
+   */
+  void setLogic(const std::string& name);
+
+  /**
+   * Returns a variable, given a name and a type.
+   * @param var_name the name of the variable
+   * @return the variable expression
+   */
+  Expr getVariable(const std::string& var_name);
+
+  /**
+   * Returns a sort, given a name
+   */
+  Type* getSort(const std::string& sort_name);
+
+  /**
+   * Checks if a symbol has been declared.
+   * @param name the symbol name
+   * @param type the symbol type
+   * @return true iff the symbol has been declared with the given type
+   */
+  bool isDeclared(const std::string& name, SymbolType type = SYM_VARIABLE);
+
+  /**
+   * Checks if the declaration policy we want to enforce holds
+   * for the given symbol.
+   * @param name the symbol to check
+   * @param check the kind of check to perform
+   * @param type the type of the symbol
+   * @throws ParserException if checks are enabled and the check fails
+   */
+  void checkDeclaration(const std::string& name, DeclarationCheck check,
+                        SymbolType type = SYM_VARIABLE) throw (ParserException);
+
+  /**
+   * Checks whether the given name is bound to a function.
+   * @param name the name to check
+   * @throws ParserException if checks are enabled and name is not bound to a function
+   */
+  void checkFunction(const std::string& name) throw (ParserException);
+
+  /**
+   * Check that <code>kind</code> can accept <code>numArgs</codes> arguments.
+   * @param kind the built-in operator to check
+   * @param numArgs the number of actual arguments
+   * @throws ParserException if checks are enabled and the operator <code>kind</code> cannot be
+   * applied to <code>numArgs</code> arguments.
+   */
+  void checkArity(Kind kind, unsigned int numArgs) throw (ParserException);
+
+  /**
+   * Returns the type for the variable with the given name.
+   * @param name the symbol to lookup
+   * @param type the (namespace) type of the symbol
+   */
+  Type* getType(const std::string& var_name, SymbolType type = SYM_VARIABLE);
+
+  /** Create a new CVC4 variable expression of the given type. */
+  Expr mkVar(const std::string& name, Type* type);
+
+  /** Create a set of new CVC4 variable expressions of the given
+   type. */
+  const std::vector<Expr>
+  mkVars(const std::vector<std::string> names, Type* type);
+
+  /** 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);
+
+  /**
+   * Creates a new sort with the given name.
+   */
+  Type* newSort(const std::string& name);
+
+  /**
+   * Creates a new sorts with the given names.
+   */
+  const std::vector<Type*>
+  newSorts(const std::vector<std::string>& names);
+
+  /** Is the symbol bound to a boolean variable? */
+  bool isBoolean(const std::string& name);
+
+  /** Is the symbol bound to a function? */
+  bool isFunction(const std::string& name);
+
+  /** Is the symbol bound to a predicate? */
+  bool isPredicate(const std::string& name);
+
+  inline void parseError(const std::string& msg) throw (ParserException) {
+    d_input->parseError(msg);
+  }
+
+}; // class ParserState
+
+} // namespace parser
+
+} // namespace CVC4
+
+#endif /* __CVC4__PARSER__PARSER_STATE_H_ */
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index 86c1b015d..9bcee54fd 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -48,7 +48,7 @@ options {
 
 @parser::includes {
 #include "expr/command.h"
-#include "parser/input.h"
+#include "parser/parser_state.h"
 
 namespace CVC4 {
   class Expr;
@@ -60,6 +60,7 @@ namespace CVC4 {
 #include "expr/kind.h"
 #include "expr/type.h"
 #include "parser/antlr_input.h"
+#include "parser/parser_state.h"
 #include "util/output.h"
 #include <vector>
 
@@ -68,10 +69,10 @@ 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 ANTLR_INPUT 
-#define ANTLR_INPUT ((Input*)PARSER->super)
+#undef PARSER_STATE 
+#define PARSER_STATE ((ParserState*)PARSER->super)
 #undef EXPR_MANAGER
-#define EXPR_MANAGER ANTLR_INPUT->getExprManager()
+#define EXPR_MANAGER PARSER_STATE->getExprManager()
 #undef MK_EXPR
 #define MK_EXPR EXPR_MANAGER->mkExpr
 #undef MK_CONST
@@ -129,7 +130,7 @@ benchAttribute returns [CVC4::Command* smt_command]
   Expr expr;
 }
   : LOGIC_TOK identifier[name,CHECK_NONE,SYM_VARIABLE]
-    { ANTLR_INPUT->setLogic(name);
+    { PARSER_STATE->setLogic(name);
       smt_command = new SetBenchmarkLogicCommand(name);   }
   | ASSUMPTION_TOK annotatedFormula[expr]
     { smt_command = new AssertCommand(expr);   }
@@ -157,7 +158,7 @@ annotatedFormula[CVC4::Expr& expr]
 } 
   : /* a built-in operator application */
     LPAREN_TOK builtinOp[kind] annotatedFormulas[args,expr] RPAREN_TOK 
-    { ANTLR_INPUT->checkArity(kind, args.size());
+    { PARSER_STATE->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. */
@@ -196,16 +197,16 @@ annotatedFormula[CVC4::Expr& expr]
     (LET_TOK LPAREN_TOK let_identifier[name,CHECK_UNDECLARED]
       | FLET_TOK LPAREN_TOK flet_identifier[name,CHECK_UNDECLARED] )
     annotatedFormula[expr] RPAREN_TOK
-    { ANTLR_INPUT->defineVar(name,expr); }
+    { PARSER_STATE->defineVar(name,expr); }
     annotatedFormula[expr]
     RPAREN_TOK
-    { ANTLR_INPUT->undefineVar(name); }
+    { PARSER_STATE->undefineVar(name); }
 
   | /* a variable */
     ( identifier[name,CHECK_DECLARED,SYM_VARIABLE]
       | let_identifier[name,CHECK_DECLARED] 
       | flet_identifier[name,CHECK_DECLARED] )
-    { expr = ANTLR_INPUT->getVariable(name); }
+    { expr = PARSER_STATE->getVariable(name); }
 
     /* constants */
   | TRUE_TOK          { expr = MK_CONST(true); }
@@ -268,8 +269,8 @@ functionSymbol[CVC4::Expr& fun]
 	std::string name;
 }
   : functionName[name,CHECK_DECLARED]
-    { ANTLR_INPUT->checkFunction(name);
-      fun = ANTLR_INPUT->getVariable(name); }
+    { PARSER_STATE->checkFunction(name);
+      fun = PARSER_STATE->getVariable(name); }
   ;
   
 /**
@@ -293,7 +294,7 @@ functionDeclaration
       } else {
         t = EXPR_MANAGER->mkFunctionType(sorts);
       }
-      ANTLR_INPUT->mkVar(name, t); } 
+      PARSER_STATE->mkVar(name, t); } 
   ;
               
 /**
@@ -311,7 +312,7 @@ predicateDeclaration
       } else { 
         t = EXPR_MANAGER->mkPredicateType(p_sorts);
       }
-      ANTLR_INPUT->mkVar(name, t); } 
+      PARSER_STATE->mkVar(name, t); } 
   ;
 
 sortDeclaration 
@@ -320,7 +321,7 @@ sortDeclaration
 }
   : sortName[name,CHECK_UNDECLARED]
     { Debug("parser") << "sort decl: '" << name << "'" << std::endl;
-      ANTLR_INPUT->newSort(name); }
+      PARSER_STATE->newSort(name); }
   ;
   
 /**
@@ -343,7 +344,7 @@ sortSymbol returns [CVC4::Type* t]
   std::string name;
 }
   : sortName[name,CHECK_NONE] 
-  	{ $t = ANTLR_INPUT->getSort(name); }
+  	{ $t = PARSER_STATE->getSort(name); }
   ;
 
 /**
@@ -376,7 +377,7 @@ identifier[std::string& id,
       Debug("parser") << "identifier: " << id
                       << " check? " << toString(check)
                       << " type? " << toString(type) << std::endl;
-      ANTLR_INPUT->checkDeclaration(id, check, type); }
+      PARSER_STATE->checkDeclaration(id, check, type); }
   ;
 
 /**
@@ -390,7 +391,7 @@ let_identifier[std::string& id,
     { id = AntlrInput::tokenText($LET_IDENTIFIER);
       Debug("parser") << "let_identifier: " << id
                       << " check? " << toString(check) << std::endl;
-      ANTLR_INPUT->checkDeclaration(id, check, SYM_VARIABLE); }
+      PARSER_STATE->checkDeclaration(id, check, SYM_VARIABLE); }
   ;
 
 /**
@@ -404,7 +405,7 @@ flet_identifier[std::string& id,
     { id = AntlrInput::tokenText($FLET_IDENTIFIER);
       Debug("parser") << "flet_identifier: " << id
                       << " check? " << toString(check) << std::endl;
-      ANTLR_INPUT->checkDeclaration(id, check); }
+      PARSER_STATE->checkDeclaration(id, check); }
   ;
 
 
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index 0b40698cd..768a56a9b 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -8,7 +8,7 @@ UNIT_TESTS = \
 	expr/node_manager_white \
 	expr/attribute_white \
 	expr/attribute_black \
-	parser/parser_black \
+	parser/parser_white \
 	context/context_black \
 	context/context_mm_black \
 	context/cdo_black \
diff --git a/test/unit/parser/parser_white.h b/test/unit/parser/parser_white.h
new file mode 100644
index 000000000..f4d104a93
--- /dev/null
+++ b/test/unit/parser/parser_white.h
@@ -0,0 +1,295 @@
+/*********************                                                        */
+/** parser_white.h
+ ** Original author: cconway
+ ** Major contributors: none
+ ** Minor contributors (to current version): dejan, mdeters
+ ** 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.
+ **
+ ** Black box testing of CVC4::parser::SmtParser.
+ **/
+
+#include <cxxtest/TestSuite.h>
+//#include <string>
+#include <sstream>
+
+#include "expr/expr.h"
+#include "expr/expr_manager.h"
+#include "parser/input.h"
+#include "parser/parser_state.h"
+#include "expr/command.h"
+#include "util/output.h"
+
+using namespace CVC4;
+using namespace CVC4::parser;
+using namespace std;
+
+
+/************************** CVC test inputs ********************************/
+
+const string goodCvc4Inputs[] = {
+      "", // empty string is OK
+      "ASSERT TRUE;",
+      "QUERY TRUE;",
+      "CHECKSAT FALSE;",
+      "a, b : BOOLEAN;",
+      "a, b : BOOLEAN; QUERY (a => b) AND a => b;",
+      "T, U : TYPE; f : T -> U; x : T; CHECKSAT f(x) = x;",
+      "T : TYPE; x, y : T; a : BOOLEAN; QUERY (IF a THEN x ELSE y ENDIF) = x;",
+      "%% nothing but a comment",
+      "% a comment\nASSERT TRUE; %a command\n% another comment",
+  };
+
+const int numGoodCvc4Inputs = sizeof(goodCvc4Inputs) / sizeof(string);
+
+
+/* The following expressions are valid after setupContext. */
+const string goodCvc4Exprs[] = {
+    "a AND b",
+    "a AND b OR c",
+    "(a => b) AND a => b",
+    "(a <=> b) AND (NOT a)",
+    "(a XOR b) <=> (a OR b) AND (NOT (a AND b))"
+};
+
+const int numGoodCvc4Exprs = sizeof(goodCvc4Exprs) / sizeof(string);
+
+const string badCvc4Inputs[] = {
+      ";", // no command
+      "ASSERT;", // no args
+      "QUERY",
+      "CHECKSAT",
+      "a, b : boolean;", // lowercase boolean isn't a type
+      "0x : INT;", // 0x isn't an identifier
+      "a, b : BOOLEAN\nQUERY (a => b) AND a => b;", // no semicolon after decl
+      "a : BOOLEAN; a: BOOLEAN;" // double decl
+      "a, b: BOOLEAN; QUERY a(b);" // non-function used as function
+  };
+
+const int numBadCvc4Inputs = sizeof(badCvc4Inputs) / sizeof(string);
+
+/* The following expressions are invalid even after setupContext. */
+const string badCvc4Exprs[] = {
+    "a AND", // wrong arity
+    "AND(a,b)", // not infix
+    "(OR (AND a b) c)", // not infix
+    "a IMPLIES b", // should be =>
+    "a NOT b", // wrong arity, not infix
+    "a and b" // wrong case
+};
+
+const int numBadCvc4Exprs = sizeof(badCvc4Exprs) / sizeof(string);
+
+/************************** SMT test inputs ********************************/
+
+const string goodSmtInputs[] = {
+    "", // empty string is OK
+    "(benchmark foo :assumption true)",
+    "(benchmark bar :formula true)",
+    "(benchmark qux :formula false)",
+    "(benchmark baz :extrapreds ( (a) (b) ) )",
+    "(benchmark zab :extrapreds ( (a) (b) ) :formula (implies (and (implies a b) a) b))",
+    "(benchmark zub :extrasorts (a) :extrafuns ( (f a a) (x a) )  :formula (= (f x) x))",
+    "(benchmark fuz :extrasorts (a) :extrafuns ((x a) (y a)) :formula (= (ite true x y) x))",
+    ";; nothing but a comment",
+    "; a comment\n(benchmark foo ; hello\n  :formula true; goodbye\n)"
+  };
+
+const int numGoodSmtInputs = sizeof(goodSmtInputs) / sizeof(string);
+
+/* The following expressions are valid after setupContext. */
+const string goodSmtExprs[] = {
+    "(and a b)",
+    "(or (and a b) c)",
+    "(implies (and (implies a b) a) b)",
+    "(and (iff a b) (not a))",
+    "(iff (xor a b) (and (or a b) (not (and a b))))",
+    "(ite a (f x) y)",
+    "(if_then_else a (f x) y)"
+};
+
+const int numGoodSmtExprs = sizeof(goodSmtExprs) / sizeof(string);
+
+const string badSmtInputs[] = {
+    "(benchmark foo)", // empty benchmark is not OK
+    "(benchmark bar :assumption)", // no args
+    "(benchmark bar :formula)",
+    "(benchmark baz :extrapreds ( (a) (a) ) )", // double decl
+    "(benchmark zub :extrasorts (a) :extrapreds (p a))" // (p a) needs parens
+  };
+
+const int numBadSmtInputs = sizeof(badSmtInputs) / sizeof(string);
+
+/* The following expressions are invalid even after setupContext. */
+const string badSmtExprs[] = {
+    "(and)", // wrong arity
+    "(and a b", // no closing paren
+    "(a and b)", // infix
+    "(OR (AND a b) c)", // wrong case
+    "(a IMPLIES b)", // infix AND wrong case
+    "(not a b)", // wrong arity
+    "not a", // needs parens
+    "(ite a x)", // wrong arity
+    "(a b)" // using non-function as function
+};
+
+const int numBadSmtExprs = sizeof(badSmtExprs) / sizeof(string);
+
+class ParserBlack : public CxxTest::TestSuite {
+  ExprManager *d_exprManager;
+
+  /* Set up declaration context for expr inputs */
+
+  void setupContext(ParserState* parserState) {
+    /* a, b, c: BOOLEAN */
+    parserState->mkVar("a",(Type*)d_exprManager->booleanType());
+    parserState->mkVar("b",(Type*)d_exprManager->booleanType());
+    parserState->mkVar("c",(Type*)d_exprManager->booleanType());
+    /* t, u, v: TYPE */
+    Type *t = parserState->newSort("t");
+    Type *u = parserState->newSort("u");
+    Type *v = parserState->newSort("v");
+    /* f : t->u; g: u->v; h: v->t; */
+    parserState->mkVar("f", (Type*)d_exprManager->mkFunctionType(t,u));
+    parserState->mkVar("g", (Type*)d_exprManager->mkFunctionType(u,v));
+    parserState->mkVar("h", (Type*)d_exprManager->mkFunctionType(v,t));
+    /* x:t; y:u; z:v; */
+    parserState->mkVar("x",t);
+    parserState->mkVar("y",u);
+    parserState->mkVar("z",v);
+  }
+
+  void tryGoodInputs(InputLanguage d_lang, const string goodInputs[], int numInputs) {
+    for(int i = 0; i < numInputs; ++i) {
+      try {
+//         Debug.on("parser");
+//         Debug.on("parser-extra");
+         Debug("test") << "Testing good input: '" << goodInputs[i] << "'\n";
+//        istringstream stream(goodInputs[i]);
+        Input* parser = Input::newStringInput(d_exprManager, d_lang, goodInputs[i], "test");
+        TS_ASSERT( !parser->done() );
+        Command* cmd;
+        while((cmd = parser->parseNextCommand())) {
+          // cout << "Parsed command: " << (*cmd) << endl;
+        }
+        TS_ASSERT( parser->parseNextCommand() == NULL );
+        TS_ASSERT( parser->done() );
+        delete parser;
+//        Debug.off("parser");
+//        Debug.off("parser-extra");
+      } catch (Exception& e) {
+        cout << "\nGood input failed:\n" << goodInputs[i] << endl
+             << e << endl;
+//        Debug.off("parser-extra");
+        throw;
+      }
+    }
+  }
+
+  void tryBadInputs(InputLanguage d_lang, const string badInputs[], int numInputs) {
+    for(int i = 0; i < numInputs; ++i) {
+//      cout << "Testing bad input: '" << badInputs[i] << "'\n";
+//      Debug.on("parser");
+      Input* parser = Input::newStringInput(d_exprManager, d_lang, badInputs[i], "test");
+      TS_ASSERT_THROWS
+        ( while(parser->parseNextCommand());
+          cout << "\nBad input succeeded:\n" << badInputs[i] << endl;,
+          ParserException );
+//      Debug.off("parser");
+      delete parser;
+    }
+  }
+
+  void tryGoodExprs(InputLanguage d_lang, const string goodBooleanExprs[], int numExprs) {
+    // cout << "Using context: " << context << endl;
+//    Debug.on("parser");
+//    Debug.on("parser-extra");
+    for(int i = 0; i < numExprs; ++i) {
+      try {
+        // cout << "Testing good expr: '" << goodBooleanExprs[i] << "'\n";
+        // Debug.on("parser");
+//        istringstream stream(context + goodBooleanExprs[i]);
+        Input* input = Input::newStringInput(d_exprManager, d_lang,
+                                              goodBooleanExprs[i], "test");
+        TS_ASSERT( !input->done() );
+        setupContext(input->getParserState());
+        TS_ASSERT( !input->done() );
+        Expr e = input->parseNextExpression();
+        TS_ASSERT( !e.isNull() );
+        e = input->parseNextExpression();
+        TS_ASSERT( input->done() );
+        TS_ASSERT( e.isNull() );
+        delete input;
+      } catch (Exception& e) {
+        cout << "\nGood expr failed:\n" << goodBooleanExprs[i] << endl;
+        cout << e;
+        throw e;
+      }
+    }
+  }
+
+  void tryBadExprs(InputLanguage d_lang, const string badBooleanExprs[], int numExprs) {
+    //Debug.on("parser");
+    for(int i = 0; i < numExprs; ++i) {
+      // cout << "Testing bad expr: '" << badBooleanExprs[i] << "'\n";
+//      istringstream stream(context + badBooleanExprs[i]);
+      Input* input = Input::newStringInput(d_exprManager, d_lang,
+                                           badBooleanExprs[i], "test");
+
+      TS_ASSERT( !input->done() );
+      setupContext(input->getParserState());
+      TS_ASSERT( !input->done() );
+      TS_ASSERT_THROWS
+        ( input->parseNextExpression();
+          cout << "\nBad expr succeeded: " << badBooleanExprs[i] << endl;,
+          ParserException );
+      delete input;
+    }
+    //Debug.off("parser");
+  }
+
+public:
+  void setUp() {
+    d_exprManager = new ExprManager();
+  }
+
+  void tearDown() {
+    delete d_exprManager;
+  }
+
+  void testGoodCvc4Inputs() {
+    tryGoodInputs(LANG_CVC4,goodCvc4Inputs,numGoodCvc4Inputs);
+  }
+
+  void testBadCvc4Inputs() {
+    tryBadInputs(LANG_CVC4,badCvc4Inputs,numBadCvc4Inputs);
+  }
+
+  void testGoodCvc4Exprs() {
+    tryGoodExprs(LANG_CVC4,goodCvc4Exprs,numGoodCvc4Exprs);
+  }
+
+  void testBadCvc4Exprs() {
+    tryBadExprs(LANG_CVC4,badCvc4Exprs,numBadCvc4Exprs);
+  }
+
+  void testGoodSmtInputs() {
+    tryGoodInputs(LANG_SMTLIB,goodSmtInputs,numGoodSmtInputs);
+  }
+
+  void testBadSmtInputs() {
+    tryBadInputs(LANG_SMTLIB,badSmtInputs,numBadSmtInputs);
+  }
+
+  void testGoodSmtExprs() {
+    tryGoodExprs(LANG_SMTLIB,goodSmtExprs,numGoodSmtExprs);
+  }
+
+  void testBadSmtExprs() {
+    tryBadExprs(LANG_SMTLIB,badSmtExprs,numBadSmtExprs);
+  }
+};