Merge from my post-smtcomp branch. Includes:

Dumping infrastructure.  Can dump preprocessed queries and clauses.  Can
also dump queries (for testing with another solver) to see if any conflicts
are missed, T-propagations are missed, all lemmas are T-valid, etc.  For a
full list of options see --dump=help.

CUDD building much cleaner.

Documentation and assertion fixes.

Printer improvements, printing of commands in language-defined way, etc.

Typechecker stuff in expr package now autogenerated, no need to manually
edit the expr package when adding a new theory.

CVC3 compatibility layer (builds as libcompat).

SWIG detection and language binding support (infrastructure).

Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode
(when not in compliance mode).

Copyright and file headers regenerated.

21 files changed, 331 insertions, 151 deletions

diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am
index 2b90da502..f1802c6c5 100644
--- a/src/parser/Makefile.am
+++ b/src/parser/Makefile.am
@@ -20,7 +20,9 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
 SUBDIRS = smt smt2 cvc
 
 nobase_lib_LTLIBRARIES = libcvc4parser.la
+if HAVE_CXXTESTGEN
 noinst_LTLIBRARIES = libcvc4parser_noinst.la
+endif
 
 libcvc4parser_la_LDFLAGS = $(ANTLR_LDFLAGS) \
 	-version-info $(LIBCVC4PARSER_VERSION)
diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index 74157acd7..c51d4b8c3 100644
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -5,7 +5,7 @@
  ** 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)
+ ** 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
diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h
index 4ae063266..913dd8013 100644
--- a/src/parser/antlr_input.h
+++ b/src/parser/antlr_input.h
@@ -3,9 +3,9 @@
  ** \verbatim
  ** Original author: cconway
  ** Major contributors: none
- ** Minor contributors (to current version): mdeters, dejan
+ ** 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)
+ ** 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
diff --git a/src/parser/bounded_token_factory.cpp b/src/parser/bounded_token_factory.cpp
index 5f42f0f29..71b8849e5 100644
--- a/src/parser/bounded_token_factory.cpp
+++ b/src/parser/bounded_token_factory.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: 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)
+ ** 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
diff --git a/src/parser/bounded_token_factory.h b/src/parser/bounded_token_factory.h
index 4d510c9e3..84697fd3e 100644
--- a/src/parser/bounded_token_factory.h
+++ b/src/parser/bounded_token_factory.h
@@ -5,7 +5,7 @@
  ** Major contributors: 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)
+ ** 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
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 75a59c6e0..1f817350c 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: cconway
  ** Major contributors: mdeters
- ** Minor contributors (to current version): dejan
+ ** Minor contributors (to current version): dejan, ajreynol
  ** 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
@@ -64,6 +64,7 @@ tokens {
   PRINT_TYPE_TOK = 'PRINT_TYPE';
   CALL_TOK = 'CALL';
   ECHO_TOK = 'ECHO';
+  EXIT_TOK = 'EXIT';
   INCLUDE_TOK = 'INCLUDE';
   DUMP_PROOF_TOK = 'DUMP_PROOF';
   DUMP_ASSUMPTIONS_TOK = 'DUMP_ASSUMPTIONS';
@@ -84,7 +85,6 @@ tokens {
 
   AND_TOK = 'AND';
   BOOLEAN_TOK = 'BOOLEAN';
-  ECHO_TOK = 'ECHO';
   ELSEIF_TOK = 'ELSIF';
   ELSE_TOK = 'ELSE';
   ENDIF_TOK = 'ENDIF';
@@ -448,38 +448,39 @@ namespace CVC4 {
       /**
        * This class is just here to get around an unfortunate bit of Antlr.
        * We use strings below as return values from rules, which require
-       * them to be constructible by a uintptr_t.  So we derive the string
+       * them to be constructible by a void*.  So we derive the string
        * class to provide just such a conversion.
        */
       class myString : public std::string {
       public:
         myString(const std::string& s) : std::string(s) {}
-        myString(uintptr_t) : std::string() {}
+        myString(void*) : std::string() {}
         myString() : std::string() {}
       };/* class myString */
 
       /**
-       * Just exists to give us the uintptr_t construction that
+       * Just exists to give us the void* construction that
        * ANTLR requires.
        */
       class mySubrangeBound : public CVC4::SubrangeBound {
       public:
         mySubrangeBound() : CVC4::SubrangeBound() {}
-        mySubrangeBound(uintptr_t) : CVC4::SubrangeBound() {}
+        mySubrangeBound(void*) : CVC4::SubrangeBound() {}
         mySubrangeBound(const Integer& i) : CVC4::SubrangeBound(i) {}
         mySubrangeBound(const SubrangeBound& b) : CVC4::SubrangeBound(b) {}
       };/* class mySubrangeBound */
 
       /**
-       * Just exists to give us the uintptr_t construction that
+       * Just exists to give us the void* construction that
        * ANTLR requires.
        */
       struct myExpr : public CVC4::Expr {
         myExpr() : CVC4::Expr() {}
-        myExpr(uintptr_t) : CVC4::Expr() {}
+        myExpr(void*) : CVC4::Expr() {}
         myExpr(const Expr& e) : CVC4::Expr(e) {}
         myExpr(const myExpr& e) : CVC4::Expr(e) {}
       };/* struct myExpr */
+
     }/* CVC4::parser::cvc namespace */
   }/* CVC4::parser namespace */
 }/* CVC4 namespace */
