* theory "tree" rewriting implemented and works

* added TheoryArith::preRewrite() to test and demonstrate
  the use of pre-rewriting.

* array types and type checking now supported

* array type checking now supported

* theoryOf() dispatching properly to arrays now

* theories now required to implement a (simple) identify()
  function that returns a string identifying them for
  debugging/user output purposes

* added "builtin" theory to hold all built-in kinds and their
  type rules and rewriting (currently only exploding distinct)

* fixed production build failure (regarding NodeSetDepth)

* removed an errant "using namespace std" in util/bitvector.h
  (and made associated trivial fixes elsewhere)

* fixes to make unexpected exceptions more verbose in debug builds

* fixes to make multiple, cascading assertion fails simpler

* minor other fixes to comments etc.

26 files changed, 983 insertions, 210 deletions

diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am
index d0d2f23d7..bb9d19b25 100644
--- a/src/theory/Makefile.am
+++ b/src/theory/Makefile.am
@@ -14,6 +14,7 @@ libtheory_la_SOURCES = \
 	theory.cpp
 
 libtheory_la_LIBADD = \
+	@builddir@/builtin/libbuiltin.la \
 	@builddir@/booleans/libbooleans.la \
 	@builddir@/uf/libuf.la \
 	@builddir@/arith/libarith.la \
@@ -38,4 +39,4 @@ BUILT_SOURCES = @srcdir@/theoryof_table.h
 dist-hook: @srcdir@/theoryof_table.h
 MAINTAINERCLEANFILES = @srcdir@/theoryof_table.h
 
-SUBDIRS = booleans uf arith arrays bv
+SUBDIRS = builtin booleans uf arith arrays bv
diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index 4e4088bb0..f270dacb4 100644
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.h
@@ -148,7 +148,7 @@ public:
         }
       }else{
         d_nonbasic.insert(x_j);
-        d_coeffs.insert(make_pair(x_j,a_sj));
+        d_coeffs.insert(std::make_pair(x_j,a_sj));
       }
     }
   }
@@ -289,7 +289,7 @@ public:
     d_activeRows.erase(basic);
     d_activeBasicVars.erase(basic);
 
-    d_inactiveRows.insert(make_pair(basic, row));
+    d_inactiveRows.insert(std::make_pair(basic, row));
   }
 
   void reinjectBasic(TNode basic){
@@ -299,7 +299,7 @@ public:
 
     d_inactiveRows.erase(basic);
     d_activeBasicVars.insert(basic);
-    d_activeRows.insert(make_pair(basic, row));
+    d_activeRows.insert(std::make_pair(basic, row));
 
     updateRow(row);
   }
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 26d554356..cb9dc85f7 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -315,6 +315,34 @@ DeltaRational TheoryArith::computeRowValueUsingSavedAssignment(TNode x){
   return sum;
 }
 
+RewriteResponse TheoryArith::preRewrite(TNode n, bool topLevel) {
+  // Look for multiplications with a 0 argument and rewrite the whole
+  // thing as 0
+  if(n.getKind() == MULT) {
+    Rational ratZero;
+    Integer intZero;
+    for(TNode::iterator i = n.begin(); i != n.end(); ++i) {
+      if((*i).getKind() == CONST_RATIONAL) {
+        if((*i).getConst<Rational>() == ratZero) {
+          n = NodeManager::currentNM()->mkConst(ratZero);
+          break;
+        }
+      } else if((*i).getKind() == CONST_INTEGER) {
+        if((*i).getConst<Integer>() == intZero) {
+          if(n.getType().isInteger()) {
+            n = NodeManager::currentNM()->mkConst(intZero);
+            break;
+          } else {
+            n = NodeManager::currentNM()->mkConst(ratZero);
+            break;
+          }
+        }
+      }
+    }
+  }
+  return RewritingComplete(Node(n));
+}
+
 Node TheoryArith::rewrite(TNode n){
   Debug("arith") << "rewrite(" << n << ")" << endl;
 
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index ba9b5329d..465adacbc 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -41,7 +41,6 @@ namespace CVC4 {
 namespace theory {
 namespace arith {
 
-
 /**
  * Implementation of QF_LRA.
  * Based upon:
@@ -109,6 +108,18 @@ public:
   Node rewrite(TNode n);
 
   /**
+   * Rewriting optimizations.
+   */
+  RewriteResponse preRewrite(TNode n, bool topLevel);
+
+  /**
+   * Plug in old rewrite to the new (pre,post)rewrite interface.
+   */
+  RewriteResponse postRewrite(TNode n, bool topLevel) {
+    return RewritingComplete(topLevel ? rewrite(n) : Node(n));
+  }
+
+  /**
    * Does non-context dependent setup for a node connected to a theory.
    */
   void preRegisterTerm(TNode n);
@@ -122,6 +133,7 @@ public:
 
   void shutdown(){ }
 
+  std::string identify() const { return std::string("TheoryArith"); }
 
 private:
   /**
@@ -254,7 +266,7 @@ private:
   Statistics d_statistics;
 
 
-};
+};/* class TheoryArith */
 
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h
index a995f90af..9b22b14bb 100644
--- a/src/theory/arith/theory_arith_type_rules.h
+++ b/src/theory/arith/theory_arith_type_rules.h
@@ -17,8 +17,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY_ARITH_TYPE_RULES_H_
-#define __CVC4__THEORY_ARITH_TYPE_RULES_H_
+#ifndef __CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H
+#define __CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H
 
 namespace CVC4 {
 namespace theory {
@@ -72,8 +72,8 @@ public:
   }
 };
 
-}
-}
-}
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
 
-#endif /* THEORY_ARITH_TYPE_RULES_H_ */
+#endif /* __CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H */
diff --git a/src/theory/arrays/Makefile.am b/src/theory/arrays/Makefile.am
index 84b9faaf4..0c6e9006f 100644
--- a/src/theory/arrays/Makefile.am
+++ b/src/theory/arrays/Makefile.am
@@ -6,6 +6,7 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
 noinst_LTLIBRARIES = libarrays.la
 
 libarrays_la_SOURCES = \
+	theory_arrays_type_rules.h \
 	theory_arrays.h \
 	theory_arrays.cpp
 
diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds
index 742b924c6..68daa8cb5 100644
--- a/src/theory/arrays/kinds
+++ b/src/theory/arrays/kinds
@@ -5,5 +5,11 @@
 #
 
 theory ::CVC4::theory::arrays::TheoryArrays "theory_arrays.h"
+
+operator ARRAY_TYPE 2 "array type"
+
+# select a i  is  a[i]
 operator SELECT 2 "array select"
+
+# store a i e  is  a[i] <= e
 operator STORE 3 "array store"
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 52e63831c..69498cfb2 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -23,9 +23,7 @@
 
 #include "theory/theory.h"
 
-namespace context {
-class Context;
-}
+#include <iostream>
 
 namespace CVC4 {
 namespace theory {
@@ -37,10 +35,25 @@ public:
   ~TheoryArrays();
   void preRegisterTerm(TNode n) { }
   void registerTerm(TNode n) { }
+
+  RewriteResponse preRewrite(TNode in, bool topLevel) {
+    Debug("arrays-rewrite") << "pre-rewriting " << in
+                            << " topLevel==" << topLevel << std::endl;
+    return RewritingComplete(in);
+  }
+
+  RewriteResponse postRewrite(TNode in, bool topLevel) {
+    Debug("arrays-rewrite") << "post-rewriting " << in
+                            << " topLevel==" << topLevel << std::endl;
+    return RewritingComplete(in);
+  }
+
   void check(Effort e);
   void propagate(Effort e) { }
   void explain(TNode n, Effort e) { }
-};
+  void shutdown() { }
+  std::string identify() const { return std::string("TheoryArrays"); }
+};/* class TheoryArrays */
 
 }/* CVC4::theory::arrays namespace */
 }/* CVC4::theory namespace */
diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h
new file mode 100644
index 000000000..0eb88d800
--- /dev/null
+++ b/src/theory/arrays/theory_arrays_type_rules.h
@@ -0,0 +1,62 @@
+/*********************                                                        */
+/*! \file theory_arrays_type_rules.h
+ ** \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  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 Theory of arrays.
+ **
+ ** Theory of arrays.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H_
+#define __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H_
+
+namespace CVC4 {
+namespace theory {
+namespace arrays {
+
+struct ArraySelectTypeRule {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
+    throw (TypeCheckingExceptionPrivate) {
+    Assert(n.getKind() == kind::SELECT);
+    TypeNode arrayType = n[0].getType();
+    TypeNode indexType = n[1].getType();
+    if(arrayType.getArrayIndexType() != indexType) {
+      throw TypeCheckingExceptionPrivate(n, "array select not indexed with correct type for array");
+    }
+    return arrayType.getArrayConstituentType();
+  }
+};/* struct ArraySelectTypeRule */
+
+struct ArrayStoreTypeRule {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
+    throw (TypeCheckingExceptionPrivate) {
+    Assert(n.getKind() == kind::STORE);
+    TypeNode arrayType = n[0].getType();
+    TypeNode indexType = n[1].getType();
+    TypeNode valueType = n[2].getType();
+    if(arrayType.getArrayIndexType() != indexType) {
+      throw TypeCheckingExceptionPrivate(n, "array store not indexed with correct type for array");
+    }
+    if(arrayType.getArrayConstituentType() != valueType) {
+      throw TypeCheckingExceptionPrivate(n, "array store not assigned with correct type for array");
+    }
+    return arrayType;
+  }
+};/* struct ArrayStoreTypeRule */
+
+}/* CVC4::theory::arrays namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H_ */
diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h
index 83effa005..512dfebcc 100644
--- a/src/theory/booleans/theory_bool.h
+++ b/src/theory/booleans/theory_bool.h
@@ -45,7 +45,7 @@ public:
   void check(Effort e) { Unimplemented(); }
   void propagate(Effort e) { Unimplemented(); }
   void explain(TNode n, Effort e) { Unimplemented(); }
-
+  std::string identify() const { return std::string("TheoryBool"); }
 };
 
 }/* CVC4::theory::booleans namespace */
