* 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, 34 insertions, 5 deletions

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 */