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.

31 files changed, 655 insertions, 379 deletions

diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index 352647642..738604f90 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -16,6 +16,7 @@ libexpr_la_SOURCES = \
 	type.cpp \
 	node_value.h \
 	node_manager.h \
+	type_checker.h \
 	attribute.h \
 	attribute_internals.h \
 	attribute.cpp \
@@ -37,7 +38,8 @@ nodist_libexpr_la_SOURCES = \
 	expr.h \
 	expr.cpp \
 	expr_manager.h \
-	expr_manager.cpp
+	expr_manager.cpp \
+	type_checker.cpp
 
 EXTRA_DIST = \
 	kind_template.h \
@@ -47,6 +49,7 @@ EXTRA_DIST = \
 	expr_manager_template.cpp \
 	expr_template.h \
 	expr_template.cpp \
+	type_checker_template.cpp \
 	mkkind \
 	mkmetakind \
 	mkexpr
@@ -59,6 +62,7 @@ BUILT_SOURCES = \
 	expr.cpp \
 	expr_manager.h \
 	expr_manager.cpp \
+	type_checker.cpp \
 	$(top_builddir)/src/theory/.subdirs
 
 CLEANFILES = \
@@ -68,6 +72,7 @@ CLEANFILES = \
 	expr.cpp \
 	expr_manager.h \
 	expr_manager.cpp \
+	type_checker.cpp \
 	$(top_builddir)/src/theory/.subdirs
 
 include @top_srcdir@/src/theory/Makefile.subdirs
@@ -127,3 +132,11 @@ expr_manager.cpp: expr_manager_template.cpp mkexpr @top_builddir@/src/theory/.su
 		$< \
 		`cat @top_builddir@/src/theory/.subdirs` \
 	> $@) || (rm -f $@ && exit 1)