diff --git a/src/theory/builtin/Makefile b/src/theory/builtin/Makefile
new file mode 100644
index 000000000..1dfd8a113
--- /dev/null
+++ b/src/theory/builtin/Makefile
@@ -0,0 +1,4 @@
+topdir = ../../..
+srcdir = src/theory/builtin
+
+include $(topdir)/Makefile.subdir
diff --git a/src/theory/builtin/Makefile.am b/src/theory/builtin/Makefile.am
new file mode 100644
index 000000000..5694dea84
--- /dev/null
+++ b/src/theory/builtin/Makefile.am
@@ -0,0 +1,13 @@
+AM_CPPFLAGS = \
+	-D__BUILDING_CVC4LIB \
+	-I@srcdir@/../../include -I@srcdir@/../..
+AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
+
+noinst_LTLIBRARIES = libbuiltin.la
+
+libbuiltin_la_SOURCES = \
+	theory_builtin_type_rules.h \
+	theory_builtin.h \
+	theory_builtin.cpp
+
+EXTRA_DIST = kinds
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
new file mode 100644
index 000000000..1f22ebef1
--- /dev/null
+++ b/src/theory/builtin/kinds
@@ -0,0 +1,130 @@
+# kinds [for builtin theory]                                          -*- sh -*-
+#
+# This "kinds" file is written in a domain-specific language for
+# declaring CVC4 kinds.  Comments are marked with #, as this line is.
+#
+# The first non-blank, non-comment line in this file must be a theory
+# declaration:
+#
+#   theory [builtin] T header
+#
+# The special tag "builtin" declares that this is the builtin theory.
+# There can be only one and it should be processed first.
+#
+# There are four basic commands for declaring kinds:
+#
+#   variable K ["comment"]
+#
+#     This declares a kind K that has no operator (it's conceptually a
+#     VARIABLE).  This is appropriate for things like VARIABLE and
+#     SKOLEM.
+#
+#   operator K #children ["comment"]
+#
+#     Declares a "built-in" operator kind K.  Really this is the same
+#     as "variable" except that it has an operator (automatically
+#     generated by NodeManager).
+#
+#     You can specify an exact # of children required as the second
+#     argument to the operator command.  In debug mode, assertions are
+#     automatically included to ensure that no Nodes can ever be
+#     created violating this.  (FIXME: the public Expr stuff should
+#     enforce them regardless of whether debugging or not.)  For
+#     example, a binary operator could be specified as:
+#
+#         operator LESS_THAN 2 "arithmetic comparison, x < y"
+#
+#     Alternatively, a range can be specified for #children as
+#     "LB:[UB]", LB and UB representing lower and upper bounds on the
+#     number of children (inclusive).  If there is no lower bound, put
+#     a "0".  If there is no upper bound, leave the colon after LB,
+#     but omit UB.  For example, an N-ary operator might be defined
+#     as:
+#
+#         operator PLUS 2: "addition on two or more arguments"
+#
+#   parameterized K #children ["comment"]
+#
+#     Declares a "built-in" parameterized operator kind K.  This is a
+#     theory-specific APPLY, e.g., APPLY_UF, which applies its first
+#     parameter (say, "f"), to its operands (say, "x" and "y", making
+#     the full application "f(x,y)").  Nodes with such a kind will
+#     have an operator (Node::hasOperator() returns true, and
+#     Node::getOperator() returns the Node of functional type
+#     representing "f" here), and the "children" are defined to be
+#     this operator's parameters, and don't include the operator
+#     itself (here, there are only two children "x" and "y").
+#
+#     LB and UB are the same as documented for the operator command.
+#     The first parameter (the function being applied) does not count
+#     as a child.
+#
+#     For consistency these should start with "APPLY_", but this is
+#     not enforced.
+#
+#   constant K T Hasher header ["comment"]
+#
+#     Declares a constant kind K.  T is the C++ type representing the
+#     constant internally (and it should be
+#     ::fully::qualified::like::this), and header is the header needed
+#     to define it.  Hasher is a hash functor type defined like this:
+#
+#       struct MyHashFcn {
+#         static size_t hash(const T& val);
+#       };
+#
+#     For consistency, constants taking a non-void payload should
+#     start with "CONST_", but this is not enforced.
+#
+# Lines may be broken with a backslash between arguments; for example:
+#
+#     constant CONST_INT \
+#         int IntHash \
+#         "" \
+#         "This is a constant representing an INT.
+#         Its payload is the C++ int type.
+#         It is used by the theory of arithmetic."
+#
+# As shown in the example, ["comment"] fields may be broken across
+# multiple lines too.
+#
+# The expr package guarantees that Nodes built with kinds have the
+# following constraints imposed on them.  (The #children guarantee
+# only holds when assertions are turned on.)
+#
+#   Node meta-kind      has operator?      # children
+#   ==================  =================  =======================
+#   variable            no                 zero
+#   operator            yes                as documented above
+#   parameterized       yes                as documented above
+#   constant            no                 zero
+#
+# NOTE THAT This file is actually an executable Bourne shell script
+# (sourced by the processing scripts after defining functions called
+# "theory," "variable," "operator," "parameterized," and "constant").
+# Please don't do anything else in this file other than using these
+# commands.
+#
+
+theory builtin ::CVC4::theory::builtin::TheoryBuiltin "theory_builtin.h"
+
+# A kind representing "inlined" operators defined with OPERATOR
+# Conceptually, (EQUAL a b) is actually an (APPLY EQUAL a b), but it's
+# not stored that way.  If you ask for the operator of (EQUAL a b),
+# you'll get a special, singleton (BUILTIN EQUAL) Node.
+constant BUILTIN ::CVC4::Kind ::CVC4::kind::KindHashStrategy \
+    "expr/kind.h" "The kind of nodes representing built-in operators"
+
+operator EQUAL 2 "equality"
+operator DISTINCT 2: "disequality"
+variable SKOLEM "skolem var"
+variable VARIABLE "variable"
+operator TUPLE 2: "a tuple"
+
+constant TYPE_CONSTANT \
+    ::CVC4::TypeConstant \
+    ::CVC4::TypeConstantHashStrategy \
+    "expr/type_constant.h" \
+    "basic types"
+operator FUNCTION_TYPE 2: "function type"
+variable SORT_TYPE "sort type"
diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp
new file mode 100644
index 000000000..1951e438c
--- /dev/null
+++ b/src/theory/builtin/theory_builtin.cpp
@@ -0,0 +1,69 @@
+/*********************                                                        */
+/*! \file theory_builtin.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  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 Implementation of the builtin theory.
+ **
+ ** Implementation of the builtin theory.
+ **/
+
+#include "theory/builtin/theory_builtin.h"
+#include "expr/kind.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::theory::builtin;
+
+namespace CVC4 {
+namespace theory {
+namespace builtin {
+
+Node blastDistinct(TNode in) {
+  Debug("theory-rewrite") << "blastDistinct: " << in << std::endl;
+  Assert(in.getKind() == kind::DISTINCT);
+  if(in.getNumChildren() == 2) {
+    // if this is the case exactly 1 != pair will be generated so the
+    // AND is not required
+    Node eq = NodeManager::currentNM()->mkNode(CVC4::kind::EQUAL, in[0], in[1]);
+    Node neq = NodeManager::currentNM()->mkNode(CVC4::kind::NOT, eq);
+    return neq;
+  }
+  // assume that in.getNumChildren() > 2 => diseqs.size() > 1
+  vector<Node> diseqs;
+  for(TNode::iterator i = in.begin(); i != in.end(); ++i) {
+    TNode::iterator j = i;
+    while(++j != in.end()) {
+      Node eq = NodeManager::currentNM()->mkNode(CVC4::kind::EQUAL, *i, *j);
+      Node neq = NodeManager::currentNM()->mkNode(CVC4::kind::NOT, eq);
+      diseqs.push_back(neq);
+    }
+  }
+  Node out = NodeManager::currentNM()->mkNode(CVC4::kind::AND, diseqs);
+  return out;
+}
+
+RewriteResponse TheoryBuiltin::postRewrite(TNode in, bool topLevel) {
+  if(topLevel) {
+    if(in.getKind() == kind::DISTINCT) {
+      return RewritingComplete(blastDistinct(in));
+    }
+  }
+
+  // EQUAL is a special case that should never end up here
+  Assert(in.getKind() != kind::EQUAL);
+
+  return RewritingComplete(in);
+}
+
+}/* CVC4::theory::builtin namespace */
+}/* CVC4::theory */
+}/* CVC4 namespace */
diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h
new file mode 100644
index 000000000..5c0a70dea
--- /dev/null
+++ b/src/theory/builtin/theory_builtin.h
@@ -0,0 +1,48 @@
+/*********************                                                        */
+/*! \file theory_builtin.h
+ ** \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  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 Built-in theory.
+ **
+ ** Built-in theory.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H
+#define __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H
+
+#include "theory/theory.h"
+
+namespace CVC4 {
+namespace theory {
+namespace builtin {
+
+class TheoryBuiltin : public Theory {
+public:
+  TheoryBuiltin(context::Context* c, OutputChannel& out) : Theory(c, out) { }
+  ~TheoryBuiltin() { }
+  void preRegisterTerm(TNode n) { Unreachable(); }
+  void registerTerm(TNode n) { Unreachable(); }
+  void check(Effort e) { Unreachable(); }
+  void propagate(Effort e) { Unreachable(); }
+  void explain(TNode n, Effort e) { Unreachable(); }
+  void shutdown() { }
+  RewriteResponse postRewrite(TNode n, bool topLevel);
+  std::string identify() const { return std::string("TheoryBuiltin"); }
+};/* class TheoryBuiltin */
+
+}/* CVC4::theory::builtin namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H */
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
new file mode 100644
index 000000000..0f4fda1a6
--- /dev/null
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -0,0 +1,60 @@
+/*********************                                                        */
+/*! \file builtin_type_rules.cpp
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors: mdeters
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Type rules for the builtin theory
+ **
+ ** Type rules for the builtin theory.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H_
+#define __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H_
+
+#include "expr/node.h"
+#include "expr/type_node.h"
+#include "expr/expr.h"
+
+namespace CVC4 {
+namespace theory {
+namespace builtin {
+
+class EqualityTypeRule {
+  public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n) throw (TypeCheckingExceptionPrivate) {
+    if (n[0].getType() != n[1].getType()) {
+      throw TypeCheckingExceptionPrivate(n, "Left and right hand side of the equation are not of the same type");
+    }
+    return nodeManager->booleanType();
+  }
+};
+
+class DistinctTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n) {
+    TNode::iterator child_it = n.begin();
+    TNode::iterator child_it_end = n.end();
+    TypeNode firstType = (*child_it).getType();
+    for (++child_it; child_it != child_it_end; ++child_it) {
+      if ((*child_it).getType() != firstType) {
+        throw TypeCheckingExceptionPrivate(n, "Not all arguments are of the same type");
+      }
+    }
+    return nodeManager->booleanType();
+  }
+};
+
+}/* CVC4::theory::builtin namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H_ */
diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds
index ba8fc4efd..f1b926d24 100644
--- a/src/theory/bv/kinds
+++ b/src/theory/bv/kinds
@@ -6,6 +6,12 @@
 
 theory ::CVC4::theory::bv::TheoryBV "theory_bv.h"
 
+constant BITVECTOR_TYPE \
+	::CVC4::BitVectorSize \
+	"::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorSize >" \
+	"util/bitvector.h" \
+	"bit-vector type"
+
 constant BITVECTOR_CONST \
     ::CVC4::BitVector \
     ::CVC4::BitVectorHashStrategy \
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index dc29183ea..17d0779ca 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -39,7 +39,8 @@ public:
   void check(Effort e) { Unimplemented(); }
   void propagate(Effort e) { Unimplemented(); }
   void explain(TNode n, Effort e) { Unimplemented(); }
-};
+  std::string identify() const { return std::string("TheoryBV"); }
+};/* class TheoryBV */
 
 }/* CVC4::theory::bv namespace */
 }/* CVC4::theory namespace */
diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h
index 142c9c963..7dd6c3e60 100644
--- a/src/theory/bv/theory_bv_type_rules.h
+++ b/src/theory/bv/theory_bv_type_rules.h
@@ -18,8 +18,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__EXPR_TYPE_THEORY_BV_TYPE_RULES_H_
-#define __CVC4__EXPR_TYPE_THEORY_BV_TYPE_RULES_H_
+#ifndef __CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H
+#define __CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H
 
 namespace CVC4 {
 namespace theory {
@@ -29,7 +29,7 @@ class BitVectorConstantTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
       throw (TypeCheckingExceptionPrivate) {
-    return nodeManager->bitVectorType(n.getConst<BitVector>().getSize());
+    return nodeManager->mkBitVectorType(n.getConst<BitVector>().getSize());
   }
 };
 
@@ -42,7 +42,7 @@ public:
     if (!lhs.isBitVector() || lhs != rhs) {
       throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms of the same width");
     }
-    return nodeManager->bitVectorType(1);
+    return nodeManager->mkBitVectorType(1);
   }
 };
 
@@ -61,7 +61,7 @@ public:
       }
       if (maxWidth < t.getBitVectorSize()) maxWidth = t.getBitVectorSize();
     }
-    return nodeManager->bitVectorType(maxWidth);
+    return nodeManager->mkBitVectorType(maxWidth);
   }
 };
 
@@ -115,7 +115,7 @@ public:
     if (extractInfo.high >= t.getBitVectorSize()) {
       throw TypeCheckingExceptionPrivate(n, "high extract index is bigger than the size of the bit-vector");
     }
-    return nodeManager->bitVectorType(extractInfo.high - extractInfo.low + 1);
+    return nodeManager->mkBitVectorType(extractInfo.high - extractInfo.low + 1);
   }
 };
 
@@ -133,7 +133,7 @@ public:
        }
        size += t.getBitVectorSize();
     }
-    return nodeManager->bitVectorType(size);
+    return nodeManager->mkBitVectorType(size);
   }
 };
 
@@ -146,7 +146,7 @@ public:
       throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
     }
     unsigned repeatAmount = n.getOperator().getConst<BitVectorRepeat>();
-    return nodeManager->bitVectorType(repeatAmount * t.getBitVectorSize());
+    return nodeManager->mkBitVectorType(repeatAmount * t.getBitVectorSize());
   }
 };
 
@@ -162,12 +162,12 @@ public:
         (unsigned) n.getOperator().getConst<BitVectorSignExtend>() :
         (unsigned) n.getOperator().getConst<BitVectorZeroExtend>();
 
-    return nodeManager->bitVectorType(extendAmount +  t.getBitVectorSize());
+    return nodeManager->mkBitVectorType(extendAmount +  t.getBitVectorSize());
   }
 };
 