@@ -532,7 +533,7 @@ using namespace CVC4::parser;
  * Parses an expression.
  * @return the parsed expression
  */
-parseExpr returns [CVC4::parser::cvc::myExpr expr]
+parseExpr returns [CVC4::Expr expr = CVC4::Expr()]
   : formula[expr]
   | EOF
   ;
@@ -541,7 +542,7 @@ parseExpr returns [CVC4::parser::cvc::myExpr expr]
  * Parses a command (the whole benchmark)
  * @return the command of the benchmark
  */
-parseCommand returns [CVC4::Command* cmd]
+parseCommand returns [CVC4::Command* cmd = NULL]
   : c=command { $cmd = c; }
   | EOF { $cmd = NULL; }
   ;
@@ -580,7 +581,6 @@ mainCommand[CVC4::Command*& cmd]
   std::vector<CVC4::Datatype> dts;
   Debug("parser-extra") << "command: " << AntlrInput::tokenText(LT(1)) << std::endl;
   std::string s;
-  k = 0;
 }
     /* our bread & butter */
   : ASSERT_TOK formula[f] { cmd = new AssertCommand(f); }
@@ -696,6 +696,9 @@ mainCommand[CVC4::Command*& cmd]
     | { Message() << std::endl; }
     )
 
+  | EXIT_TOK
+    { cmd = new QuitCommand(); }
+
   | INCLUDE_TOK
     ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } )
       { UNSUPPORTED("INCLUDE command"); }
@@ -752,15 +755,15 @@ toplevelDeclaration[CVC4::Command*& cmd]
   Debug("parser-extra") << "declaration: " << AntlrInput::tokenText(LT(1)) << std::endl;
 }
   : identifierList[ids,CHECK_NONE,SYM_VARIABLE] COLON
-    ( declareVariables[t,ids,true] { cmd = new DeclarationCommand(ids, t); }
-    | declareTypes[ids] { cmd = new DeclarationCommand(ids, EXPR_MANAGER->kindType()); } )
+    ( declareVariables[cmd,t,ids,true]
+    | declareTypes[cmd,ids] )
   ;
 
 /**
  * A bound variable declaration.
  */
 boundVarDecl[std::vector<std::string>& ids, CVC4::Type& t]
-  : identifierList[ids,CHECK_NONE,SYM_VARIABLE] COLON declareVariables[t,ids,false]
+  : identifierList[ids,CHECK_NONE,SYM_VARIABLE] COLON declareVariables[*(Command**)NULL,t,ids,false]
   ;
 
 /**
@@ -808,13 +811,14 @@ boundVarDeclReturn[std::vector<CVC4::Expr>& terms,
  * because type declarations are always top-level, except for
  * type-lets, which don't use this rule.
  */
-declareTypes[const std::vector<std::string>& idList]
+declareTypes[CVC4::Command*& cmd, const std::vector<std::string>& idList]
 @init {
   Type t;
 }
     /* A sort declaration (e.g., "T : TYPE") */
   : TYPE_TOK
