* 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

10 files changed, 240 insertions, 77 deletions

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