* Added white-box TheoryEngine test that tests the rewriter

* Added regression documentation to test/regress/README

* Added ability to print types of vars in expr printouts
  with iomanipulator Node::printtypes(true)... for example,
    Warning() << Node::printtypes(true) << n << std::endl;

* Types-printing can be specified on the command line with
  --print-expr-types

* Improved type handling facilities and theoryOf().
  For now, SORT_TYPE moved from builtin theory to UF theory
  to match old behavior.

* Additional gdb debug functionality.  Now we have:

    debugPrintNode(Node)            debugPrintRawNode(Node)
    debugPrintTNode(TNode)          debugPrintRawTNode(TNode)
    debugPrintTypeNode(TypeNode)    debugPrintRawTypeNode(TypeNode)
    debugPrintNodeValue(NodeValue*) debugPrintRawNodeValue(NodeValue*)

  they all print a {Node,TNode,NodeValue*} from the debugger.
  The "Raw" versions print a very low-level AST-like form.
  The regular versions do the same as operator<<, but force
  full printing on (no depth-limiting).

* Other trivial fixes

24 files changed, 830 insertions, 206 deletions

diff --git a/contrib/update-copyright.pl b/contrib/update-copyright.pl
index cf02e1ece..5cf543459 100755
--- a/contrib/update-copyright.pl
+++ b/contrib/update-copyright.pl
@@ -161,7 +161,7 @@ sub recurse {
         print $OUT " ** Minor contributors (to current version): $minor_contributors\n";
         print $OUT $standard_template;
         print $OUT " **\n";
-        print $OUT " ** \brief [[ Add one-line brief description here ]]\n";
+        print $OUT " ** \\brief [[ Add one-line brief description here ]]\n";
         print $OUT " **\n";
         print $OUT " ** [[ Add lengthier description here ]]\n";
         print $OUT " ** \\todo document this file\n";
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 05d31499d..c3191ab48 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -39,6 +39,7 @@ namespace CVC4 {
 namespace expr {
 
 const int ExprSetDepth::s_iosIndex = std::ios_base::xalloc();
+const int ExprPrintTypes::s_iosIndex = std::ios_base::xalloc();
 
 }/* CVC4::expr namespace */
 
@@ -198,9 +199,9 @@ bool Expr::isConst() const {
   return d_node->isConst();
 }
 
-void Expr::toStream(std::ostream& out) const {
+void Expr::toStream(std::ostream& out, int depth, bool types) const {
   ExprManagerScope ems(*this);
-  d_node->toStream(out);
+  d_node->toStream(out, depth, types);
 }
 
 Node Expr::getNode() const {
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 1749971a5..34d4a1a9e 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -44,6 +44,7 @@ class Expr;
 
 namespace expr {
   class CVC4_PUBLIC ExprSetDepth;
+  class CVC4_PUBLIC ExprPrintTypes;
 }/* CVC4::expr namespace */
 
 /**
@@ -70,8 +71,8 @@ public:
   ~TypeCheckingException() throw ();
 
   /**
-   * Get the Node that caused the type-checking to fail.
-   * @return the node
+   * Get the Expr that caused the type-checking to fail.
+   * @return the expr
    */
   Expr getExpression() const;
 
@@ -205,7 +206,7 @@ public:
    * Outputs the string representation of the expression to the stream.
    * @param out the output stream
    */
-  void toStream(std::ostream& out) const;
+  void toStream(std::ostream& out, int depth = -1, bool types = false) const;
 
   /**
    * Check if this is a null expression.
@@ -249,22 +250,33 @@ public:
   ExprManager* getExprManager() const;
 
   /**
-   * IOStream manipulator to set the maximum depth of Nodes when
+   * IOStream manipulator to set the maximum depth of Exprs when
    * pretty-printing.  -1 means print to any depth.  E.g.:
    *
    *   // let a, b, c, and d be VARIABLEs
-   *   Node n = nm->mkNode(OR, a, b, nm->mkNode(AND, c, nm->mkNode(NOT, d)))
-   *   out << setdepth(3) << n;
+   *   Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d)))
+   *   out << setdepth(3) << e;
    *
    * gives "(OR a b (AND c (NOT d)))", but
    *
-   *   out << setdepth(1) << [same node as above]
+   *   out << setdepth(1) << [same expr as above]
    *
    * gives "(OR a b (...))"
    */
   typedef expr::ExprSetDepth setdepth;
 
   /**
+   * IOStream manipulator to print type ascriptions or not.
+   *
+   *   // let a, b, c, and d be variables of sort U
+   *   Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d)))
+   *   out << e;
+   *
+   * gives "(OR a:U b:U (AND c:U (NOT d:U)))", but
+   */
+  typedef expr::ExprPrintTypes printtypes;
+
+  /**
    * Very basic pretty printer for Expr.
    * This is equivalent to calling e.getNode().printAst(...)
    * @param out output stream to print to.
@@ -290,7 +302,7 @@ protected:
    */
   NodeTemplate<true> getNode() const;
 
-  // Friend to access the actual internal node information and private methods
+  // Friend to access the actual internal expr information and private methods
   friend class SmtEngine;
   friend class ExprManager;
 };
@@ -385,16 +397,16 @@ public:
 namespace expr {
 
 /**
- * IOStream manipulator to set the maximum depth of Nodes when
+ * IOStream manipulator to set the maximum depth of Exprs when
  * pretty-printing.  -1 means print to any depth.  E.g.:
  *
  *   // let a, b, c, and d be VARIABLEs
- *   Node n = nm->mkNode(OR, a, b, nm->mkNode(AND, c, nm->mkNode(NOT, d)))
- *   out << setdepth(3) << n;
+ *   Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d)))
+ *   out << setdepth(3) << e;
  *
  * gives "(OR a b (AND c (NOT d)))", but
  *
- *   out << setdepth(1) << [same node as above]
+ *   out << setdepth(1) << [same expr as above]
  *
  * gives "(OR a b (...))".
  *
@@ -416,7 +428,7 @@ class CVC4_PUBLIC ExprSetDepth {
   static const int s_defaultPrintDepth = 3;
 
   /**
-   * When this manipulator is 
+   * When this manipulator is used, the depth is stored here.
    */
   long d_depth;
 
@@ -444,6 +456,51 @@ public:
   }
 };
 
+/**
+ * IOStream manipulator to print type ascriptions or not.
+ *
+ *   // let a, b, c, and d be variables of sort U
+ *   Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d)))
+ *   out << e;
+ *
+ * gives "(OR a:U b:U (AND c:U (NOT d:U)))", but
+ */
+class CVC4_PUBLIC ExprPrintTypes {
+  /**
+   * The allocated index in ios_base for our depth setting.
+   */
+  static const int s_iosIndex;
+
+  /**
+   * The default depth to print, for ostreams that haven't yet had a
+   * setdepth() applied to them.
+   */
+  static const int s_defaultPrintTypes = false;
+
+  /**
+   * When this manipulator is used, the setting is stored here.
+   */
+  bool d_printTypes;
+
+public:
+  /**
+   * Construct a ExprPrintTypes with the given setting.
+   */
+  ExprPrintTypes(bool printTypes) : d_printTypes(printTypes) {}
+
+  inline void applyPrintTypes(std::ostream& out) {
+    out.iword(s_iosIndex) = d_printTypes;
+  }
+
+  static inline bool getPrintTypes(std::ostream& out) {
+    return out.iword(s_iosIndex);
+  }
+
+  static inline void setPrintTypes(std::ostream& out, bool printTypes) {
+    out.iword(s_iosIndex) = printTypes;
+  }
+};
+
 }/* CVC4::expr namespace */
 
 ${getConst_instantiations}
@@ -453,11 +510,11 @@ ${getConst_instantiations}
 namespace expr {
 
 /**
- * Sets the default depth when pretty-printing a Node to an ostream.
- * Use like this:
+ * Sets the default print-types setting when pretty-printing an Expr
+ * to an ostream.  Use like this:
  *
- *   // let out be an ostream, n a Node
- *   out << Node::setdepth(n) << n << endl;
+ *   // let out be an ostream, e an Expr
+ *   out << Expr::setdepth(n) << e << endl;
  *
  * The depth stays permanently (until set again) with the stream.
  */
@@ -466,6 +523,20 @@ inline std::ostream& operator<<(std::ostream& out, ExprSetDepth sd) {
   return out;
 }
 
+/**
+ * Sets the default depth when pretty-printing a Expr to an ostream.
+ * Use like this:
+ *
+ *   // let out be an ostream, e an Expr
+ *   out << Expr::setprinttypes(true) << e << endl;
+ *
+ * The setting stays permanently (until set again) with the stream.
+ */
+inline std::ostream& operator<<(std::ostream& out, ExprPrintTypes pt) {
+  pt.applyPrintTypes(out);
+  return out;
+}
+
 }/* CVC4::expr namespace */
 
 }/* CVC4 namespace */
