Highlights of this commit are:

* add NodeManagerWhite unit test

* change kind::APPLY to kind::APPLY_UF

* better APPLY handling: operators are no longer considered children

* more efficient pool lookup; the NodeValue doesn't have to be as fully constructed for the lookup to proceed

* extend DSL for kind declarations
  + new "theory" command declares a theory and its header.  theory_def.h no longer required.
  + arity enforced on operators
  + constant mapping, hashing, equality

* CONSTANT metakinds supported (via Node::getConst<T>(), for example, Node::getConst<CVC4::Rational>() gets a Rational out of a Node (assuming it is of CONST_RATIONAL kind)

* added CONST_RATIONAL and CONST_INTEGER kinds

* builtin operators (AND, OR, PLUS, etc..) returned by Node::getOperator() are now CONSTANT metakind and are created by NodeManager

* Pretty-printing of Nodes now has a depth limit settable by a stream manipulator (e.g. "cout << Node::setdepth(5) << m << endl;" prints DAG rooted at m to a depth of 5)

* getters added to Node, TNode, NodeValue, etc., for operators and metakinds

* build-time generators for kind.h, metakind.h, and theoryof_table.h headers now have a simpler design and flag errors better, and the templates (kind_template.h etc.) are easier to understand.

* DISTINCT is now a kind, and the SMT parser now passes through DISTINCT nodes instead of blowing them up into ANDs.  Until theory rewriting is online, though, DISTINCTs are directly blown up into conjunctions in TheoryEngine::rewrite().

* add gmpxx detection and inclusion

* better Asserts throughout, some documentation, cleanup

1 files changed, 183 insertions, 71 deletions

diff --git a/src/expr/node.h b/src/expr/node.h
index ebe06ead2..343f03a1f 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -58,6 +58,7 @@ class NodeValue;
     class AttributeManager;
   }/* CVC4::expr::attr namespace */
 
+  class NodeSetDepth;
 }/* CVC4::expr namespace */
 
 /**
@@ -208,8 +209,7 @@ public:
    * @return the node representing the i-th child
    */
   NodeTemplate operator[](int i) const {
-    Assert(i >= 0 && unsigned(i) < d_nv->d_nchildren);
-    return NodeTemplate(d_nv->d_children[i]);
+    return NodeTemplate(d_nv->getChild(i));
   }
 
   /**
@@ -234,7 +234,7 @@ public:
   NodeTemplate<true> getOperator() const;
 
   /** Returns true if the node has an operator (i.e., it's not a variable or a constant). */
-  bool hasOperator() const;
+  inline bool hasOperator() const;
 
   /**
    * Returns the type of this node.
@@ -251,12 +251,26 @@ public:
   }
 
   /**
+   * Returns the metakind of this node.
+   * @return the metakind
+   */
+  inline kind::MetaKind getMetaKind() const {
+    return kind::metaKindOf(getKind());
+  }
+
+  /**
    * Returns the number of children this node has.
    * @return the number of children
    */
   inline size_t getNumChildren() const;
 
   /**
+   * If this is a CONST_* Node, extract the constant from it.
+   */
+  template <class T>
+  inline const T& getConst() const;
+
+  /**
    * Returns the value of the given attribute that this has been attached.
    * @param attKind the kind of the attribute
    * @return the value of the attribute
@@ -352,11 +366,27 @@ public:
    * given stream
    * @param out the sream to serialise this node to
    */
