Merging from branches/antlr3 (r246:354)

7 files changed, 643 insertions, 561 deletions

diff --git a/src/parser/cvc/.gitignore b/src/parser/cvc/.gitignore
new file mode 100644
index 000000000..7fd0cf319
--- /dev/null
+++ b/src/parser/cvc/.gitignore
@@ -0,0 +1,4 @@
+/.deps
+/stamp-generated
+/generated
+/Makefile.in
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
new file mode 100644
index 000000000..a9dff77bf
--- /dev/null
+++ b/src/parser/cvc/Cvc.g
@@ -0,0 +1,496 @@
+/* *******************                                                        */
+/*  Cvc.g
+ ** 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 for CVC-LIB input language.
+ **/
+
+grammar Cvc;
+
+options {
+  language = 'C';                  // C output for antlr
+//  defaultErrorHandler = false;      // Skip the default error handling, just break with exceptions
+  k = 2;
+}
+
+@header {
+/**
+ ** 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.
+ **/
+}
+
+@lexer::includes {
+/* This improves performance by ~10 percent on big inputs.
+ * This option is only valid if we know the input is ASCII (or some 8-bit encoding).
+ * If we know the input is UTF-16, we can use ANTLR3_INLINE_INPUT_UTF16.
+ * Otherwise, we have to let the lexer detect the encoding at runtime.
+ */
+#define ANTLR3_INLINE_INPUT_ASCII
+}
+
+@parser::includes {
+#include "expr/command.h"
+#include "parser/input.h"
+
+namespace CVC4 {
+  class Expr;
+namespace parser {
+  class CvcInput;
+}
+}
+
+extern
+void SetCvcInput(CVC4::parser::CvcInput* input);
+
+}
+
+@parser::postinclude {
+#include "expr/expr.h"
+#include "expr/kind.h"
+#include "expr/type.h"
+#include "parser/input.h"
+#include "parser/cvc/cvc_input.h"
+#include "util/output.h"
+#include <vector>
+
+using namespace CVC4;
+using namespace CVC4::parser;
+}
+
+@members {
+static CVC4::parser::CvcInput *input;
+
+extern
+void SetCvcInput(CVC4::parser::CvcInput* _input) {
+  input = _input;
+}
+}
+
+/**
+ * Parses an expression.
+ * @return the parsed expression
+ */
+parseExpr returns [CVC4::Expr expr]
+  : formula[expr]
+  | EOF
+  ;
+
+/**
+ * Parses a command (the whole benchmark)
+ * @return the command of the benchmark
+ */
+parseCommand returns [CVC4::Command* cmd]
+  : c = command { $cmd = c; }
+  ;
+
+/**
+ * Matches a command of the input. If a declaration, it will return an empty
+ * command.
+ */
+command returns [CVC4::Command* cmd = 0]
+@init {
+  Expr f;
+  Debug("parser-extra") << "command: " << AntlrInput::tokenText(LT(1)) << std::endl;
+}
+  : ASSERT_TOK formula[f] SEMICOLON { cmd = new AssertCommand(f);   }
+  | QUERY_TOK formula[f] SEMICOLON { cmd = new QueryCommand(f);    }
+  | CHECKSAT_TOK formula[f] SEMICOLON { cmd = new CheckSatCommand(f); }
+  | CHECKSAT_TOK SEMICOLON { cmd = new CheckSatCommand(input->getTrueExpr()); }
+  | PUSH_TOK SEMICOLON { cmd = new PushCommand(); }
+  | POP_TOK SEMICOLON { cmd = new PopCommand(); }
+  | declaration[cmd]
+  | EOF
+  ;
+
+/**
+ * Match a declaration
+ */
+
+declaration[CVC4::Command*& cmd]
+@init {
+  std::vector<std::string> ids;
+  Type* t;
+  Debug("parser-extra") << "declaration: " << AntlrInput::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
+    { cmd = new DeclarationCommand(ids,t); }
+  ;
+
+/** 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;
+}
+  : /* A sort declaration (e.g., "T : TYPE") */
+    TYPE_TOK { input->newSorts(idList); t = input->kindType(); }
+  | /* A variable declaration */
+    type[t] { input->mkVars(idList,t); }
+  ;
+
+/**
+ * Match the type in a declaration and do the declaration binding.
+ * TODO: Actually parse sorts into Type objects.
+ */
+type[CVC4::Type*& t]
+@init {
+  std::vector<Type*> typeList;
+  Debug("parser-extra") << "type: " << AntlrInput::tokenText(LT(1)) << std::endl;
+}
+  : /* Simple type */
+    baseType[t]
+  | /* Single-parameter function type */
+    baseType[t] { typeList.push_back(t); }
+    ARROW_TOK baseType[t] 
+    { t = input->functionType(typeList,t); }
+  | /* Multi-parameter function type */
+    LPAREN baseType[t]
+    { typeList.push_back(t); }
+    (COMMA baseType[t] { typeList.push_back(t); } )+
+    RPAREN ARROW_TOK baseType[t]
+    { t = input->functionType(typeList,t); }
+  ;
+
+/**
+ * Matches a list of identifiers separated by a comma and puts them in the
+ * given list.
+ * @param idList the list to fill with identifiers.
+ * @param check what kinds of check to perform on the symbols
+ */
+identifierList[std::vector<std::string>& idList,
+               CVC4::parser::DeclarationCheck check,
+               CVC4::parser::SymbolType type]
+@init {
+  std::string id;
+}
+  : identifier[id,check,type] { idList.push_back(id); }
+    (COMMA identifier[id,check,type] { idList.push_back(id); })*
+  ;
+
+
+/**
+ * Matches an identifier and returns a string.
+ */
+identifier[std::string& id,
+           CVC4::parser::DeclarationCheck check,
+           CVC4::parser::SymbolType type]
+  : IDENTIFIER
+    { id = AntlrInput::tokenText($IDENTIFIER);
+      input->checkDeclaration(id, check, type); }
+  ;
+
+/**
+ * Matches a type.
+ * TODO: parse more types
+ */
+baseType[CVC4::Type*& t]
+@init {
+  std::string id;
+  Debug("parser-extra") << "base type: " << AntlrInput::tokenText(LT(1)) << std::endl;
+}
+  : BOOLEAN_TOK { t = input->booleanType(); }
+  | typeSymbol[t]
+  ;
+
+/**
+ * Matches a type identifier
+ */
+typeSymbol[CVC4::Type*& t]
+@init {
+  std::string id;
+  Debug("parser-extra") << "type symbol: " << AntlrInput::tokenText(LT(1)) << std::endl;
+}
+  : identifier[id,CHECK_DECLARED,SYM_SORT]
+    { t = input->getSort(id); }
+  ;
+
+/**
+ * Matches a CVC4 formula.
+ * @return the expression representing the formula
+ */
+formula[CVC4::Expr& formula]
+@init {
+  Debug("parser-extra") << "formula: " << AntlrInput::tokenText(LT(1)) << std::endl;
+}
+  :  iffFormula[formula]
+  ;
+
+/**
+ * Matches a comma-separated list of formulas
+ */
+formulaList[std::vector<CVC4::Expr>& formulas]
+@init {
+  Expr f;
+}
+  : formula[f] { formulas.push_back(f); }
+    ( COMMA formula[f]
+      { formulas.push_back(f); }
+    )*
+  ;
+
+/**
+ * Matches a Boolean IFF formula (right-associative)
+ */
+iffFormula[CVC4::Expr& f]
+@init {
+  Expr e;
+  Debug("parser-extra") << "<=> formula: " << AntlrInput::tokenText(LT(1)) << std::endl;
+}
+  : impliesFormula[f]
+    ( IFF_TOK 
+    	iffFormula[e]
+        { f = input->mkExpr(CVC4::kind::IFF, f, e); }
+    )?
+  ;
+
+/**
+ * Matches a Boolean IMPLIES formula (right-associative)
+ */
+impliesFormula[CVC4::Expr& f]
+@init {
+  Expr e;
+  Debug("parser-extra") << "=> Formula: " << AntlrInput::tokenText(LT(1)) << std::endl;
+}
+  : orFormula[f]
+    ( IMPLIES_TOK impliesFormula[e]
+        { f = input->mkExpr(CVC4::kind::IMPLIES, f, e); }
+    )?
+  ;
+
+/**
+ * Matches a Boolean OR formula (left-associative)
+ */
+orFormula[CVC4::Expr& f]
+@init {
+  std::vector<Expr> exprs;
+  Debug("parser-extra") << "OR Formula: " << AntlrInput::tokenText(LT(1)) << std::endl;
+}
+  : xorFormula[f]
+      ( OR_TOK  { exprs.push_back(f); }
+        xorFormula[f] { exprs.push_back(f); } )*
+    {
+      if( exprs.size() > 0 ) {
+        f = input->mkExpr(CVC4::kind::OR, exprs);
+      }
+    }
+  ;
+
+/**
+ * Matches a Boolean XOR formula (left-associative)
+ */
+xorFormula[CVC4::Expr& f]
+@init {
+  Expr e;
+  Debug("parser-extra") << "XOR formula: " << AntlrInput::tokenText(LT(1)) << std::endl;
+}
+  : andFormula[f]
+    ( XOR_TOK andFormula[e]
+      { f = input->mkExpr(CVC4::kind::XOR,f, e); }
+    )*
+  ;
+
+/**
+ * Matches a Boolean AND formula (left-associative)
+ */
+andFormula[CVC4::Expr& f]
+@init {
+  std::vector<Expr> exprs;
+  Debug("parser-extra") << "AND Formula: " << AntlrInput::tokenText(LT(1)) << std::endl;
+}
+  : notFormula[f] 
+    ( AND_TOK { exprs.push_back(f); }
+      notFormula[f] { exprs.push_back(f); } )*
+    {
+      if( exprs.size() > 0 ) {
+        f = input->mkExpr(CVC4::kind::AND, exprs);
+      }
+    }
+  ;
+
+/**
+ * Parses a NOT formula.
+ * @return the expression representing the formula
+ */
+notFormula[CVC4::Expr& f]
+@init {
+  Debug("parser-extra") << "NOT formula: " << AntlrInput::tokenText(LT(1)) << std::endl;
+}
+  : /* negation */
+    NOT_TOK notFormula[f]
+    { f = input->mkExpr(CVC4::kind::NOT, f); }
+  | /* a boolean atom */
+    predFormula[f]
+  ;
+
+predFormula[CVC4::Expr& f]
+@init {
+  Expr e;
+  Debug("parser-extra") << "predicate formula: " << AntlrInput::tokenText(LT(1)) << std::endl;
+}
+  : term[f]
+    (EQUAL_TOK term[e]
+      { f = input->mkExpr(CVC4::kind::EQUAL, f, e); }
+    )?
+  ; // TODO: lt, gt, etc.
+
+/**
+ * Parses a term.
+ */
+term[CVC4::Expr& f]
+@init {
+  std::string name;
+  std::vector<Expr> args;
+  Debug("parser-extra") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl;
+}
+  : /* function application */
+    // { isFunction(AntlrInput::tokenText(LT(1))) }?
+    functionSymbol[f]
+    { args.push_back( f ); }
+    LPAREN formulaList[args] RPAREN
+    // TODO: check arity
+    { f = input->mkExpr(CVC4::kind::APPLY_UF, args); }
+
+  | /* if-then-else */
+    iteTerm[f]
+
+  | /* parenthesized sub-formula */
+    LPAREN formula[f] RPAREN
+
+    /* constants */
+  | TRUE_TOK  { f = input->getTrueExpr(); }
+  | FALSE_TOK { f = input->getFalseExpr(); }
+
+  | /* variable */
+    identifier[name,CHECK_DECLARED,SYM_VARIABLE]
+    { f = input->getVariable(name); }
+  ;
+
+/**
+ * Parses an ITE term.
+ */
+iteTerm[CVC4::Expr& f]
+@init {
+  std::vector<Expr> args;
+  Debug("parser-extra") << "ite: " << AntlrInput::tokenText(LT(1)) << std::endl;
+}
+  : IF_TOK formula[f] { args.push_back(f); }
+    THEN_TOK formula[f] { args.push_back(f); }
+    iteElseTerm[f] { args.push_back(f); }
+    ENDIF_TOK
+    { f = input->mkExpr(CVC4::kind::ITE, args); }
+  ;
+
+/**
+ * Parses the else part of the ITE, i.e. ELSE f, or ELSIF b THEN f1 ...
+ */
+iteElseTerm[CVC4::Expr& f]
+@init {
+  std::vector<Expr> args;
+  Debug("parser-extra") << "else: " << AntlrInput::tokenText(LT(1)) << std::endl;
+}
+  : ELSE_TOK formula[f] 
+  | ELSEIF_TOK iteCondition = formula[f] { args.push_back(f); }
+    THEN_TOK iteThen = formula[f] { args.push_back(f); }
+    iteElse = iteElseTerm[f] { args.push_back(f); }
+    { f = input->mkExpr(CVC4::kind::ITE, args); }
+  ;
+
+/**
+ * Parses a function symbol (an identifier).
+ * @param what kind of check to perform on the id
+ * @return the predicate symol
+ */
+functionSymbol[CVC4::Expr& f]
+@init {
+  Debug("parser-extra") << "function symbol: " << AntlrInput::tokenText(LT(1)) << std::endl;
+  std::string name;
+}
+  : identifier[name,CHECK_DECLARED,SYM_FUNCTION]
+    { input->checkFunction(name);
+      f = input->getFunction(name); }
+  ;
+
+
+// Keywords
+
+AND_TOK : 'AND';
+ASSERT_TOK : 'ASSERT';
+BOOLEAN_TOK : 'BOOLEAN';
+CHECKSAT_TOK : 'CHECKSAT';
+ECHO_TOK : 'ECHO';
+ELSEIF_TOK : 'ELSIF';
+ELSE_TOK : 'ELSE';
+ENDIF_TOK : 'ENDIF';
+FALSE_TOK : 'FALSE';
+IF_TOK : 'IF';
+NOT_TOK : 'NOT';
+OR_TOK : 'OR';
+POPTO_TOK : 'POPTO';
+POP_TOK : 'POP';
+PRINT_TOK : 'PRINT';
+PUSH_TOK : 'PUSH';
+QUERY_TOK : 'QUERY';
+THEN_TOK : 'THEN';
+TRUE_TOK : 'TRUE';
+TYPE_TOK : 'TYPE';
+XOR_TOK : 'XOR';
+
+// Symbols
+
+COLON : ':';
+COMMA : ',';
+LPAREN : '(';
+RPAREN : ')';
+SEMICOLON : ';';
+
+// Operators
+
+IMPLIES_TOK : '=>';
+IFF_TOK     : '<=>';
+ARROW_TOK : '->';
+EQUAL_TOK   : '=';
+
+/**
+ * Matches an identifier from the input. An identifier is a sequence of letters,
+ * digits and "_", "'", "." symbols, starting with a letter.
+ */
+IDENTIFIER : ALPHA (ALPHA | DIGIT | '_' | '\'' | '.')*;
+
+/**
+ * Matches a numeral from the input (non-empty sequence of digits).
+ */
+NUMERAL: (DIGIT)+;
+
+/**
+ * Matches any letter ('a'-'z' and 'A'-'Z').
+ */
+fragment ALPHA : 'a'..'z' | 'A'..'Z';
+
+/**
+ * Matches the digits (0-9)
+ */
+fragment DIGIT : '0'..'9';
+
+/**
+ * Matches and skips whitespace in the input and ignores it.
+ */
+WHITESPACE : (' ' | '\t' | '\f' | '\r' | '\n') { $channel = HIDDEN;; };
+
+/**
+ * Matches the comments and ignores them
+ */
+COMMENT : '%' (~('\n' | '\r'))* { $channel = HIDDEN;; };
+
diff --git a/src/parser/cvc/Makefile.am b/src/parser/cvc/Makefile.am
index c1b5f752e..f02c9345c 100644
--- a/src/parser/cvc/Makefile.am
+++ b/src/parser/cvc/Makefile.am
@@ -1,30 +1,30 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4PARSERLIB \
-	-I@srcdir@/../../include -I@srcdir@/../..
+	-I@srcdir@/../../include -I@srcdir@/../.. $(ANTLR_INCLUDES)
 AM_CXXFLAGS = -Wall -fvisibility=hidden
+# Compile generated C files using C++ compiler
+CC=$(CXX)
 
 noinst_LTLIBRARIES = libparsercvc.la
 
 ANTLR_TOKEN_STUFF = \
-	@srcdir@/generated/CvcVocabularyTokenTypes.hpp \
-	@srcdir@/generated/CvcVocabularyTokenTypes.txt \
-	@srcdir@/generated/AntlrCvcParserTokenTypes.hpp \
-	@srcdir@/generated/AntlrCvcParserTokenTypes.txt
+	@srcdir@/generated/Cvc.tokens
 ANTLR_LEXER_STUFF = \
-	@srcdir@/generated/AntlrCvcLexer.hpp \
-	@srcdir@/generated/AntlrCvcLexer.cpp \
-	$(ANTLR_TOKEN_STUFF)
+    @srcdir@/generated/CvcLexer.h \
+    @srcdir@/generated/CvcLexer.c \
+    $(ANTLR_TOKEN_STUFF)
 ANTLR_PARSER_STUFF = \
-	@srcdir@/generated/AntlrCvcParser.hpp \
-	@srcdir@/generated/AntlrCvcParser.cpp
+    @srcdir@/generated/CvcParser.h \
+    @srcdir@/generated/CvcParser.c
 ANTLR_STUFF = \
-	$(ANTLR_LEXER_STUFF) \
-	$(ANTLR_PARSER_STUFF)
+    $(ANTLR_LEXER_STUFF) \
+    $(ANTLR_PARSER_STUFF)
 
 libparsercvc_la_SOURCES = \
-	cvc_lexer.g \
-	cvc_parser.g \
-	$(ANTLR_STUFF)
+    Cvc.g \
+    cvc_input.h \
+    cvc_input.cpp \
+    $(ANTLR_STUFF)
 
 BUILT_SOURCES = $(ANTLR_STUFF)
 dist-hook: $(ANTLR_STUFF)
@@ -36,16 +36,14 @@ maintainer-clean-local:
 @srcdir@/stamp-generated:
 	mkdir -p @srcdir@/generated
 	touch @srcdir@/stamp-generated
+
 # antlr doesn't overwrite output files, it just leaves them.  So we have to delete them first.
-@srcdir@/generated/AntlrCvcLexer.hpp: cvc_lexer.g @srcdir@/stamp-generated
-	$(AM_V_at)-rm -f $(ANTLR_LEXER_STUFF)
-	$(AM_V_GEN)$(ANTLR) -o "@srcdir@/generated" "@srcdir@/cvc_lexer.g"
-@srcdir@/generated/AntlrCvcLexer.cpp $(ANTLR_TOKEN_STUFF): @srcdir@/generated/AntlrCvcLexer.hpp
-# doesn't actually depend on the lexer, but if we're doing parallel
+@srcdir@/generated/CvcLexer.h: Cvc.g @srcdir@/stamp-generated
+	-rm -f $(ANTLR_STUFF)
+	$(ANTLR) -o "@srcdir@/generated" "@srcdir@/Cvc.g"
+
+# These don't actually depend on CvcLexer.h, but if we're doing parallel
 # make and the lexer needs to be rebuilt, we have to keep the rules
 # from running in parallel (since the token files will be deleted &
 # recreated)
-@srcdir@/generated/AntlrCvcParser.hpp: cvc_parser.g cvc_lexer.g $(ANTLR_TOKEN_STUFF) @srcdir@/stamp-generated
-	$(AM_V_at)-rm -f $(ANTLR_PARSER_STUFF)
-	$(AM_V_GEN)$(ANTLR) -o "@srcdir@/generated" "@srcdir@/cvc_parser.g"
-@srcdir@/generated/AntlrCvcParser.cpp: @srcdir@/generated/AntlrCvcParser.hpp
+@srcdir@/generated/CvcLexer.c @srcdir@/generated/CvcParser.h @srcdir@/generated/CvcParser.c $(ANTLR_TOKEN_STUFF): @srcdir@/generated/CvcLexer.h
diff --git a/src/parser/cvc/cvc_input.cpp b/src/parser/cvc/cvc_input.cpp
new file mode 100644
index 000000000..9de608aae
--- /dev/null
+++ b/src/parser/cvc/cvc_input.cpp
@@ -0,0 +1,73 @@
+/*
+ * cvc_parser.cpp
+ *
+ *  Created on: Mar 5, 2010
+ *      Author: chris
+ */
+
+#include <antlr3.h>
+
+#include "expr/expr_manager.h"
+#include "parser/parser_exception.h"
+#include "parser/cvc/cvc_input.h"
+#include "parser/cvc/generated/CvcLexer.h"
+#include "parser/cvc/generated/CvcParser.h"
+
+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();
+  AlwaysAssert( input != NULL );
+
+  d_pCvcLexer = CvcLexerNew(input);
+  if( d_pCvcLexer == NULL ) {
+    throw ParserException("Failed to create CVC lexer.");
+  }
+
+  setLexer( d_pCvcLexer->pLexer );
+
+  pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream();
+  AlwaysAssert( tokenStream != NULL );
+
+  d_pCvcParser = CvcParserNew(tokenStream);
+  if( d_pCvcParser == NULL ) {
+    throw ParserException("Failed to create CVC parser.");
+  }
+
+  setParser(d_pCvcParser->pParser);
+  SetCvcInput(this);
+}
+
+
+CvcInput::~CvcInput() {
+  d_pCvcLexer->free(d_pCvcLexer);
+  d_pCvcParser->free(d_pCvcParser);
+}
+
+Command* CvcInput::doParseCommand() throw (ParserException) {
+  return d_pCvcParser->parseCommand(d_pCvcParser);
+}
+
+Expr CvcInput::doParseExpr() throw (ParserException) {
+  return d_pCvcParser->parseExpr(d_pCvcParser);
+}
+
+pANTLR3_LEXER CvcInput::getLexer() {
+  return d_pCvcLexer->pLexer;
+}
+
+} // namespace parser
+
+} // namespace CVC4
diff --git a/src/parser/cvc/cvc_input.h b/src/parser/cvc/cvc_input.h
new file mode 100644
index 000000000..659123401
--- /dev/null
+++ b/src/parser/cvc/cvc_input.h
@@ -0,0 +1,48 @@
+/*
+ * cvc_parser.h
+ *
+ *  Created on: Mar 5, 2010
+ *      Author: chris
+ */
+
+#ifndef CVC_PARSER_H_
+#define CVC_PARSER_H_
+
+#include "parser/antlr_input.h"
+#include "parser/cvc/generated/CvcLexer.h"
+#include "parser/cvc/generated/CvcParser.h"
+
+// extern void CvcParserSetAntlrParser(CVC4::parser::AntlrParser* newAntlrParser);
+
+namespace CVC4 {
+
+class Command;
+class Expr;
+class ExprManager;
+
+namespace parser {
+
+class CvcInput : public AntlrInput {
+public:
+  CvcInput(ExprManager* exprManager, const std::string& filename, bool useMmap);
+  CvcInput(ExprManager* exprManager, const std::string& input, const std::string& name);
+  ~CvcInput();
+
+protected:
+  Command* doParseCommand() throw(ParserException);
+  Expr doParseExpr() throw(ParserException);
+  pANTLR3_LEXER getLexer();
+  pANTLR3_LEXER createLexer(pANTLR3_INPUT_STREAM input);
+  pANTLR3_PARSER createParser(pANTLR3_COMMON_TOKEN_STREAM tokenStream);
+
+private:
+  void init();
+  pCvcLexer d_pCvcLexer;
+  pCvcParser d_pCvcParser;
+}; // class CvcInput
+
+} // namespace parser
+
+} // namespace CVC4
+
+#endif /* CVC_PARSER_H_ */
diff --git a/src/parser/cvc/cvc_lexer.g b/src/parser/cvc/cvc_lexer.g
deleted file mode 100644
index b5bf90015..000000000
--- a/src/parser/cvc/cvc_lexer.g
+++ /dev/null
@@ -1,151 +0,0 @@
-/* *******************                                                        */
-/*  cvc_lexer.g
- ** Original author: dejan
- ** Major contributors: mdeters
- ** Minor contributors (to current version): cconway
- ** 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.
- **
- ** Lexer for CVC presentation language.
- **/
-
-options {
-  language = "Cpp";            // C++ output for antlr
-  namespaceStd  = "std";       // Cosmetic option to get rid of long defines in generated code
-  namespaceAntlr = "antlr";    // Cosmetic option to get rid of long defines in generated code
-  namespace = "CVC4::parser";  // Wrap everything in the smtparser namespace
-}
-
-/**
- * AntlrCvcLexer class is a stream tokenizer (lexer) for the CVC language.
- */
-class AntlrCvcLexer extends Lexer;
-
-options {
-  exportVocab = CvcVocabulary;  // Name of the shared token vocabulary
-  testLiterals = false;         // Do not check for literals by default
-  defaultErrorHandler = false;  // Skip the defaul error handling, just break with exceptions
-  k = 2;
-}
-
-/*
- * The tokens that might match with the identifiers go here. Otherwise define
- * them below.
- */
-tokens {
-  // Types
-  BOOLEAN       = "BOOLEAN";
-  TYPE          = "TYPE";
-  // Boolean oparators
-  AND           = "AND";
-  IF            = "IF";
-  THEN          = "THEN";
-  ELSE          = "ELSE";
-  ELSEIF        = "ELSIF";
-  ENDIF         = "ENDIF";
-  NOT           = "NOT";
-  OR            = "OR";
-  TRUE          = "TRUE";
-  FALSE         = "FALSE";
-  XOR           = "XOR";
-  // Commands
-  ASSERT        = "ASSERT";
-  QUERY         = "QUERY";
-  CHECKSAT      = "CHECKSAT";
-  PRINT         = "PRINT";
-  ECHO          = "ECHO";
-
-  PUSH          = "PUSH";
-  POP           = "POP";
-  POPTO         = "POPTO";
-}
-
-// Operators
-COMMA   : ',';
-IMPLIES : "=>";
-IFF     : "<=>";
-RIGHT_ARROW : "->";
-EQUAL   : "=";
-
-/**
- * Matches any letter ('a'-'z' and 'A'-'Z').
- */
-protected
-ALPHA options { paraphrase = "a letter"; }
-  : 'a'..'z'
-  | 'A'..'Z'
-  ;
-
-/**
- * Matches the digits (0-9)
- */
-protected
-DIGIT options { paraphrase = "a digit"; }
-  : '0'..'9'
-  ;
-
-/**
- * Matches the ':'
- */
-COLON options { paraphrase = "a colon"; }
-  : ':'
-  ;
-
-/**
- * Matches the 'l'
- */
-SEMICOLON options { paraphrase = "a semicolon"; }
-  : ';'
-  ;
-
-/**
- * Matches an identifier from the input. An identifier is a sequence of letters,
- * digits and "_", "'", "." symbols, starting with a letter.
- */
-IDENTIFIER options { paraphrase = "an identifier"; testLiterals = true; }
-  : ALPHA (ALPHA | DIGIT | '_' | '\'' | '.')*
-  ;
-
-/**
- * Matches the left bracket ('(').
- */
-LPAREN options { paraphrase = "a left parenthesis '('"; }
-  : '(';
-
-/**
- * Matches the right bracket ('(').
- */
-RPAREN options { paraphrase = "a right parenthesis ')'"; }
-  : ')';
-
-/**
- * Matches and skips whitespace in the input and ignores it.
- */
-WHITESPACE options { paraphrase = "whitespace"; }
-  : (' ' | '\t' | '\f')              { $setType(antlr::Token::SKIP); }
-  ;
-
-/**
- * Matches and skips the newline symbols in the input.
- */
-NEWLINE options { paraphrase = "a newline"; }
-  : ('\r' '\n' | '\r' | '\n')       { $setType(antlr::Token::SKIP); newline(); }
-  ;
-
-/**
- * Matches the comments and ignores them
- */
-COMMENT options { paraphrase = "comment"; }
-  : '%' (~('\n' | '\r'))*                    { $setType(antlr::Token::SKIP); }
-  ;
-
-/**
- * Matches a numeral from the input (non-empty sequence of digits).
- */
-NUMERAL options { paraphrase = "a numeral"; }
-  : (DIGIT)+
-  ;
diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g
deleted file mode 100644
index acf0394d0..000000000
--- a/src/parser/cvc/cvc_parser.g
+++ /dev/null
@@ -1,386 +0,0 @@
-/* *******************                                                        */
-/*  cvc_parser.g
- ** Original author: dejan
- ** Major contributors: cconway
- ** 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.
- **
- ** Parser for CVC presentation language.
- **/
-
-header "post_include_hpp" {
-#include "parser/antlr_parser.h"
-#include "expr/command.h"
-#include "expr/type.h"
-#include "util/output.h"
-}
-
-header "post_include_cpp" {
-#include <vector>
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::parser;
-}
-
-options {
-  language = "Cpp";                  // C++ output for antlr
-  namespaceStd = "std";              // Cosmetic option to get rid of long defines in generated code
-  namespaceAntlr = "antlr";          // Cosmetic option to get rid of long defines in generated code
-  namespace = "CVC4::parser";        // Wrap everything in the smtparser namespace
-}
-
-/**
- * AntlrCvcParser class is the parser for the files in CVC format.
- */
-class AntlrCvcParser extends Parser("AntlrParser");
-options {
-  genHashLines = true;              // Include line number information
-  importVocab = CvcVocabulary;      // Import the common vocabulary
-  defaultErrorHandler = false;      // Skip the defaul error handling, just break with exceptions
-  k = 2;
-}
-
-/**
- * Parses the next command.
- * @return command or 0 if EOF
- */
-parseCommand returns [CVC4::Command* cmd]
-  : cmd = command
-  ;
-
-/**
- * Parses the next expression.
- * @return the parsed expression (null expression if EOF)
- */
-parseExpr returns [CVC4::Expr expr]
-  : expr = formula
-  | EOF
-  ;
-
-/**
- * Matches a command of the input. If a declaration, it will return an empty
- * command.
- */
-command returns [CVC4::Command* cmd = 0]
-{
-  Expr f;
-  Debug("parser") << "command: " << LT(1)->getText() << endl;
-}
-  : ASSERT   f = formula  SEMICOLON { cmd = new AssertCommand(f);   }
-  | QUERY    f = formula  SEMICOLON { cmd = new QueryCommand(f);    }
-  | CHECKSAT f = formula  SEMICOLON { cmd = new CheckSatCommand(f); }
-  | CHECKSAT              SEMICOLON { cmd = new CheckSatCommand(getTrueExpr()); }
-  | PUSH                  SEMICOLON { cmd = new PushCommand(); }
-  | POP                   SEMICOLON { cmd = new PopCommand(); }
-  | cmd = declaration
-  | EOF
-  ;
-
-/**
- * Match a declaration
- */
-
-declaration returns [CVC4::DeclarationCommand* cmd]
-{
-  vector<string> ids;
-  Type* t;
-  Debug("parser") << "declaration: " << LT(1)->getText() << endl;
-}
-  : identifierList[ids, CHECK_UNDECLARED] COLON t = declType[ids] SEMICOLON
-    { cmd = new DeclarationCommand(ids,t); }
-  ;
-
-/** Match the right-hand side of a declaration. Returns the type. */
-declType[std::vector<std::string>& idList] returns [CVC4::Type* t]
-{
-  Debug("parser") << "declType: " << LT(1)->getText() << endl;
-}
-  : /* A sort declaration (e.g., "T : TYPE") */
-    TYPE { newSorts(idList); t = kindType(); }
-  | /* A variable declaration */
-    t = type { mkVars(idList,t); }
-  ;
-
-/**
- * Match the type in a declaration and do the declaration binding.
- * TODO: Actually parse sorts into Type objects.
- */
-type returns  [CVC4::Type* t]
-{
-  Type *t1, *t2;
-  Debug("parser") << "type: " << LT(1)->getText() << endl;
-}
-  : /* Simple type */
-    t = baseType
-  | /* Single-parameter function type */
-    t1 = baseType RIGHT_ARROW t2 = baseType
-    { t = functionType(t1,t2); }
-  | /* Multi-parameter function type */
-    LPAREN t1 = baseType
-    { std::vector<Type*> argTypes;
-      argTypes.push_back(t1); }
-    (COMMA t1 = baseType { argTypes.push_back(t1); } )+
-    RPAREN RIGHT_ARROW t2 = baseType
-    { t = functionType(argTypes,t2); }
-  ;
-
-/**
- * Matches a list of identifiers separated by a comma and puts them in the
- * given list.
- * @param idList the list to fill with identifiers.
- * @param check what kinds of check to perform on the symbols
- */
-identifierList[std::vector<std::string>& idList,
-               DeclarationCheck check = CHECK_NONE]
-{
-  string id;
-}
-  : id = identifier[check] { idList.push_back(id); }
-      (COMMA id = identifier[check] { idList.push_back(id); })*
-  ;
-
-
-/**
- * Matches an identifier and returns a string.
- */
-identifier[DeclarationCheck check = CHECK_NONE,
-           SymbolType type = SYM_VARIABLE]
-returns [std::string id]
-  : x:IDENTIFIER
-    { id = x->getText();
-      checkDeclaration(id, check, type); }
-  ;
-
-/**
- * Matches a type.
- * TODO: parse more types
- */
-baseType returns [CVC4::Type* t]
-{
-  std::string id;
-  Debug("parser") << "base type: " << LT(1)->getText() << endl;
-}
-  : BOOLEAN { t = booleanType(); }
-  | t = typeSymbol
-  ;
-
-/**
- * Matches a type identifier
- */
-typeSymbol returns [CVC4::Type* t]
-{
-  std::string id;
-  Debug("parser") << "type symbol: " << LT(1)->getText() << endl;
-}
-  : id = identifier[CHECK_DECLARED,SYM_SORT]
-    { t = getSort(id); }
-  ;
-
-/**
- * Matches a CVC4 formula.
- * @return the expression representing the formula
- */
-formula returns [CVC4::Expr formula]
-{
-  Debug("parser") << "formula: " << LT(1)->getText() << endl;
-}
-  :  formula = iffFormula
-  ;
-
-/**
- * Matches a comma-separated list of formulas
- */
-formulaList[std::vector<CVC4::Expr>& formulas]
-{
-  Expr f;
-}
-  : f = formula { formulas.push_back(f); }
-    ( COMMA f = formula
-      { formulas.push_back(f); }
-    )*
-  ;
-
-/**
- * Matches a Boolean IFF formula (right-associative)
- */
-iffFormula returns [CVC4::Expr f]
-{
-  Expr e;
-  Debug("parser") << "<=> formula: " << LT(1)->getText() << endl;
-}
-  : f = impliesFormula
-    ( IFF e = iffFormula
-        { f = mkExpr(CVC4::kind::IFF, f, e); }
-    )?
-  ;
-
-/**
- * Matches a Boolean IMPLIES formula (right-associative)
- */
-impliesFormula returns [CVC4::Expr f]
-{
-  Expr e;
-  Debug("parser") << "=> Formula: " << LT(1)->getText() << endl;
-}
-  : f = orFormula
-    ( IMPLIES e = impliesFormula
-        { f = mkExpr(CVC4::kind::IMPLIES, f, e); }
-    )?
-  ;
-
-/**
- * Matches a Boolean OR formula (left-associative)
- */
-orFormula returns [CVC4::Expr f]
-{
-  Expr e;
-  vector<Expr> exprs;
-  Debug("parser") << "OR Formula: " << LT(1)->getText() << endl;
-}
-  : e = xorFormula { exprs.push_back(e); }
-      ( OR e = xorFormula { exprs.push_back(e); } )*
-    {
-      f = (exprs.size() > 1 ? mkExpr(CVC4::kind::OR, exprs) : exprs[0]);
-    }
-  ;
-
-/**
- * Matches a Boolean XOR formula (left-associative)
- */
-xorFormula returns [CVC4::Expr f]
-{
-  Expr e;
-  Debug("parser") << "XOR formula: " << LT(1)->getText() << endl;
-}
-  : f = andFormula
-    ( XOR e = andFormula
-      { f = mkExpr(CVC4::kind::XOR,f, e); }
-    )*
-  ;
-
-/**
- * Matches a Boolean AND formula (left-associative)
- */
-andFormula returns [CVC4::Expr f]
-{
-  Expr e;
-  vector<Expr> exprs;
-  Debug("parser") << "AND Formula: " << LT(1)->getText() << endl;
-}
-  : e = notFormula { exprs.push_back(e); }
-    ( AND e = notFormula { exprs.push_back(e); } )*
-    {
-      f = (exprs.size() > 1 ? mkExpr(CVC4::kind::AND, exprs) : exprs[0]);
-    }
-  ;
-
-/**
- * Parses a NOT formula.
- * @return the expression representing the formula
- */
-notFormula returns [CVC4::Expr f]
-{
-  Debug("parser") << "NOT formula: " << LT(1)->getText() << endl;
-}
-  : /* negation */
-    NOT f = notFormula
-    { f = mkExpr(CVC4::kind::NOT, f); }
-  | /* a boolean atom */
-    f = predFormula
-  ;
-
-predFormula returns [CVC4::Expr f]
-{
-  Debug("parser") << "predicate formula: " << LT(1)->getText() << endl;
-}
-  : { Expr e; }
-    f = term
-    (EQUAL e = term
-      { f = mkExpr(CVC4::kind::EQUAL, f, e); }
-    )?
-  ; // TODO: lt, gt, etc.
-
-/**
- * Parses a term.
- */
-term returns [CVC4::Expr t]
-{
-  std::string name;
-  Debug("parser") << "term: " << LT(1)->getText() << endl;
-}
-  : /* function application */
-    // { isFunction(LT(1)->getText()) }?
-    { Expr f;
-      std::vector<CVC4::Expr> args; }
-    f = functionSymbol[CHECK_DECLARED]
-    { args.push_back( f ); }
-
-    LPAREN formulaList[args] RPAREN
-    // TODO: check arity
-    { t = mkExpr(CVC4::kind::APPLY_UF, args); }
-
-  | /* if-then-else */
-    t = iteTerm
-
-  | /* parenthesized sub-formula */
-    LPAREN t = formula RPAREN
-
-    /* constants */
-  | TRUE  { t = getTrueExpr(); }
-  | FALSE { t = getFalseExpr(); }
-
-  | /* variable */
-    name = identifier[CHECK_DECLARED]
-    { t = getVariable(name); }
-  ;
-
-/**
- * Parses an ITE term.
- */
-iteTerm returns [CVC4::Expr t]
-{
-  Expr iteCondition, iteThen, iteElse;
-  Debug("parser") << "ite: " << LT(1)->getText() << endl;
-}
-  : IF iteCondition = formula
-    THEN iteThen = formula
-    iteElse = iteElseTerm
-    ENDIF
-    { t = mkExpr(CVC4::kind::ITE, iteCondition, iteThen, iteElse); }
-  ;
-
-/**
- * Parses the else part of the ITE, i.e. ELSE f, or ELSIF b THEN f1 ...
- */
-iteElseTerm returns [CVC4::Expr t]
-{
-  Expr iteCondition, iteThen, iteElse;
-  Debug("parser") << "else: " << LT(1)->getText() << endl;
-}
-  : ELSE t = formula
-  | ELSEIF iteCondition = formula
-    THEN iteThen = formula
-    iteElse = iteElseTerm
-    { t = mkExpr(CVC4::kind::ITE, iteCondition, iteThen, iteElse); }
-  ;
-
-/**
- * Parses a function symbol (an identifier).
- * @param what kind of check to perform on the id
- * @return the predicate symol
- */
-functionSymbol[DeclarationCheck check = CHECK_NONE] returns [CVC4::Expr f]
-{
-  Debug("parser") << "function symbol: " << LT(1)->getText() << endl;
-  std::string name;
-}
-  : name = identifier[check,SYM_FUNCTION]
-    { checkFunction(name);
-      f = getFunction(name); }
-  ;