diff --git a/src/expr/node.h b/src/expr/node.h
index e3fb42ead..09a1ad8bc 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -455,12 +455,13 @@ public:
    * given stream
    * @param out the sream to serialise this node to
    */
-  inline void toStream(std::ostream& out, int toDepth = -1) const {
+  inline void toStream(std::ostream& out, int toDepth = -1,
+                       bool types = false) const {
     if(!ref_count) {
       Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" );
     }
 
-    d_nv->toStream(out, toDepth);
+    d_nv->toStream(out, toDepth, types);
   }
 
   /**
@@ -480,11 +481,22 @@ public:
   typedef expr::ExprSetDepth setdepth;
 
   /**
+   * IOStream manipulator to print type ascriptions or not.
+   *
+   *   // let a, b, c, and d be variables of sort U
+   *   Node n = nm->mkNode(OR, a, b, nm->mkNode(AND, c, nm->mkNode(NOT, d)))
+   *   out << n;
+   *
+   * gives "(OR a:U b:U (AND c:U (NOT d:U)))", but
+   */
+  typedef expr::ExprPrintTypes printtypes;
+
+  /**
    * Very basic pretty printer for Node.
    * @param o output stream to print to.
    * @param indent number of spaces to indent the formula by.
    */
-  void printAst(std::ostream & o, int indent = 0) const;
+  inline void printAst(std::ostream& out, int indent = 0) const;
 
   NodeTemplate<true> eqNode(const NodeTemplate& right) const;
 
@@ -497,19 +509,6 @@ public:
   NodeTemplate<true> impNode(const NodeTemplate& right) const;
   NodeTemplate<true> xorNode(const NodeTemplate& right) const;
 
-private:
-
-  /**
-   * Indents the given stream a given amount of spaces.
-   * @param out the stream to indent
-   * @param indent the numer of spaces
-   */
-  static void indent(std::ostream& out, int indent) {
-    for(int i = 0; i < indent; i++) {
-      out << ' ';
-    }
-  }
-
 };/* class NodeTemplate<ref_count> */
 
 /**
@@ -519,7 +518,9 @@ private:
  * @return the changed stream.
  */
 inline std::ostream& operator<<(std::ostream& out, TNode n) {
-  n.toStream(out, Node::setdepth::getDepth(out));
+  n.toStream(out,
+             Node::setdepth::getDepth(out),
+             Node::printtypes::getPrintTypes(out));
   return out;
 }
 
@@ -805,30 +806,9 @@ NodeTemplate<ref_count>::xorNode(const NodeTemplate<ref_count>& right) const {
 }
 
 template <bool ref_count>
