* 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

1 files changed, 23 insertions, 31 deletions

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,