* 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, 38 insertions, 2 deletions

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