-void NodeTemplate<ref_count>::printAst(std::ostream& out, int ind) const {
-  indent(out, ind);
-  out << '(';
-  out << getKind();
-  if(getMetaKind() == kind::metakind::VARIABLE) {
-    out << ' ' << getId();
-  } else if(getMetaKind() == kind::metakind::CONSTANT) {
-    out << ' ';
-    kind::metakind::NodeValueConstPrinter::toStream(out, d_nv);
-  } else {
-    if(hasOperator()) {
-      out << std::endl;
-      getOperator().printAst(out, ind + 1);
-    }
-    if(getNumChildren() >= 1) {
-      for(const_iterator child = begin(); child != end(); ++child) {
-        out << std::endl;
-        (*child).printAst(out, ind + 1);
-      }
-      out << std::endl;
-      indent(out, ind);
-    }
-  }
-  out << ')';
+inline void
+NodeTemplate<ref_count>::printAst(std::ostream& out, int indent) const {
+  d_nv->printAst(out, indent);
 }
 
 /**
@@ -910,11 +890,19 @@ TypeNode NodeTemplate<ref_count>::getType() const
  * to meet. A cleaner solution is welcomed.
  */
 static void __attribute__((used)) debugPrintNode(const NodeTemplate<true>& n) {
+  Warning() << Node::setdepth(-1) << n << std::endl;
+  Warning().flush();
+}
+static void __attribute__((used)) debugPrintRawNode(const NodeTemplate<true>& n) {
   n.printAst(Warning(), 0);
   Warning().flush();
 }
 
 static void __attribute__((used)) debugPrintTNode(const NodeTemplate<false>& n) {
+  Warning() << Node::setdepth(-1) << n << std::endl;
+  Warning().flush();
+}
+static void __attribute__((used)) debugPrintRawTNode(const NodeTemplate<false>& n) {
   n.printAst(Warning(), 0);
   Warning().flush();
 }
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 0cb9ed026..402116842 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -661,10 +661,11 @@ public:
   operator Node();
   operator Node() const;
 
-  inline void toStream(std::ostream& out, int depth = -1) const {
+  inline void toStream(std::ostream& out, int depth = -1,
+                       bool types = false) const {
     Assert(!isUsed(), "NodeBuilder is one-shot only; "
            "attempt to access it after conversion");
-    d_nv->toStream(out, depth);
+    d_nv->toStream(out, depth, types);
   }
 
   NodeBuilder<nchild_thresh>& operator&=(TNode);
@@ -1211,7 +1212,9 @@ void NodeBuilder<nchild_thresh>::internalCopy(const NodeBuilder<N>& nb) {
 template <unsigned nchild_thresh>
 inline std::ostream& operator<<(std::ostream& out,
                                 const NodeBuilder<nchild_thresh>& b) {
-  b.toStream(out, Node::setdepth::getDepth(out));
+  b.toStream(out,
+             Node::setdepth::getDepth(out),
+             Node::printtypes::getPrintTypes(out));
   return out;
 }
 
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 8f7196e0c..2e45fe9d0 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -190,6 +190,9 @@ TypeNode NodeManager::getType(TNode n)
   if(!hasType) {
     // Infer the type
     switch(n.getKind()) {
+    case kind::SORT_TYPE:
+      typeNode = kindType();
+      break;
     case kind::EQUAL:
       typeNode = CVC4::theory::builtin::EqualityTypeRule::computeType(this, n);
       break;
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 3586440d4..4d796d81c 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -745,8 +745,7 @@ inline bool NodeManager::hasOperator(Kind k) {
 }
 
 inline TypeNode NodeManager::mkSort() {
-  TypeNode type = NodeBuilder<0>(this, kind::VARIABLE).constructTypeNode();
-  return type;
+  return NodeBuilder<0>(this, kind::SORT_TYPE).constructTypeNode();
 }
 
 inline TypeNode NodeManager::mkSort(const std::string& name) {
diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp
index c64a608fb..8add462e0 100644
--- a/src/expr/node_value.cpp
+++ b/src/expr/node_value.cpp
@@ -41,27 +41,34 @@ string NodeValue::toString() const {
   return ss.str();
 }
 
-void NodeValue::toStream(std::ostream& out, int toDepth) const {
+void NodeValue::toStream(std::ostream& out, int toDepth, bool types) const {
   using namespace CVC4::kind;
   using namespace CVC4;
 
   if(getKind() == kind::NULL_EXPR) {
     out << "null";
   } else if(getMetaKind() == kind::metakind::VARIABLE) {
-    if(getKind() != kind::VARIABLE) {
+    if(getKind() != kind::VARIABLE &&
+       getKind() != kind::SORT_TYPE) {
       out << getKind() << ':';
     }
 
     string s;
+    NodeManager* nm = NodeManager::currentNM();
 
     // conceptually "this" is const, and hasAttribute() doesn't change
     // its argument, but it requires a non-const key arg (for now)
-    if(NodeManager::currentNM()->getAttribute(const_cast<NodeValue*>(this),
-                                              VarNameAttr(), s)) {
+    if(nm->getAttribute(const_cast<NodeValue*>(this),
+                        VarNameAttr(), s)) {
       out << s;
     } else {
       out << "var_" << d_id;
     }
+    if(types) {
+      // print the whole type, but not *its* type
+      out << ":";
+      nm->getType(TNode(this)).toStream(out, -1, false);
+    }
   } else {
     out << '(' << Kind(d_kind);
     if(getMetaKind() == kind::metakind::CONSTANT) {
@@ -73,7 +80,7 @@ void NodeValue::toStream(std::ostream& out, int toDepth) const {
           out << ' ';
         }
         if(toDepth != 0) {
-          (*i)->toStream(out, toDepth < 0 ? toDepth : toDepth - 1);
+          (*i)->toStream(out, toDepth < 0 ? toDepth : toDepth - 1, types);
         } else {
           out << "(...)";
         }
@@ -83,5 +90,27 @@ void NodeValue::toStream(std::ostream& out, int toDepth) const {
   }
 }
 
+void NodeValue::printAst(std::ostream& out, int ind) const {
+  indent(out, ind);
+  out << '(';
+  out << getKind();
+  if(getMetaKind() == kind::metakind::VARIABLE) {
+    out << ' ' << getId();
+  } else if(getMetaKind() == kind::metakind::CONSTANT) {
+    out << ' ';
+    kind::metakind::NodeValueConstPrinter::toStream(out, this);
+  } else {
+    if(nv_begin() != nv_end()) {
+      for(const_nv_iterator child = nv_begin(); child != nv_end(); ++child) {
+        out << std::endl;
+        (*child)->printAst(out, ind + 1);
+      }
+      out << std::endl;
+      indent(out, ind);
+    }
+  }
+  out << ')';
+}
+
 }/* CVC4::expr namespace */
 }/* CVC4 namespace */
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 8b2056560..9f8a8f45b 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -213,7 +213,7 @@ public:
   }
 
   std::string toString() const;
-  void toStream(std::ostream& out, int toDepth = -1) const;
+  void toStream(std::ostream& out, int toDepth = -1, bool types = false) const;
 
   static inline unsigned kindToDKind(Kind k) {
     return ((unsigned) k) & kindMask;
@@ -235,6 +235,21 @@ public:
 
   NodeValue* getChild(int i) const;
 
+  void printAst(std::ostream& out, int indent = 0) const;
+
+private:
+
+  /**
+   * Indents the given stream a given amount of spaces.
+   * @param out the stream to indent
+   * @param indent the numer of spaces
+   */
+  static inline void indent(std::ostream& out, int indent) {
+    for(int i = 0; i < indent; i++) {
+      out << ' ';
+    }
+  }
+
 };/* class NodeValue */
 
 /**
@@ -264,6 +279,7 @@ inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv);
 }/* CVC4 namespace */
 
 #include "expr/node_manager.h"
+#include "expr/type_node.h"
 
 namespace CVC4 {
 namespace expr {
@@ -363,11 +379,31 @@ inline T NodeValue::iterator<T>::operator*() {
 }
 
 inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv) {
-  nv.toStream(out, Node::setdepth::getDepth(out));
+  nv.toStream(out,
+              Node::setdepth::getDepth(out),
+              Node::printtypes::getPrintTypes(out));
   return out;
 }
 
 }/* CVC4::expr namespace */
+
+#ifdef CVC4_DEBUG
+/**
+ * Pretty printer for use within gdb.  This is not intended to be used
+ * outside of gdb.  This writes to the Warning() stream and immediately
+ * flushes the stream.
+ */
+static void __attribute__((used)) debugPrintNodeValue(const expr::NodeValue* nv) {
+  Warning() << Node::setdepth(-1) << *nv << std::endl;
+  Warning().flush();
+}
+
+static void __attribute__((used)) debugPrintRawNodeValue(const expr::NodeValue* nv) {
+  nv->printAst(Warning(), 0);
+  Warning().flush();
+}
+#endif /* CVC4_DEBUG */
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__EXPR__NODE_VALUE_H */
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 6f8911280..43d3c761e 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -77,7 +77,7 @@ TypeNode TypeNode::getRangeType() const {
 
 /** Is this a sort kind */
 bool TypeNode::isSort() const {
-  return getKind() == kind::VARIABLE;
+  return getKind() == kind::SORT_TYPE;
 }
 
 /** Is this a kind type (i.e., the type of a type)? */
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index da277a382..a58d9dc89 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -280,8 +280,9 @@ public:
    * given stream
    * @param out the sream to serialise this node to
    */
-  inline void toStream(std::ostream& out, int toDepth = -1) const {
-    d_nv->toStream(out, toDepth);
+  inline void toStream(std::ostream& out, int toDepth = -1,
+                       bool types = false) const {
+    d_nv->toStream(out, toDepth, types);
   }
 
   /**
@@ -289,7 +290,7 @@ public:
    * @param o output stream to print to.
    * @param indent number of spaces to indent the formula by.
    */
-  void printAst(std::ostream & o, int indent = 0) const;
+  void printAst(std::ostream& out, int indent = 0) const;
 
   /**
    * Returns true if this type is a null type.
@@ -369,7 +370,9 @@ private:
  * @return the changed stream.
  */
 inline std::ostream& operator<<(std::ostream& out, const TypeNode& n) {
-  n.toStream(out, Node::setdepth::getDepth(out));
+  n.toStream(out,
+             Node::setdepth::getDepth(out),
+             Node::printtypes::getPrintTypes(out));
   return out;
 }
 
@@ -465,6 +468,36 @@ setAttribute(const AttrKind&, const typename AttrKind::value_type& value) {
   NodeManager::currentNM()->setAttribute(d_nv, AttrKind(), value);
 }
 
+inline void TypeNode::printAst(std::ostream& out, int indent) const {
+  d_nv->printAst(out, indent);
+}
+
+#ifdef CVC4_DEBUG
+/**
+ * Pretty printer for use within gdb.  This is not intended to be used
+ * outside of gdb.  This writes to the Warning() stream and immediately
+ * flushes the stream.
+ *
+ * Note that this function cannot be a template, since the compiler
+ * won't instantiate it.  Even if we explicitly instantiate.  (Odd?)
+ * So we implement twice.  We mark as __attribute__((used)) so that
+ * GCC emits code for it even though static analysis indicates it's
+ * never called.
+ *
+ * Tim's Note: I moved this into the node.h file because this allows gdb
+ * to find the symbol, and use it, which is the first standard this code needs
+ * to meet. A cleaner solution is welcomed.
+ */
+static void __attribute__((used)) debugPrintTypeNode(const TypeNode& n) {
+  Warning() << Node::setdepth(-1) << n << std::endl;
+  Warning().flush();
+}
+static void __attribute__((used)) debugPrintRawTypeNode(const TypeNode& n) {
+  n.printAst(Warning(), 0);
+  Warning().flush();
+}
+#endif /* CVC4_DEBUG */
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__NODE_H */
diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp
index 88840a8e8..e050a0dfb 100644
--- a/src/main/getopt.cpp
+++ b/src/main/getopt.cpp
@@ -68,7 +68,8 @@ enum OptionValue {
   USE_MMAP,
   SHOW_CONFIG,
   STRICT_PARSING,
-  DEFAULT_EXPR_DEPTH
+  DEFAULT_EXPR_DEPTH,
+  PRINT_EXPR_TYPES
 };/* enum OptionValue */
 
 /**
@@ -113,6 +114,7 @@ static struct option cmdlineOptions[] = {
   { "mmap",        no_argument      , NULL, USE_MMAP    },
   { "strict-parsing", no_argument   , NULL, STRICT_PARSING },
   { "default-expr-depth", required_argument, NULL, DEFAULT_EXPR_DEPTH },
+  { "print-expr-types", no_argument , NULL, PRINT_EXPR_TYPES },
 };/* if you add things to the above, please remember to update usage.h! */
 
 /** Full argv[0] */
@@ -234,6 +236,17 @@ throw(OptionException) {
       }
       break;
 
+    case PRINT_EXPR_TYPES:
+      {
+        Debug.getStream() << Expr::printtypes(true);
+        Trace.getStream() << Expr::printtypes(true);
+        Notice.getStream() << Expr::printtypes(true);
+        Chat.getStream() << Expr::printtypes(true);
+        Message.getStream() << Expr::printtypes(true);
+        Warning.getStream() << Expr::printtypes(true);
+      }
+      break;
+
     case SHOW_CONFIG:
       fputs(Configuration::about().c_str(), stdout);
       printf("\n");
diff --git a/src/main/usage.h b/src/main/usage.h
index ef37b7650..b56f083a5 100644
--- a/src/main/usage.h
+++ b/src/main/usage.h
@@ -30,27 +30,22 @@ usage: %s [options] [input-file]\n\
 Without an input file, or with `-', CVC4 reads from standard input.\n\
 \n\
 CVC4 options:\n\
-   --lang | -L      force input language (default is `auto'; see --lang help)\n\
-   --version | -V   identify this CVC4 binary\n\
-   --help | -h      this command line reference\n\
-   --parse-only     exit after parsing input\n\
-   --mmap           memory map file input\n\
-   --show-config    show CVC4 static configuration\n"
-#ifdef CVC4_DEBUG
-"\
-   --segv-nospin    don't spin on segfault waiting for gdb\n"
-#endif
-#ifndef CVC4_MUZZLE
-"\
-   --no-checking    disable semantic checks in the parser\n\
-   --strict-parsing fail on inputs that are not strictly conformant (SMT2 only)\n\
-   --verbose | -v   increase verbosity (repeatable)\n\
-   --quiet | -q     decrease verbosity (repeatable)\n\
-   --trace | -t     tracing for something (e.g. --trace pushpop)\n\
-   --debug | -d     debugging for something (e.g. --debug arith), implies -t\n\
-   --stats          give statistics on exit\n\
-   --default-expr-depth=N print exprs to depth N (0 == default, -1 == no limit)\n"
-#endif
+   --lang | -L            force input language (default is `auto'; see --lang help)\n\
+   --version | -V         identify this CVC4 binary\n\
+   --help | -h            this command line reference\n\
+   --parse-only           exit after parsing input\n\
+   --mmap                 memory map file input\n\
+   --show-config          show CVC4 static configuration\n\
+   --segv-nospin          don't spin on segfault waiting for gdb\n\
+   --no-checking          disable semantic checks in the parser\n\
+   --strict-parsing       fail on inputs that are not strictly conformant (SMT2 only)\n\
+   --verbose | -v         increase verbosity (repeatable)\n\
+   --quiet | -q           decrease verbosity (repeatable)\n\
+   --trace | -t           tracing for something (e.g. --trace pushpop)\n\
+   --debug | -d           debugging for something (e.g. --debug arith), implies -t\n\
+   --stats                give statistics on exit\n\
+   --default-expr-depth=N print exprs to depth N (0 == default, -1 == no limit)\n\
+   --print-expr-types     print types with variables when printing exprs\n"
 ;
 
 }/* CVC4::main namespace */
diff --git a/src/parser/antlr_input_imports.cpp b/src/parser/antlr_input_imports.cpp
index b647842fa..a1ebee523 100644
--- a/src/parser/antlr_input_imports.cpp
+++ b/src/parser/antlr_input_imports.cpp
@@ -11,7 +11,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** rief [[ Add one-line brief description here ]]
+ ** \brief [[ Add one-line brief description here ]]
  **
  ** [[ Add lengthier description here ]]
  ** \todo document this file
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index 1f22ebef1..dfa94a66d 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -127,4 +127,3 @@ constant TYPE_CONSTANT \
     "expr/type_constant.h" \
     "basic types"
 operator FUNCTION_TYPE 2: "function type"
-variable SORT_TYPE "sort type"
diff --git a/src/theory/theory.h b/src/theory/theory.h
index bb598d410..8481aa5ff 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -38,6 +38,14 @@ class TheoryEngine;
 
 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;
+
 /**
  * Instances of this class serve as response codes from
  * Theory::preRewrite() and Theory::postRewrite().  Instances of
@@ -374,6 +382,96 @@ protected:
     return true;
   }
 
+  /**
+   * Check whether a node is in the pre-rewrite cache or not.
+   */
+  static bool inPreRewriteCache(TNode n, bool topLevel) throw() {
+    if(topLevel) {
+      return n.hasAttribute(PreRewriteCacheTop());
+    } else {
+      return n.hasAttribute(PreRewriteCache());
+    }
+  }
+
+  /**
+   * Get the value of the pre-rewrite cache (or Node::null()) if there is
+   * none).
+   */
+  static Node getPreRewriteCache(TNode n, bool topLevel) throw() {
+    if(topLevel) {
+      Node out;
+      if(n.getAttribute(PreRewriteCacheTop(), out)) {
+        return out.isNull() ? Node(n) : out;
+      }
+    } else {
+      Node out;
+      if(n.getAttribute(PreRewriteCache(), out)) {
+        return out.isNull() ? Node(n) : out;
+      }
+    }
+    return Node::null();
+  }
+
+  /**
+   * Set the value of the pre-rewrite cache.  v cannot be a null Node.
+   */
+  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(PreRewriteCacheTop(), n == v ? TNode::null() : v);
+    } else {
+      n.setAttribute(PreRewriteCache(), n == v ? TNode::null() : v);
+    }
+  }
+
+  /**
+   * Check whether a node is in the post-rewrite cache or not.
+   */
+  static bool inPostRewriteCache(TNode n, bool topLevel) throw() {
+    if(topLevel) {
+      return n.hasAttribute(PostRewriteCacheTop());
+    } else {
+      return n.hasAttribute(PostRewriteCache());
+    }
+  }
+
+  /**
+   * Get the value of the post-rewrite cache (or Node::null()) if there is
+   * none).
+   */
+  static Node getPostRewriteCache(TNode n, bool topLevel) throw() {
+    if(topLevel) {
+      Node out;
+      if(n.getAttribute(PostRewriteCacheTop(), out)) {
+        return out.isNull() ? Node(n) : out;
+      }
+    } else {
+      Node out;
+      if(n.getAttribute(PostRewriteCache(), out)) {
+        return out.isNull() ? Node(n) : out;
+      }
+    }
+    return Node::null();
+  }
+
+  /**
+   * Set the value of the post-rewrite cache.  v cannot be a null Node.
+   */
+  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(PostRewriteCacheTop(), n == v ? TNode::null() : v);
+    } else {
+      n.setAttribute(PostRewriteCache(), n == v ? TNode::null() : v);
+    }
+  }
+
 };/* class Theory */
 
 std::ostream& operator<<(std::ostream& os, Theory::Effort level);
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index e41df92d0..f496f1fd5 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -47,38 +47,30 @@ Theory* TheoryEngine::theoryOf(TNode n) {
   Assert(k >= 0 && k < kind::LAST_KIND);
 
   if(n.getMetaKind() == kind::metakind::VARIABLE) {
+    // FIXME: we don't yet have a Type-to-Theory map.  When we do,
+    // look up the type of the var and return that Theory (?)
+
+    //The following JUST hacks around this lack of a table
     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();
+    Kind k = t.getKind();
+    if(k == kind::TYPE_CONSTANT) {
+      switch(TypeConstant tc = t.getConst<TypeConstant>()) {
+      case BOOLEAN_TYPE:
+        return d_theoryOfTable[kind::CONST_BOOLEAN];
+      case INTEGER_TYPE:
+        return d_theoryOfTable[kind::CONST_INTEGER];
+      case REAL_TYPE:
+        return d_theoryOfTable[kind::CONST_RATIONAL];
+      case KIND_TYPE:
+      default:
+        Unhandled(tc);
       }
-    } else {
-      return theoryOf(lhs);
     }
+
+    return d_theoryOfTable[k];
+  } else if(k == kind::EQUAL) {
+    // equality is special: use LHS
+    return theoryOf(n[0]);
   } else {
     // use our Kind-to-Theory mapping
     return d_theoryOfTable[k];
@@ -141,7 +133,7 @@ Node TheoryEngine::preprocess(TNode t) {
 
 /* Our goal is to tease out any ITE's sitting under a theory operator. */
 Node TheoryEngine::removeITEs(TNode node) {
-  Debug("ite") << "handleNonAtomicNode(" << node << ")" << endl;
+  Debug("ite") << "removeITEs(" << node << ")" << endl;
 
   /* The result may be cached already */
   Node cachedRewrite;
@@ -155,7 +147,7 @@ Node TheoryEngine::removeITEs(TNode node) {
     TypeNode nodeType = node[1].getType();
     if(!nodeType.isBoolean()){
 
-      Node skolem = nodeManager->mkVar(node.getType());
+      Node skolem = nodeManager->mkSkolem(node.getType());
       Node newAssertion =
         nodeManager->mkNode(
                             kind::ITE,
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 2575c4c2d..79eec4301 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -37,18 +37,6 @@
 
 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.
 
@@ -136,95 +124,48 @@ class TheoryEngine {
   theory::arrays::TheoryArrays d_arrays;
   theory::bv::TheoryBV d_bv;
 
-
   /**
    * Check whether a node is in the pre-rewrite cache or not.
    */
   static bool inPreRewriteCache(TNode n, bool topLevel) throw() {
-    if(topLevel) {
-      return n.hasAttribute(theory::PreRewriteCacheTop());
-    } else {
-      return n.hasAttribute(theory::PreRewriteCache());
-    }
+    return theory::Theory::inPreRewriteCache(n, topLevel);
   }
 
   /**
    * Get the value of the pre-rewrite cache (or Node::null()) if there is
    * none).
    */
-  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();
+  static Node getPreRewriteCache(TNode n, bool topLevel) throw() {
+    return theory::Theory::getPreRewriteCache(n, topLevel);
   }
 
   /**
    * Set the value of the pre-rewrite cache.  v cannot be a null Node.
    */
   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);
-    }
+    return theory::Theory::setPreRewriteCache(n, topLevel, v);
   }
 
   /**
    * Check whether a node is in the post-rewrite cache or not.
    */
   static bool inPostRewriteCache(TNode n, bool topLevel) throw() {
-    if(topLevel) {
-      return n.hasAttribute(theory::PostRewriteCacheTop());
-    } else {
-      return n.hasAttribute(theory::PostRewriteCache());
-    }
+    return theory::Theory::inPostRewriteCache(n, topLevel);
   }
 
   /**
    * Get the value of the post-rewrite cache (or Node::null()) if there is
    * none).
    */
-  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;
-      }
-    }
-    return Node::null();
+  static Node getPostRewriteCache(TNode n, bool topLevel) throw() {
+    return theory::Theory::getPostRewriteCache(n, topLevel);
   }
 
   /**
    * Set the value of the post-rewrite cache.  v cannot be a null Node.
    */
   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);
-    }
+    return theory::Theory::setPostRewriteCache(n, topLevel, v);
   }
 
   /**
@@ -233,6 +174,9 @@ class TheoryEngine {
    */
   Node rewrite(TNode in);
 
+  /**
+   * Replace ITE forms in a node.
+   */
   Node removeITEs(TNode t);
 
 public:
@@ -386,6 +330,14 @@ private:
       StatisticsRegistry::registerStat(&d_statAugLemma);
       StatisticsRegistry::registerStat(&d_statExplanatation);
     }
+
+    ~Statistics() {
+      StatisticsRegistry::unregisterStat(&d_statConflicts);
+      StatisticsRegistry::unregisterStat(&d_statPropagate);
+      StatisticsRegistry::unregisterStat(&d_statLemma);
+      StatisticsRegistry::unregisterStat(&d_statAugLemma);
+      StatisticsRegistry::unregisterStat(&d_statExplanatation);
+    }
   };
   Statistics d_statistics;
 
diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds
index f95bfb582..4bfba382c 100644
--- a/src/theory/uf/kinds
+++ b/src/theory/uf/kinds
@@ -7,3 +7,4 @@
 theory ::CVC4::theory::uf::TheoryUF "theory_uf.h"
 
 parameterized APPLY_UF VARIABLE 1: "uninterpreted function application"
+variable SORT_TYPE "sort type"
diff --git a/src/util/stats.cpp b/src/util/stats.cpp
index cf7b3ad51..1677e0ce5 100644
--- a/src/util/stats.cpp
+++ b/src/util/stats.cpp
@@ -11,7 +11,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** rief [[ Add one-line brief description here ]]
+ ** \brief [[ Add one-line brief description here ]]
  **
  ** [[ Add lengthier description here ]]
  ** \todo document this file
diff --git a/src/util/stats.h b/src/util/stats.h
index 8d3d4cfda..6efe7f856 100644
--- a/src/util/stats.h
+++ b/src/util/stats.h
@@ -11,7 +11,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** rief [[ Add one-line brief description here ]]
+ ** \brief [[ Add one-line brief description here ]]
  **
  ** [[ Add lengthier description here ]]
  ** \todo document this file
@@ -31,9 +31,9 @@ namespace CVC4 {
 
 
 #ifdef CVC4_STATISTICS_ON
-#define USE_STATISTICS true
+#  define USE_STATISTICS true
 #else
-#define USE_STATISTICS false
+#  define USE_STATISTICS false
 #endif
 
 class CVC4_PUBLIC Stat;
@@ -50,7 +50,7 @@ public:
 
   static inline void registerStat(Stat* s) throw (AssertionException);
   static inline void unregisterStat(Stat* s) throw (AssertionException);
-}; /* class StatisticsRegistry */
+};/* class StatisticsRegistry */
 
 
 class CVC4_PUBLIC Stat {
@@ -106,7 +106,7 @@ inline void StatisticsRegistry::unregisterStat(Stat* s) throw (AssertionExceptio
 
 
 /**
- *  class T must have stream insertion operation defined.
+ * class T must have stream insertion operation defined.
  * std::ostream& operator<<(std::ostream&, const T&);
  */
 template<class T>
diff --git a/test/regress/README b/test/regress/README
new file mode 100644
index 000000000..bef93b140
--- /dev/null
+++ b/test/regress/README
@@ -0,0 +1,56 @@
+Regressions
+===========
+
+To insert a new regression, add the file to Subversion, for example:
+
+  svn add regress/regress0/testMyFunctionality.cvc
+
+Also add it to the relevant Makefile.am, here, in regress/regress0/Makefile.am.
+
+A number of regressions exist under test/regress that aren't listed in any
+Makefile.am.  These are regressions that may someday be included in the standard
+suite of tests, but aren't yet included (perhaps they test functionality not
+yet supported).
+
+If you want to add a new directory of regressions, add the directory name to
+SUBDIRS (with . running first, by convention), and set up the new directory
+with a new Makefile.am, adding all to the Subversion repository.
+
+=== EXPECTED OUTPUT, ERROR, AND EXIT CODES ===
+
+In the case of CVC input, you can specify expected stdout, stderr, and exit
+codes with the following lines directly in the CVC regression file:
+
+% EXPECT: stdout
+% EXPECT-ERROR: stderr
+% EXIT: 0
+
+expects an exit status of 0 from cvc4, the single line "stderr" on stderr,
+and the single line "stdout" on stdout.  You can repeat EXPECT and EXPECT-ERROR
+lines as many times as you like, and at different points of the file.  This is
+useful for multiple queries:
+
+% EXPECT: INVALID
+QUERY FALSE;
+% EXPECT: VALID
+QUERY TRUE;
+% EXPECT-ERROR: CVC4 Error:
+% EXPECT-ERROR: Parse Error: regress.cvc:7.13: Unexpected token: 'error'.
+syntax error;
+% EXIT: 1
+
+Use of % gestures in CVC format is natural, as these are comments and ignored
+by the CVC presentation language lexer.  In SMT and SMT2 formats, you can do the
+same, putting % gestures in the file.  However, the run_regression script
+separates these from the benchmark before running cvc4, so the cvc4 SMT and SMT2
+lexers never see (and get tripped up on) the % gestures.  But there's then the
+annoyance that you can't run SMT and SMT2 regressions from the command line
+without the aid of the run_regression script.  So, if you prefer, you can separate
+the benchmark from the output expectations yourself, putting the benchmark in
+(e.g.) regress/regress0/benchmark.smt, and the % EXPECT: lines in
+regress/regress0/benchmark.smt.expect, which is specifically looked for by
+the run_regression script.  If such an .expect file exists, the benchmark
+is left verbatim (and never processed to remove the % EXPECT: lines) by the
+run_regression script.
+
+ -- Morgan Deters <mdeters@cs.nyu.edu>  Thu, 01 Jul 2010 13:36:53 -0400
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index ddab915bf..42589d84c 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -21,6 +21,7 @@ UNIT_TESTS = \
 	context/cdlist_black \
 	context/cdmap_black \
 	context/cdmap_white \
+	theory/theory_engine_white \
 	theory/theory_black \
 	theory/theory_uf_white \
 	theory/theory_arith_white \
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
new file mode 100644
index 000000000..715799435
--- /dev/null
+++ b/test/unit/theory/theory_engine_white.h
@@ -0,0 +1,354 @@
+/*********************                                                        */
+/*! \file theory_engine_white.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 White box testing of CVC4::theory::Theory.
+ **
+ ** White box testing of CVC4::theory::Theory.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include <iostream>
+#include <string>
+#include <deque>
+
+#include "theory/theory.h"
+#include "theory/theory_engine.h"
+#include "theory/theoryof_table.h"
+#include "expr/node.h"
+#include "expr/node_manager.h"
+#include "expr/kind.h"
+#include "context/context.h"
+#include "util/rational.h"
+#include "util/integer.h"
+#include "util/Assert.h"
+
+using namespace CVC4;
+using namespace CVC4::theory;
+using namespace CVC4::expr;
+using namespace CVC4::context;
+using namespace CVC4::kind;
+
+using namespace std;
+
+class FakeOutputChannel : public OutputChannel {
+  void conflict(TNode n, bool safe) throw(AssertionException) {
+    Unimplemented();
+  }
+  void propagate(TNode n, bool safe) throw(AssertionException) {
+    Unimplemented();
+  }
+  void lemma(TNode n, bool safe) throw(AssertionException) {
+    Unimplemented();
+  }
+  void augmentingLemma(TNode n, bool safe) throw(AssertionException) {
+    Unimplemented();
+  }
+  void explanation(TNode n, bool safe) throw(AssertionException) {
+    Unimplemented();
+  }
+};/* class FakeOutputChannel */
+
+class FakeTheory;
+
+enum RewriteType {
+  PRE,
+  POST
+};/* enum RewriteType */
+
+struct RewriteItem {
+  RewriteType d_type;
+  FakeTheory* d_theory;
+  Node d_node;
+  bool d_topLevel;
+};/* struct RewriteItem */
+
+class FakeTheory : public Theory {
+  std::string d_id;
+
+  static std::deque<RewriteItem> s_expected;
+
+public:
+  FakeTheory(context::Context* ctxt, OutputChannel& out, std::string id) :
+    Theory(ctxt, out),
+    d_id(id) {
+  }
+
+  static void expect(RewriteType type, FakeTheory* thy,
+                     TNode n, bool topLevel) throw() {
+    RewriteItem item = { type, thy, n, topLevel };
+    s_expected.push_back(item);
+  }
+
+  static bool nothingMoreExpected() throw() {
+    return s_expected.empty();
+  }
+
+  RewriteResponse preRewrite(TNode n, bool topLevel) {
+    if(s_expected.empty()) {
+      cout << std::endl
+           << "didn't expect anything more, but got" << std::endl
+           << "     PRE  " << topLevel << " " << identify() << " " << n << std::endl;
+    }
+    TS_ASSERT(!s_expected.empty());
+
+    RewriteItem expected = s_expected.front();
+    s_expected.pop_front();
+
+    if(expected.d_type != PRE ||
+       expected.d_theory != this ||
+       expected.d_node != n ||
+       expected.d_topLevel != topLevel) {
+      cout << std::endl
+           << "HAVE PRE  " << topLevel << " " << identify() << " " << n << std::endl
+           << "WANT " << (expected.d_type == PRE ? "PRE  " : "POST ") << expected.d_topLevel << " " << expected.d_theory->identify() << " " << expected.d_node << std::endl << std::endl;
+    }
+
+    TS_ASSERT_EQUALS(expected.d_type, PRE);
+    TS_ASSERT_EQUALS(expected.d_theory, this);
+    TS_ASSERT_EQUALS(expected.d_node, n);
+    TS_ASSERT_EQUALS(expected.d_topLevel, topLevel);
+
+    return RewritingComplete(n);
+  }
+
+  RewriteResponse postRewrite(TNode n, bool topLevel) {
+    if(s_expected.empty()) {
+      cout << std::endl
+           << "didn't expect anything more, but got" << std::endl
+           << "     POST " << topLevel << " " << identify() << " " << n << std::endl;
+    }
+    TS_ASSERT(!s_expected.empty());
+
+    RewriteItem expected = s_expected.front();
+    s_expected.pop_front();
+
+    if(expected.d_type != POST ||
+       expected.d_theory != this ||
+       expected.d_node != n ||
+       expected.d_topLevel != topLevel) {
+      cout << std::endl
+           << "HAVE POST " << topLevel << " " << identify() << " " << n << std::endl
+           << "WANT " << (expected.d_type == PRE ? "PRE  " : "POST ") << expected.d_topLevel << " " << expected.d_theory->identify() << " " << expected.d_node << std::endl << std::endl;
+    }
+
+    TS_ASSERT_EQUALS(expected.d_type, POST);
+    TS_ASSERT_EQUALS(expected.d_theory, this);
+    TS_ASSERT_EQUALS(expected.d_node, n);
+    TS_ASSERT_EQUALS(expected.d_topLevel, topLevel);
+
+    return RewritingComplete(n);
+  }
+
+  std::string identify() const throw() {
+    return "Fake" + d_id;
+  }
+
+  void preRegisterTerm(TNode) { Unimplemented(); }
+  void registerTerm(TNode) { Unimplemented(); }
+  void check(Theory::Effort) { Unimplemented(); }
+  void propagate(Theory::Effort) { Unimplemented(); }
+  void explain(TNode, Theory::Effort) { Unimplemented(); }
+};/* class FakeTheory */
+
+std::deque<RewriteItem> FakeTheory::s_expected;
+
+/**
+ * Test the TheoryEngine.
+ */
+class TheoryEngineWhite : public CxxTest::TestSuite {
+  Context* d_ctxt;
+
+  NodeManager* d_nm;
+  NodeManagerScope* d_scope;
+  FakeOutputChannel *d_nullChannel;
+  FakeTheory *d_builtin, *d_bool, *d_uf, *d_arith, *d_arrays, *d_bv;
+  TheoryEngine* d_theoryEngine;
+
+public:
+
+  void setUp() {
+    d_ctxt = new Context;
+
+    d_nm = new NodeManager(d_ctxt);
+    d_scope = new NodeManagerScope(d_nm);
+
+    d_nullChannel = new FakeOutputChannel;
+
+    d_builtin = new FakeTheory(d_ctxt, *d_nullChannel, "Builtin");
+    d_bool = new FakeTheory(d_ctxt, *d_nullChannel, "Bool");
+    d_uf = new FakeTheory(d_ctxt, *d_nullChannel, "UF");
+    d_arith = new FakeTheory(d_ctxt, *d_nullChannel, "Arith");
+    d_arrays = new FakeTheory(d_ctxt, *d_nullChannel, "Arrays");
+    d_bv = new FakeTheory(d_ctxt, *d_nullChannel, "BV");
+
+    d_theoryEngine = new TheoryEngine(d_ctxt);
+
+    // insert our fake versions into the theoryOf table
+    d_theoryEngine->d_theoryOfTable.
+      registerTheory(reinterpret_cast<theory::builtin::TheoryBuiltin*>(d_builtin));
+    d_theoryEngine->d_theoryOfTable.
+      registerTheory(reinterpret_cast<theory::booleans::TheoryBool*>(d_bool));
+    d_theoryEngine->d_theoryOfTable.
+      registerTheory(reinterpret_cast<theory::uf::TheoryUF*>(d_uf));
+    d_theoryEngine->d_theoryOfTable.
+      registerTheory(reinterpret_cast<theory::arith::TheoryArith*>(d_arith));
+    d_theoryEngine->d_theoryOfTable.
+      registerTheory(reinterpret_cast<theory::arrays::TheoryArrays*>(d_arrays));
+    d_theoryEngine->d_theoryOfTable.
+      registerTheory(reinterpret_cast<theory::bv::TheoryBV*>(d_bv));
+
+    Debug.on("theory-rewrite");
+  }
+
+  void tearDown() {
+    delete d_theoryEngine;
+
+    delete d_bv;
+    delete d_arrays;
+    delete d_arith;
+    delete d_uf;
+    delete d_bool;
+    delete d_builtin;
+
+    delete d_nullChannel;
+
+    delete d_scope;
+    delete d_nm;
+
+    delete d_ctxt;
+  }
+
+  void testRewriterSimple() {
+    Node x = d_nm->mkVar("x", d_nm->integerType());
+    Node y = d_nm->mkVar("y", d_nm->integerType());
+    Node z = d_nm->mkVar("z", d_nm->integerType());
+
+    // make the expression (PLUS x y (MULT z 0))
+    Node zero = d_nm->mkConst(Rational("0"));
+    Node zTimesZero = d_nm->mkNode(MULT, z, zero);
+    Node n = d_nm->mkNode(PLUS, x, y, zTimesZero);
+
+    Node nExpected = n;
+    Node nOut;
+
+    FakeTheory::expect(PRE, d_arith, n, true);
+    FakeTheory::expect(PRE, d_arith, x, false);
+    FakeTheory::expect(POST, d_arith, x, false);
+    FakeTheory::expect(PRE, d_arith, y, false);
+    FakeTheory::expect(POST, d_arith, y, false);
+    FakeTheory::expect(PRE, d_arith, zTimesZero, false);
+    FakeTheory::expect(PRE, d_arith, z, false);
+    FakeTheory::expect(POST, d_arith, z, false);
+    FakeTheory::expect(PRE, d_arith, zero, false);
+    FakeTheory::expect(POST, d_arith, zero, false);
+    FakeTheory::expect(POST, d_arith, zTimesZero, false);
+    FakeTheory::expect(POST, d_arith, n, true);
+    nOut = d_theoryEngine->rewrite(n);
+    TS_ASSERT(FakeTheory::nothingMoreExpected());
+
+    TS_ASSERT_EQUALS(nOut, nExpected);
+  }
+
+  void testRewriterComplicated() {
+    Node x = d_nm->mkVar("x", d_nm->integerType());
+    Node y = d_nm->mkVar("y", d_nm->realType());
+    Node z1 = d_nm->mkVar("z1", d_nm->mkSort("U"));
+    Node z2 = d_nm->mkVar("z2", d_nm->mkSort("U"));
+    Node f = d_nm->mkVar("f", d_nm->mkFunctionType(d_nm->integerType(),
+                                                   d_nm->integerType()));
+    Node g = d_nm->mkVar("g", d_nm->mkFunctionType(d_nm->realType(),
+                                                   d_nm->integerType()));
+    Node one = d_nm->mkConst(Rational("1"));
+    Node two = d_nm->mkConst(Rational("2"));
+
+    Node f1 = d_nm->mkNode(APPLY_UF, f, one);
+    Node f2 = d_nm->mkNode(APPLY_UF, f, two);
+    Node fx = d_nm->mkNode(APPLY_UF, f, x);
+    Node ffx = d_nm->mkNode(APPLY_UF, f, fx);
+    Node gy = d_nm->mkNode(APPLY_UF, g, y);
+    Node z1eqz2 = d_nm->mkNode(EQUAL, z1, z2);
+    Node f1eqf2 = d_nm->mkNode(EQUAL, f1, f2);
+    Node ffxeqgy = d_nm->mkNode(EQUAL,
+                                ffx,
+                                gy);
+    Node and1 = d_nm->mkNode(AND, ffxeqgy, z1eqz2, ffx);
+    Node ffxeqf1 = d_nm->mkNode(EQUAL, ffx, f1);
+    Node or1 = d_nm->mkNode(OR, and1, ffxeqf1);
+    // make the expression:
+    // (IMPLIES (EQUAL (f 1) (f 2)) (OR (AND (EQUAL (f (f x)) (g y)) (EQUAL z1 z2) (f (f x)))) (EQUAL (f (f x)) (f 1)))
+    Node n = d_nm->mkNode(IMPLIES, f1eqf2, or1);
+    Node nExpected = n;
+    Node nOut;
+
+    // We WOULD expect that the commented-out calls were made, except
+    // for the cache
+    FakeTheory::expect(PRE, d_bool, n, true);
+    FakeTheory::expect(PRE, d_uf, f1eqf2, true);
+    FakeTheory::expect(PRE, d_uf, f1, false);
+    FakeTheory::expect(PRE, d_builtin, f, true);
+    FakeTheory::expect(POST, d_builtin, f, true);
+    FakeTheory::expect(PRE, d_arith, one, true);
+    FakeTheory::expect(POST, d_arith, one, true);
+    FakeTheory::expect(POST, d_uf, f1, false);
+    FakeTheory::expect(PRE, d_uf, f2, false);
+    //FakeTheory::expect(PRE, d_builtin, f, true);
+    //FakeTheory::expect(POST, d_builtin, f, true);
+    FakeTheory::expect(PRE, d_arith, two, true);
+    FakeTheory::expect(POST, d_arith, two, true);
+    FakeTheory::expect(POST, d_uf, f2, false);
+    FakeTheory::expect(POST, d_uf, f1eqf2, true);
+    FakeTheory::expect(PRE, d_bool, or1, false);
+    FakeTheory::expect(PRE, d_bool, and1, false);
+    FakeTheory::expect(PRE, d_uf, ffxeqgy, true);
+    FakeTheory::expect(PRE, d_uf, ffx, false);
+    FakeTheory::expect(PRE, d_uf, fx, false);
+    //FakeTheory::expect(PRE, d_builtin, f, true);
+    //FakeTheory::expect(POST, d_builtin, f, true);
+    FakeTheory::expect(PRE, d_arith, x, true);
+    FakeTheory::expect(POST, d_arith, x, true);
+    FakeTheory::expect(POST, d_uf, fx, false);
+    FakeTheory::expect(POST, d_uf, ffx, false);
+    FakeTheory::expect(PRE, d_uf, gy, false);
+    FakeTheory::expect(PRE, d_builtin, g, true);
+    FakeTheory::expect(POST, d_builtin, g, true);
+    FakeTheory::expect(PRE, d_arith, y, true);
+    FakeTheory::expect(POST, d_arith, y, true);
+    FakeTheory::expect(POST, d_uf, gy, false);
+    FakeTheory::expect(POST, d_uf, ffxeqgy, true);
+    FakeTheory::expect(PRE, d_uf, z1eqz2, true);
+    FakeTheory::expect(PRE, d_uf, z1, false);
+    FakeTheory::expect(POST, d_uf, z1, false);
+    FakeTheory::expect(PRE, d_uf, z2, false);
+    FakeTheory::expect(POST, d_uf, z2, false);
+    FakeTheory::expect(POST, d_uf, z1eqz2, true);
+    // tricky one: ffx is in cache but for a non-topLevel !
+    FakeTheory::expect(PRE, d_uf, ffx, true);
+    //FakeTheory::expect(PRE, d_uf, fx, false);
+    //FakeTheory::expect(POST, d_uf, fx, false);
+    FakeTheory::expect(POST, d_uf, ffx, true);
+    FakeTheory::expect(POST, d_bool, and1, false);
+    FakeTheory::expect(PRE, d_uf, ffxeqf1, true);
+    //FakeTheory::expect(PRE, d_uf, ffx, false);
+    //FakeTheory::expect(POST, d_uf, ffx, false);
+    //FakeTheory::expect(PRE, d_uf, f1, false);
+    //FakeTheory::expect(POST, d_uf, f1, false);
+    FakeTheory::expect(POST, d_uf, ffxeqf1, true);
+    FakeTheory::expect(POST, d_bool, or1, false);
+    FakeTheory::expect(POST, d_bool, n, true);
+    nOut = d_theoryEngine->rewrite(n);
+    TS_ASSERT(FakeTheory::nothingMoreExpected());
+
+    TS_ASSERT_EQUALS(nOut, nExpected);
+  }
+};