-    { for(std::vector<std::string>::const_iterator i = idList.begin();
+    { DeclarationSequence* seq = new DeclarationSequence();
+      for(std::vector<std::string>::const_iterator i = idList.begin();
           i != idList.end();
           ++i) {
         // Don't allow a type variable to clash with a previously
@@ -822,8 +826,11 @@ declareTypes[const std::vector<std::string>& idList]
         // non-type variable can clash unambiguously.  Break from CVC3
         // behavior here.
         PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_SORT);
+        Type sort = PARSER_STATE->mkSort(*i);
+        Command* decl = new DeclareTypeCommand(*i, 0, sort);
+        seq->addCommand(decl);
       }
-      PARSER_STATE->mkSorts(idList);
+      cmd = seq;
     }
 
     /* A type alias "T : TYPE = foo..." */
@@ -843,16 +850,20 @@ declareTypes[const std::vector<std::string>& idList]
  * re-declared if topLevel is true (CVC allows re-declaration if the
  * types are compatible---if they aren't compatible, an error is
  * thrown).  Also if topLevel is true, variable definitions are
- * permitted.
+ * permitted and "cmd" is output.
  */
-declareVariables[CVC4::Type& t, const std::vector<std::string>& idList, bool topLevel]
+declareVariables[CVC4::Command*& cmd, CVC4::Type& t, const std::vector<std::string>& idList, bool topLevel]
 @init {
   Expr f;
   Debug("parser-extra") << "declType: " << AntlrInput::tokenText(LT(1)) << std::endl;
 }
     /* A variable declaration (or definition) */
   : type[t,CHECK_DECLARED] ( EQUAL_TOK formula[f] )?
-    { if(f.isNull()) {
+    { DeclarationSequence* seq = NULL;
+      if(topLevel) {
+        cmd = seq = new DeclarationSequence();
+      }
+      if(f.isNull()) {
         Debug("parser") << "working on " << idList.front() << " : " << t << std::endl;
         // CVC language allows redeclaration of variables if types are the same
         for(std::vector<std::string>::const_iterator i = idList.begin(),
@@ -877,6 +888,10 @@ declareVariables[CVC4::Type& t, const std::vector<std::string>& idList, bool top
           } else {
             Debug("parser") << "  " << *i << " not declared" << std::endl;
             PARSER_STATE->mkVar(*i, t);
+            if(topLevel) {
+              Command* decl = new DeclareFunctionCommand(*i, t);
+              seq->addCommand(decl);
+            }
           }
         }
       } else {
@@ -892,6 +907,8 @@ declareVariables[CVC4::Type& t, const std::vector<std::string>& idList, bool top
             ++i) {
           PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_VARIABLE);
           PARSER_STATE->defineFunction(*i, f);
+          Command* decl = new DefineFunctionCommand(*i, Expr(), f);
+          seq->addCommand(decl);
         }
       }
     }
@@ -1007,10 +1024,10 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t,
     /* named types */
   : identifier[id,check,SYM_SORT]
     parameterization[check,types]?
-    { 
+    {
       if(check == CHECK_DECLARED ||
          PARSER_STATE->isDeclared(id, SYM_SORT)) {
-        Debug("parser-param") << "param: getSort " << id << " " << types.size() << " " << PARSER_STATE->getArity( id ) 
+        Debug("parser-param") << "param: getSort " << id << " " << types.size() << " " << PARSER_STATE->getArity( id )
                               << " " << PARSER_STATE->isDeclared(id, SYM_SORT) << std::endl;
         if( types.size()>0 ){
           t = PARSER_STATE->getSort(id, types);
@@ -1024,7 +1041,7 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t,
         }else{
           t = PARSER_STATE->mkUnresolvedTypeConstructor(id,types);
           t = SortConstructorType(t).instantiate( types );
-          Debug("parser-param") << "param: make unres param type " << id << " " << types.size() << " " 
+          Debug("parser-param") << "param: make unres param type " << id << " " << types.size() << " "
                                 << PARSER_STATE->getArity( id ) << std::endl;
         }
       }
@@ -1095,7 +1112,7 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t,
     }
   ;
 
-parameterization[CVC4::parser::DeclarationCheck check, 
+parameterization[CVC4::parser::DeclarationCheck check,
                  std::vector<CVC4::Type>& params]
 @init {
   Type t;
@@ -1146,7 +1163,7 @@ formula[CVC4::Expr& f]
   ;
 
 morecomparisons[std::vector<CVC4::Expr>& expressions,
-                std::vector<unsigned>& operators] returns [size_t i]
+                std::vector<unsigned>& operators] returns [size_t i = 0]
 @init {
   unsigned op;
   Expr f;
@@ -1165,10 +1182,7 @@ morecomparisons[std::vector<CVC4::Expr>& expressions,
   ;
 
 /** Matches 0 or more NOTs. */
-nots returns [size_t n]
-@init {
-  $n = 0;
-}
+nots returns [size_t n = 0]
   : ( NOT_TOK { ++$n; } )*
   ;
 
@@ -1208,8 +1222,9 @@ prefixFormula[CVC4::Expr& f]
     RPAREN COLON formula[f]
     { PARSER_STATE->popScope();
       Type t = EXPR_MANAGER->mkFunctionType(types, f.getType());
-      Expr func = PARSER_STATE->mkAnonymousFunction("lambda", t);
-      Command* cmd = new DefineFunctionCommand(func, terms, f);
+      std::string name = "lambda";
+      Expr func = PARSER_STATE->mkAnonymousFunction(name, t);
+      Command* cmd = new DefineFunctionCommand(name, func, terms, f);
       PARSER_STATE->preemptCommand(cmd);
       f = func;
     }
@@ -1735,17 +1750,18 @@ datatypeDef[std::vector<CVC4::Datatype>& datatypes]
   Type t;
   std::vector< Type > params;
 }
-    /* This really needs to be CHECK_NONE, or mutually-recursive datatypes
-     * won't work, because this type will already be "defined" as an
-     * unresolved type; don't worry, we check below. */
+    /* This really needs to be CHECK_NONE, or mutually-recursive
+     * datatypes won't work, because this type will already be
+     * "defined" as an unresolved type; don't worry, we check
+     * below. */
   : identifier[id,CHECK_NONE,SYM_SORT] { PARSER_STATE->pushScope(); }
-    ( LBRACKET identifier[id2,CHECK_UNDECLARED,SYM_SORT] { 
+    ( LBRACKET identifier[id2,CHECK_UNDECLARED,SYM_SORT] {
         t = PARSER_STATE->mkSort(id2);
-        params.push_back( t ); 
+        params.push_back( t );
       }
-      ( COMMA identifier[id2,CHECK_UNDECLARED,SYM_SORT] { 
+      ( COMMA identifier[id2,CHECK_UNDECLARED,SYM_SORT] {
         t = PARSER_STATE->mkSort(id2);
-        params.push_back( t ); } 
+        params.push_back( t ); }
       )* RBRACKET
     )?
     { datatypes.push_back(Datatype(id,params));
@@ -1768,8 +1784,7 @@ constructorDef[CVC4::Datatype& type]
   CVC4::Datatype::Constructor* ctor = NULL;
 }
   : identifier[id,CHECK_UNDECLARED,SYM_SORT]
-    {
-      // make the tester
+    { // make the tester
       std::string testerId("is_");
       testerId.append(id);
       PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_SORT);
@@ -1826,7 +1841,7 @@ DECIMAL_LITERAL
  * in the BVPLUS/BVMINUS/BVMULT rules where $INTEGER_LITERAL was
  * returning a reference to the wrong token?!
  */
-numeral returns [unsigned k]
+numeral returns [unsigned k = 0]
   : INTEGER_LITERAL
     { $k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL); }
   ;
@@ -1834,7 +1849,7 @@ numeral returns [unsigned k]
 /**
  * Similar to numeral but for arbitrary-precision, signed integer.
  */
-integer returns [CVC4::Integer k]
+integer returns [CVC4::Integer k = 0]
   : INTEGER_LITERAL
     { $k = AntlrInput::tokenToInteger($INTEGER_LITERAL); }
   | MINUS_TOK INTEGER_LITERAL
diff --git a/src/parser/cvc/cvc_input.cpp b/src/parser/cvc/cvc_input.cpp
index 541ac0eac..d91a13bee 100644
--- a/src/parser/cvc/cvc_input.cpp
+++ b/src/parser/cvc/cvc_input.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: 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)
+ ** 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
diff --git a/src/parser/cvc/cvc_input.h b/src/parser/cvc/cvc_input.h
index efe0a522f..9a1f24fde 100644
--- a/src/parser/cvc/cvc_input.h
+++ b/src/parser/cvc/cvc_input.h
@@ -5,7 +5,7 @@
  ** Major contributors: 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)
+ ** 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
diff --git a/src/parser/input.cpp b/src/parser/input.cpp
index 36e96516f..27b207342 100644
--- a/src/parser/input.cpp
+++ b/src/parser/input.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: mdeters, cconway
  ** 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)
+ ** 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
diff --git a/src/parser/memory_mapped_input_buffer.cpp b/src/parser/memory_mapped_input_buffer.cpp
index aad5aaec0..dad38c913 100644
--- a/src/parser/memory_mapped_input_buffer.cpp
+++ b/src/parser/memory_mapped_input_buffer.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: 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)
+ ** 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
diff --git a/src/parser/memory_mapped_input_buffer.h b/src/parser/memory_mapped_input_buffer.h
index 18618a090..ccbe04059 100644
--- a/src/parser/memory_mapped_input_buffer.h
+++ b/src/parser/memory_mapped_input_buffer.h
@@ -5,7 +5,7 @@
  ** Major contributors: 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)
+ ** 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
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 78e70572a..3f2ec107a 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: dejan
  ** Major contributors: cconway, mdeters
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): ajreynol
  ** 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
@@ -227,15 +227,6 @@ Parser::mkSortConstructor(const std::string& name, size_t arity) {
   return type;
 }
 
-std::vector<SortType>
-Parser::mkSorts(const std::vector<std::string>& names) {
-  std::vector<SortType> types;
-  for(unsigned i = 0; i < names.size(); ++i) {
-    types.push_back(mkSort(names[i]));
-  }
-  return types;
-}
-
 SortType Parser::mkUnresolvedType(const std::string& name) {
   SortType unresolved = mkSort(name);
   d_unresolved.insert(unresolved);
@@ -243,7 +234,7 @@ SortType Parser::mkUnresolvedType(const std::string& name) {
 }
 
 SortConstructorType
-Parser::mkUnresolvedTypeConstructor(const std::string& name, 
+Parser::mkUnresolvedTypeConstructor(const std::string& name,
                                     size_t arity) {
   SortConstructorType unresolved = mkSortConstructor(name,arity);
   d_unresolved.insert(unresolved);
@@ -251,7 +242,7 @@ Parser::mkUnresolvedTypeConstructor(const std::string& name,
 }
 
 SortConstructorType
-Parser::mkUnresolvedTypeConstructor(const std::string& name, 
+Parser::mkUnresolvedTypeConstructor(const std::string& name,
                                     const std::vector<Type>& params) {
   Debug("parser") << "newSortConstructor(P)(" << name << ", " << params.size() << ")"
                   << std::endl;
@@ -356,13 +347,15 @@ void Parser::checkDeclaration(const std::string& varName,
   switch(check) {
   case CHECK_DECLARED:
     if( !isDeclared(varName, type) ) {
-      parseError("Symbol " + varName + " not declared as a " + (type == SYM_VARIABLE ? "variable" : "type"));
+      parseError("Symbol " + varName + " not declared as a " +
+                 (type == SYM_VARIABLE ? "variable" : "type"));
     }
     break;
 
   case CHECK_UNDECLARED:
     if( isDeclared(varName, type) ) {
-      parseError("Symbol " + varName + " previously declared as a " + (type == SYM_VARIABLE ? "variable" : "type"));
+      parseError("Symbol " + varName + " previously declared as a " +
+                 (type == SYM_VARIABLE ? "variable" : "type"));
     }
     break;
 
diff --git a/src/parser/parser.h b/src/parser/parser.h
index b2f76b39d..5ce016b85 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: cconway
  ** Major contributors: mdeters
- ** Minor contributors (to current version): dejan
+ ** Minor contributors (to current version): dejan, ajreynol
  ** 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
@@ -368,11 +368,6 @@ public:
   SortConstructorType mkSortConstructor(const std::string& name, size_t arity);
 
   /**
-   * Creates new sorts with the given names (all of arity 0).
-   */
-  std::vector<SortType> mkSorts(const std::vector<std::string>& names);
-
-  /**
    * Creates a new "unresolved type," used only during parsing.
    */
   SortType mkUnresolvedType(const std::string& name);
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index 2a3a79125..da20c68a2 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -2,7 +2,7 @@
 /*! \file Smt.g
  ** \verbatim
  ** Original author: cconway
- ** Major contributors: mdeters, dejan
+ ** 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)
@@ -143,7 +143,7 @@ parseExpr returns [CVC4::parser::smt::myExpr expr]
  * Parses a command (the whole benchmark)
  * @return the command of the benchmark
  */
-parseCommand returns [CVC4::Command* cmd]
+parseCommand returns [CVC4::Command* cmd = NULL]
   : b = benchmark { $cmd = b; }
   ;
 
@@ -151,7 +151,7 @@ parseCommand returns [CVC4::Command* cmd]
  * Matches the whole SMT-LIB benchmark.
  * @return the sequence command containing the whole problem
  */
-benchmark returns [CVC4::Command* cmd]
+benchmark returns [CVC4::Command* cmd = NULL]
   : LPAREN_TOK BENCHMARK_TOK IDENTIFIER c = benchAttributes RPAREN_TOK
   	{ $cmd = c; }
   | EOF { $cmd = 0; }
@@ -162,7 +162,7 @@ benchmark returns [CVC4::Command* cmd]
  * command sequence.
  * @return the command sequence
  */
-benchAttributes returns [CVC4::CommandSequence* cmd_seq]
+benchAttributes returns [CVC4::CommandSequence* cmd_seq = NULL]
 @init {
   cmd_seq = new CommandSequence();
 }
@@ -174,26 +174,42 @@ benchAttributes returns [CVC4::CommandSequence* cmd_seq]
  * a corresponding command
  * @return a command corresponding to the attribute
  */
-benchAttribute returns [CVC4::Command* smt_command]
+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->setLogic(name);
-      smt_command = new SetBenchmarkLogicCommand(name);   }
+    { PARSER_STATE->preemptCommand(new SetBenchmarkLogicCommand(name));
+      PARSER_STATE->setLogic(name);
+      smt_command = new EmptyCommand();
+    }
   | ASSUMPTION_TOK annotatedFormula[expr]
-    { smt_command = new AssertCommand(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 (functionDeclaration)+ RPAREN_TOK
-  | EXTRAPREDS_TOK LPAREN_TOK (predicateDeclaration)+ RPAREN_TOK
-  | EXTRASORTS_TOK LPAREN_TOK sortDeclaration+ RPAREN_TOK
+  | 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
-  | annotation
+    { smt_command = new CommentCommand(AntlrInput::tokenText($STRING_LITERAL)); }
+  | annotation[smt_command]
   ;
 
 /**
@@ -417,11 +433,12 @@ functionSymbol[CVC4::Expr& fun]
 /**
  * Matches an attribute name from the input (:attribute_name).
  */
-attribute
+attribute[std::string& s]
   :  ATTR_IDENTIFIER
+    { s = AntlrInput::tokenText($ATTR_IDENTIFIER); }
   ;
 
-functionDeclaration
+functionDeclaration[CVC4::Command*& smt_command]
 @declarations {
   std::string name;
   std::vector<Type> sorts;
@@ -435,13 +452,15 @@ functionDeclaration
       } else {
         t = EXPR_MANAGER->mkFunctionType(sorts);
       }
-      PARSER_STATE->mkVar(name, t); }
+      PARSER_STATE->mkVar(name, t);
+      smt_command = new DeclareFunctionCommand(name, t);
+    }
   ;
 
 /**
  * Matches the declaration of a predicate and declares it
  */
-predicateDeclaration
+predicateDeclaration[CVC4::Command*& smt_command]
 @declarations {
   std::string name;
   std::vector<Type> p_sorts;
@@ -453,16 +472,20 @@ predicateDeclaration
       } else {
         t = EXPR_MANAGER->mkPredicateType(p_sorts);
       }
-      PARSER_STATE->mkVar(name, t); }
+      PARSER_STATE->mkVar(name, t);
+      smt_command = new DeclareFunctionCommand(name, t);
+    }
   ;
 
-sortDeclaration
+sortDeclaration[CVC4::Command*& smt_command]
 @declarations {
   std::string name;
 }
   : sortName[name,CHECK_UNDECLARED]
     { Debug("parser") << "sort decl: '" << name << "'" << std::endl;
-      PARSER_STATE->mkSort(name); }
+      Type type = PARSER_STATE->mkSort(name);
+      smt_command = new DeclareTypeCommand(name, 0, type);
+    }
   ;
 
 /**
@@ -503,8 +526,19 @@ status[ CVC4::BenchmarkStatus& status ]
 /**
  * Matches an annotation, which is an attribute name, with an optional user
  */
-annotation
-  : attribute (USER_VALUE)?
+annotation[CVC4::Command*& smt_command]
+@init {
+  std::string key;
+  smt_command = NULL;
+}
+  : attribute[key]
+    ( USER_VALUE
+      { smt_command = new SetInfoCommand(key, AntlrInput::tokenText($USER_VALUE)); }
+    )?
+    { if(smt_command == NULL) {
+        smt_command = new EmptyCommand(std::string("annotation: ") + key);
+      }
+    }
   ;
 
 /**
@@ -676,21 +710,20 @@ FLET_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.
+ * 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();; }
+  : (' ' | '\t' | '\f' | '\r' | '\n')+
+    { SKIP(); }
   ;
 
 /**
@@ -716,7 +749,8 @@ STRING_LITERAL
  * Matches the comments and ignores them
  */
 COMMENT
-  : ';' (~('\n' | '\r'))*                    { SKIP();; }
+  : ';' (~('\n' | '\r'))*
+    { SKIP(); }
   ;
 
 
diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp
index a8dabeffe..a6e716b77 100644
--- a/src/parser/smt/smt.cpp
+++ b/src/parser/smt/smt.cpp
@@ -2,8 +2,8 @@
 /*! \file smt.cpp
  ** \verbatim
  ** Original author: cconway
- ** Major contributors: none
- ** Minor contributors (to current version): dejan, mdeters
+ ** 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
@@ -20,6 +20,7 @@ namespace std {
 }
 
 #include "expr/type.h"
+#include "expr/command.h"
 #include "parser/parser.h"
 #include "parser/smt/smt.h"
 
@@ -80,6 +81,10 @@ void Smt::addTheory(Theory theory) {
   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));
 
@@ -88,9 +93,11 @@ void Smt::addTheory(Theory theory) {
     break;
   }
 
-  case THEORY_EMPTY:
-    mkSort("U");
+  case THEORY_EMPTY: {
+    Type sort = mkSort("U");
+    preemptCommand(new DeclareTypeCommand("U", 0, sort));
     break;
+  }
 
   case THEORY_REALS_INTS:
     defineType("Real", getExprManager()->realType());
diff --git a/src/parser/smt/smt.h b/src/parser/smt/smt.h
index 98ebf6410..11a30c2fc 100644
--- a/src/parser/smt/smt.h
+++ b/src/parser/smt/smt.h
@@ -2,8 +2,8 @@
 /*! \file smt.h
  ** \verbatim
  ** Original author: cconway
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
+ ** 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
diff --git a/src/parser/smt/smt_input.cpp b/src/parser/smt/smt_input.cpp
index d062683d3..d368339f5 100644
--- a/src/parser/smt/smt_input.cpp
+++ b/src/parser/smt/smt_input.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: 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)
+ ** 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
diff --git a/src/parser/smt/smt_input.h b/src/parser/smt/smt_input.h
index 2fb037f06..b976a3b6a 100644
--- a/src/parser/smt/smt_input.h
+++ b/src/parser/smt/smt_input.h
@@ -5,7 +5,7 @@
  ** Major contributors: 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)
+ ** 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
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 091e6c93c..5ae04adea 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -143,7 +143,7 @@ parseExpr returns [CVC4::parser::smt2::myExpr expr]
  * Parses a command
  * @return the parsed command, or NULL if we've reached the end of the input
  */
-parseCommand returns [CVC4::Command* cmd]
+parseCommand returns [CVC4::Command* cmd = NULL]
   : LPAREN_TOK c = command RPAREN_TOK { $cmd = c; }
   | EOF { $cmd = 0; }
   ;
@@ -151,7 +151,7 @@ parseCommand returns [CVC4::Command* cmd]
 /**
  * Parse the internal portion of the command, ignoring the surrounding parentheses.
  */
-command returns [CVC4::Command* cmd]
+command returns [CVC4::Command* cmd = NULL]
 @declarations {
   std::string name;
   std::vector<std::string> names;
@@ -192,11 +192,11 @@ command returns [CVC4::Command* cmd]
                       << "' arity=" << n << std::endl;
       unsigned arity = AntlrInput::tokenToUnsigned(n);
       if(arity == 0) {
-        PARSER_STATE->mkSort(name);
-        $cmd = new DeclarationCommand(name, EXPR_MANAGER->kindType());
+        Type type = PARSER_STATE->mkSort(name);
+        $cmd = new DeclareTypeCommand(name, 0, type);
       } else {
-        PARSER_STATE->mkSortConstructor(name, arity);
-        $cmd = new DeclarationCommand(name, EXPR_MANAGER->kindType());
+        Type type = PARSER_STATE->mkSortConstructor(name, arity);
+        $cmd = new DeclareTypeCommand(name, arity, type);
       }
     }
   | /* sort definition */
@@ -216,7 +216,7 @@ command returns [CVC4::Command* cmd]
       // Do NOT call mkSort, since that creates a new sort!
       // This name is not its own distinct sort, it's an alias.
       PARSER_STATE->defineParameterizedType(name, sorts, t);
-      $cmd = new EmptyCommand;
+      $cmd = new DefineTypeCommand(name, sorts, t);
     }
   | /* function declaration */
     DECLARE_FUN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
@@ -227,7 +227,7 @@ command returns [CVC4::Command* cmd]
         t = EXPR_MANAGER->mkFunctionType(sorts, t);
       }
       PARSER_STATE->mkVar(name, t);
-      $cmd = new DeclarationCommand(name,t); }
+      $cmd = new DeclareFunctionCommand(name, t); }
   | /* function definition */
     DEFINE_FUN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
     LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
@@ -259,10 +259,16 @@ command returns [CVC4::Command* cmd]
       // must not be extended with the name itself; no recursion
       // permitted)
       Expr func = PARSER_STATE->mkFunction(name, t);
-      $cmd = new DefineFunctionCommand(func, terms, expr);
+      $cmd = new DefineFunctionCommand(name, func, terms, expr);
     }
   | /* value query */