-  inline void toStream(std::ostream& out) const {
-    d_nv->toStream(out);
+  inline void toStream(std::ostream& out, int toDepth = -1) const {
+    d_nv->toStream(out, toDepth);
   }
 
   /**
+   * IOStream manipulator to set the maximum depth of Nodes 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;
+   *
+   * gives "(OR a b (AND c (NOT d)))", but
+   *
+   *   out << setdepth(1) << [same node as above]
+   *
+   * gives "(OR a b (...))"
+   */
+  typedef expr::NodeSetDepth setdepth;
+
+  /**
    * Very basic pretty printer for Node.
    * @param o output stream to print to.
    * @param indent number of spaces to indent the formula by.
@@ -387,7 +417,85 @@ private:
     }
   }
 
-};/* class NodeTemplate */
+};/* class NodeTemplate<ref_count> */
+
+namespace expr {
+
+/**
+ * IOStream manipulator to set the maximum depth of Nodes 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;
+ *
+ * gives "(OR a b (AND c (NOT d)))", but
+ *
+ *   out << setdepth(1) << [same node as above]
+ *
+ * gives "(OR a b (...))".
+ *
+ * The implementation of this class serves two purposes; it holds
+ * information about the depth setting (such as the index of the
+ * allocated word in ios_base), and serves also as the manipulator
+ * itself (as above).
+ */
+class NodeSetDepth {
+  /**
+   * 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_defaultPrintDepth = 3;
+
+  /**
+   * When this manipulator is 
+   */
+  long d_depth;
+
+public:
+  /**
+   * Construct a NodeSetDepth with the given depth.
+   */
+  NodeSetDepth(long depth) : d_depth(depth) {}
+
+  inline void applyDepth(std::ostream& out) {
+    out.iword(s_iosIndex) = d_depth;
+  }
+
+  static inline long getDepth(std::ostream& out) {
+    long& l = out.iword(s_iosIndex);
+    if(l == 0) {
+      // set the default print depth on this ostream
+      l = s_defaultPrintDepth;
+    }
+    return l;
+  }
+
+  static inline void setDepth(std::ostream& out, long depth) {
+    out.iword(s_iosIndex) = depth;
+  }
+};
+
+/**
+ * Sets the default depth when pretty-printing a Node to an ostream.
+ * Use like this:
+ *
+ *   // let out be an ostream, n a Node
+ *   out << Node::setdepth(n) << n << endl;
+ *
+ * The depth stays permanently (until set again) with the stream.
+ */
+inline std::ostream& operator<<(std::ostream& out, NodeSetDepth sd) {
+  sd.applyDepth(out);
+  return out;
+}
+
+}/* CVC4::expr namespace */
 
 /**
  * Serializes a given node to the given stream.
@@ -395,8 +503,8 @@ private:
  * @param node the node to output to the stream
  * @return the changed stream.
  */
