* Rename SMT parts (printer, parser) to SMT1

* Change --lang smt to mean SMT-LIBv2
* --lang smt1 now means SMT-LIBv1

* SMT-LIBv2 parser now gives helpful error if input looks like v1
* SMT-LIBv1 parser now gives helpful error if input looks like v2
* CVC presentation language parser now gives helpful error if input
  looks like either SMT-LIB v1 or v2

* Other associated changes

(this commit was certified error- and warning-free by the test-and-commit script.)

7 files changed, 1508 insertions, 0 deletions

diff --git a/src/parser/smt1/Makefile b/src/parser/smt1/Makefile
new file mode 100644
index 000000000..7e97ed357
--- /dev/null
+++ b/src/parser/smt1/Makefile
@@ -0,0 +1,4 @@
+topdir = ../../..
+srcdir = src/parser/smt
+
+include $(topdir)/Makefile.subdir
diff --git a/src/parser/smt1/Makefile.am b/src/parser/smt1/Makefile.am
new file mode 100644
index 000000000..34b979ef9
--- /dev/null
+++ b/src/parser/smt1/Makefile.am
@@ -0,0 +1,65 @@
+AM_CPPFLAGS = \
+	-D__BUILDING_CVC4PARSERLIB \
+	-I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../.. $(ANTLR_INCLUDES)
+AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -Wno-unused-function -Wno-unused-variable
+
+# Compile generated C files using C++ compiler
+AM_CFLAGS = $(AM_CXXFLAGS)
+CC=$(CXX)
+
+ANTLR_OPTS =
+
+# hide this included makefile from automake
+@mk_include@ @srcdir@/../Makefile.antlr_tracing
+
+noinst_LTLIBRARIES = libparsersmt1.la
+
+ANTLR_TOKEN_STUFF = \
+	generated/Smt1.tokens
+ANTLR_LEXER_STUFF = \
+	generated/Smt1Lexer.h \
+	generated/Smt1Lexer.c \
+	$(ANTLR_TOKEN_STUFF)
+ANTLR_PARSER_STUFF = \
+	generated/Smt1Parser.h \
+	generated/Smt1Parser.c
+ANTLR_STUFF = \
+	$(ANTLR_LEXER_STUFF) \
+	$(ANTLR_PARSER_STUFF)
+
+libparsersmt1_la_SOURCES = \
+	Smt1.g \
+        smt1.h \
+        smt1.cpp \
+	smt1_input.h \
+	smt1_input.cpp \
+	$(ANTLR_STUFF)
+
+BUILT_SOURCES = \
+	generated/Smt1.tokens \
+	generated/Smt1Lexer.h \
+	generated/Smt1Lexer.c \
+	generated/Smt1Parser.h \
+	generated/Smt1Parser.c \
+	stamp-generated
+
+DISTCLEANFILES = $(ANTLR_STUFF)
+distclean-local:
+	-$(AM_V_at)rmdir generated
+	-$(AM_V_at)rm -f stamp-generated
+
+stamp-generated:
+	$(AM_V_at)mkdir -p generated
+	$(AM_V_at)touch stamp-generated
+
+# antlr doesn't overwrite output files, it just leaves them.  So we have to delete them first.
+generated/Smt1Lexer.h: Smt1.g stamp-generated
+	-$(AM_V_at)rm -f $(ANTLR_STUFF)
+	@if test -z "$(ANTLR)"; then echo "ERROR: antlr parser generator cannot be found, cannot generate the parser" >&2; exit 1; fi
+	$(AM_V_GEN)$(ANTLR) $(ANTLR_OPTS) -fo "generated" "@srcdir@/Smt1.g"
+
+# These don't actually depend on Smt1Lexer.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)
+generated/Smt1Lexer.c generated/Smt1Parser.h generated/Smt1Parser.c $(ANTLR_TOKEN_STUFF): generated/Smt1Lexer.h
diff --git a/src/parser/smt1/Smt1.g b/src/parser/smt1/Smt1.g
new file mode 100644
index 000000000..b228fb9ec
--- /dev/null
+++ b/src/parser/smt1/Smt1.g
@@ -0,0 +1,817 @@
+/* *******************                                                        */
+/*! \file Smt1.g
+ ** \verbatim
+ ** Original author: cconway
+ ** Major contributors: dejan, mdeters
+ ** Minor contributors (to current version): taking
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  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.\endverbatim
+ **
+ ** \brief Parser for SMT-LIB input language.
+ **
+ ** Parser for SMT-LIB input language.
+ **/
+
+grammar Smt1;
+
+options {
+  // C output for antlr
+  language = 'C';
+
+  // Skip the default error handling, just break with exceptions
+  // defaultErrorHandler = false;
+
+  // Only lookahead of <= k requested (disable for LL* parsing)
+  // Note that CVC4's BoundedTokenBuffer requires a fixed k !
+  // If you change this k, change it also in smt1_input.cpp !
+  k = 2;
+}/* options */
+
+@header {
+/**
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  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.
+ **/
+}/* @header */
+
+@lexer::includes {
+/** This suppresses warnings about the redefinition of token symbols between
+  * different parsers. The redefinitions should be harmless as long as no
+  * client: (a) #include's the lexer headers for two grammars AND (b) uses the
+  * token symbol definitions.
+  */
+#pragma GCC system_header
+
+#if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
+/* 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
+#  define ANTLR3_INLINE_INPUT_8BIT
+#endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
+
+#include "parser/antlr_tracing.h"
+}/* @lexer::includes */
+
+@parser::includes {
+
+#include <stdint.h>
+
+#include "expr/command.h"
+#include "parser/parser.h"
+#include "parser/antlr_tracing.h"
+
+namespace CVC4 {
+  class Expr;
+
+  namespace parser {
+    namespace smt1 {
+      /**
+       * Just exists to provide the uintptr_t constructor that ANTLR
+       * requires.
+       */
+      struct myExpr : public CVC4::Expr {
+        myExpr() : CVC4::Expr() {}
+        myExpr(void*) : CVC4::Expr() {}
+        myExpr(const Expr& e) : CVC4::Expr(e) {}
+        myExpr(const myExpr& e) : CVC4::Expr(e) {}
+      };/* struct myExpr */
+
+      /**
+       * Just exists to provide the uintptr_t constructor that ANTLR
+       * requires.
+       */
+      struct myType : public CVC4::Type {
+        myType() : CVC4::Type() {}
+        myType(void*) : CVC4::Type() {}
+        myType(const Type& t) : CVC4::Type(t) {}
+        myType(const myType& t) : CVC4::Type(t) {}
+      };/* struct myType */
+    }/* CVC4::parser::smt1 namespace */
+  }/* CVC4::parser namespace */
+}/* CVC4 namespace */
+
+}/* @parser::includes */
+
+@parser::postinclude {
+
+#include "expr/expr.h"
+#include "expr/kind.h"
+#include "expr/type.h"
+#include "parser/antlr_input.h"
+#include "parser/parser.h"
+#include "parser/smt1/smt1.h"
+#include "util/integer.h"
+#include "util/output.h"
+#include "util/rational.h"
+#include <vector>
+
+using namespace CVC4;
+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 ((Smt1*)PARSER->super)
+#undef EXPR_MANAGER
+#define EXPR_MANAGER PARSER_STATE->getExprManager()
+#undef MK_EXPR
+#define MK_EXPR EXPR_MANAGER->mkExpr
+#undef MK_CONST
+#define MK_CONST EXPR_MANAGER->mkConst
+
+}/* @parser::postinclude */
+
+
+/**
+ * Parses an expression.
+ * @return the parsed expression
+ */
+parseExpr returns [CVC4::parser::smt1::myExpr expr]
+  : annotatedFormula[expr]
+  | EOF
+  ;
+
+/**
+ * Parses a command (the whole benchmark)
+ * @return the command of the benchmark
+ */
+parseCommand returns [CVC4::Command* cmd = NULL]
+  : b = benchmark { $cmd = b; }
+  | LPAREN_TOK c=IDENTIFIER
+    { std::string s = AntlrInput::tokenText($c);
+      if(s == "set" || s == "get") {
+        PARSER_STATE->parseError(std::string("In SMT-LIBv1 mode, expected keyword `benchmark', but it looks like you're writing SMT-LIBv2.  Use --lang smt for SMT-LIBv2."));
+      } else {
+        PARSER_STATE->parseError(std::string("expected keyword `benchmark', got `" + s + "'"));
+      }
+    }
+  ;
+
+/**
+ * Matches the whole SMT-LIB benchmark.
+ * @return the sequence command containing the whole problem
+ */
+benchmark returns [CVC4::Command* cmd = NULL]
+  : LPAREN_TOK BENCHMARK_TOK IDENTIFIER c = benchAttributes RPAREN_TOK
+  	{ $cmd = c; }
+  | EOF { $cmd = 0; }
+  ;
+
+/**
+ * Matches a sequence of benchmark attributes and returns a pointer to a
+ * command sequence.
+ * @return the command sequence
+ */
+benchAttributes returns [CVC4::CommandSequence* cmd_seq = NULL]
+@init {
+  cmd_seq = new CommandSequence();
+}
+  : (cmd = benchAttribute { if (cmd) cmd_seq->addCommand(cmd); } )+
+  ;
+
+/**
+ * Matches a benchmark attribute, such as ':logic', ':formula', and returns
+ * a corresponding command
+ * @return a command corresponding to the attribute
+ */
+benchAttribute returns [CVC4::Command* smt_command = NULL]
+@declarations {
+  std::string name;
+  BenchmarkStatus b_status;
+  Expr expr;
+  Command* c;
+}
+  : LOGIC_TOK identifier[name,CHECK_NONE,SYM_VARIABLE]
+    { PARSER_STATE->preemptCommand(new SetBenchmarkLogicCommand(name));
+      PARSER_STATE->setLogic(name);
+      smt_command = new EmptyCommand();
+    }
+  | ASSUMPTION_TOK annotatedFormula[expr]
+    { smt_command = new AssertCommand(expr); }
+  | FORMULA_TOK annotatedFormula[expr]
+    { smt_command = new CheckSatCommand(expr); }
+  | STATUS_TOK status[b_status]
+    { smt_command = new SetBenchmarkStatusCommand(b_status); }
+  | EXTRAFUNS_TOK LPAREN_TOK
+    { smt_command = new CommandSequence(); }
+    ( functionDeclaration[c]
+      { ((CommandSequence*) smt_command)->addCommand(c); }
+    )+ RPAREN_TOK
+  | EXTRAPREDS_TOK LPAREN_TOK
+    ( { smt_command = new CommandSequence(); }
+      predicateDeclaration[c]
+      { ((CommandSequence*) smt_command)->addCommand(c); }
+    )+ RPAREN_TOK
+  | EXTRASORTS_TOK LPAREN_TOK
+    ( { smt_command = new CommandSequence(); }
+      sortDeclaration[c]
+      { ((CommandSequence*) smt_command)->addCommand(c); }
+    )+ RPAREN_TOK
+  | NOTES_TOK STRING_LITERAL
+    { smt_command = new CommentCommand(AntlrInput::tokenText($STRING_LITERAL)); }
+  | annotation[smt_command]
+  ;
+
+/**
+ * Matches an annotated formula.
+ * @return the expression representing the formula
+ */
+annotatedFormula[CVC4::Expr& expr]
+@init {
+  Debug("parser") << "annotated formula: " << AntlrInput::tokenText(LT(1)) << std::endl;
+  Kind kind;
+  std::string name;
+  std::vector<Expr> args; /* = getExprVector(); */
+  std::vector<Expr> args2;
+  Expr op; /* Operator expression FIXME: move away kill it */
+}
+  : /* a built-in operator application */
+    LPAREN_TOK builtinOp[kind] annotatedFormulas[args,expr] RPAREN_TOK
+    { if((kind == CVC4::kind::AND || kind == CVC4::kind::OR) && args.size() == 1) {
+        /* Unary AND/OR can be replaced with the argument.
+	       It just so happens expr should already by the only argument. */
+        Assert( expr == args[0] );
+      } else if( CVC4::kind::isAssociative(kind) &&
+                 args.size() > EXPR_MANAGER->maxArity(kind) ) {
+    	/* Special treatment for associative operators with lots of children */
+        expr = EXPR_MANAGER->mkAssociative(kind,args);
+      } else if(!PARSER_STATE->strictModeEnabled() &&
+                kind == CVC4::kind::MINUS && args.size() == 1) {
+        /* Special fix-up for unary minus improperly used in some benchmarks */
+        expr = MK_EXPR(CVC4::kind::UMINUS, args[0]);
+      } else {
+        PARSER_STATE->checkArity(kind, args.size());
+        expr = MK_EXPR(kind, args);
+      }
+    }
+
+  | /* A quantifier */
+    LPAREN_TOK
+    ( FORALL_TOK { kind = kind::FORALL; } | EXISTS_TOK { kind = kind::EXISTS; } )
+    { PARSER_STATE->pushScope(); }
+    ( LPAREN_TOK let_identifier[name,CHECK_NONE] t=sortSymbol RPAREN_TOK
+      { args.push_back(PARSER_STATE->mkBoundVar(name, t)); }
+    )+
+    annotatedFormula[expr] RPAREN_TOK
+    { args2.push_back( MK_EXPR( kind::BOUND_VAR_LIST, args ) );
+      args2.push_back(expr);
+      expr = MK_EXPR(kind, args2);
+      PARSER_STATE->popScope();
+    }
+
+  | /* A non-built-in function application */
+
+    // Semantic predicate not necessary if parenthesized subexpressions
+    // are disallowed
+    // { isFunction(LT(2)->getText()) }?
+    LPAREN_TOK
+    parameterizedOperator[op]
+    annotatedFormulas[args,expr] RPAREN_TOK
+    // TODO: check arity
+    { expr = MK_EXPR(op,args); }
+
+  | /* An ite expression */
+    LPAREN_TOK ITE_TOK
+    annotatedFormula[expr]
+    { args.push_back(expr); }
+    annotatedFormula[expr]
+    { args.push_back(expr); }
+    annotatedFormula[expr]
+    { args.push_back(expr); }
+    RPAREN_TOK
+    { expr = MK_EXPR(CVC4::kind::ITE, args); }
+
+  | /* a let/flet binding */
+    LPAREN_TOK
+    ( LET_TOK LPAREN_TOK let_identifier[name,CHECK_UNDECLARED]
+      | FLET_TOK LPAREN_TOK flet_identifier[name,CHECK_UNDECLARED] )
+    annotatedFormula[expr] RPAREN_TOK
+    { PARSER_STATE->pushScope();
+      PARSER_STATE->defineVar(name,expr); }
+    annotatedFormula[expr]
+    RPAREN_TOK
+    { PARSER_STATE->popScope(); }
+
+    /* constants */
+  | TRUE_TOK          { expr = MK_CONST(bool(true)); }
+  | FALSE_TOK         { expr = MK_CONST(bool(false)); }
+  | NUMERAL_TOK
+    { expr = MK_CONST( AntlrInput::tokenToInteger($NUMERAL_TOK) ); }
+  | RATIONAL_TOK
+    { // FIXME: This doesn't work because an SMT rational is not a
+      // valid GMP rational string
+      expr = MK_CONST( AntlrInput::tokenToRational($RATIONAL_TOK) ); }
+  | n = BITVECTOR_BV_CONST '[' size = NUMERAL_TOK  ']'
+    { expr = MK_CONST( AntlrInput::tokenToBitvector($n, $size) ); }
+    // NOTE: Theory constants go here
+    /* TODO: quantifiers, arithmetic constants */
+
+  | /* a variable */
+    ( identifier[name,CHECK_DECLARED,SYM_VARIABLE]
+      | let_identifier[name,CHECK_DECLARED]
+      | flet_identifier[name,CHECK_DECLARED] )
+    { expr = PARSER_STATE->getVariable(name); }
+
+  ;
+
+/**
+ * Matches a sequence of annotated formulas and puts them into the
+ * formulas vector.
+ * @param formulas the vector to fill with formulas
+ * @param expr an Expr reference for the elements of the sequence
+ */
+/* NOTE: We pass an Expr in here just to avoid allocating a fresh Expr every
+ * time through this rule. */
+annotatedFormulas[std::vector<CVC4::Expr>& formulas, CVC4::Expr& expr]
+  : ( annotatedFormula[expr] { formulas.push_back(expr); } )+
+  ;
+
+/**
+* Matches a builtin operator symbol and sets kind to its associated Expr kind.
+*/
+builtinOp[CVC4::Kind& kind]
+@init {
+  Debug("parser") << "builtin: " << AntlrInput::tokenText(LT(1)) << std::endl;
+}
+  : NOT_TOK      { $kind = CVC4::kind::NOT;     }
+  | IMPLIES_TOK  { $kind = CVC4::kind::IMPLIES; }
+  | AND_TOK      { $kind = CVC4::kind::AND;     }
+  | OR_TOK       { $kind = CVC4::kind::OR;      }
+  | XOR_TOK      { $kind = CVC4::kind::XOR;     }
+  | IFF_TOK      { $kind = CVC4::kind::IFF;     }
+  | EQUAL_TOK    { $kind = CVC4::kind::EQUAL;   }
+  | DISTINCT_TOK { $kind = CVC4::kind::DISTINCT; }
+  // Arithmetic
+  | GREATER_THAN_TOK
+                 { $kind = CVC4::kind::GT; }
+  | GREATER_THAN_TOK EQUAL_TOK
+                 { $kind = CVC4::kind::GEQ; }
+  | LESS_THAN_TOK EQUAL_TOK
+                 { $kind = CVC4::kind::LEQ; }
+  | LESS_THAN_TOK
+                 { $kind = CVC4::kind::LT; }
+  | PLUS_TOK     { $kind = CVC4::kind::PLUS; }
+  | STAR_TOK     { $kind = CVC4::kind::MULT; }
+  | TILDE_TOK    { $kind = CVC4::kind::UMINUS; }
+  | MINUS_TOK    { $kind = CVC4::kind::MINUS; }
+  | DIV_TOK      { $kind = CVC4::kind::DIVISION; }
+  // Bit-vectors
+  | CONCAT_TOK   { $kind = CVC4::kind::BITVECTOR_CONCAT; }
+  | BVAND_TOK    { $kind = CVC4::kind::BITVECTOR_AND;    }
+  | BVOR_TOK     { $kind = CVC4::kind::BITVECTOR_OR;     }
+  | BVXOR_TOK    { $kind = CVC4::kind::BITVECTOR_XOR;    }
+  | BVNOT_TOK    { $kind = CVC4::kind::BITVECTOR_NOT;    }
+  | BVNAND_TOK   { $kind = CVC4::kind::BITVECTOR_NAND;   }
+  | BVNOR_TOK    { $kind = CVC4::kind::BITVECTOR_NOR;    }
+  | BVXNOR_TOK   { $kind = CVC4::kind::BITVECTOR_XNOR;   }
+  | BVCOMP_TOK   { $kind = CVC4::kind::BITVECTOR_COMP;   }
+  | BVMUL_TOK    { $kind = CVC4::kind::BITVECTOR_MULT;   }
+  | BVADD_TOK    { $kind = CVC4::kind::BITVECTOR_PLUS;   }
+  | BVSUB_TOK    { $kind = CVC4::kind::BITVECTOR_SUB;    }
+  | BVNEG_TOK    { $kind = CVC4::kind::BITVECTOR_NEG;    }
+  | BVUDIV_TOK   { $kind = CVC4::kind::BITVECTOR_UDIV;   }
+  | BVUREM_TOK   { $kind = CVC4::kind::BITVECTOR_UREM;   }
+  | BVSDIV_TOK   { $kind = CVC4::kind::BITVECTOR_SDIV;   }
+  | BVSREM_TOK   { $kind = CVC4::kind::BITVECTOR_SREM;   }
+  | BVSMOD_TOK   { $kind = CVC4::kind::BITVECTOR_SMOD;   }
+  | BVSHL_TOK    { $kind = CVC4::kind::BITVECTOR_SHL;    }
+  | BVLSHR_TOK   { $kind = CVC4::kind::BITVECTOR_LSHR;   }
+  | BVASHR_TOK   { $kind = CVC4::kind::BITVECTOR_ASHR;   }
+  | BVULT_TOK    { $kind = CVC4::kind::BITVECTOR_ULT;    }
+  | BVULE_TOK    { $kind = CVC4::kind::BITVECTOR_ULE;    }
+  | BVUGT_TOK    { $kind = CVC4::kind::BITVECTOR_UGT;    }
+  | BVUGE_TOK    { $kind = CVC4::kind::BITVECTOR_UGE;    }
+  | BVSLT_TOK    { $kind = CVC4::kind::BITVECTOR_SLT;    }
+  | BVSLE_TOK    { $kind = CVC4::kind::BITVECTOR_SLE;    }
+  | BVSGT_TOK    { $kind = CVC4::kind::BITVECTOR_SGT;    }
+  | BVSGE_TOK    { $kind = CVC4::kind::BITVECTOR_SGE;    }
+  // arrays
+  | SELECT_TOK   { $kind = CVC4::kind::SELECT; }
+  | STORE_TOK    { $kind = CVC4::kind::STORE; }
+  // NOTE: Theory operators go here
+  ;
+
+/**
+ * Matches an operator.
+ */
+parameterizedOperator[CVC4::Expr& op]
+  : functionSymbol[op]
+  | bitVectorOperator[op]
+  ;
+
+/**
+ * Matches a bit-vector operator (the ones parametrized by numbers)
+ */
+bitVectorOperator[CVC4::Expr& op]
+  : EXTRACT_TOK '[' n1 = NUMERAL_TOK ':' n2 = NUMERAL_TOK ']'
+    { op = MK_CONST(BitVectorExtract(AntlrInput::tokenToUnsigned($n1), AntlrInput::tokenToUnsigned($n2))); }
+  | REPEAT_TOK '[' n = NUMERAL_TOK ']'
+    { op = MK_CONST(BitVectorRepeat(AntlrInput::tokenToUnsigned($n))); }
+  | ZERO_EXTEND_TOK '[' n = NUMERAL_TOK ']'
+    { op = MK_CONST(BitVectorZeroExtend(AntlrInput::tokenToUnsigned($n))); }
+  | SIGN_EXTEND_TOK '[' n = NUMERAL_TOK ']'
+    { op = MK_CONST(BitVectorSignExtend(AntlrInput::tokenToUnsigned($n))); }
+  | ROTATE_LEFT_TOK '[' n = NUMERAL_TOK ']'
+    { op = MK_CONST(BitVectorRotateLeft(AntlrInput::tokenToUnsigned($n))); }
+  | ROTATE_RIGHT_TOK '[' n = NUMERAL_TOK ']'
+    { op = MK_CONST(BitVectorRotateRight(AntlrInput::tokenToUnsigned($n))); }
+  ;
+
+/**
+ * Matches a (possibly undeclared) predicate identifier (returning the string).
+ * @param check what kind of check to do with the symbol
+ */
+predicateName[std::string& name, CVC4::parser::DeclarationCheck check]
+  :  functionName[name,check]
+  ;
+
+/**
+ * Matches a (possibly undeclared) function identifier (returning the string)
+ * @param check what kind of check to do with the symbol
+ */
+functionName[std::string& name, CVC4::parser::DeclarationCheck check]
+  :  identifier[name,check,SYM_VARIABLE]
+  ;
+
+/**
+ * Matches an previously declared function symbol (returning an Expr)
+ */
+functionSymbol[CVC4::Expr& fun]
+@declarations {
+	std::string name;
+}
+  : functionName[name,CHECK_DECLARED]
+    { PARSER_STATE->checkFunctionLike(name);
+      fun = PARSER_STATE->getVariable(name); }
+  ;
+
+/**
+ * Matches an attribute name from the input (:attribute_name).
+ */
+attribute[std::string& s]
+  :  ATTR_IDENTIFIER
+    { s = AntlrInput::tokenText($ATTR_IDENTIFIER); }
+  ;
+
+functionDeclaration[CVC4::Command*& smt_command]
+@declarations {
+  std::string name;
+  std::vector<Type> sorts;
+}
+  : LPAREN_TOK functionName[name,CHECK_UNDECLARED]
+      t = sortSymbol // require at least one sort
+    { sorts.push_back(t); }
+      sortList[sorts] RPAREN_TOK
+    { if( sorts.size() == 1 ) {
+        Assert( t == sorts[0] );
+      } else {
+        t = EXPR_MANAGER->mkFunctionType(sorts);
+      }
+      Expr func = PARSER_STATE->mkVar(name, t);
+      smt_command = new DeclareFunctionCommand(name, func, t);
+    }
+  ;
+
+/**
+ * Matches the declaration of a predicate and declares it
+ */
+predicateDeclaration[CVC4::Command*& smt_command]
+@declarations {
+  std::string name;
+  std::vector<Type> p_sorts;
+}
+  : LPAREN_TOK predicateName[name,CHECK_UNDECLARED] sortList[p_sorts] RPAREN_TOK
+    { Type t;
+      if( p_sorts.empty() ) {
+        t = EXPR_MANAGER->booleanType();
+      } else {
+        t = EXPR_MANAGER->mkPredicateType(p_sorts);
+      }
+      Expr func = PARSER_STATE->mkVar(name, t);
+      smt_command = new DeclareFunctionCommand(name, func, t);
+    }
+  ;
+
+sortDeclaration[CVC4::Command*& smt_command]
+@declarations {
+  std::string name;
+}
+  : sortName[name,CHECK_UNDECLARED]
+    { Debug("parser") << "sort decl: '" << name << "'" << std::endl;
+      Type type = PARSER_STATE->mkSort(name);
+      smt_command = new DeclareTypeCommand(name, 0, type);
+    }
+  ;
+
+/**
+ * Matches a sequence of sort symbols and fills them into the given vector.
+ */
+sortList[std::vector<CVC4::Type>& sorts]
+  : ( t = sortSymbol { sorts.push_back(t); })*
+  ;
+
+/**
+ * Matches the sort symbol, which can be an arbitrary identifier.
+ * @param check the check to perform on the name
+ */
+sortName[std::string& name, CVC4::parser::DeclarationCheck check]
+  : identifier[name,check,SYM_SORT]
+  ;
+
+sortSymbol returns [CVC4::parser::smt1::myType t]
+@declarations {
+  std::string name;
+}
+  : sortName[name,CHECK_NONE]
+  	{ $t = PARSER_STATE->getSort(name); }
+  | BITVECTOR_TOK '[' NUMERAL_TOK ']' {
+  	$t = EXPR_MANAGER->mkBitVectorType(AntlrInput::tokenToUnsigned($NUMERAL_TOK));
+    }
+  /* attaching 'Array' to '[' allows us to parse regular 'Array' correctly in
+   * e.g. QF_AX, and also 'Array[m:n]' in e.g. QF_AUFBV */
+  | 'Array[' n1=NUMERAL_TOK ':' n2=NUMERAL_TOK ']' {
+        $t = EXPR_MANAGER->mkArrayType(EXPR_MANAGER->mkBitVectorType(AntlrInput::tokenToUnsigned(n1)),
+                                       EXPR_MANAGER->mkBitVectorType(AntlrInput::tokenToUnsigned(n2)));
+    }
+  ;
+
+/**
+ * Matches the status of the benchmark, one of 'sat', 'unsat' or 'unknown'.
+ */
+status[ CVC4::BenchmarkStatus& status ]
+  : SAT_TOK       { $status = SMT_SATISFIABLE;    }
+  | UNSAT_TOK     { $status = SMT_UNSATISFIABLE;  }
+  | UNKNOWN_TOK   { $status = SMT_UNKNOWN;        }
+  ;
+
+/**
+ * Matches an annotation, which is an attribute name, with an optional user
+ */
+annotation[CVC4::Command*& smt_command]
+@init {
+  std::string key;
+  smt_command = NULL;
+}
+  : attribute[key]
+    ( USER_VALUE
+      { std::string value = AntlrInput::tokenText($USER_VALUE);
+        Assert(*value.begin() == '{');
+        Assert(*value.rbegin() == '}');
+        // trim whitespace
+        value.erase(value.begin(), value.begin() + 1);
+        value.erase(value.begin(), std::find_if(value.begin(), value.end(), std::not1(std::ptr_fun<int, int>(std::isspace))));
+        value.erase(value.end() - 1);
+        value.erase(std::find_if(value.rbegin(), value.rend(), std::not1(std::ptr_fun<int, int>(std::isspace))).base(), value.end());
+        smt_command = new SetInfoCommand(key.c_str() + 1, value); }
+    )?
+    { if(smt_command == NULL) {
+        smt_command = new EmptyCommand(std::string("annotation: ") + key);
+      }
+    }
+  ;
+
+/**
+ * Matches an identifier and sets the string reference parameter id.
+ * @param id string to hold the identifier
+ * @param check what kinds of check to do on the symbol
+ * @param type the intended namespace for the identifier
+ */
+identifier[std::string& id,
+		   CVC4::parser::DeclarationCheck check,
+           CVC4::parser::SymbolType type]
+  : IDENTIFIER
+    { id = AntlrInput::tokenText($IDENTIFIER);
+      Debug("parser") << "identifier: " << id
+                      << " check? " << check
+                      << " type? " << type << std::endl;
+      PARSER_STATE->checkDeclaration(id, check, type); }
+  ;
+
+/**
+ * Matches a let-bound identifier and sets the string reference parameter id.
+ * @param id string to hold the identifier
+ * @param check what kinds of check to do on the symbol
+ */
+let_identifier[std::string& id,
+    		   CVC4::parser::DeclarationCheck check]
+  : LET_IDENTIFIER
+    { id = AntlrInput::tokenText($LET_IDENTIFIER);
+      Debug("parser") << "let_identifier: " << id
+                      << " check? " << check << std::endl;
+      PARSER_STATE->checkDeclaration(id, check, SYM_VARIABLE); }
+  ;
+
+/**
+ * Matches an flet-bound identifier and sets the string reference parameter id.
+ * @param id string to hold the identifier
+ * @param check what kinds of check to do on the symbol
+ */
+flet_identifier[std::string& id,
+    		    CVC4::parser::DeclarationCheck check]
+  : FLET_IDENTIFIER
+    { id = AntlrInput::tokenText($FLET_IDENTIFIER);
+      Debug("parser") << "flet_identifier: " << id
+                      << " check? " << check << std::endl;
+      PARSER_STATE->checkDeclaration(id, check); }
+  ;
+
+// Base SMT-LIB tokens
+ASSUMPTION_TOK  : ':assumption';
+BENCHMARK_TOK   : 'benchmark';
+EXTRAFUNS_TOK   : ':extrafuns';
+EXTRAPREDS_TOK  : ':extrapreds';
+EXTRASORTS_TOK  : ':extrasorts';
+FALSE_TOK       : 'false';
+FLET_TOK        : 'flet';
+FORMULA_TOK     : ':formula';
+ITE_TOK         : 'ite' | 'if_then_else';
+LET_TOK         : 'let';
+LOGIC_TOK       : ':logic';
+LPAREN_TOK      : '(';
+NOTES_TOK       : ':notes';
+RPAREN_TOK      : ')';
+SAT_TOK         : 'sat';
+STATUS_TOK      : ':status';
+THEORY_TOK      : 'theory';
+TRUE_TOK        : 'true';
+UNKNOWN_TOK     : 'unknown';
+UNSAT_TOK       : 'unsat';
+
+// operators (NOTE: theory symbols go here)
+AMPERSAND_TOK     : '&';
+AND_TOK           : 'and';
+AT_TOK            : '@';
+DISTINCT_TOK      : 'distinct';
+DIV_TOK           : '/';
+EQUAL_TOK         : '=';
+EXISTS_TOK        : 'exists';
+FORALL_TOK        : 'forall';
+GREATER_THAN_TOK  : '>';
+IFF_TOK           : 'iff';
+IMPLIES_TOK       : 'implies';
+LESS_THAN_TOK     : '<';
+MINUS_TOK         : '-';
+NOT_TOK           : 'not';
+OR_TOK            : 'or';
+PERCENT_TOK       : '%';
+PIPE_TOK          : '|';
+PLUS_TOK          : '+';
+POUND_TOK         : '#';
+SELECT_TOK        : 'select';
+STAR_TOK          : '*';
+STORE_TOK         : 'store';
+TILDE_TOK         : '~';
+XOR_TOK           : 'xor';
+
+// Bitvector tokens
+BITVECTOR_TOK     : 'BitVec';
+CONCAT_TOK        : 'concat';
+EXTRACT_TOK       : 'extract';
+BVAND_TOK         : 'bvand';
+BVOR_TOK          : 'bvor';
+BVXOR_TOK         : 'bvxor';
+BVNOT_TOK         : 'bvnot';
+BVNAND_TOK        : 'bvnand';
+BVNOR_TOK         : 'bvnor';
+BVXNOR_TOK        : 'bvxnor';
+BVCOMP_TOK        : 'bvcomp';
+BVMUL_TOK         : 'bvmul';
+BVADD_TOK         : 'bvadd';
+BVSUB_TOK         : 'bvsub';
+BVNEG_TOK         : 'bvneg';
+BVUDIV_TOK        : 'bvudiv';
+BVUREM_TOK        : 'bvurem';
+BVSDIV_TOK        : 'bvsdiv';
+BVSREM_TOK        : 'bvsrem';
+BVSMOD_TOK        : 'bvsmod';
+BVSHL_TOK         : 'bvshl';
+BVLSHR_TOK        : 'bvlshr';
+BVASHR_TOK        : 'bvashr';
+BVULT_TOK         : 'bvult';
+BVULE_TOK         : 'bvule';
+BVUGT_TOK         : 'bvugt';
+BVUGE_TOK         : 'bvuge';
+BVSLT_TOK         : 'bvslt';
+BVSLE_TOK         : 'bvsle';
+BVSGT_TOK         : 'bvsgt';
+BVSGE_TOK         : 'bvsge';
+REPEAT_TOK        : 'repeat';
+ZERO_EXTEND_TOK   : 'zero_extend';
+SIGN_EXTEND_TOK   : 'sign_extend';
+ROTATE_LEFT_TOK   : 'rotate_left';
+ROTATE_RIGHT_TOK  : 'rotate_right';
+
+/**
+ * Matches a bit-vector constant of the form bv123
+ */
+BITVECTOR_BV_CONST
+  : 'bv' DIGIT+
+  ;
+
+
+/**
+ * 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 an identifier starting with a colon.
+ */
+ATTR_IDENTIFIER
+  :  ':' IDENTIFIER
+  ;
+
+/**
+ * Matches an identifier starting with a question mark.
+ */
+LET_IDENTIFIER
+  : '?' IDENTIFIER
+  ;
+
+/**
+ * Matches an identifier starting with a dollar sign.
+ */
+FLET_IDENTIFIER
+  : '$' IDENTIFIER
+  ;
+
+/**
+ * Matches the value of user-defined annotations or attributes. The
+ * only constraint imposed on a user-defined value is that it start
+ * with an open brace and end with closed brace.
+ */
+USER_VALUE
+  : '{' ('\\{' | '\\}' | ~('{' | '}'))* '}'
+  ;
+
+/**
+ * Matches and skips whitespace in the input.
+ */
+WHITESPACE
+  : (' ' | '\t' | '\f' | '\r' | '\n')+
+    { SKIP(); }
+  ;
+
+/**
+ * Matches a numeral from the input (non-empty sequence of digits).
+ */
+NUMERAL_TOK
+  : DIGIT+
+  ;
+
+RATIONAL_TOK
+  : DIGIT+ '.' DIGIT+
+  ;
+
+/**
+ * Matches a double quoted string literal. Escaping is supported, and escape
+ * character '\' has to be escaped.
+ */
+STRING_LITERAL
+  :  '"' (ESCAPE | ~('"'|'\\'))* '"'
+  ;
+
+/**
+ * Matches the comments and ignores them
+ */
+COMMENT
+  : ';' (~('\n' | '\r'))*
+    { SKIP(); }
+  ;
+
+
+/**
+ * Matches any letter ('a'-'z' and 'A'-'Z').
+ */
+fragment
+ALPHA
+  :  'a'..'z'
+  |  'A'..'Z'
+  ;
+
+/**
+ * Matches the digits (0-9)
+ */
+fragment DIGIT :   '0'..'9';
+// fragment NON_ZERO_DIGIT : '1'..'9';
+// fragment NUMERAL_SEQ : '0' | NON_ZERO_DIGIT DIGIT*;
+
+/**
+ * Matches an allowed escaped character.
+ */
+fragment ESCAPE : '\\' ('"' | '\\' | 'n' | 't' | 'r');
+
diff --git a/src/parser/smt1/smt1.cpp b/src/parser/smt1/smt1.cpp
new file mode 100644
index 000000000..c91743226
--- /dev/null
+++ b/src/parser/smt1/smt1.cpp
@@ -0,0 +1,328 @@
+/*********************                                                        */
+/*! \file smt1.cpp
+ ** \verbatim
+ ** Original author: cconway
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): dejan
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  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.\endverbatim
+ **
+ ** Definitions of SMT-LIB (v1) constants.
+ **/
+
+#include <ext/hash_map>
+namespace std {
+  using namespace __gnu_cxx;
+}
+
+#include "expr/type.h"
+#include "expr/command.h"
+#include "parser/parser.h"
+#include "parser/smt1/smt1.h"
+
+namespace CVC4 {
+namespace parser {
+
+std::hash_map<const std::string, Smt1::Logic, CVC4::StringHashFunction> Smt1::newLogicMap() {
+  std::hash_map<const std::string, Smt1::Logic, CVC4::StringHashFunction> logicMap;
+  logicMap["AUFLIA"] = AUFLIA;
+  logicMap["AUFLIRA"] = AUFLIRA;
+  logicMap["AUFNIRA"] = AUFNIRA;
+  logicMap["LRA"] = LRA;
+  logicMap["QF_AX"] = QF_AX;
+  logicMap["QF_BV"] = QF_BV;
+  logicMap["QF_IDL"] = QF_IDL;
+  logicMap["QF_LIA"] = QF_LIA;
+  logicMap["QF_LRA"] = QF_LRA;
+  logicMap["QF_NIA"] = QF_NIA;
+  logicMap["QF_NRA"] = QF_NRA;
+  logicMap["QF_RDL"] = QF_RDL;
+  logicMap["QF_SAT"] = QF_SAT;
+  logicMap["QF_UF"] = QF_UF;
+  logicMap["QF_UFIDL"] = QF_UFIDL;
+  logicMap["QF_UFBV"] = QF_UFBV;
+  logicMap["QF_UFLRA"] = QF_UFLRA;
+  logicMap["QF_UFLIA"] = QF_UFLIA;
+  logicMap["QF_UFLIRA"] = QF_UFLIRA;
+  logicMap["QF_UFNIA"] = QF_UFNIA;
+  logicMap["QF_UFNIRA"] = QF_UFNIRA;
+  logicMap["QF_UFNRA"] = QF_UFNRA;
+  logicMap["QF_ABV"] = QF_ABV;
+  logicMap["QF_AUFBV"] = QF_AUFBV;
+  logicMap["QF_AUFBVLIA"] = QF_AUFBVLIA;
+  logicMap["QF_AUFBVLRA"] = QF_AUFBVLRA;
+  logicMap["QF_UFNIRA"] = QF_UFNIRA;
+  logicMap["QF_AUFLIA"] = QF_AUFLIA;
+  logicMap["QF_AUFLIRA"] = QF_AUFLIRA;
+  logicMap["UFNIA"] = UFNIA;
+  logicMap["UFNIRA"] = UFNIRA;
+  logicMap["UFLRA"] = UFLRA;
+  logicMap["QF_ALL_SUPPORTED"] = QF_ALL_SUPPORTED;
+  logicMap["ALL_SUPPORTED"] = ALL_SUPPORTED;
+  return logicMap;
+}
+
+Smt1::Logic Smt1::toLogic(const std::string& name) {
+  static std::hash_map<const std::string, Smt1::Logic, CVC4::StringHashFunction> logicMap = newLogicMap();
+  return logicMap[name];
+}
+
+Smt1::Smt1(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) :
+  Parser(exprManager,input,strictMode,parseOnly),
+  d_logicSet(false) {
+
+  // Boolean symbols are always defined
+  addOperator(kind::AND);
+  addOperator(kind::EQUAL);
+  addOperator(kind::IFF);
+  addOperator(kind::IMPLIES);
+  addOperator(kind::ITE);
+  addOperator(kind::NOT);
+  addOperator(kind::OR);
+  addOperator(kind::XOR);
+
+}
+
+void Smt1::addArithmeticOperators() {
+  addOperator(kind::PLUS);
+  addOperator(kind::MINUS);
+  addOperator(kind::UMINUS);
+  addOperator(kind::MULT);
+  addOperator(kind::LT);
+  addOperator(kind::LEQ);
+  addOperator(kind::GT);
+  addOperator(kind::GEQ);
+}
+
+void Smt1::addTheory(Theory theory) {
+  switch(theory) {
+  case THEORY_ARRAYS:
+  case THEORY_ARRAYS_EX: {
+    Type indexType = mkSort("Index");
+    Type elementType = mkSort("Element");
+    DeclarationSequence* seq = new DeclarationSequence();
+    seq->addCommand(new DeclareTypeCommand("Index", 0, indexType));
+    seq->addCommand(new DeclareTypeCommand("Element", 0, elementType));
+    preemptCommand(seq);
+
+    defineType("Array", getExprManager()->mkArrayType(indexType, elementType));
+
+    addOperator(kind::SELECT);
+    addOperator(kind::STORE);
+    break;
+  }
+
+  case THEORY_BITVECTOR_ARRAYS_EX: {
+    Unimplemented("Cannot yet handle SMT-LIBv1 bitvector arrays (i.e., the BitVector_ArraysEx theory)");
+    //addOperator(kind::SELECT);
+    //addOperator(kind::STORE);
+    break;
+  }
+
+  case THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX: {
+    defineType("Array1", getExprManager()->mkArrayType(getSort("Int"), getSort("Real")));
+    defineType("Array2", getExprManager()->mkArrayType(getSort("Int"), getSort("Array1")));
+    addOperator(kind::SELECT);
+    addOperator(kind::STORE);
+    break;
+  }
+
+  case THEORY_INT_ARRAYS:
+  case THEORY_INT_ARRAYS_EX: {
+    defineType("Array", getExprManager()->mkArrayType(getExprManager()->integerType(), getExprManager()->integerType()));
+
+    addOperator(kind::SELECT);
+    addOperator(kind::STORE);
+    break;
+  }
+
+  case THEORY_EMPTY: {
+    Type sort = mkSort("U");
+    preemptCommand(new DeclareTypeCommand("U", 0, sort));
+    break;
+  }
+
+  case THEORY_REALS_INTS:
+    defineType("Real", getExprManager()->realType());
+    // falling-through on purpose, to add Ints part of RealsInts
+
+  case THEORY_INTS:
+    defineType("Int", getExprManager()->integerType());
+    addArithmeticOperators();
+    break;
+
+  case THEORY_REALS:
+    defineType("Real", getExprManager()->realType());
+    addArithmeticOperators();
+    break;
+
+  case THEORY_BITVECTORS:
+    break;
+
+  case THEORY_QUANTIFIERS:
+    break;
+
+  default:
+    Unhandled(theory);
+  }
+}
+
+bool Smt1::logicIsSet() {
+  return d_logicSet;
+}
+
+void Smt1::setLogic(const std::string& name) {
+  d_logicSet = true;
+  d_logic = toLogic(name);
+
+  switch(d_logic) {
+  case QF_AX:
+    addTheory(THEORY_ARRAYS_EX);
+    break;
+
+  case QF_IDL:
+  case QF_LIA:
+  case QF_NIA:
+    addTheory(THEORY_INTS);
+    break;
+
+  case QF_RDL:
+  case QF_LRA:
+  case QF_NRA:
+    addTheory(THEORY_REALS);
+    break;
+
+  case QF_SAT:
+    /* no extra symbols needed */
+    break;
+
+  case QF_UFIDL:
+  case QF_UFLIA:
+  case QF_UFNIA:// nonstandard logic
+    addTheory(THEORY_INTS);
+    addOperator(kind::APPLY_UF);
+    break;
+
+  case QF_UFLRA:
+  case QF_UFNRA:
+    addTheory(THEORY_REALS);
+    addOperator(kind::APPLY_UF);
+    break;
+
+  case QF_UFLIRA:// nonstandard logic
+  case QF_UFNIRA:// nonstandard logic
+    addTheory(THEORY_INTS);
+    addTheory(THEORY_REALS);
+    addOperator(kind::APPLY_UF);
+    break;
+
+  case QF_UF:
+    addTheory(THEORY_EMPTY);
+    addOperator(kind::APPLY_UF);
+    break;
+
+  case QF_BV:
+    addTheory(THEORY_BITVECTORS);
+    break;
+
+  case QF_ABV:
+    addTheory(THEORY_ARRAYS_EX);
+    addTheory(THEORY_BITVECTORS);
+    break;
+
+  case QF_UFBV:
+    addOperator(kind::APPLY_UF);
+    addTheory(THEORY_BITVECTORS);
+    break;
+
+  case QF_AUFBV:
+    addOperator(kind::APPLY_UF);
+    addTheory(THEORY_ARRAYS_EX);
+    addTheory(THEORY_BITVECTORS);
+    break;
+
+  case QF_AUFBVLIA:
+    addOperator(kind::APPLY_UF);
+    addTheory(THEORY_ARRAYS_EX);
+    addTheory(THEORY_BITVECTORS);
+    addTheory(THEORY_INTS);
+    break;
+
+  case QF_AUFBVLRA:
+    addOperator(kind::APPLY_UF);
+    addTheory(THEORY_ARRAYS_EX);
+    addTheory(THEORY_BITVECTORS);
+    addTheory(THEORY_REALS);
+    break;
+
+  case QF_AUFLIA:
+    addTheory(THEORY_INT_ARRAYS_EX);
+    addOperator(kind::APPLY_UF);
+    addTheory(THEORY_INTS);
+    break;
+
+  case QF_AUFLIRA:
+    addTheory(THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX);
+    addOperator(kind::APPLY_UF);
+    addTheory(THEORY_INTS);
+    addTheory(THEORY_REALS);
+    break;
+
+  case ALL_SUPPORTED:
+    addTheory(THEORY_QUANTIFIERS);
+    /* fall through */
+  case QF_ALL_SUPPORTED:
+    addTheory(THEORY_ARRAYS_EX);
+    addOperator(kind::APPLY_UF);
+    addTheory(THEORY_INTS);
+    addTheory(THEORY_REALS);
+    addTheory(THEORY_BITVECTORS);
+    break;
+
+  case AUFLIA:
+    addOperator(kind::APPLY_UF);
+    addTheory(THEORY_INTS);
+    addTheory(THEORY_INT_ARRAYS_EX);
+    addTheory(THEORY_QUANTIFIERS);
+    break;
+
+  case AUFLIRA:
+  case AUFNIRA:
+    addOperator(kind::APPLY_UF);
+    addTheory(THEORY_INTS);
+    addTheory(THEORY_REALS);
+    addTheory(THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX);
+    addTheory(THEORY_QUANTIFIERS);
+    break;
+
+  case LRA:
+    addTheory(THEORY_REALS);
+    addTheory(THEORY_QUANTIFIERS);
+    break;
+
+  case UFNIA:
+    addOperator(kind::APPLY_UF);
+    addTheory(THEORY_INTS);
+    addTheory(THEORY_QUANTIFIERS);
+    break;
+  case UFNIRA:
+    addOperator(kind::APPLY_UF);
+    addTheory(THEORY_INTS);
+    addTheory(THEORY_REALS);
+    addTheory(THEORY_QUANTIFIERS);
+    break;
+
+  case UFLRA:
+    addOperator(kind::APPLY_UF);
+    addTheory(THEORY_REALS);
+    addTheory(THEORY_QUANTIFIERS);
+    break;
+  }
+}/* Smt1::setLogic() */
+
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
diff --git a/src/parser/smt1/smt1.h b/src/parser/smt1/smt1.h
new file mode 100644
index 000000000..f6c99da04
--- /dev/null
+++ b/src/parser/smt1/smt1.h
@@ -0,0 +1,125 @@
+/*********************                                                        */
+/*! \file smt1.h
+ ** \verbatim
+ ** Original author: cconway
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  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.\endverbatim
+ **
+ ** Definitions of SMT constants.
+ **/
+
+#include "cvc4parser_private.h"
+
+#ifndef __CVC4__PARSER__SMT1_H
+#define __CVC4__PARSER__SMT1_H
+
+#include <ext/hash_map>
+namespace std { using namespace __gnu_cxx; }
+
+#include "util/hash.h"
+#include "parser/parser.h"
+
+namespace CVC4 {
+
+class SExpr;
+
+namespace parser {
+
+class Smt1 : public Parser {
+  friend class ParserBuilder;
+
+public:
+  enum Logic {
+    AUFLIA, // +p and -p?
+    AUFLIRA,
+    AUFNIRA,
+    LRA,
+    QF_ABV,
+    QF_AUFBV,
+    QF_AUFBVLIA,
+    QF_AUFBVLRA,
+    QF_AUFLIA,
+    QF_AUFLIRA,
+    QF_AX,
+    QF_BV,
+    QF_IDL,
+    QF_LIA,
+    QF_LRA,
+    QF_NIA,
+    QF_NRA,
+    QF_RDL,
+    QF_SAT,
+    QF_UF,
+    QF_UFIDL,
+    QF_UFBV,
+    QF_UFLIA,
+    QF_UFNIA, // nonstandard
+    QF_UFLRA,
+    QF_UFLIRA, // nonstandard
+    QF_UFNIRA, // nonstandard
+    QF_UFNRA,
+    UFLRA,
+    UFNIRA, // nonstandard
+    UFNIA,
+    QF_ALL_SUPPORTED, // nonstandard
+    ALL_SUPPORTED // nonstandard
+  };
+
+  enum Theory {
+    THEORY_ARRAYS,
+    THEORY_ARRAYS_EX,
+    THEORY_BITVECTORS,
+    THEORY_BITVECTORS_32,
+    THEORY_BITVECTOR_ARRAYS_EX,
+    THEORY_EMPTY,
+    THEORY_INTS,
+    THEORY_INT_ARRAYS,
+    THEORY_INT_ARRAYS_EX,
+    THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX,
+    THEORY_REALS,
+    THEORY_REALS_INTS,
+    THEORY_QUANTIFIERS
+  };
+
+private:
+  bool d_logicSet;
+  Logic d_logic;
+
+protected:
+  Smt1(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false);
+
+public:
+  /**
+   * Add theory symbols to the parser state.
+   *
+   * @param theory the theory to open (e.g., Core, Ints)
+   */
+  void addTheory(Theory theory);
+
+  bool logicIsSet();
+
+  /**
+   * Sets the logic for the current benchmark. Declares any logic and theory symbols.
+   *
+   * @param name the name of the logic (e.g., QF_UF, AUFLIA)
+   */
+  void setLogic(const std::string& name);
+
+  static Logic toLogic(const std::string& name);
+
+private:
+
+  void addArithmeticOperators();
+  static std::hash_map<const std::string, Logic, CVC4::StringHashFunction> newLogicMap();
+};/* class Smt1 */
+
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__PARSER__SMT1_H */
diff --git a/src/parser/smt1/smt1_input.cpp b/src/parser/smt1/smt1_input.cpp
new file mode 100644
index 000000000..4987cd793
--- /dev/null
+++ b/src/parser/smt1/smt1_input.cpp
@@ -0,0 +1,73 @@
+/*********************                                                        */
+/*! \file smt1_input.cpp
+ ** \verbatim
+ ** Original author: cconway
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  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.\endverbatim
+ **
+ ** \brief [[ Add file-specific comments here ]].
+ **
+ ** [[ Add file-specific comments here ]]
+ **/
+
+#include <antlr3.h>
+
+#include "parser/smt1/smt1_input.h"
+#include "expr/expr_manager.h"
+#include "parser/input.h"
+#include "parser/parser.h"
+#include "parser/parser_exception.h"
+#include "parser/smt1/generated/Smt1Lexer.h"
+#include "parser/smt1/generated/Smt1Parser.h"
+
+namespace CVC4 {
+namespace parser {
+
+/* Use lookahead=2 */
+Smt1Input::Smt1Input(AntlrInputStream& inputStream) :
+  AntlrInput(inputStream, 2) {
+  pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream();
+  AlwaysAssert( input != NULL );
+
+  d_pSmt1Lexer = Smt1LexerNew(input);
+  if( d_pSmt1Lexer == NULL ) {
+    throw ParserException("Failed to create SMT lexer.");
+  }
+
+  setAntlr3Lexer( d_pSmt1Lexer->pLexer );
+
+  pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream();
+  AlwaysAssert( tokenStream != NULL );
+
+  d_pSmt1Parser = Smt1ParserNew(tokenStream);
+  if( d_pSmt1Parser == NULL ) {
+    throw ParserException("Failed to create SMT parser.");
+  }
+
+  setAntlr3Parser(d_pSmt1Parser->pParser);
+}
+
+
+Smt1Input::~Smt1Input() {
+  d_pSmt1Lexer->free(d_pSmt1Lexer);
+  d_pSmt1Parser->free(d_pSmt1Parser);
+}
+
+Command* Smt1Input::parseCommand()
+  throw (ParserException, TypeCheckingException, AssertionException) {
+  return d_pSmt1Parser->parseCommand(d_pSmt1Parser);
+}
+
+Expr Smt1Input::parseExpr()
+  throw (ParserException, TypeCheckingException, AssertionException) {
+  return d_pSmt1Parser->parseExpr(d_pSmt1Parser);
+}
+
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
diff --git a/src/parser/smt1/smt1_input.h b/src/parser/smt1/smt1_input.h
new file mode 100644
index 000000000..77d6f4b50
--- /dev/null
+++ b/src/parser/smt1/smt1_input.h
@@ -0,0 +1,96 @@
+/*********************                                                        */
+/*! \file smt_input.h
+ ** \verbatim
+ ** Original author: cconway
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  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.\endverbatim
+ **
+ ** \brief [[ Add file-specific comments here ]].
+ **
+ ** [[ Add file-specific comments here ]]
+ **/
+
+#include "cvc4parser_private.h"
+
+#ifndef __CVC4__PARSER__SMT1_INPUT_H
+#define __CVC4__PARSER__SMT1_INPUT_H
+
+#include "parser/antlr_input.h"
+#include "parser/smt1/generated/Smt1Lexer.h"
+#include "parser/smt1/generated/Smt1Parser.h"
+
+// extern void Smt1ParserSetAntlrParser(CVC4::parser::AntlrParser* newAntlrParser);
+
+namespace CVC4 {
+
+class Command;
+class Expr;
+class ExprManager;
+
+namespace parser {
+
+class Smt1Input : public AntlrInput {
+
+  /** The ANTLR3 SMT lexer for the input. */
+  pSmt1Lexer d_pSmt1Lexer;
+
+  /** The ANTLR3 CVC parser for the input. */
+  pSmt1Parser d_pSmt1Parser;
+
+public:
+
+  /**
+   * Create an input.
+   *
+   * @param inputStream the input stream to use
+   */
+  Smt1Input(AntlrInputStream& inputStream);
+
+  /** Destructor. Frees the lexer and the parser. */
+  virtual ~Smt1Input();
+
+  /** Get the language that this Input is reading. */
+  InputLanguage getLanguage() const throw() {
+    return language::input::LANG_SMTLIB_V1;
+  }
+
+protected:
+
+  /**
+   * Parse a command from the input. Returns <code>NULL</code> if
+   * there is no command there to parse.
+   *
+   * @throws ParserException if an error is encountered during parsing.
+   */
+  Command* parseCommand()
+    throw(ParserException, TypeCheckingException, AssertionException);
+
+  /**
+   * 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 parseExpr()
+    throw(ParserException, TypeCheckingException, AssertionException);
+
+private:
+
+  /**
+   * Initialize the class. Called from the constructors once the input
+   * stream is initialized.
+   */
+  void init();
+
+};/* class Smt1Input */
+
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__PARSER__SMT1_INPUT_H */