-}
-}
-}
+}/* CVC4::theory::bv namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
 
-#endif /* __CVC4__EXPR_TYPE_THEORY_BV_TYPE_RULES_H_ */
+#endif /* __CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H */
diff --git a/src/theory/mktheoryof b/src/theory/mktheoryof
index 227831451..4b7dfcef5 100755
--- a/src/theory/mktheoryof
+++ b/src/theory/mktheoryof
@@ -51,6 +51,7 @@ function theory {
       exit 1
     fi
     seen_theory_builtin=true
+    shift
   elif [ -z "$1" -o -z "$2" ]; then
     echo "$kf:$lineno: error: \"theory\" directive missing class or header argument" >&2
     exit 1
@@ -113,6 +114,12 @@ function check_theory_seen {
   fi
 }
 
+function check_builtin_theory_seen {
+  if ! $seen_theory_builtin; then
+    echo "$me: warning: no declaration for the builtin theory found" >&2
+  fi
+}
+
 while [ $# -gt 0 ]; do
   kf=$1
   seen_theory=false
@@ -123,6 +130,7 @@ while [ $# -gt 0 ]; do
 "
   shift
 done
+check_builtin_theory_seen
 
 ## output
 
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 6f4effe78..bb598d410 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -29,7 +29,8 @@
 #include <deque>
 #include <list>
 
-#include <typeinfo>
+#include <string>
+#include <iostream>
 
 namespace CVC4 {
 
@@ -37,9 +38,43 @@ class TheoryEngine;
 
 namespace theory {
 
-// rewrite cache support
-struct RewriteCacheTag {};
-typedef expr::Attribute<RewriteCacheTag, TNode> RewriteCache;
+/**
+ * Instances of this class serve as response codes from
+ * Theory::preRewrite() and Theory::postRewrite().  Instances of
+ * derived classes RewritingComplete(n) and RewriteAgain(n) should
+ * be used for better self-documenting behavior.
+ */
+class RewriteResponse {
+protected:
+  enum Status { DONE, REWRITE };
+
+  RewriteResponse(Status s, Node n) : d_status(s), d_node(n) {}
+
+private:
+  const Status d_status;
+  const Node d_node;
+
+public:
+  bool isDone() const { return d_status == DONE; }
+  bool needsMoreRewriting() const { return d_status == REWRITE; }
+  Node getNode() const { return d_node; }
+};
+
+/**
+ * Return n, but request additional (pre,post)rewriting of it.
+ */
+class RewriteAgain : public RewriteResponse {
+public:
+  RewriteAgain(Node n) : RewriteResponse(REWRITE, n) {}
+};
+
+/**
+ * Signal that (pre,post)rewriting of the node is complete at n.
+ */
+class RewritingComplete : public RewriteResponse {
+public:
+  RewritingComplete(Node n) : RewriteResponse(DONE, n) {}
+};
 
 /**
  * Base class for T-solvers.  Abstract DPLL(T).
@@ -121,6 +156,9 @@ protected:
     d_facts.clear();
   }
 
+  /**
+   * Get the context associated to this Theory.
+   */
   context::Context* getContext() const {
     return d_context;
   }
@@ -142,21 +180,6 @@ protected:
    */
   bool isShared(TNode n) throw();
 
-  /**
-   * Check whether a node is in the rewrite cache or not.
-   */
-  static bool inRewriteCache(TNode n) throw() {
-    return n.hasAttribute(RewriteCache());
-  }
-
-  /**
-   * Get the value of the rewrite cache (or Node::null()) if there is
-   * none).
-   */
-  static Node getRewriteCache(TNode n) throw() {
-    return n.getAttribute(RewriteCache());
-  }
-
   /** Tag for the "registerTerm()-has-been-called" flag on Nodes */
   struct Registered {};
   /** The "registerTerm()-has-been-called" flag on Nodes */
@@ -230,15 +253,31 @@ public:
 
   /**
    * Pre-register a term.  Done one time for a Node, ever.
-   *
    */
   virtual void preRegisterTerm(TNode) = 0;
 
   /**
-   * Rewrite a term.  Done one time for a Node, ever.
+   * Pre-rewrite a term.  This default base-class implementation
+   * simply returns RewritingComplete(n).  A theory should never
+   * rewrite a term to a strictly larger term that contains itself, as
+   * this will cause a loop of hard Node links in the cache (and thus
+   * memory leakage).
    */
-  virtual Node rewrite(TNode n) {
-    return n;
+  virtual RewriteResponse preRewrite(TNode n, bool topLevel) {
+    Debug("theory-rewrite") << "no pre-rewriting to perform for " << n << std::endl;
+    return RewritingComplete(n);
+  }
+
+  /**
+   * Post-rewrite a term.  This default base-class implementation
+   * simply returns RewritingComplete(n).  A theory should never
+   * rewrite a term to a strictly larger term that contains itself, as
+   * this will cause a loop of hard Node links in the cache (and thus
+   * memory leakage).
+   */
+  virtual RewriteResponse postRewrite(TNode n, bool topLevel) {
+    Debug("theory-rewrite") << "no post-rewriting to perform for " << n << std::endl;
+    return RewritingComplete(n);
   }
 
   /**
@@ -285,6 +324,12 @@ public:
    */
   virtual void explain(TNode n, Effort level = FULL_EFFORT) = 0;
 
+  /**
+   * Identify this theory (for debugging, dynamic configuration,
+   * etc..)
+   */
+  virtual std::string identify() const = 0;
+
   //
   // CODE INVARIANT CHECKING (used only with CVC4_ASSERTIONS)
   //
@@ -334,6 +379,11 @@ protected:
 std::ostream& operator<<(std::ostream& os, Theory::Effort level);
 
 }/* CVC4::theory namespace */
+
+inline std::ostream& operator<<(std::ostream& out, const CVC4::theory::Theory& theory) {
+  return out << theory.identify();
+}
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__THEORY__THEORY_H */
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 9dfaed68b..e41df92d0 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -19,13 +19,18 @@
 #include "theory/theory_engine.h"
 #include "expr/node.h"
 #include "expr/attribute.h"
+#include "theory/theory.h"
+#include "expr/node_builder.h"
 
+#include <vector>
 #include <list>
 
 using namespace std;
 
-namespace CVC4 {
+using namespace CVC4;
+using namespace CVC4::theory;
 
+namespace CVC4 {
 namespace theory {
 
 struct PreRegisteredTag {};
@@ -36,6 +41,50 @@ typedef expr::Attribute<IteRewriteTag, Node> IteRewriteAttr;
 
 }/* CVC4::theory namespace */
 
+Theory* TheoryEngine::theoryOf(TNode n) {
+  Kind k = n.getKind();
+
+  Assert(k >= 0 && k < kind::LAST_KIND);
+
+  if(n.getMetaKind() == kind::metakind::VARIABLE) {
+    TypeNode t = n.getType();
+    if(t.isBoolean()) {
+      return &d_bool;
+    } else if(t.isReal()) {
+      return &d_arith;
+    } else if(t.isArray()) {
+      return &d_arrays;
+    } else {
+      return &d_uf;
+    }
+    //Unimplemented();
+  } else if(k == kind::EQUAL) {
+    // if LHS is a variable, use theoryOf(LHS.getType())
+    // otherwise, use theoryOf(LHS)
+    TNode lhs = n[0];
+    if(lhs.getMetaKind() == kind::metakind::VARIABLE) {
+      // FIXME: we don't yet have a Type-to-Theory map.  When we do,
+      // look up the type of the LHS and return that Theory (?)
+
+      //The following JUST hacks around this lack of a table
+      TypeNode type_of_n = lhs.getType();
+      if(type_of_n.isReal()) {
+        return &d_arith;
+      } else if(type_of_n.isArray()) {
+        return &d_arrays;
+      } else {
+        return &d_uf;
+        //Unimplemented();
+      }
+    } else {
+      return theoryOf(lhs);
+    }
+  } else {
+    // use our Kind-to-Theory mapping
+    return d_theoryOfTable[k];
+  }
+}
+
 Node TheoryEngine::preprocess(TNode t) {
   Node top = rewrite(t);
   Debug("rewrite") << "rewrote: " << t << endl << "to     : " << top << endl;
@@ -70,7 +119,7 @@ Node TheoryEngine::preprocess(TNode t) {
    * and the above registration of leaves, this should ensure that
    * all subterms in the entire tree were registered in
    * reverse-topological order. */
-  for(std::list<TNode>::reverse_iterator i = toReg.rbegin();
+  for(list<TNode>::reverse_iterator i = toReg.rbegin();
       i != toReg.rend();
       ++i) {
 
@@ -128,9 +177,11 @@ Node TheoryEngine::removeITEs(TNode node) {
       return skolem;
     }
   }
-  std::vector<Node> newChildren;
+  vector<Node> newChildren;
   bool somethingChanged = false;
-  for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
+  for(TNode::const_iterator it = node.begin(), end = node.end();
+      it != end;
+      ++it) {
     Node newChild = removeITEs(*it);
     somethingChanged |= (newChild != *it);
     newChildren.push_back(newChild);
@@ -145,66 +196,243 @@ Node TheoryEngine::removeITEs(TNode node) {
     nodeManager->setAttribute(node, theory::IteRewriteAttr(), Node::null());
     return node;
   }
-
 }
 
-Node blastDistinct(TNode in){
-  Assert(in.getKind() == kind::DISTINCT);
-  if(in.getNumChildren() == 2){
-    //If this is the case exactly 1 != pair will be generated so the AND is not required
-    Node eq = NodeManager::currentNM()->mkNode(CVC4::kind::EQUAL, in[0], in[1]);
-    Node neq = NodeManager::currentNM()->mkNode(CVC4::kind::NOT, eq);
-    return neq;
-  }
-  //Assume that in.getNumChildren() > 2
-  // => diseqs.size() > 1
-  vector<Node> diseqs;
-  for(TNode::iterator i = in.begin(); i != in.end(); ++i) {
-    TNode::iterator j = i;
-    while(++j != in.end()) {
-      Node eq = NodeManager::currentNM()->mkNode(CVC4::kind::EQUAL, *i, *j);
-      Node neq = NodeManager::currentNM()->mkNode(CVC4::kind::NOT, eq);
-      diseqs.push_back(neq);
-    }
+namespace theory {
+namespace rewrite {
+
+/**
+ * TheoryEngine::rewrite() keeps a stack of things that are being pre-
+ * and post-rewritten.  Each element of the stack is a
+ * RewriteStackElement.
+ */
+struct RewriteStackElement {
+  /**
+   * The node at this rewrite level.  For example (AND (OR x y) z)
+   * will have, as it's rewriting x, the stack:
+   *    x
+   *    (OR x y)
+   *    (AND (OR x y) z)
+   */
+  Node d_node;
+
+  /**
+   * The theory associated to d_node.  Cached here to avoid having to
+   * look it up again.
+   */
+  Theory* d_theory;
+
+  /**
+   * Whether or not this was a top-level rewrite.  Note that at theory
+   * boundaries, topLevel is forced to true, so it's not the case that
+   * this is true only at the lowest stack level.
+   */
+  bool d_topLevel;
+
+  /**
+   * A saved index to the "next child" to pre- and post-rewrite.  In
+   * the case when (AND (OR x y) z) is being rewritten, the AND, OR,
+   * and x are pre-rewritten, then (assuming they don't change), x is
+   * post-rewritten, then y is pre- and post-rewritten, then the OR is
+   * post-rewritten, then z is pre-rewritten, then the AND is
+   * post-rewritten.  At each stack level, we need to remember the
+   * child index we're currently processing.
+   */
+  int d_nextChild;
+
+  /**
+   * A (re)builder for this node.  As this node's children are
+   * post-rewritten, in order, they append to this builder.  When this
+   * node is post-rewritten, it is reformed from d_builder since the
+   * children may have changed.  Note Nodes aren't rebuilt if they
+   * have metakinds CONSTANT (which is illegal) or VARIABLE (which
+   * would create a fresh variable, not what we want)---which is fine,
+   * since those types don't have children anyway.
+   */
+  NodeBuilder<> d_builder;
+
+  /**
+   * Construct a fresh stack element.
+   */
+  RewriteStackElement(Node n, Theory* thy, bool top) :
+    d_node(n),
+    d_theory(thy),
+    d_topLevel(top),
+    d_nextChild(0) {
   }
-  Node out = NodeManager::currentNM()->mkNode(CVC4::kind::AND, diseqs);
-  return out;
-}
+};
+
+}/* CVC4::theory::rewrite namespace */
+}/* CVC4::theory namespace */
 
 Node TheoryEngine::rewrite(TNode in) {
-  if(inRewriteCache(in)) {
-    return getRewriteCache(in);
-  }
+  using theory::rewrite::RewriteStackElement;
+
+  Node noItes = removeITEs(in);
+  Node out;
+
+  // descend top-down into the theory rewriters
+  vector<RewriteStackElement> stack;
+  stack.push_back(RewriteStackElement(noItes, theoryOf(noItes), true));
+  Debug("theory-rewrite") << "TheoryEngine::rewrite() starting at" << endl
+                          << "  " << noItes << " " << theoryOf(noItes)
+                          << " TOP-LEVEL 0" << endl;
+  // This whole thing is essentially recursive, but we avoid actually
+  // doing any recursion.
+  do {// do until the stack is empty..
+   RewriteStackElement& rse = stack.back();
+    bool done;
+
+    Debug("theory-rewrite") << "rewriter looking at level " << stack.size()
+                            << endl
+                            << "  " << rse.d_node << " " << rse.d_theory
+                            << "[" << *rse.d_theory << "]"
+                            << " " << (rse.d_topLevel ? "TOP-LEVEL " : "")
+                            << rse.d_nextChild << endl;
+
+    if(rse.d_nextChild == 0) {
+      Node original = rse.d_node;
+      bool wasTopLevel = rse.d_topLevel;
+      Node cached = getPreRewriteCache(original, wasTopLevel);
+      if(cached.isNull()) {
+        do {
+          Debug("theory-rewrite") << "doing pre-rewrite in " << *rse.d_theory
+                                  << " topLevel==" << rse.d_topLevel << endl;
+          RewriteResponse response =
+            rse.d_theory->preRewrite(rse.d_node, rse.d_topLevel);
+          rse.d_node = response.getNode();
+          Assert(!rse.d_node.isNull(), "node illegally rewritten to null");
+          Theory* thy2 = theoryOf(rse.d_node);
+          Assert(thy2 != NULL, "node illegally rewritten to null theory");
+          Debug("theory-rewrite") << "got back " << rse.d_node << " "
+                                  << thy2 << "[" << *thy2 << "]"
+                                  << (response.needsMoreRewriting() ?
+                                      " MORE-REWRITING" : " DONE")
+                                  << endl;
+          if(rse.d_theory != thy2) {
+            Debug("theory-rewrite") << "pre-rewritten from " << *rse.d_theory
+                                    << " into " << *thy2
+                                    << ", marking top-level and !done" << endl;
+            rse.d_theory = thy2;
+            done = false;
+            // FIXME how to handle the "top-levelness" of a node that's
+            // rewritten from theory T1 into T2, then back to T1 ?
+            rse.d_topLevel = true;
+          } else {
+            done = !response.needsMoreRewriting();
+          }
+        } while(!done);
+        setPreRewriteCache(original, wasTopLevel, rse.d_node);
+      } else {// is in pre-rewrite cache
+        Debug("theory-rewrite") << "in pre-cache: " << cached << endl;
+        rse.d_node = cached;
+        Theory* thy2 = theoryOf(cached);
+        if(rse.d_theory != thy2) {
+          Debug("theory-rewrite") << "[cache-]pre-rewritten from "
+                                  << *rse.d_theory << " into " << *thy2
+                                  << ", marking top-level" << endl;
+          rse.d_theory = thy2;
+          rse.d_topLevel = true;
+        }
+      }
+    }
 
-  if(in.getMetaKind() == kind::metakind::VARIABLE) {
-    return in;
-  }
+    // children
+    Node original = rse.d_node;
+    bool wasTopLevel = rse.d_topLevel;
+    Node cached = getPostRewriteCache(original, wasTopLevel);
+
+    if(cached.isNull()) {
+      if(rse.d_nextChild == 0 &&
+         rse.d_node.getMetaKind() == kind::metakind::PARAMETERIZED) {
+        ++rse.d_nextChild;
+        Node op = rse.d_node.getOperator();
+        Theory* t = theoryOf(op);
+        Debug("theory-rewrite") << "pushing operator of " << rse.d_node << endl;
+        stack.push_back(RewriteStackElement(op, t, t != rse.d_theory));
+        continue;// break out of this node, do its operator
+      } else {
+        unsigned nch = rse.d_nextChild++;
+        if(rse.d_node.getMetaKind() == kind::metakind::PARAMETERIZED) {
+          --nch;
+        }
+        if(nch < rse.d_node.getNumChildren()) {
+          Debug("theory-rewrite") << "pushing child " << nch
+                                  << " of " << rse.d_node << endl;
+          Node c = rse.d_node[nch];
+          Theory* t = theoryOf(c);
+          stack.push_back(RewriteStackElement(c, t, t != rse.d_theory));
+          continue;// break out of this node, do its child
+        }
+      }
 
-  Node intermediate = removeITEs(in);
+      // incorporate the children's rewrites
+      if(rse.d_node.getMetaKind() != kind::metakind::VARIABLE &&
+         rse.d_node.getMetaKind() != kind::metakind::CONSTANT) {
+        Debug("theory-rewrite") << "builder here is " << &rse.d_builder
+                                << " and it gets " << rse.d_node.getKind()
+                                << endl;
+        rse.d_builder << rse.d_node.getKind();
+        rse.d_node = Node(rse.d_builder);
+      }
 
-  // these special cases should go away when theory rewriting comes online
-  if(intermediate.getKind() == kind::DISTINCT) {
-    Node out = blastDistinct(intermediate);
-    //setRewriteCache(intermediate, out);
-    return rewrite(out); //TODO let this fall through?
-  }
+      // post-rewriting
+      do {
+        Debug("theory-rewrite") << "doing post-rewrite of "
+                                << rse.d_node << endl
+                                << " in " << *rse.d_theory
+                                << " topLevel==" << rse.d_topLevel << endl;
+        RewriteResponse response =
+          rse.d_theory->postRewrite(rse.d_node, rse.d_topLevel);
+        rse.d_node = response.getNode();
+        Assert(!rse.d_node.isNull(), "node illegally rewritten to null");
+        Theory* thy2 = theoryOf(rse.d_node);
+        Assert(thy2 != NULL, "node illegally rewritten to null theory");
+        Debug("theory-rewrite") << "got back " << rse.d_node << " "
+                                << thy2 << "[" << *thy2 << "]"
+                                << (response.needsMoreRewriting() ?
+                                    " MORE-REWRITING" : " DONE")
+                                << endl;
+        if(rse.d_theory != thy2) {
+          Debug("theory-rewrite") << "post-rewritten from " << *rse.d_theory
+                                  << " into " << *thy2
+                                  << ", marking top-level and !done" << endl;
+          rse.d_theory = thy2;
+          done = false;
+          // FIXME how to handle the "top-levelness" of a node that's
+          // rewritten from theory T1 into T2, then back to T1 ?
+          rse.d_topLevel = true;
+        } else {
+          done = !response.needsMoreRewriting();
+        }
+      } while(!done);
+
+      setPostRewriteCache(original, wasTopLevel, rse.d_node);
+
+      out = rse.d_node;
+    } else {
+      Debug("theory-rewrite") << "in post-cache: " << cached << endl;
+      out = cached;
+      Theory* thy2 = theoryOf(cached);
+      if(rse.d_theory != thy2) {
+        Debug("theory-rewrite") << "[cache-]post-rewritten from "
+                                << *rse.d_theory << " into " << *thy2 << endl;
+        rse.d_theory = thy2;
+      }
+    }
 
-  theory::Theory* thy = theoryOf(intermediate);
-  if(thy == NULL) {
-    Node out = rewriteBuiltins(intermediate);
-    //setRewriteCache(intermediate, out);
-    return out;
-  } else if(thy != &d_bool){
-    Node out = thy->rewrite(intermediate);
-    //setRewriteCache(intermediate, out);
-    return out;
-  }else{
-    Node out = rewriteChildren(intermediate);
-    //setRewriteCache(intermediate, out);
-    return out;
-  }
+    stack.pop_back();
+    if(!stack.empty()) {
+      Debug("theory-rewrite") << "asserting " << out << " to previous builder "
+                              << &stack.back().d_builder << endl;
+      stack.back().d_builder << out;
+    }
+  } while(!stack.empty());
 
-  Unreachable();
-}
+  Debug("theory-rewrite") << "DONE with theory rewriter." << endl;
+  Debug("theory-rewrite") << "result is:" << endl << out << endl;
+
+  return out;
+}/* TheoryEngine::rewrite(TNode in) */
 
 }/* CVC4 namespace */
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 15b406cdd..2575c4c2d 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -26,6 +26,7 @@
 #include "theory/theoryof_table.h"
 
 #include "prop/prop_engine.h"
+#include "theory/builtin/theory_builtin.h"
 #include "theory/booleans/theory_bool.h"
 #include "theory/uf/theory_uf.h"
 #include "theory/arith/theory_arith.h"
@@ -36,6 +37,18 @@
 
 namespace CVC4 {
 
+namespace theory {
+
+// rewrite cache support
+template <bool topLevel> struct PreRewriteCacheTag {};
+typedef expr::Attribute<PreRewriteCacheTag<true>, Node> PreRewriteCacheTop;
+typedef expr::Attribute<PreRewriteCacheTag<false>, Node> PreRewriteCache;
+template <bool topLevel> struct PostRewriteCacheTag {};
+typedef expr::Attribute<PostRewriteCacheTag<true>, Node> PostRewriteCacheTop;
+typedef expr::Attribute<PostRewriteCacheTag<false>, Node> PostRewriteCache;
+
+}/* CVC4::theory namespace */
+
 // In terms of abstraction, this is below (and provides services to)
 // PropEngine.
 
@@ -116,6 +129,7 @@ class TheoryEngine {
 
   EngineOutputChannel d_theoryOut;
 
+  theory::builtin::TheoryBuiltin d_builtin;
   theory::booleans::TheoryBool d_bool;
   theory::uf::TheoryUF d_uf;
   theory::arith::TheoryArith d_arith;
@@ -124,81 +138,101 @@ class TheoryEngine {
 
 
   /**
-   * Check whether a node is in the rewrite cache or not.
+   * Check whether a node is in the pre-rewrite cache or not.
    */
-  static bool inRewriteCache(TNode n) throw() {
-    return n.hasAttribute(theory::RewriteCache());
+  static bool inPreRewriteCache(TNode n, bool topLevel) throw() {
+    if(topLevel) {
+      return n.hasAttribute(theory::PreRewriteCacheTop());
+    } else {
+      return n.hasAttribute(theory::PreRewriteCache());
+    }
   }
 
   /**
-   * Get the value of the rewrite cache (or Node::null()) if there is
+   * Get the value of the pre-rewrite cache (or Node::null()) if there is
    * none).
    */
-  static Node getRewriteCache(TNode n) throw() {
-    return n.getAttribute(theory::RewriteCache());
+  static Node getPreRewriteCache(TNode in, bool topLevel) throw() {
+    if(topLevel) {
+      Node out;
+      if(in.getAttribute(theory::PreRewriteCacheTop(), out)) {
+        return out.isNull() ? Node(in) : out;
+      }
+    } else {
+      Node out;
+      if(in.getAttribute(theory::PreRewriteCache(), out)) {
+        return out.isNull() ? Node(in) : out;
+      }
+    }
+    return Node::null();
   }
 
   /**
-   * Get the value of the rewrite cache (or Node::null()) if there is
-   * none).
+   * Set the value of the pre-rewrite cache.  v cannot be a null Node.
    */
-  static void setRewriteCache(TNode n, TNode v) throw() {
-    return n.setAttribute(theory::RewriteCache(), v);
+  static void setPreRewriteCache(TNode n, bool topLevel, TNode v) throw() {
+    AssertArgument(!n.isNull(), n, "n cannot be null in setPostRewriteCache()");
+    AssertArgument(!v.isNull(), v, "v cannot be null in setPreRewriteCache()");
+    // mappings from  n -> n  are actually stored as  n -> null  as a
+    // special case, to avoid cycles in the reference-counting of Nodes
+    if(topLevel) {
+      n.setAttribute(theory::PreRewriteCacheTop(), n == v ? TNode::null() : v);
+    } else {
+      n.setAttribute(theory::PreRewriteCache(), n == v ? TNode::null() : v);
+    }
   }
 
   /**
-   * This is the top rewrite entry point, called during preprocessing.
-   * It dispatches to the proper theories to rewrite the given Node.
+   * Check whether a node is in the post-rewrite cache or not.
    */
-  Node rewrite(TNode in);
+  static bool inPostRewriteCache(TNode n, bool topLevel) throw() {
+    if(topLevel) {
+      return n.hasAttribute(theory::PostRewriteCacheTop());
+    } else {
+      return n.hasAttribute(theory::PostRewriteCache());
+    }
+  }
 
   /**
-   * Convenience function to recurse through the children, rewriting,
-   * while leaving the Node's kind alone.
+   * Get the value of the post-rewrite cache (or Node::null()) if there is
+   * none).
    */
-  Node rewriteChildren(TNode in) {
-    if(in.getMetaKind() == kind::metakind::CONSTANT) {
-      return in;
-    }
-
-    NodeBuilder<> b(in.getKind());
-    if(in.getMetaKind() == kind::metakind::PARAMETERIZED){
-      Assert(in.hasOperator());
-      b << in.getOperator();
-    }
-    for(TNode::iterator c = in.begin(); c != in.end(); ++c) {
-      b << rewrite(*c);
+  static Node getPostRewriteCache(TNode in, bool topLevel) throw() {
+    if(topLevel) {
+      Node out;
+      if(in.getAttribute(theory::PostRewriteCacheTop(), out)) {
+        return out.isNull() ? Node(in) : out;
+      }
+    } else {
+      Node out;
+      if(in.getAttribute(theory::PostRewriteCache(), out)) {
+        return out.isNull() ? Node(in) : out;
+      }
     }
-    Debug("rewrite") << "rewrote-children of " << in << std::endl
-                     << "got " << b << std::endl;
-    Node ret = b;
-    return ret;
+    return Node::null();
   }
 
   /**
-   * Rewrite Nodes with builtin kind (that is, those Nodes n for which
-   * theoryOf(n) == NULL).  The master list is in expr/builtin_kinds.
+   * Set the value of the post-rewrite cache.  v cannot be a null Node.
    */
-  Node rewriteBuiltins(TNode in) {
-    switch(Kind k = in.getKind()) {
-    case kind::EQUAL:
-      return rewriteChildren(in);
-
-    case kind::ITE:
-      Unhandled(k);
-
-    case kind::SKOLEM:
-    case kind::VARIABLE:
-      return in;
-
-    case kind::TUPLE:
-      return rewriteChildren(in);
-
-    default:
-      Unhandled(k);
+  static void setPostRewriteCache(TNode n, bool topLevel, TNode v) throw() {
+    AssertArgument(!n.isNull(), n, "n cannot be null in setPostRewriteCache()");
+    AssertArgument(!v.isNull(), v, "v cannot be null in setPostRewriteCache()");
+    // mappings from  n -> n  are actually stored as  n -> null  as a
+    // special case, to avoid cycles in the reference-counting of Nodes
+    if(topLevel) {
+      n.setAttribute(theory::PostRewriteCacheTop(), n == v ? TNode::null() : v);
+    } else {
+      n.setAttribute(theory::PostRewriteCache(), n == v ? TNode::null() : v);
     }
   }
 
+  /**
+   * This is the top rewrite entry point, called during preprocessing.
+   * It dispatches to the proper theories to rewrite the given Node.
+   */
+  Node rewrite(TNode in);
+
   Node removeITEs(TNode t);
 
 public:
@@ -209,6 +243,7 @@ public:
   TheoryEngine(context::Context* ctxt) :
     d_propEngine(NULL),
     d_theoryOut(this, ctxt),
+    d_builtin(ctxt, d_theoryOut),
     d_bool(ctxt, d_theoryOut),
     d_uf(ctxt, d_theoryOut),
     d_arith(ctxt, d_theoryOut),
@@ -216,6 +251,7 @@ public:
     d_bv(ctxt, d_theoryOut),
     d_statistics() {
 
+    d_theoryOfTable.registerTheory(&d_builtin);
     d_theoryOfTable.registerTheory(&d_bool);
     d_theoryOfTable.registerTheory(&d_uf);
     d_theoryOfTable.registerTheory(&d_arith);
@@ -235,6 +271,7 @@ public:
    * ordering issues between PropEngine and Theory.
    */
   void shutdown() {
+    d_builtin.shutdown();
     d_bool.shutdown();
     d_uf.shutdown();
     d_arith.shutdown();
@@ -248,45 +285,7 @@ public:
    * @returns the theory, or NULL if the TNode is
    * of built-in type.
    */
-  theory::Theory* theoryOf(TNode n) {
-    Kind k = n.getKind();
-
-    Assert(k >= 0 && k < kind::LAST_KIND);
-
-    if(k == kind::VARIABLE) {
-      TypeNode t = n.getType();
-      if(t.isBoolean()){
-        return &d_bool;
-      }else if(t.isReal()){
-        return &d_arith;
-      }else{
-        return &d_uf;
-      }
-      //Unimplemented();
-    } else if(k == kind::EQUAL) {
-      // if LHS is a VARIABLE, use theoryOf(LHS.getType())
-      // otherwise, use theoryOf(LHS)
-      TNode lhs = n[0];
-      if(lhs.getKind() == kind::VARIABLE) {
-        // FIXME: we don't yet have a Type-to-Theory map.  When we do,
-        // look up the type of the LHS and return that Theory (?)
-
-        //The following JUST hacks around this lack of a table
-        TypeNode type_of_n = lhs.getType();
-        if(type_of_n.isReal()){
-          return &d_arith;
-        }else{
-          return &d_uf;
-          //Unimplemented();
-        }
-      } else {
-        return theoryOf(lhs);
-      }
-    } else {
-      // use our Kind-to-Theory mapping
-      return d_theoryOfTable[k];
-    }
-  }
+  theory::Theory* theoryOf(TNode n);
 
   /**
    * Preprocess a node.  This involves theory-specific rewriting, then
@@ -318,6 +317,7 @@ public:
     d_theoryOut.d_propagatedLiterals.clear();
     // Do the checking
     try {
+      //d_builtin.check(effort);
       //d_bool.check(effort);
       d_uf.check(effort);
       d_arith.check(effort);
diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h
index dc08788f3..cd0b4ef66 100644
--- a/src/theory/theory_test_utils.h
+++ b/src/theory/theory_test_utils.h
@@ -12,8 +12,10 @@
 #include "theory/interrupted.h"
 
 #include <vector>
+#include <utility>
+#include <iostream>
 
-namespace CVC4{
+namespace CVC4 {
 
 namespace theory {
 
@@ -21,12 +23,32 @@ namespace theory {
  * Very basic OutputChannel for testing simple Theory Behaviour.
  * Stores a call sequence for the output channel
  */
-enum OutputChannelCallType { CONFLICT, PROPOGATE, AUG_LEMMA, LEMMA, EXPLANATION };
+enum OutputChannelCallType {
+  CONFLICT,
+  PROPAGATE,
+  AUG_LEMMA,
+  LEMMA,
+  EXPLANATION
+};
+
+}/* CVC4::theory namespace */
+
+inline std::ostream& operator<<(std::ostream& out, theory::OutputChannelCallType type) {
+  switch(type) {
+  case theory::CONFLICT: return out << "CONFLICT";
+  case theory::PROPAGATE: return out << "PROPAGATE";
+  case theory::AUG_LEMMA: return out << "AUG_LEMMA";
+  case theory::LEMMA: return out << "LEMMA";
+  case theory::EXPLANATION: return out << "EXPLANATION";
+  default: return out << "UNDEFINED-OutputChannelCallType!" << int(type);
+  }
+}
 
+namespace theory {
 
 class TestOutputChannel : public theory::OutputChannel {
 public:
-  std::vector< pair<enum OutputChannelCallType, Node> > d_callHistory;
+  std::vector< std::pair<enum OutputChannelCallType, Node> > d_callHistory;
 
   TestOutputChannel() {}
 
@@ -34,12 +56,14 @@ public:
 
   void safePoint()  throw(Interrupted, AssertionException) {}
 
-  void conflict(TNode n, bool safe = false)  throw(Interrupted, AssertionException) {
+  void conflict(TNode n, bool safe = false)
+    throw(Interrupted, AssertionException) {
     push(CONFLICT, n);
   }
 
-  void propagate(TNode n, bool safe = false)  throw(Interrupted, AssertionException) {
-    push(PROPOGATE, n);
+  void propagate(TNode n, bool safe = false)
+    throw(Interrupted, AssertionException) {
+    push(PROPAGATE, n);
   }
 
   void lemma(TNode n, bool safe = false) throw(Interrupted, AssertionException) {
@@ -71,11 +95,11 @@ public:
 
 private:
   void push(OutputChannelCallType call, TNode n) {
-    d_callHistory.push_back(make_pair(call,n));
+    d_callHistory.push_back(std::make_pair(call,n));
   }
 };/* class TestOutputChannel */
 
-}/* namespace theory */
-}/* namespace CVC4 */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
 
 #endif /* __CVC4__THEORY__THEORY_TEST_UTILS_H */
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 5add2e92a..108102b9f 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -132,6 +132,13 @@ public:
   Node rewrite(TNode n);
 
   /**
+   * Plug in old rewrite to the new (pre,post)rewrite interface.
+   */
+  RewriteResponse postRewrite(TNode n, bool topLevel) {
+    return RewritingComplete(topLevel ? rewrite(n) : Node(n));
+  }
+
+  /**
    * Propagates theory literals. Currently does nothing.
    *
    * Overloads void propagate(Effort level); from theory.h.
@@ -147,6 +154,8 @@ public:
    */
   void explain(TNode n, Effort level) {}
 
+  std::string identify() const { return std::string("TheoryUF"); }
+
 private:
   /**
    * Checks whether 2 nodes are already in the same equivalence class tree.
diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h
index 33123cd8f..419e3d078 100644
--- a/src/theory/uf/theory_uf_type_rules.h
+++ b/src/theory/uf/theory_uf_type_rules.h
@@ -17,8 +17,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY_UF_TYPE_RULES_H_
-#define __CVC4__THEORY_UF_TYPE_RULES_H_
+#ifndef __CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H_
+#define __CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H_
 
 namespace CVC4 {
 namespace theory {
@@ -49,4 +49,4 @@ public:
 }
 
 
-#endif /* THEORY_UF_TYPE_RULES_H_ */
+#endif /* __CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H_ */