* 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

5 files changed, 141 insertions, 99 deletions

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"