-    GET_VALUE_TOK LPAREN_TOK termList[terms,expr] RPAREN_TOK
+    ( GET_VALUE_TOK |
+      EVAL_TOK
+      { if(PARSER_STATE->strictModeEnabled()) {
+          PARSER_STATE->parseError("Strict compliance mode doesn't recognize \"eval\".  Maybe you want (get-value...)?");
+        }
+      } )
+    LPAREN_TOK termList[terms,expr] RPAREN_TOK
     { if(terms.size() == 1) {
         $cmd = new GetValueCommand(terms[0]);
       } else {
@@ -289,36 +295,86 @@ command returns [CVC4::Command* cmd]
     GET_ASSERTIONS_TOK
     { cmd = new GetAssertionsCommand; }
   | /* push */
-    PUSH_TOK k=INTEGER_LITERAL
-    { unsigned n = AntlrInput::tokenToUnsigned(k);
-      if(n == 0) {
-        cmd = new EmptyCommand;
-      } else if(n == 1) {
-        cmd = new PushCommand;
-      } else {
-        CommandSequence* seq = new CommandSequence;
-        do {
-          seq->addCommand(new PushCommand);
-        } while(--n > 0);
-        cmd = seq;
+    PUSH_TOK
+    ( k=INTEGER_LITERAL
+      { unsigned n = AntlrInput::tokenToUnsigned(k);
+        if(n == 0) {
+          cmd = new EmptyCommand;
+        } else if(n == 1) {
+          cmd = new PushCommand;
+        } else {
+          CommandSequence* seq = new CommandSequence;
+          do {
+            seq->addCommand(new PushCommand);
+          } while(--n > 0);
+          cmd = seq;
+        }
       }
-    }
-  | POP_TOK k=INTEGER_LITERAL
-    { unsigned n = AntlrInput::tokenToUnsigned(k);
-      if(n == 0) {
-        cmd = new EmptyCommand;
-      } else if(n == 1) {
-        cmd = new PopCommand;
-      } else {
-        CommandSequence* seq = new CommandSequence;
-        do {
-          seq->addCommand(new PopCommand);
-        } while(--n > 0);
-        cmd = seq;
+    | { if(PARSER_STATE->strictModeEnabled()) {
+          PARSER_STATE->parseError("Strict compliance mode demands an integer to be provided to PUSH.  Maybe you want (push 1)?");
+        } else {
+          cmd = new PushCommand;
+        }
+      } )
+  | POP_TOK
+    ( k=INTEGER_LITERAL
+      { unsigned n = AntlrInput::tokenToUnsigned(k);
+        if(n == 0) {
+          cmd = new EmptyCommand;
+        } else if(n == 1) {
+          cmd = new PopCommand;
+        } else {
+          CommandSequence* seq = new CommandSequence;
+          do {
+            seq->addCommand(new PopCommand);
+          } while(--n > 0);
+          cmd = seq;
+        }
       }
-    }
+    | { if(PARSER_STATE->strictModeEnabled()) {
+          PARSER_STATE->parseError("Strict compliance mode demands an integer to be provided to POP.  Maybe you want (pop 1)?");
+        } else {
+          cmd = new PopCommand;
+        }
+      } )
   | EXIT_TOK
     { cmd = new QuitCommand; }
+
+    /* CVC4-extended SMT-LIBv2 commands */
+  | extendedCommand[cmd]
+    { if(PARSER_STATE->strictModeEnabled()) {
+        PARSER_STATE->parseError("Extended commands are not permitted while operating in strict compliance mode.");
+      }
+    }
+  ;
+
+extendedCommand[CVC4::Command*& cmd]
+@declarations {
+  std::vector<CVC4::Datatype> dts;
+  Expr e;
+}
+    /* Z3's extended SMT-LIBv2 set of commands syntax */
+  : DECLARE_DATATYPES_TOK
+    { /* open a scope to keep the UnresolvedTypes contained */
+      PARSER_STATE->pushScope(); }
+    LPAREN_TOK ( LPAREN_TOK datatypeDef[dts] RPAREN_TOK )+ RPAREN_TOK
+    { PARSER_STATE->popScope();
+      cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); }
+
+    
+  | DECLARE_SORTS_TOK
+  | DECLARE_FUNS_TOK
+  | DECLARE_PREDS_TOK
+  | DEFINE_TOK
+  | DEFINE_SORTS_TOK
+  | DECLARE_CONST_TOK
+    
+  | SIMPLIFY_TOK term[e]
+    { cmd = new SimplifyCommand(e); }
+  | ECHO_TOK
+    ( STRING_LITERAL
+      { Message() << AntlrInput::tokenText($STRING_LITERAL) << std::endl; }
+    | { Message() << std::endl; } )
   ;
 
 symbolicExpr[CVC4::SExpr& sexpr]
@@ -441,7 +497,7 @@ term[CVC4::Expr& expr]
         Expr func = PARSER_STATE->mkFunction(name, expr.getType());
         // bind name to expr with define-fun
         Command* c =
-          new DefineNamedFunctionCommand(func, std::vector<Expr>(), expr);
+          new DefineNamedFunctionCommand(name, func, std::vector<Expr>(), expr);
         PARSER_STATE->preemptCommand(c);
       } else {
         std::stringstream ss;
@@ -716,6 +772,73 @@ nonemptyNumeralList[std::vector<uint64_t>& numerals]
     )+
   ;
 
+/**
+ * Parses a datatype definition
+ */
+datatypeDef[std::vector<CVC4::Datatype>& datatypes]
+@init {
+  std::string id, id2;
+  Type t;
+  std::vector< Type > params;
+}
+    /* This really needs to be CHECK_NONE, or mutually-recursive
+     * datatypes won't work, because this type will already be
+     * "defined" as an unresolved type; don't worry, we check
+     * below. */
+  : symbol[id,CHECK_NONE,SYM_SORT] { PARSER_STATE->pushScope(); }
+    ( '[' symbol[id2,CHECK_UNDECLARED,SYM_SORT] {
+        t = PARSER_STATE->mkSort(id2);
+        params.push_back( t );
+      }
+      ( symbol[id2,CHECK_UNDECLARED,SYM_SORT] {
+        t = PARSER_STATE->mkSort(id2);
+        params.push_back( t ); }
+      )* ']'
+    )?
+    { datatypes.push_back(Datatype(id,params));
+      if(!PARSER_STATE->isUnresolvedType(id)) {
+        // if not unresolved, must be undeclared
+        PARSER_STATE->checkDeclaration(id, CHECK_UNDECLARED, SYM_SORT);
+      }
+    }
+    ( LPAREN_TOK constructorDef[datatypes.back()] RPAREN_TOK )+
+    { PARSER_STATE->popScope(); }
+  ;
+
+/**
+ * Parses a constructor defintion for type
+ */
+constructorDef[CVC4::Datatype& type]
+@init {
+  std::string id;
+  CVC4::Datatype::Constructor* ctor = NULL;
+}
+  : symbol[id,CHECK_UNDECLARED,SYM_SORT]
+    { // make the tester
+      std::string testerId("is_");
+      testerId.append(id);
+      PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_SORT);
+      ctor = new CVC4::Datatype::Constructor(id, testerId);
+    }
+    ( LPAREN_TOK selector[*ctor] RPAREN_TOK )*
+    { // make the constructor
+      type.addConstructor(*ctor);
+      Debug("parser-idt") << "constructor: " << id.c_str() << std::endl;
+      delete ctor;
+    }
+  ;
+
+selector[CVC4::Datatype::Constructor& ctor]
+@init {
+  std::string id;
+  Type t, t2;
+}
+  : symbol[id,CHECK_UNDECLARED,SYM_SORT] sortSymbol[t]
+    { ctor.addArg(id, t);
+      Debug("parser-idt") << "selector: " << id.c_str() << std::endl;
+    }
+  ;
+
 // Base SMT-LIB tokens
 ASSERT_TOK : 'assert';
 CHECKSAT_TOK : 'check-sat';
@@ -741,6 +864,18 @@ GET_OPTION_TOK : 'get-option';
 PUSH_TOK : 'push';
 POP_TOK : 'pop';
 
+// extended commands
+DECLARE_DATATYPES_TOK : 'declare-datatypes';
+DECLARE_SORTS_TOK : 'declare-sorts';
+DECLARE_FUNS_TOK : 'declare-funs';
+DECLARE_PREDS_TOK : 'declare-preds';
+DEFINE_TOK : 'define';
+DEFINE_SORTS_TOK : 'define-sorts';
+DECLARE_CONST_TOK : 'declare-const';
+SIMPLIFY_TOK : 'simplify';
+EVAL_TOK : 'eval';
+ECHO_TOK : 'echo';
+
 // operators (NOTE: theory symbols go here)
 AMPERSAND_TOK     : '&';
 AND_TOK           : 'and';
@@ -759,7 +894,6 @@ MINUS_TOK         : '-';
 NOT_TOK           : 'not';
 OR_TOK            : 'or';
 PERCENT_TOK       : '%';
-PIPE_TOK          : '|';
 PLUS_TOK          : '+';
 POUND_TOK         : '#';
 SELECT_TOK        : 'select';
diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp
index 9a349785c..acd0e17f6 100644
--- a/src/parser/smt2/smt2_input.cpp
+++ b/src/parser/smt2/smt2_input.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: 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)
+ ** 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
diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h
index 04fe48fe1..05a62c30d 100644
--- a/src/parser/smt2/smt2_input.h
+++ b/src/parser/smt2/smt2_input.h
@@ -2,10 +2,10 @@
 /*! \file smt2_input.h
  ** \verbatim
  ** Original author: cconway
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
+ ** Major contributors: 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)
+ ** 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