+
+type_checker.cpp: type_checker_template.cpp mkexpr @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
+	$(AM_V_at)chmod +x @srcdir@/mkexpr
+	$(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
+	$(AM_V_GEN)(@srcdir@/mkexpr \
+		$< \
+		`cat @top_builddir@/src/theory/.subdirs` \
+	> $@) || (rm -f $@ && exit 1)
diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp
index 85c0fe528..d58173454 100644
--- a/src/expr/attribute.cpp
+++ b/src/expr/attribute.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: dejan
  ** 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/expr/attribute.h b/src/expr/attribute.h
index 9b21184d0..3da3799be 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -5,7 +5,7 @@
  ** Major contributors: dejan
  ** Minor contributors (to current version): cconway, taking
  ** 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/expr/command.cpp b/src/expr/command.cpp
index 2783e8eaa..5fb4d1fbd 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -78,6 +78,10 @@ EmptyCommand::EmptyCommand(std::string name) :
   d_name(name) {
 }
 
+std::string EmptyCommand::getName() const {
+  return d_name;
+}
+
 void EmptyCommand::invoke(SmtEngine* smtEngine) {
   /* empty commands have no implementation */
 }
@@ -88,6 +92,10 @@ AssertCommand::AssertCommand(const BoolExpr& e) :
   d_expr(e) {
 }
 
+BoolExpr AssertCommand::getExpr() const {
+  return d_expr;
+}
+
 void AssertCommand::invoke(SmtEngine* smtEngine) {
   smtEngine->assertFormula(d_expr);
 }
@@ -106,10 +114,18 @@ void PopCommand::invoke(SmtEngine* smtEngine) {
 
 /* class CheckSatCommand */
 
+CheckSatCommand::CheckSatCommand() :
+  d_expr() {
+}
+
 CheckSatCommand::CheckSatCommand(const BoolExpr& expr) :
   d_expr(expr) {
 }
 
+BoolExpr CheckSatCommand::getExpr() const {
+  return d_expr;
+}
+
 void CheckSatCommand::invoke(SmtEngine* smtEngine) {
   d_result = smtEngine->checkSat(d_expr);
 }
@@ -128,6 +144,10 @@ QueryCommand::QueryCommand(const BoolExpr& e) :
   d_expr(e) {
 }
 
+BoolExpr QueryCommand::getExpr() const {
+  return d_expr;
+}
+
 void QueryCommand::invoke(SmtEngine* smtEngine) {
   d_result = smtEngine->query(d_expr);
 }
@@ -145,6 +165,23 @@ void QueryCommand::printResult(std::ostream& out) const {
 QuitCommand::QuitCommand() {
 }
 
+void QuitCommand::invoke(SmtEngine* smtEngine) {
+  Dump("benchmark") << *this;
+}
+
+/* class CommentCommand */
+
+CommentCommand::CommentCommand(std::string comment) : d_comment(comment) {
+}
+
+std::string CommentCommand::getComment() const {
+  return d_comment;
+}
+
+void CommentCommand::invoke(SmtEngine* smtEngine) {
+  Dump("benchmark") << *this;
+}
+
 /* class CommandSequence */
 
 CommandSequence::CommandSequence() :
@@ -175,51 +212,150 @@ void CommandSequence::invoke(SmtEngine* smtEngine, std::ostream& out) {
   }
 }
 
-/* class DeclarationCommand */
+CommandSequence::const_iterator CommandSequence::begin() const {
+  return d_commandSequence.begin();
+}
+
+CommandSequence::const_iterator CommandSequence::end() const {
+  return d_commandSequence.end();
+}
+
+CommandSequence::iterator CommandSequence::begin() {
+  return d_commandSequence.begin();
+}
+
+CommandSequence::iterator CommandSequence::end() {
+  return d_commandSequence.end();
+}
+
+/* class DeclarationSequenceCommand */
+
+/* class DeclarationDefinitionCommand */
+
+DeclarationDefinitionCommand::DeclarationDefinitionCommand(const std::string& id) :
+  d_symbol(id) {
+}
+
+std::string DeclarationDefinitionCommand::getSymbol() const {
+  return d_symbol;
+}
+
+/* class DeclareFunctionCommand */
+
+DeclareFunctionCommand::DeclareFunctionCommand(const std::string& id, Type t) :
+  DeclarationDefinitionCommand(id),
+  d_type(t) {
+}
+
+Type DeclareFunctionCommand::getType() const {
+  return d_type;
+}
+
+void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) {
+  Dump("declarations") << *this << endl;
+}
+
+/* class DeclareTypeCommand */
+
+DeclareTypeCommand::DeclareTypeCommand(const std::string& id, size_t arity, Type t) :
+  DeclarationDefinitionCommand(id),
+  d_arity(arity),
+  d_type(t) {
+}
+
+size_t DeclareTypeCommand::getArity() const {
+  return d_arity;
+}
+
+Type DeclareTypeCommand::getType() const {
+  return d_type;
+}
+
+void DeclareTypeCommand::invoke(SmtEngine* smtEngine) {
+  Dump("declarations") << *this << endl;
+}
+
+/* class DefineTypeCommand */
 
-DeclarationCommand::DeclarationCommand(const std::string& id, Type t) :
+DefineTypeCommand::DefineTypeCommand(const std::string& id,
+                                     Type t) :
+  DeclarationDefinitionCommand(id),
+  d_params(),
   d_type(t) {
-  d_declaredSymbols.push_back(id);
 }
 
-DeclarationCommand::DeclarationCommand(const std::vector<std::string>& ids, Type t) :
-  d_declaredSymbols(ids),
+DefineTypeCommand::DefineTypeCommand(const std::string& id,
+                                     const std::vector<Type>& params,
+                                     Type t) :
+  DeclarationDefinitionCommand(id),
+  d_params(params),
   d_type(t) {
 }
 
-const std::vector<std::string>& DeclarationCommand::getDeclaredSymbols() const {
-  return d_declaredSymbols;
+const std::vector<Type>& DefineTypeCommand::getParameters() const {
+  return d_params;
 }
 
-Type DeclarationCommand::getDeclaredType() const {
+Type DefineTypeCommand::getType() const {
   return d_type;
 }
 
+void DefineTypeCommand::invoke(SmtEngine* smtEngine) {
+  Dump("declarations") << *this << endl;
+}
+
 /* class DefineFunctionCommand */
 
-DefineFunctionCommand::DefineFunctionCommand(Expr func,
+DefineFunctionCommand::DefineFunctionCommand(const std::string& id,
+                                             Expr func,
+                                             Expr formula) :
+  DeclarationDefinitionCommand(id),
+  d_func(func),
+  d_formals(),
+  d_formula(formula) {
+}
+
+DefineFunctionCommand::DefineFunctionCommand(const std::string& id,
+                                             Expr func,
                                              const std::vector<Expr>& formals,
                                              Expr formula) :
+  DeclarationDefinitionCommand(id),
   d_func(func),
   d_formals(formals),
   d_formula(formula) {
 }
 
+Expr DefineFunctionCommand::getFunction() const {
+  return d_func;
+}
+
+const std::vector<Expr>& DefineFunctionCommand::getFormals() const {
+  return d_formals;
+}
+
+Expr DefineFunctionCommand::getFormula() const {
+  return d_formula;
+}
+
 void DefineFunctionCommand::invoke(SmtEngine* smtEngine) {
-  smtEngine->defineFunction(d_func, d_formals, d_formula);
+  Dump("declarations") << *this << endl;
+  if(!d_func.isNull()) {
+    smtEngine->defineFunction(d_func, d_formals, d_formula);
+  }
 }
 
-/* class DefineFunctionCommand */
+/* class DefineNamedFunctionCommand */
 
-DefineNamedFunctionCommand::DefineNamedFunctionCommand(Expr func,
+DefineNamedFunctionCommand::DefineNamedFunctionCommand(const std::string& id,
+                                                       Expr func,
                                                        const std::vector<Expr>& formals,
                                                        Expr formula) :
-  DefineFunctionCommand(func, formals, formula) {
+  DefineFunctionCommand(id, func, formals, formula) {
 }
 
 void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine) {
   this->DefineFunctionCommand::invoke(smtEngine);
-  if(d_func.getType().isBoolean()) {
+  if(!d_func.isNull() && d_func.getType().isBoolean()) {
     smtEngine->addToAssignment(d_func.getExprManager()->mkExpr(kind::APPLY,
                                                                d_func));
   }
@@ -231,6 +367,10 @@ SimplifyCommand::SimplifyCommand(Expr term) :
   d_term(term) {
 }
 
+Expr SimplifyCommand::getTerm() const {
+  return d_term;
+}
+
 void SimplifyCommand::invoke(SmtEngine* smtEngine) {
   d_result = smtEngine->simplify(d_term);
 }
@@ -249,6 +389,10 @@ GetValueCommand::GetValueCommand(Expr term) :
   d_term(term) {
 }
 
+Expr GetValueCommand::getTerm() const {
+  return d_term;
+}
+
 void GetValueCommand::invoke(SmtEngine* smtEngine) {
   d_result = d_term.getExprManager()->mkExpr(kind::TUPLE, d_term,
                                              smtEngine->getValue(d_term));
@@ -305,6 +449,10 @@ SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) :
   d_status(status) {
 }
 
+BenchmarkStatus SetBenchmarkStatusCommand::getStatus() const {
+  return d_status;
+}
+
 void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) {
   stringstream ss;
   ss << d_status;
@@ -326,6 +474,10 @@ SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic) :
   d_logic(logic) {
 }
 
+std::string SetBenchmarkLogicCommand::getLogic() const {
+  return d_logic;
+}
+
 void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) {
   try {
     smtEngine->setLogic(d_logic);
@@ -337,11 +489,19 @@ void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) {
 
 /* class SetInfoCommand */
 
-SetInfoCommand::SetInfoCommand(std::string flag, SExpr& sexpr) :
+SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr) :
   d_flag(flag),
   d_sexpr(sexpr) {
 }
 
+std::string SetInfoCommand::getFlag() const {
+  return d_flag;
+}
+
+SExpr SetInfoCommand::getSExpr() const {
+  return d_sexpr;
+}
+
 void SetInfoCommand::invoke(SmtEngine* smtEngine) {
   try {
     smtEngine->setInfo(d_flag, d_sexpr);
@@ -369,6 +529,10 @@ GetInfoCommand::GetInfoCommand(std::string flag) :
   d_flag(flag) {
 }
 
+std::string GetInfoCommand::getFlag() const {
+  return d_flag;
+}
+
 void GetInfoCommand::invoke(SmtEngine* smtEngine) {
   try {
     stringstream ss;
@@ -391,11 +555,19 @@ void GetInfoCommand::printResult(std::ostream& out) const {
 
 /* class SetOptionCommand */
 
-SetOptionCommand::SetOptionCommand(std::string flag, SExpr& sexpr) :
+SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr) :
   d_flag(flag),
   d_sexpr(sexpr) {
 }
 
+std::string SetOptionCommand::getFlag() const {
+  return d_flag;
+}
+
+SExpr SetOptionCommand::getSExpr() const {
+  return d_sexpr;
+}
+
 void SetOptionCommand::invoke(SmtEngine* smtEngine) {
   try {
     smtEngine->setOption(d_flag, d_sexpr);
@@ -423,6 +595,10 @@ GetOptionCommand::GetOptionCommand(std::string flag) :
   d_flag(flag) {
 }
 
+std::string GetOptionCommand::getFlag() const {
+  return d_flag;
+}
+
 void GetOptionCommand::invoke(SmtEngine* smtEngine) {
   try {
     d_result = smtEngine->getOption(d_flag).getValue();
@@ -446,17 +622,19 @@ void GetOptionCommand::printResult(std::ostream& out) const {
 DatatypeDeclarationCommand::DatatypeDeclarationCommand(const DatatypeType& datatype) :
   d_datatypes() {
   d_datatypes.push_back(datatype);
-  Debug("datatypes") << "Create datatype command." << endl;
 }
 
 DatatypeDeclarationCommand::DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes) :
   d_datatypes(datatypes) {
-  Debug("datatypes") << "Create datatype command." << endl;
+}
+
+const std::vector<DatatypeType>&
+DatatypeDeclarationCommand::getDatatypes() const {
+  return d_datatypes;
 }
 
 void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) {
-  Debug("datatypes") << "Invoke datatype command." << endl;
-  //smtEngine->addDatatypeDefinitions(d_datatype);
+  Dump("declarations") << *this << endl;
 }
 
 /* output stream insertion operator for benchmark statuses */
diff --git a/src/expr/command.h b/src/expr/command.h
index 50d382038..5cf4f6fa0 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -2,8 +2,8 @@
 /*! \file command.h
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: dejan
- ** Minor contributors (to current version): cconway
+ ** Major contributors: none
+ ** Minor contributors (to current version): cconway, 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
@@ -59,26 +59,31 @@ std::ostream& operator<<(std::ostream& out,
 
 class CVC4_PUBLIC Command {
 public:
+  virtual ~Command() {}
+
   virtual void invoke(SmtEngine* smtEngine) = 0;
   virtual void invoke(SmtEngine* smtEngine, std::ostream& out);
-  virtual ~Command() {};
+
   virtual void toStream(std::ostream& out, int toDepth = -1, bool types = false,
                         OutputLanguage language = language::output::LANG_AST) const;
+
   std::string toString() const;
+
   virtual void printResult(std::ostream& out) const;
+
 };/* class Command */
 
 /**
- * EmptyCommands (and its subclasses) are the residue of a command
- * after the parser handles them (and there's nothing left to do).
+ * EmptyCommands are the residue of a command after the parser handles
+ * them (and there's nothing left to do).
  */
 class CVC4_PUBLIC EmptyCommand : public Command {
 protected:
   std::string d_name;
 public:
   EmptyCommand(std::string name = "");
+  std::string getName() const;
   void invoke(SmtEngine* smtEngine);
-  std::string getName() const { return d_name; }
 };/* class EmptyCommand */
 
 class CVC4_PUBLIC AssertCommand : public Command {
@@ -86,8 +91,8 @@ protected:
   BoolExpr d_expr;
 public:
   AssertCommand(const BoolExpr& e);
+  BoolExpr getExpr() const;
   void invoke(SmtEngine* smtEngine);
-  BoolExpr getExpr() const { return d_expr; }
 };/* class AssertCommand */
 
 class CVC4_PUBLIC PushCommand : public Command {
@@ -100,30 +105,59 @@ public:
   void invoke(SmtEngine* smtEngine);
 };/* class PopCommand */
 
-class CVC4_PUBLIC DeclarationCommand : public EmptyCommand {
+class CVC4_PUBLIC DeclarationDefinitionCommand : public Command {
+protected:
+  std::string d_symbol;
+public:
+  DeclarationDefinitionCommand(const std::string& id);
+  std::string getSymbol() const;
+};/* class DeclarationDefinitionCommand */
+
+class CVC4_PUBLIC DeclareFunctionCommand : public DeclarationDefinitionCommand {
+protected:
+  Type d_type;
+public:
+  DeclareFunctionCommand(const std::string& id, Type type);
+  Type getType() const;
+  void invoke(SmtEngine* smtEngine);
+};/* class DeclareFunctionCommand */
+
+class CVC4_PUBLIC DeclareTypeCommand : public DeclarationDefinitionCommand {
+protected:
+  size_t d_arity;
+  Type d_type;
+public:
+  DeclareTypeCommand(const std::string& id, size_t arity, Type t);
+  size_t getArity() const;
+  Type getType() const;
+  void invoke(SmtEngine* smtEngine);
+};/* class DeclareTypeCommand */
+
+class CVC4_PUBLIC DefineTypeCommand : public DeclarationDefinitionCommand {
 protected:
-  std::vector<std::string> d_declaredSymbols;
+  std::vector<Type> d_params;
   Type d_type;
 public:
-  DeclarationCommand(const std::string& id, Type t);
-  DeclarationCommand(const std::vector<std::string>& ids, Type t);
-  const std::vector<std::string>& getDeclaredSymbols() const;
-  Type getDeclaredType() const;
-};/* class DeclarationCommand */
+  DefineTypeCommand(const std::string& id, Type t);
+  DefineTypeCommand(const std::string& id, const std::vector<Type>& params, Type t);
+  const std::vector<Type>& getParameters() const;
+  Type getType() const;
+  void invoke(SmtEngine* smtEngine);
+};/* class DefineTypeCommand */
 
-class CVC4_PUBLIC DefineFunctionCommand : public Command {
+class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand {
 protected:
   Expr d_func;
   std::vector<Expr> d_formals;
   Expr d_formula;
 public:
-  DefineFunctionCommand(Expr func,
-                        const std::vector<Expr>& formals,
-                        Expr formula);
+  DefineFunctionCommand(const std::string& id, Expr func, Expr formula);
+  DefineFunctionCommand(const std::string& id, Expr func,
+                        const std::vector<Expr>& formals, Expr formula);
+  Expr getFunction() const;
+  const std::vector<Expr>& getFormals() const;
+  Expr getFormula() const;
   void invoke(SmtEngine* smtEngine);
-  Expr getFunction() const { return d_func; }
-  const std::vector<Expr>& getFormals() const { return d_formals; }
-  Expr getFormula() const { return d_formula; }
 };/* class DefineFunctionCommand */
 
 /**
@@ -133,9 +167,8 @@ public:
  */
 class CVC4_PUBLIC DefineNamedFunctionCommand : public DefineFunctionCommand {
 public:
-  DefineNamedFunctionCommand(Expr func,
-                             const std::vector<Expr>& formals,
-                             Expr formula);
+  DefineNamedFunctionCommand(const std::string& id, Expr func,
+                             const std::vector<Expr>& formals, Expr formula);
   void invoke(SmtEngine* smtEngine);
 };/* class DefineNamedFunctionCommand */
 
@@ -144,9 +177,10 @@ protected:
   BoolExpr d_expr;
   Result d_result;
 public:
+  CheckSatCommand();
   CheckSatCommand(const BoolExpr& expr);
+  BoolExpr getExpr() const;
   void invoke(SmtEngine* smtEngine);
-  BoolExpr getExpr() const { return d_expr; }
   Result getResult() const;
   void printResult(std::ostream& out) const;
 };/* class CheckSatCommand */
@@ -157,8 +191,8 @@ protected:
   Result d_result;
 public:
   QueryCommand(const BoolExpr& e);
+  BoolExpr getExpr() const;
   void invoke(SmtEngine* smtEngine);
-  BoolExpr getExpr() const { return d_expr; }
   Result getResult() const;
   void printResult(std::ostream& out) const;
 };/* class QueryCommand */
@@ -170,8 +204,8 @@ protected:
   Expr d_result;
 public:
   SimplifyCommand(Expr term);
+  Expr getTerm() const;
   void invoke(SmtEngine* smtEngine);
-  Expr getTerm() const { return d_term; }
   Expr getResult() const;
   void printResult(std::ostream& out) const;
 };/* class SimplifyCommand */
@@ -182,8 +216,8 @@ protected:
   Expr d_result;
 public:
   GetValueCommand(Expr term);
+  Expr getTerm() const;
   void invoke(SmtEngine* smtEngine);
-  Expr getTerm() const { return d_term; }
   Expr getResult() const;
   void printResult(std::ostream& out) const;
 };/* class GetValueCommand */
@@ -214,8 +248,8 @@ protected:
   BenchmarkStatus d_status;
 public:
   SetBenchmarkStatusCommand(BenchmarkStatus status);
+  BenchmarkStatus getStatus() const;
   void invoke(SmtEngine* smtEngine);
-  BenchmarkStatus getStatus() const { return d_status; }
 };/* class SetBenchmarkStatusCommand */
 
 class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command {
@@ -224,8 +258,8 @@ protected:
   std::string d_logic;
 public:
   SetBenchmarkLogicCommand(std::string logic);
+  std::string getLogic() const;
   void invoke(SmtEngine* smtEngine);
-  std::string getLogic() const { return d_logic; }
 };/* class SetBenchmarkLogicCommand */
 
 class CVC4_PUBLIC SetInfoCommand : public Command {
@@ -234,10 +268,10 @@ protected:
   SExpr d_sexpr;
   std::string d_result;
 public:
-  SetInfoCommand(std::string flag, SExpr& sexpr);
+  SetInfoCommand(std::string flag, const SExpr& sexpr);
+  std::string getFlag() const;
+  SExpr getSExpr() const;
   void invoke(SmtEngine* smtEngine);
-  std::string getFlag() const { return d_flag; }
-  SExpr getSExpr() const { return d_sexpr; }
   std::string getResult() const;
   void printResult(std::ostream& out) const;
 };/* class SetInfoCommand */
@@ -248,8 +282,8 @@ protected:
   std::string d_result;
 public:
   GetInfoCommand(std::string flag);
+  std::string getFlag() const;
   void invoke(SmtEngine* smtEngine);
-  std::string getFlag() const { return d_flag; }
   std::string getResult() const;
   void printResult(std::ostream& out) const;
 };/* class GetInfoCommand */
@@ -260,10 +294,10 @@ protected:
   SExpr d_sexpr;
   std::string d_result;
 public:
-  SetOptionCommand(std::string flag, SExpr& sexpr);
+  SetOptionCommand(std::string flag, const SExpr& sexpr);
+  std::string getFlag() const;
+  SExpr getSExpr() const;
   void invoke(SmtEngine* smtEngine);
-  std::string getFlag() const { return d_flag; }
-  SExpr getSExpr() const { return d_sexpr; }
   std::string getResult() const;
   void printResult(std::ostream& out) const;
 };/* class SetOptionCommand */
@@ -274,8 +308,8 @@ protected:
   std::string d_result;
 public:
   GetOptionCommand(std::string flag);
+  std::string getFlag() const;
   void invoke(SmtEngine* smtEngine);
-  std::string getFlag() const { return d_flag; }
   std::string getResult() const;
   void printResult(std::ostream& out) const;
 };/* class GetOptionCommand */
@@ -286,15 +320,24 @@ private:
 public:
   DatatypeDeclarationCommand(const DatatypeType& datatype);
   DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes);
+  const std::vector<DatatypeType>& getDatatypes() const;
   void invoke(SmtEngine* smtEngine);
-  const std::vector<DatatypeType>& getDatatypes() const { return d_datatypes; }
 };/* class DatatypeDeclarationCommand */
 
-class CVC4_PUBLIC QuitCommand : public EmptyCommand {
+class CVC4_PUBLIC QuitCommand : public Command {
 public:
   QuitCommand();
+  void invoke(SmtEngine* smtEngine);
 };/* class QuitCommand */
 
+class CVC4_PUBLIC CommentCommand : public Command {
+  std::string d_comment;
+public:
+  CommentCommand(std::string comment);
+  std::string getComment() const;
+  void invoke(SmtEngine* smtEngine);
+};/* class CommentCommand */
+
 class CVC4_PUBLIC CommandSequence : public Command {
 private:
   /** All the commands to be executed (in sequence) */
@@ -304,20 +347,27 @@ private:
 public:
   CommandSequence();
   ~CommandSequence();
+
+  void addCommand(Command* cmd);
+
   void invoke(SmtEngine* smtEngine);
   void invoke(SmtEngine* smtEngine, std::ostream& out);
-  void addCommand(Command* cmd);
 
   typedef std::vector<Command*>::iterator iterator;
   typedef std::vector<Command*>::const_iterator const_iterator;
 
-  const_iterator begin() const { return d_commandSequence.begin(); }
-  const_iterator end() const { return d_commandSequence.end(); }
+  const_iterator begin() const;
+  const_iterator end() const;
+
+  iterator begin();
+  iterator end();
 
-  iterator begin() { return d_commandSequence.begin(); }
-  iterator end() { return d_commandSequence.end(); }
 };/* class CommandSequence */
 
+class CVC4_PUBLIC DeclarationSequence : public CommandSequence {
+public:
+};/* class DeclarationSequence */
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__COMMAND_H */
diff --git a/src/expr/convenience_node_builders.h b/src/expr/convenience_node_builders.h
index 655accde3..451250e52 100644
--- a/src/expr/convenience_node_builders.h
+++ b/src/expr/convenience_node_builders.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** 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/expr/declaration_scope.cpp b/src/expr/declaration_scope.cpp
index ae91efa68..37c709b6a 100644
--- a/src/expr/declaration_scope.cpp
+++ b/src/expr/declaration_scope.cpp
@@ -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
diff --git a/src/expr/declaration_scope.h b/src/expr/declaration_scope.h
index d695a3bf8..4bce5e1be 100644
--- a/src/expr/declaration_scope.h
+++ b/src/expr/declaration_scope.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: cconway
  ** Major contributors: 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
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 038f58f95..f013c1644 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.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
@@ -116,6 +116,10 @@ ExprManager::~ExprManager() {
   delete d_ctxt;
 }
 
+const Options* ExprManager::getOptions() const {
+  return d_nodeManager->getOptions();
+}
+
 BooleanType ExprManager::booleanType() const {
   NodeManagerScope nms(d_nodeManager);
   return BooleanType(Type(d_nodeManager, new TypeNode(d_nodeManager->booleanType())));
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index eb67277a1..2828ae381 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: dejan
  ** Major contributors: mdeters
- ** Minor contributors (to current version): taking, cconway
+ ** Minor contributors (to current version): ajreynol, taking, cconway
  ** 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
@@ -114,6 +114,9 @@ public:
    */
   ~ExprManager();
 
+  /** Get this node manager's options */
+  const Options* getOptions() const;
+
   /** Get the type for booleans */
   BooleanType booleanType() const;
 
diff --git a/src/expr/expr_stream.h b/src/expr/expr_stream.h
index a6b99fb73..990ce9982 100644
--- a/src/expr/expr_stream.h
+++ b/src/expr/expr_stream.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** 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/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 7c2d02809..619fd5280 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -21,15 +21,19 @@
 #include "expr/expr_manager_scope.h"
 #include "util/Assert.h"
 
+#include <iterator>
+#include <utility>
+
 ${includes}
 
 // This is a hack, but an important one: if there's an error, the
 // compiler directs the user to the template file instead of the
 // generated one.  We don't want the user to modify the generated one,
 // since it'll get overwritten on a later build.
-#line 31 "${template}"
+#line 34 "${template}"
 
 using namespace CVC4::kind;
+using namespace std;
 
 namespace CVC4 {
 
@@ -73,7 +77,7 @@ TypeCheckingException::~TypeCheckingException() throw () {
 }
 
 void TypeCheckingException::toStream(std::ostream& os) const {
-  os << "Error type-checking " << d_expr << ": " << d_msg << std::endl << *d_expr;
+  os << "Error type-checking " << d_expr << ": " << d_msg << endl << *d_expr;
 }
 
 Expr TypeCheckingException::getExpression() const {
@@ -208,6 +212,59 @@ Type Expr::getType(bool check) const throw (TypeCheckingException) {
   return d_exprManager->getType(*this, check);
 }
 
+Expr Expr::substitute(Expr e, Expr replacement) const {
+  return Expr(d_exprManager, new Node(d_node->substitute(TNode(*e.d_node), TNode(*replacement.d_node))));
+}
+
+template <class Iterator>
+class NodeIteratorAdaptor : public std::iterator<std::input_iterator_tag, Node> {
+  Iterator d_iterator;
+public:
+  NodeIteratorAdaptor(Iterator i) : d_iterator(i) {
+  }
+  NodeIteratorAdaptor& operator++() { ++d_iterator; return *this; }
+  NodeIteratorAdaptor operator++(int) { NodeIteratorAdaptor i(d_iterator); ++d_iterator; return i; }
+  bool operator==(NodeIteratorAdaptor i) { return d_iterator == i.d_iterator; }
+  bool operator!=(NodeIteratorAdaptor i) { return !(*this == i); }
+  Node operator*() { return Node::fromExpr(*d_iterator); }
+};/* class NodeIteratorAdaptor */
+
+template <class Iterator>
+static inline NodeIteratorAdaptor<Iterator> mkNodeIteratorAdaptor(Iterator i) {
+  return NodeIteratorAdaptor<Iterator>(i);
+}
+
+Expr Expr::substitute(const std::vector<Expr> exes,
+                      const std::vector<Expr>& replacements) const {
+  return Expr(d_exprManager,
+              new Node(d_node->substitute(mkNodeIteratorAdaptor(exes.begin()),
+                                          mkNodeIteratorAdaptor(exes.end()),
+                                          mkNodeIteratorAdaptor(replacements.begin()),
+                                          mkNodeIteratorAdaptor(replacements.end()))));
+}
+
+template <class Iterator>
+class NodePairIteratorAdaptor : public std::iterator<std::input_iterator_tag, pair<Node, Node> > {
+  Iterator d_iterator;
+public:
+  NodePairIteratorAdaptor(Iterator i) : d_iterator(i) {
+  }
+  NodePairIteratorAdaptor& operator++() { ++d_iterator; return *this; }
+  NodePairIteratorAdaptor operator++(int) { NodePairIteratorAdaptor i(d_iterator); ++d_iterator; return i; }
+  bool operator==(NodePairIteratorAdaptor i) { return d_iterator == i.d_iterator; }
+  bool operator!=(NodePairIteratorAdaptor i) { return !(*this == i); }
+  pair<Node, Node> operator*() { return make_pair(Node::fromExpr((*d_iterator).first), Node::fromExpr((*d_iterator).second)); }
+};/* class NodePairIteratorAdaptor */
+
+template <class Iterator>
+static inline NodePairIteratorAdaptor<Iterator> mkNodePairIteratorAdaptor(Iterator i) {
+  return NodePairIteratorAdaptor<Iterator>(i);
+}
+
+Expr Expr::substitute(const std::hash_map<Expr, Expr, ExprHashFunction> map) const {
+  return Expr(d_exprManager, new Node(d_node->substitute(mkNodePairIteratorAdaptor(map.begin()), mkNodePairIteratorAdaptor(map.end()))));
+}
+
 Expr::const_iterator::const_iterator() :
   d_iterator(NULL) {
 }
@@ -280,6 +337,12 @@ Expr::operator bool() const {
   return !isNull();
 }
 
+bool Expr::isVariable() const {
+  ExprManagerScope ems(*this);
+  Assert(d_node != NULL, "Unexpected NULL expression pointer!");
+  return d_node->getMetaKind() == kind::metakind::VARIABLE;
+}
+
 bool Expr::isConst() const {
   ExprManagerScope ems(*this);
   Assert(d_node != NULL, "Unexpected NULL expression pointer!");
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index bffb37ddb..e95e434fe 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -35,12 +35,13 @@ ${includes}
 
 #include "util/exception.h"
 #include "util/language.h"
+#include "util/hash.h"
 
 // This is a hack, but an important one: if there's an error, the
 // compiler directs the user to the template file instead of the
 // generated one.  We don't want the user to modify the generated one,
 // since it'll get overwritten on a later build.
-#line 44 "${template}"
+#line 45 "${template}"
 
 namespace CVC4 {
 
@@ -121,6 +122,11 @@ std::ostream& operator<<(std::ostream& out,
  */
 std::ostream& operator<<(std::ostream& out, const Expr& e) CVC4_PUBLIC;
 
+// for hash_maps, hash_sets..
+struct ExprHashFunction {
+  size_t operator()(CVC4::Expr e) const;
+};/* struct ExprHashFunction */
+
 /**
  * Class encapsulating CVC4 expressions and methods for constructing new
  * expressions.
@@ -344,6 +350,22 @@ public:
   Type getType(bool check = false) const throw (TypeCheckingException);
 
   /**
+   * Substitute "replacement" in for "e".
+   */
+  Expr substitute(Expr e, Expr replacement) const;
+
+  /**
+   * Substitute "replacements" in for "exes".
+   */
+  Expr substitute(const std::vector<Expr> exes,
+                  const std::vector<Expr>& replacements) const;
+
+  /**
+   * Substitute pairs of (ex,replacement) from the given map.
+   */
+  Expr substitute(const std::hash_map<Expr, Expr, ExprHashFunction> map) const;
+
+  /**
    * Returns the string representation of the expression.
    * @return a string representation of the expression
    */
@@ -365,18 +387,28 @@ public:
 
   /**
    * Check if this is a null expression.
+   *
    * @return true if a null expression
    */
   bool isNull() const;
 
   /**
    * Check if this is a null expression.
+   *
    * @return true if NOT a null expression
    */
   operator bool() const;
 
   /**
+   * Check if this is an expression representing a variable.
+   *
+   * @return true if a variable expression
+   */
+  bool isVariable() const;
+
+  /**
    * Check if this is an expression representing a constant.
+   *
    * @return true if a constant expression
    */
   bool isConst() const;
@@ -541,7 +573,7 @@ public:
 
   /**
    * Make a Boolean if-then-else expression using this expression as the
-   * condition, and given the then and else parts
+   * condition, and given the then and else parts.
    * @param then_e the then branch expression
    * @param else_e the else branch expression
    * @return the if-then-else expression
@@ -550,13 +582,14 @@ public:
 
   /**
    * Make a term if-then-else expression using this expression as the
-   * condition, and given the then and else parts
+   * condition, and given the then and else parts.
    * @param then_e the then branch expression
    * @param else_e the else branch expression
    * @return the if-then-else expression
    */
   Expr iteExpr(const Expr& then_e, const Expr& else_e) const;
-};
+
+};/* class BoolExpr */
 
 namespace expr {
 
@@ -791,7 +824,7 @@ public:
 
 ${getConst_instantiations}
 
-#line 795 "${template}"
+#line 828 "${template}"
 
 namespace expr {
 
@@ -839,12 +872,9 @@ inline std::ostream& operator<<(std::ostream& out, ExprSetLanguage l) {
 
 }/* CVC4::expr namespace */
 
-// for hash_maps, hash_sets..
-struct ExprHashFunction {
-  size_t operator()(CVC4::Expr e) const {
-    return (size_t) e.getId();
-  }
-};/* struct ExprHashFunction */
+inline size_t ExprHashFunction::operator()(CVC4::Expr e) const {
+  return (size_t) e.getId();
+}
 
 }/* CVC4 namespace */
 
diff --git a/src/expr/kind_map.h b/src/expr/kind_map.h
index a02339e5e..974bd6791 100644
--- a/src/expr/kind_map.h
+++ b/src/expr/kind_map.h
@@ -1,7 +1,7 @@
 /*********************                                                        */
 /*! \file kind_map.h
  ** \verbatim
- ** Original author: mdeters
+ ** Original author: dejan
  ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index 5f9aa6619..a954a7f70 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): dejan
  ** 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/expr/mkexpr b/src/expr/mkexpr
index 479ef6d11..69f7019ab 100755
--- a/src/expr/mkexpr
+++ b/src/expr/mkexpr
@@ -107,6 +107,25 @@ function endtheory {
   seen_endtheory=true
 }
 
+function typechecker {
+  # typechecker header
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+  typechecker_includes="${typechecker_includes}
+#include \"$1\""
+}
+
+function typerule {
+  # typerule OPERATOR typechecking-class
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+  typerules="${typerules}
+  case kind::$1:
+    typeNode = $2::computeType(nodeManager, n, check);
+    break;
+"
+}
+
 function sort {
   # sort TYPE cardinality [well-founded ground-term header | not-well-founded] ["comment"]
   lineno=${BASH_LINENO[0]}
@@ -225,6 +244,8 @@ for var in \
     getConst_implementations \
     mkConst_instantiations \
     mkConst_implementations \
+    typechecker_includes \
+    typerules \
     ; do
   eval text="\${text//\\\$\\{$var\\}/\${$var}}"
 done
diff --git a/src/expr/mkkind b/src/expr/mkkind
index 47d02863e..abb238f1a 100755
--- a/src/expr/mkkind
+++ b/src/expr/mkkind
@@ -118,6 +118,18 @@ function endtheory {
   seen_endtheory=true
 }
 
+function typechecker {
+  # typechecker header
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+}
+
+function typerule {
+  # typerule OPERATOR typechecking-class
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+}
+
 function rewriter {
   # properties prop*
   lineno=${BASH_LINENO[0]}
diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
index 46a69dee5..d84691e14 100755
--- a/src/expr/mkmetakind
+++ b/src/expr/mkmetakind
@@ -93,6 +93,18 @@ function endtheory {
   seen_endtheory=true
 }
 
+function typechecker {
+  # typechecker header
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+}
+
+function typerule {
+  # typerule OPERATOR typechecking-class
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+}
+
 function rewriter {
   # rewriter class header
   lineno=${BASH_LINENO[0]}
diff --git a/src/expr/node.h b/src/expr/node.h
index f501dba21..0f4b55d4a 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -28,6 +28,8 @@
 #include <string>
 #include <iostream>
 #include <utility>
+#include <algorithm>
+#include <functional>
 #include <stdint.h>
 
 #include "expr/type.h"
@@ -832,16 +834,23 @@ public:
    */
   inline bool hasSubterm(NodeTemplate<false> t, bool strict = false) const;
 
-  NodeTemplate<true> eqNode(const NodeTemplate& right) const;
+  template <bool ref_count2>
+  NodeTemplate<true> eqNode(const NodeTemplate<ref_count2>& right) const;
 
   NodeTemplate<true> notNode() const;
-  NodeTemplate<true> andNode(const NodeTemplate& right) const;
-  NodeTemplate<true> orNode(const NodeTemplate& right) const;
-  NodeTemplate<true> iteNode(const NodeTemplate& thenpart,
-                             const NodeTemplate& elsepart) const;
-  NodeTemplate<true> iffNode(const NodeTemplate& right) const;
-  NodeTemplate<true> impNode(const NodeTemplate& right) const;
-  NodeTemplate<true> xorNode(const NodeTemplate& right) const;
+  template <bool ref_count2>
+  NodeTemplate<true> andNode(const NodeTemplate<ref_count2>& right) const;
+  template <bool ref_count2>
+  NodeTemplate<true> orNode(const NodeTemplate<ref_count2>& right) const;
+  template <bool ref_count2, bool ref_count3>
+  NodeTemplate<true> iteNode(const NodeTemplate<ref_count2>& thenpart,
+                             const NodeTemplate<ref_count3>& elsepart) const;
+  template <bool ref_count2>
+  NodeTemplate<true> iffNode(const NodeTemplate<ref_count2>& right) const;
+  template <bool ref_count2>
+  NodeTemplate<true> impNode(const NodeTemplate<ref_count2>& right) const;
+  template <bool ref_count2>
+  NodeTemplate<true> xorNode(const NodeTemplate<ref_count2>& right) const;
 
 };/* class NodeTemplate<ref_count> */
 
@@ -1085,8 +1094,9 @@ operator=(const NodeTemplate<!ref_count>& e) {
 }
 
 template <bool ref_count>
+template <bool ref_count2>
 NodeTemplate<true>
-NodeTemplate<ref_count>::eqNode(const NodeTemplate<ref_count>& right) const {
+NodeTemplate<ref_count>::eqNode(const NodeTemplate<ref_count2>& right) const {
   assertTNodeNotExpired();
   return NodeManager::currentNM()->mkNode(kind::EQUAL, *this, right);
 }
@@ -1098,44 +1108,50 @@ NodeTemplate<true> NodeTemplate<ref_count>::notNode() const {
 }
 
 template <bool ref_count>
+template <bool ref_count2>
 NodeTemplate<true>
-NodeTemplate<ref_count>::andNode(const NodeTemplate<ref_count>& right) const {
+NodeTemplate<ref_count>::andNode(const NodeTemplate<ref_count2>& right) const {
   assertTNodeNotExpired();
   return NodeManager::currentNM()->mkNode(kind::AND, *this, right);
 }
 
 template <bool ref_count>
+template <bool ref_count2>
 NodeTemplate<true>
-NodeTemplate<ref_count>::orNode(const NodeTemplate<ref_count>& right) const {
+NodeTemplate<ref_count>::orNode(const NodeTemplate<ref_count2>& right) const {
   assertTNodeNotExpired();
   return NodeManager::currentNM()->mkNode(kind::OR, *this, right);
 }
 
 template <bool ref_count>
+template <bool ref_count2, bool ref_count3>
 NodeTemplate<true>
-NodeTemplate<ref_count>::iteNode(const NodeTemplate<ref_count>& thenpart,
-                                 const NodeTemplate<ref_count>& elsepart) const {
+NodeTemplate<ref_count>::iteNode(const NodeTemplate<ref_count2>& thenpart,
+                                 const NodeTemplate<ref_count3>& elsepart) const {
   assertTNodeNotExpired();
   return NodeManager::currentNM()->mkNode(kind::ITE, *this, thenpart, elsepart);
 }
 
 template <bool ref_count>
+template <bool ref_count2>
 NodeTemplate<true>
-NodeTemplate<ref_count>::iffNode(const NodeTemplate<ref_count>& right) const {
+NodeTemplate<ref_count>::iffNode(const NodeTemplate<ref_count2>& right) const {
   assertTNodeNotExpired();
   return NodeManager::currentNM()->mkNode(kind::IFF, *this, right);
 }
 
 template <bool ref_count>
+template <bool ref_count2>
 NodeTemplate<true>
-NodeTemplate<ref_count>::impNode(const NodeTemplate<ref_count>& right) const {
+NodeTemplate<ref_count>::impNode(const NodeTemplate<ref_count2>& right) const {
   assertTNodeNotExpired();
   return NodeManager::currentNM()->mkNode(kind::IMPLIES, *this, right);
 }
 
 template <bool ref_count>
+template <bool ref_count2>
 NodeTemplate<true>
-NodeTemplate<ref_count>::xorNode(const NodeTemplate<ref_count>& right) const {
+NodeTemplate<ref_count>::xorNode(const NodeTemplate<ref_count2>& right) const {
   assertTNodeNotExpired();
   return NodeManager::currentNM()->mkNode(kind::XOR, *this, right);
 }
@@ -1273,11 +1289,13 @@ NodeTemplate<ref_count>::substitute(Iterator1 nodesBegin,
   }
 
   // otherwise compute
-  Assert( nodesEnd - nodesBegin == replacementsEnd - replacementsBegin,
+  Assert( std::distance(nodesBegin, nodesEnd) == std::distance(replacementsBegin, replacementsEnd),
           "Substitution iterator ranges must be equal size" );
-  Iterator1 j = find(nodesBegin, nodesEnd, *this);
+  Iterator1 j = find(nodesBegin, nodesEnd, TNode(*this));
   if(j != nodesEnd) {
-    Node n = *(replacementsBegin + (j - nodesBegin));
+    Iterator2 b = replacementsBegin;
+    std::advance(b, std::distance(nodesBegin, j));
+    Node n = *b;
     cache[*this] = n;
     return n;
   } else if(getNumChildren() == 0) {
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 156d14299..2cb2527b2 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -5,7 +5,7 @@
  ** Major contributors: dejan
  ** Minor contributors (to current version): taking, cconway
  ** 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/expr/node_manager.cpp b/src/expr/node_manager.cpp
index ce3db4a40..3b4d8ac66 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -18,21 +18,15 @@
  ** Reviewed by Chris Conway, Apr 5 2010 (bug #65).
  **/
 
-#include "node_manager.h"
-
-#include "theory/builtin/theory_builtin_type_rules.h"
-#include "theory/booleans/theory_bool_type_rules.h"
-#include "theory/uf/theory_uf_type_rules.h"
-#include "theory/arith/theory_arith_type_rules.h"
-#include "theory/arrays/theory_arrays_type_rules.h"
-#include "theory/bv/theory_bv_type_rules.h"
-#include "theory/datatypes/theory_datatypes_type_rules.h"
+#include "expr/node_manager.h"
 
 #include "util/Assert.h"
 #include "util/options.h"
 #include "util/stats.h"
 #include "util/tls.h"
 
+#include "expr/type_checker.h"
+
 #include <algorithm>
 #include <stack>
 #include <ext/hash_set>
@@ -241,234 +235,6 @@ void NodeManager::reclaimZombies() {
   }
 }/* NodeManager::reclaimZombies() */
 
-TypeNode NodeManager::computeType(TNode n, bool check)
-  throw (TypeCheckingExceptionPrivate, AssertionException) {
-  TypeNode typeNode;
-
-  // Infer the type
-  switch(n.getKind()) {
-  case kind::VARIABLE:
-    typeNode = getAttribute(n, TypeAttr());
-    break;
-  case kind::SKOLEM:
-    typeNode = getAttribute(n, TypeAttr());
-    break;
-  case kind::BUILTIN:
-    typeNode = builtinOperatorType();
-    break;
-  case kind::SORT_TYPE:
-    typeNode = kindType();
-    break;
-  case kind::APPLY:
-    typeNode = CVC4::theory::builtin::ApplyTypeRule::computeType(this, n, check);
-    break;
-  case kind::EQUAL:
-    typeNode = CVC4::theory::builtin::EqualityTypeRule::computeType(this, n, check);
-    break;
-  case kind::DISTINCT:
-    typeNode = CVC4::theory::builtin::DistinctTypeRule::computeType(this, n, check);
-    break;
-  case kind::TUPLE:
-    typeNode = CVC4::theory::builtin::TupleTypeRule::computeType(this, n, check);
-    break;
-  case kind::CONST_BOOLEAN:
-    typeNode = CVC4::theory::boolean::BooleanTypeRule::computeType(this, n, check);
-    break;
-  case kind::NOT:
-    typeNode = CVC4::theory::boolean::BooleanTypeRule::computeType(this, n, check);
-    break;
-  case kind::AND:
-    typeNode = CVC4::theory::boolean::BooleanTypeRule::computeType(this, n, check);
-    break;
-  case kind::IFF:
-    typeNode = CVC4::theory::boolean::BooleanTypeRule::computeType(this, n, check);
-    break;
-  case kind::IMPLIES:
-    typeNode = CVC4::theory::boolean::BooleanTypeRule::computeType(this, n, check);
-    break;
-  case kind::OR:
-    typeNode = CVC4::theory::boolean::BooleanTypeRule::computeType(this, n, check);
-    break;
-  case kind::XOR:
-    typeNode = CVC4::theory::boolean::BooleanTypeRule::computeType(this, n, check);
-    break;
-  case kind::ITE:
-    typeNode = CVC4::theory::boolean::IteTypeRule::computeType(this, n, check);
-    break;
-  case kind::APPLY_UF:
-    typeNode = CVC4::theory::uf::UfTypeRule::computeType(this, n, check);
-    break;
-  case kind::PLUS:
-    typeNode = CVC4::theory::arith::ArithOperatorTypeRule::computeType(this, n, check);
-    break;
-  case kind::MULT:
-    typeNode = CVC4::theory::arith::ArithOperatorTypeRule::computeType(this, n, check);
-    break;
-  case kind::MINUS:
-    typeNode = CVC4::theory::arith::ArithOperatorTypeRule::computeType(this, n, check);
-    break;
-  case kind::UMINUS:
-    typeNode = CVC4::theory::arith::ArithOperatorTypeRule::computeType(this, n, check);
-    break;
-  case kind::DIVISION:
-    typeNode = CVC4::theory::arith::ArithOperatorTypeRule::computeType(this, n, check);
-    break;
-  case kind::CONST_RATIONAL:
-    typeNode = CVC4::theory::arith::ArithConstantTypeRule::computeType(this, n, check);
-    break;
-  case kind::CONST_INTEGER:
-    typeNode = CVC4::theory::arith::ArithConstantTypeRule::computeType(this, n, check);
-    break;
-  case kind::LT:
-    typeNode = CVC4::theory::arith::ArithPredicateTypeRule::computeType(this, n, check);
-    break;
-  case kind::LEQ:
-    typeNode = CVC4::theory::arith::ArithPredicateTypeRule::computeType(this, n, check);
-    break;
-  case kind::GT:
-    typeNode = CVC4::theory::arith::ArithPredicateTypeRule::computeType(this, n, check);
-    break;
-  case kind::GEQ:
-    typeNode = CVC4::theory::arith::ArithPredicateTypeRule::computeType(this, n, check);
-    break;
-  case kind::SELECT:
-    typeNode = CVC4::theory::arrays::ArraySelectTypeRule::computeType(this, n, check);
-    break;
-  case kind::STORE:
-    typeNode = CVC4::theory::arrays::ArrayStoreTypeRule::computeType(this, n, check);
-    break;
-  case kind::CONST_BITVECTOR:
-    typeNode = CVC4::theory::bv::BitVectorConstantTypeRule::computeType(this, n, check);
-    break;
-  case kind::BITVECTOR_AND:
-    typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check);
-    break;
-  case kind::BITVECTOR_OR:
-    typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check);
-    break;
-  case kind::BITVECTOR_XOR:
-    typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check);
-    break;
-  case kind::BITVECTOR_NOT:
-    typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check);
-    break;
-  case kind::BITVECTOR_NAND:
-    typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check);
-    break;
-  case kind::BITVECTOR_NOR:
-    typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check);
-    break;
-  case kind::BITVECTOR_XNOR:
-    typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check);
-    break;
-  case kind::BITVECTOR_COMP:
-    typeNode = CVC4::theory::bv::BitVectorCompRule::computeType(this, n, check);
-    break;
-  case kind::BITVECTOR_MULT:
-    typeNode = CVC4::theory::bv::BitVectorArithRule::computeType(this, n, check);
-    break;
-  case kind::BITVECTOR_PLUS:
-    typeNode = CVC4::theory::bv::BitVectorArithRule::computeType(this, n, check);
-    break;
-  case kind::BITVECTOR_SUB:
-    typeNode = CVC4::theory::bv::BitVectorArithRule::computeType(this, n, check);
-    break;
-  case kind::BITVECTOR_NEG:
-    typeNode = CVC4::theory::bv::BitVectorArithRule::computeType(this, n, check);
-    break;
-  case kind::BITVECTOR_UDIV:
-    typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check);
-    break;
-  case kind::BITVECTOR_UREM:
-    typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check);
-    break;
-  case kind::BITVECTOR_SDIV:
-    typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check);
-    break;
-  case kind::BITVECTOR_SREM:
-    typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check);
-    break;
-  case kind::BITVECTOR_SMOD:
-    typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check);
-    break;
-  case kind::BITVECTOR_SHL:
-    typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check);
-    break;
-  case kind::BITVECTOR_LSHR:
-    typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check);
-    break;
-  case kind::BITVECTOR_ASHR:
-    typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check);
-    break;
-  case kind::BITVECTOR_ROTATE_LEFT:
-    typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check);
-    break;
-  case kind::BITVECTOR_ROTATE_RIGHT:
-    typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check);
-    break;
-  case kind::BITVECTOR_ULT:
-    typeNode = CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(this, n, check);
-    break;
-  case kind::BITVECTOR_ULE:
-    typeNode = CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(this, n, check);
-    break;
-  case kind::BITVECTOR_UGT:
-    typeNode = CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(this, n, check);
-    break;
-  case kind::BITVECTOR_UGE:
-    typeNode = CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(this, n, check);
-    break;
-  case kind::BITVECTOR_SLT:
-    typeNode = CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(this, n, check);
-    break;
-  case kind::BITVECTOR_SLE:
-    typeNode = CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(this, n, check);
-    break;
-  case kind::BITVECTOR_SGT:
-    typeNode = CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(this, n, check);
-    break;
-  case kind::BITVECTOR_SGE:
-    typeNode = CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(this, n, check);
-    break;
-  case kind::BITVECTOR_EXTRACT:
-    typeNode = CVC4::theory::bv::BitVectorExtractTypeRule::computeType(this, n, check);
-    break;
-  case kind::BITVECTOR_CONCAT:
-    typeNode = CVC4::theory::bv::BitVectorConcatRule::computeType(this, n, check);
-    break;
-  case kind::BITVECTOR_REPEAT:
-    typeNode = CVC4::theory::bv::BitVectorRepeatTypeRule::computeType(this, n, check);
-    break;
-  case kind::BITVECTOR_ZERO_EXTEND:
-    typeNode = CVC4::theory::bv::BitVectorExtendTypeRule::computeType(this, n, check);
-    break;
-  case kind::BITVECTOR_SIGN_EXTEND:
-    typeNode = CVC4::theory::bv::BitVectorExtendTypeRule::computeType(this, n, check);
-    break;
-  case kind::APPLY_CONSTRUCTOR:
-    typeNode = CVC4::theory::datatypes::DatatypeConstructorTypeRule::computeType(this, n, check);
-    break;
-  case kind::APPLY_SELECTOR:
-    typeNode = CVC4::theory::datatypes::DatatypeSelectorTypeRule::computeType(this, n, check);
-    break;
-  case kind::APPLY_TESTER:
-    typeNode = CVC4::theory::datatypes::DatatypeTesterTypeRule::computeType(this, n, check);
-    break;
-  case kind::APPLY_TYPE_ASCRIPTION:
-    typeNode = CVC4::theory::datatypes::DatatypeAscriptionTypeRule::computeType(this, n, check);
-    break;
-  default:
-    Debug("getType") << "FAILURE" << std::endl;
-    Unhandled(n.getKind());
-  }
-
-  setAttribute(n, TypeAttr(), typeNode);
-  setAttribute(n, TypeCheckedAttr(),
-               check || getAttribute(n, TypeCheckedAttr()));
-
-  return typeNode;
-}
-
 TypeNode NodeManager::getType(TNode n, bool check)
   throw (TypeCheckingExceptionPrivate, AssertionException) {
   // Many theories' type checkers call Node::getType() directly.
@@ -510,7 +276,7 @@ TypeNode NodeManager::getType(TNode n, bool check)
 
       if( readyToCompute ) {
         /* All the children have types, time to compute */
-        typeNode = computeType(m, check);
+        typeNode = TypeChecker::computeType(this, m, check);
         worklist.pop();
       }
     } // end while
@@ -520,7 +286,7 @@ TypeNode NodeManager::getType(TNode n, bool check)
   } else if( !hasType || needsCheck ) {
     /* We can compute the type top-down, without worrying about
        deep recursion. */
-    typeNode = computeType(n, check);
+    typeNode = TypeChecker::computeType(this, n, check);
   }
 
   /* The type should be have been computed and stored. */
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 0ac215f1e..6adcb62a9 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -11,7 +11,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief A manager for Nodes.
+ ** \brief A manager for Nodes
  **
  ** A manager for Nodes.
  **