-inline std::ostream& operator<<(std::ostream& out, const Node& node) {
-  node.toStream(out);
+inline std::ostream& operator<<(std::ostream& out, TNode n) {
+  n.toStream(out, Node::setdepth::getDepth(out));
   return out;
 }
 
@@ -418,7 +526,13 @@ struct NodeHashFunction {
 
 template <bool ref_count>
 inline size_t NodeTemplate<ref_count>::getNumChildren() const {
-  return d_nv->d_nchildren;
+  return d_nv->getNumChildren();
+}
+
+template <bool ref_count>
+template <class T>
+inline const T& NodeTemplate<ref_count>::getConst() const {
+  return d_nv->getConst<T>();
 }
 
 template <bool ref_count>
@@ -493,17 +607,25 @@ NodeTemplate<ref_count>::NodeTemplate(const expr::NodeValue* ev) :
   Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
   if(ref_count) {
     d_nv->inc();
+  } else {
+    Assert(d_nv->d_rc > 0, "TNode constructed from NodeValue with rc == 0");
   }
 }
 
-// the code for these two "conversion/copy constructors" is identical, but
-// apparently we need both.  see comment in the class.
+// the code for these two following constructors ("conversion/copy
+// constructors") is identical, but we need both.  see comment in the
+// class.
+
 template <bool ref_count>
 NodeTemplate<ref_count>::NodeTemplate(const NodeTemplate<!ref_count>& e) {
   Assert(e.d_nv != NULL, "Expecting a non-NULL expression value!");
   d_nv = e.d_nv;
   if(ref_count) {
     d_nv->inc();
+  } else {
+    // shouldn't ever happen
+    Assert(d_nv->d_rc > 0,
+           "INTERNAL ERROR: TNode constructed from Node with rc == 0");
   }
 }
 
@@ -513,6 +635,8 @@ NodeTemplate<ref_count>::NodeTemplate(const NodeTemplate& e) {
   d_nv = e.d_nv;
   if(ref_count) {
     d_nv->inc();
+  } else {
+    Assert(d_nv->d_rc > 0, "TNode constructed from TNode with rc == 0");
   }
 }
 
@@ -521,11 +645,10 @@ NodeTemplate<ref_count>::~NodeTemplate() throw(AssertionException) {
   Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
   if(ref_count) {
     d_nv->dec();
+  } else {
+    Assert(d_nv->d_rc > 0 || d_nv->isBeingDeleted(),
+           "TNode pointing to an expired NodeValue at destruction time");
   }
-  Assert(ref_count ||
-         d_nv->d_rc > 0 ||
-         d_nv->isBeingDeleted(),
-         "Temporary node pointing to an expired node");
 }
 
 template <bool ref_count>
@@ -533,6 +656,8 @@ void NodeTemplate<ref_count>::assignNodeValue(expr::NodeValue* ev) {
   d_nv = ev;
   if(ref_count) {
     d_nv->inc();
+  } else {
+    Assert(d_nv->d_rc > 0, "TNode assigned to NodeValue with rc == 0");
   }
 }
 
@@ -548,6 +673,8 @@ operator=(const NodeTemplate& e) {
     d_nv = e.d_nv;
     if(ref_count) {
       d_nv->inc();
+    } else {
+      Assert(d_nv->d_rc > 0, "TNode assigned from TNode with rc == 0");
     }
   }
   return *this;
@@ -565,6 +692,10 @@ operator=(const NodeTemplate<!ref_count>& e) {
     d_nv = e.d_nv;
     if(ref_count) {
       d_nv->inc();
+    } else {
+      // shouldn't ever happen
+      Assert(d_nv->d_rc > 0,
+             "INTERNAL ERROR: TNode assigned from Node with rc == 0");
     }
   }
   return *this;
@@ -623,16 +754,24 @@ void NodeTemplate<ref_count>::printAst(std::ostream& out, int ind) const {
   indent(out, ind);
   out << '(';
   out << getKind();
-  if(getKind() == kind::VARIABLE) {
+  if(getMetaKind() == kind::metakind::VARIABLE) {
     out << ' ' << getId();
-
-  } else if(getNumChildren() >= 1) {
-    for(const_iterator child = begin(); child != end(); ++child) {
+  } 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;
-      NodeTemplate((*child)).printAst(out, ind + 1);
+      indent(out, ind);
     }
-    out << std::endl;
-    indent(out, ind);
   }
   out << ')';
 }
@@ -644,36 +783,31 @@ void NodeTemplate<ref_count>::printAst(std::ostream& out, int ind) const {
  */
 template <bool ref_count>
 NodeTemplate<true> NodeTemplate<ref_count>::getOperator() const {
-  switch(Kind k = getKind()) {
-  case kind::APPLY:
-    /* The operator is the first child. */
-    return NodeTemplate<true>(d_nv->d_children[0]);
-
-  case kind::EQUAL:
-  case kind::ITE:
-  case kind::TUPLE:
-  case kind::NOT:
-  case kind::AND:
-  case kind::IFF:
-  case kind::IMPLIES:
-  case kind::OR:
-  case kind::XOR:
-  case kind::PLUS: {
+  Assert( NodeManager::currentNM() != NULL,
+          "There is no current CVC4::NodeManager associated to this thread.\n"
+          "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+
+  switch(kind::MetaKind mk = getMetaKind()) {
+  case kind::metakind::INVALID:
+    IllegalArgument(*this, "getOperator() called on Node with INVALID-kinded kind");
+
+  case kind::metakind::VARIABLE:
+    IllegalArgument(*this, "getOperator() called on Node with VARIABLE-kinded kind");
+
+  case kind::metakind::OPERATOR: {
     /* Returns a BUILTIN node. */
-    /* TODO: construct a singleton at load-time? */
-    /* TODO: maybe keep a table like the TheoryOfTable ? */
-    NodeTemplate<true> n = NodeManager::currentNM()->mkNode(k);
-    return NodeManager::currentNM()->mkNode(kind::BUILTIN, n);
+    return NodeManager::currentNM()->operatorOf(getKind());
   }
 
-  case kind::FALSE:
-  case kind::TRUE:
-  case kind::SKOLEM:
-  case kind::VARIABLE:
-    IllegalArgument(*this, "getOperator() called on kind with no operator");
+  case kind::metakind::PARAMETERIZED:
+    /* The operator is the first child. */
+    return Node(d_nv->d_children[0]);
+
+  case kind::metakind::CONSTANT:
+    IllegalArgument(*this, "getOperator() called on Node with CONSTANT-kinded kind");
 
   default:
-    Unhandled(getKind());
+    Unhandled(mk);
   }
 }
 
@@ -682,30 +816,8 @@ NodeTemplate<true> NodeTemplate<ref_count>::getOperator() const {
  * or a constant).
  */
 template <bool ref_count>
-bool NodeTemplate<ref_count>::hasOperator() const {
-  switch(getKind()) {
-  case kind::APPLY:
-  case kind::EQUAL:
-  case kind::ITE:
-  case kind::TUPLE:
-  case kind::FALSE:
-  case kind::TRUE:
-  case kind::NOT:
-  case kind::AND:
-  case kind::IFF:
-  case kind::IMPLIES:
-  case kind::OR:
-  case kind::XOR:
-  case kind::PLUS:
-    return true;
-
-  case kind::SKOLEM:
-  case kind::VARIABLE:
-    return false;
-
-  default:
-    Unhandled(getKind());
-  }
+inline bool NodeTemplate<ref_count>::hasOperator() const {
+  return NodeManager::hasOperator(getKind());
 }
 
 template <bool ref_count>