@@ -48,6 +48,8 @@ class StatisticsRegistry;
 
 namespace expr {
 
+class TypeChecker;
+
 // Definition of an attribute for the variable name.
 // TODO: hide this attribute behind a NodeManager interface.
 namespace attr {
@@ -64,6 +66,7 @@ class NodeManager {
   template <unsigned nchild_thresh> friend class CVC4::NodeBuilder;
   friend class NodeManagerScope;
   friend class expr::NodeValue;
+  friend class expr::TypeChecker;
 
   /** Predicate for use with STL algorithms */
   struct NodeValueReferenceCountNonZero {
@@ -250,9 +253,6 @@ class NodeManager {
   // undefined private copy constructor (disallow copy)
   NodeManager(const NodeManager&) CVC4_UNDEFINED;
 
-  TypeNode computeType(TNode n, bool check = false)
-    throw (TypeCheckingExceptionPrivate, AssertionException);
-
   void init();
 
 public:
diff --git a/src/expr/node_self_iterator.h b/src/expr/node_self_iterator.h
index c38243b0a..37c28ab07 100644
--- a/src/expr/node_self_iterator.h
+++ b/src/expr/node_self_iterator.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** 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/expr/node_value.cpp b/src/expr/node_value.cpp
index 666462875..5fe48b01d 100644
--- a/src/expr/node_value.cpp
+++ b/src/expr/node_value.cpp
@@ -2,10 +2,10 @@
 /*! \file node_value.cpp
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): dejan
+ ** Major contributors: dejan
+ ** 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/expr/node_value.h b/src/expr/node_value.h
index 2c11b58d5..71aa37926 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -2,10 +2,10 @@
 /*! \file node_value.h
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: dejan
- ** Minor contributors (to current version): cconway, taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): cconway, taking, dejan
  ** 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/expr/type.cpp b/src/expr/type.cpp
index e162065b0..28bcb460f 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: cconway
  ** Major contributors: dejan, 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
diff --git a/src/expr/type.h b/src/expr/type.h
index a63ca6cf0..5bff8d12a 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -2,8 +2,8 @@
 /*! \file type.h
  ** \verbatim
  ** Original author: cconway
- ** Major contributors: mdeters, dejan
- ** Minor contributors (to current version): none
+ ** Major contributors: dejan, mdeters
+ ** 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
@@ -397,7 +397,7 @@ class CVC4_PUBLIC BooleanType : public Type {
 public:
 
   /** Construct from the base type */
-  BooleanType(const Type& type) throw(AssertionException);
+  BooleanType(const Type& type = Type()) throw(AssertionException);
 };/* class BooleanType */
 
 /**
@@ -408,7 +408,7 @@ class CVC4_PUBLIC IntegerType : public Type {
 public:
 
   /** Construct from the base type */
-  IntegerType(const Type& type) throw(AssertionException);
+  IntegerType(const Type& type = Type()) throw(AssertionException);
 };/* class IntegerType */
 
 /**
@@ -419,7 +419,7 @@ class CVC4_PUBLIC RealType : public Type {
 public:
 
   /** Construct from the base type */
-  RealType(const Type& type) throw(AssertionException);
+  RealType(const Type& type = Type()) throw(AssertionException);
 };/* class RealType */
 
 /**
@@ -441,7 +441,7 @@ class CVC4_PUBLIC FunctionType : public Type {
 public:
 
   /** Construct from the base type */
-  FunctionType(const Type& type) throw(AssertionException);
+  FunctionType(const Type& type = Type()) throw(AssertionException);
 
   /** Get the argument types */
   std::vector<Type> getArgTypes() const;
@@ -458,7 +458,7 @@ class CVC4_PUBLIC TupleType : public Type {
 public:
 
   /** Construct from the base type */
-  TupleType(const Type& type) throw(AssertionException);
+  TupleType(const Type& type = Type()) throw(AssertionException);
 
   /** Get the constituent types */
   std::vector<Type> getTypes() const;
@@ -472,7 +472,7 @@ class CVC4_PUBLIC ArrayType : public Type {
 public:
 
   /** Construct from the base type */
-  ArrayType(const Type& type) throw(AssertionException);
+  ArrayType(const Type& type = Type()) throw(AssertionException);
 
   /** Get the index type */
   Type getIndexType() const;
@@ -489,7 +489,7 @@ class CVC4_PUBLIC SortType : public Type {
 public:
 
   /** Construct from the base type */
-  SortType(const Type& type) throw(AssertionException);
+  SortType(const Type& type = Type()) throw(AssertionException);
 
   /** Get the name of the sort */
   std::string getName() const;
@@ -510,7 +510,7 @@ class CVC4_PUBLIC SortConstructorType : public Type {
 public:
 
   /** Construct from the base type */
-  SortConstructorType(const Type& type) throw(AssertionException);
+  SortConstructorType(const Type& type = Type()) throw(AssertionException);
 
   /** Get the name of the sort constructor */
   std::string getName() const;
@@ -530,7 +530,7 @@ class CVC4_PUBLIC KindType : public Type {
 public:
 
   /** Construct from the base type */
-  KindType(const Type& type) throw(AssertionException);
+  KindType(const Type& type = Type()) throw(AssertionException);
 };/* class KindType */
 
 /**
@@ -541,7 +541,7 @@ class CVC4_PUBLIC BitVectorType : public Type {
 public:
 
   /** Construct from the base type */
-  BitVectorType(const Type& type) throw(AssertionException);
+  BitVectorType(const Type& type = Type()) throw(AssertionException);
 
   /**
    * Returns the size of the bit-vector type.
@@ -559,7 +559,7 @@ class CVC4_PUBLIC DatatypeType : public Type {
 public:
 
   /** Construct from the base type */
-  DatatypeType(const Type& type) throw(AssertionException);
+  DatatypeType(const Type& type = Type()) throw(AssertionException);
 
   /** Get the underlying datatype */
   const Datatype& getDatatype() const;
@@ -599,7 +599,7 @@ class CVC4_PUBLIC ConstructorType : public Type {
 public:
 
   /** Construct from the base type */
-  ConstructorType(const Type& type) throw(AssertionException);
+  ConstructorType(const Type& type = Type()) throw(AssertionException);
 
   /** Get the range type */
   DatatypeType getRangeType() const;
@@ -621,7 +621,7 @@ class CVC4_PUBLIC SelectorType : public Type {
 public:
 
   /** Construct from the base type */
-  SelectorType(const Type& type) throw(AssertionException);
+  SelectorType(const Type& type = Type()) throw(AssertionException);
 
   /** Get the domain type for this selector (the datatype type) */
   DatatypeType getDomain() const;
@@ -639,7 +639,7 @@ class CVC4_PUBLIC TesterType : public Type {
 public:
 
   /** Construct from the base type */
-  TesterType(const Type& type) throw(AssertionException);
+  TesterType(const Type& type = Type()) throw(AssertionException);
 
   /** Get the type that this tester tests (the datatype type) */
   DatatypeType getDomain() const;
diff --git a/src/expr/type_checker.h b/src/expr/type_checker.h
new file mode 100644
index 000000000..0c8093469
--- /dev/null
+++ b/src/expr/type_checker.h
@@ -0,0 +1,40 @@
+/*********************                                                        */
+/*! \file type_checker.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: cconway, dejan
+ ** Minor contributors (to current version): acsys, 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 A type checker
+ **
+ ** A type checker.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__EXPR__TYPE_CHECKER_H
+#define __CVC4__EXPR__TYPE_CHECKER_H
+
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace expr {
+
+class TypeChecker {
+public:
+
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check = false)
+    throw (TypeCheckingExceptionPrivate, AssertionException);
+
+};/* class TypeChecker */
+
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__EXPR__TYPE_CHECKER_H */
diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp
new file mode 100644
index 000000000..2791376b5
--- /dev/null
+++ b/src/expr/type_checker_template.cpp
@@ -0,0 +1,66 @@
+/*********************                                                        */
+/*! \file type_checker_template.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** 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 TypeChecker implementation
+ **
+ ** TypeChecker implementation.
+ **/
+
+#line 20 "${template}"
+
+#include "expr/type_checker.h"
+#include "expr/node_manager.h"
+
+${typechecker_includes}
+
+#line 27 "${template}"
+
+namespace CVC4 {
+namespace expr {
+
+TypeNode TypeChecker::computeType(NodeManager* nodeManager, TNode n, bool check)
+  throw (TypeCheckingExceptionPrivate, AssertionException) {
+  TypeNode typeNode;
+
+  // Infer the type
+  switch(n.getKind()) {
+  case kind::VARIABLE:
+  case kind::SKOLEM:
+    typeNode = nodeManager->getAttribute(n, NodeManager::TypeAttr());
+    break;
+  case kind::BUILTIN:
+    typeNode = nodeManager->builtinOperatorType();
+    break;
+  case kind::SORT_TYPE:
+    typeNode = nodeManager->kindType();
+    break;
+
+${typerules}
+
+#line 51 "${template}"
+
+  default:
+    Debug("getType") << "FAILURE" << std::endl;
+    Unhandled(n.getKind());
+  }
+
+  nodeManager->setAttribute(n, NodeManager::TypeAttr(), typeNode);
+  nodeManager->setAttribute(n, NodeManager::TypeCheckedAttr(),
+                            check || nodeManager->getAttribute(n, NodeManager::TypeCheckedAttr()));
+
+  return typeNode;
+
+}/* TypeChecker::computeType */
+
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 76a084204..51d86904a 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -2,8 +2,8 @@
 /*! \file type_node.cpp
  ** \verbatim
  ** Original author: dejan
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): taking, 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
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 3f4e52d36..25af3aae6 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: dejan
  ** Major contributors: mdeters
- ** Minor contributors (to current version): taking
+ ** Minor contributors (to current version): taking, 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