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, 100 insertions, 62 deletions

diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 995a63180..7dd90913f 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -19,12 +19,15 @@
 
 #include "cvc4_private.h"
 
+// circular dependency
+#include "expr/metakind.h"
+
 #ifndef __CVC4__EXPR__NODE_VALUE_H
 #define __CVC4__EXPR__NODE_VALUE_H
 
 #include "cvc4_config.h"
-#include <stdint.h>
 #include "expr/kind.h"
+#include <stdint.h>
 
 #include <string>
 #include <iterator>
@@ -40,8 +43,25 @@ class PlusNodeBuilder;
 class MultNodeBuilder;
 class NodeManager;
 
+namespace kind {
+  namespace metakind {
+    template < ::CVC4::Kind k, bool pool >
+    struct NodeValueConstCompare;
+
+    struct NodeValueCompare;
+    struct NodeValueConstPrinter;
+  }/* CVC4::kind::metakind namespace */
+}/* CVC4::kind namespace */
+
 namespace expr {
 
+#if __CVC4__EXPR__NODE_VALUE__NBITS__REFCOUNT + \
+    __CVC4__EXPR__NODE_VALUE__NBITS__KIND + \
+    __CVC4__EXPR__NODE_VALUE__NBITS__ID + \
+    __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN != 64
+#  error NodeValue header bit assignment does not sum to 64 !
+#endif /* sum != 64 */
+
 /**
  * This is an NodeValue.
  */
@@ -50,39 +70,47 @@ class NodeValue {
   /** A convenient null-valued expression value */
   static NodeValue s_null;
 
+  static const unsigned NBITS_REFCOUNT = __CVC4__EXPR__NODE_VALUE__NBITS__REFCOUNT;
+  static const unsigned NBITS_KIND = __CVC4__EXPR__NODE_VALUE__NBITS__KIND;
+  static const unsigned NBITS_ID = __CVC4__EXPR__NODE_VALUE__NBITS__ID;
+  static const unsigned NBITS_NCHILDREN = __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN;
+
   /** Maximum reference count possible.  Used for sticky
    *  reference-counting.  Should be (1 << num_bits(d_rc)) - 1 */
-  static const unsigned MAX_RC = 255;
-
-  /** Number of bits assigned to the kind in the NodeValue header */
-  static const unsigned KINDBITS = 8;
+  static const unsigned MAX_RC = (1u << NBITS_REFCOUNT) - 1;
 
   /** A mask for d_kind */
-  static const unsigned kindMask = (1u << KINDBITS) - 1;
+  static const unsigned kindMask = (1u << NBITS_KIND) - 1;
 
   // this header fits into one 64-bit word
 
   /** The ID (0 is reserved for the null value) */
-  unsigned d_id        : 32;
+  unsigned d_id        : NBITS_ID;
 
   /** The expression's reference count.  @see cvc4::Node. */
-  unsigned d_rc        :  8;
+  unsigned d_rc        : NBITS_REFCOUNT;
 
   /** Kind of the expression */
-  unsigned d_kind      : KINDBITS;
+  unsigned d_kind      : NBITS_KIND;
 
   /** Number of children */
-  unsigned d_nchildren : 16;
+  unsigned d_nchildren : NBITS_NCHILDREN;
 
   /** Variable number of child nodes */
   NodeValue* d_children[0];
 
   // todo add exprMgr ref in debug case
 
-  template <bool> friend class CVC4::NodeTemplate;
-  template <class Builder> friend class CVC4::NodeBuilderBase;
-  template <unsigned nchild_thresh> friend class CVC4::NodeBuilder;
-  friend class CVC4::NodeManager;
+  template <bool> friend class ::CVC4::NodeTemplate;
+  template <class Builder> friend class ::CVC4::NodeBuilderBase;
+  template <unsigned nchild_thresh> friend class ::CVC4::NodeBuilder;
+  friend class ::CVC4::NodeManager;
+
+  template <Kind k, bool pool>
+  friend struct ::CVC4::kind::metakind::NodeValueConstCompare; 
+
+  friend struct ::CVC4::kind::metakind::NodeValueCompare;
+  friend struct ::CVC4::kind::metakind::NodeValueConstPrinter;
 
   void inc();
   void dec();
@@ -146,14 +174,10 @@ private:
 public:
 
   template <bool ref_count>
-  iterator<ref_count> begin() const {
-    return iterator<ref_count>(d_children);
-  }
+  inline iterator<ref_count> begin() const;
 
   template <bool ref_count>
-  iterator<ref_count> end() const {
-    return iterator<ref_count>(d_children + d_nchildren);
-  }
+  inline iterator<ref_count> end() const;
 
   /**
    * Hash this NodeValue.  For hash_maps, hash_sets, etc.. but this is
@@ -162,7 +186,11 @@ public:
    * collisions for all VARIABLEs.
    * @return the hash value of this expression.
    */
-  size_t internalHash() const {
+  size_t poolHash() const {
+    if(getMetaKind() == kind::metakind::CONSTANT) {
+      return kind::metakind::NodeValueCompare::constHash(this);
+    }
+
     size_t hash = d_kind;
     const_nv_iterator i = nv_begin();
     const_nv_iterator i_end = nv_end();
@@ -173,43 +201,17 @@ public:
     return hash;
   }
 
-  inline bool compareTo(const NodeValue* nv) const {
-    if(d_kind != nv->d_kind) {
-      return false;
-    }
-
-    if(d_nchildren != nv->d_nchildren) {
-      return false;
-    }
-
-    const_nv_iterator i = nv_begin();
-    const_nv_iterator j = nv->nv_begin();
-    const_nv_iterator i_end = nv_end();
-
-    while(i != i_end) {
-      if((*i) != (*j)) {
-        return false;
-      }
-      ++i;
-      ++j;
-    }
-
-    return true;
-  }
-
-  // Comparison predicate
-  struct NodeValueEq {
-    bool operator()(const NodeValue* nv1, const NodeValue* nv2) const {
-      return nv1->compareTo(nv2);
-    }
-  };
-
   unsigned getId() const { return d_id; }
   Kind getKind() const { return dKindToKind(d_kind); }
-  unsigned getNumChildren() const { return d_nchildren; }
+  kind::MetaKind getMetaKind() const { return kind::metaKindOf(getKind()); }
+  unsigned getNumChildren() const {
+    return (getMetaKind() == kind::metakind::PARAMETERIZED)
+      ? d_nchildren - 1
+      : d_nchildren;
+  }
 
   std::string toString() const;
-  void toStream(std::ostream& out) const;
+  void toStream(std::ostream& out, int toDepth = -1) const;
 
   static inline unsigned kindToDKind(Kind k) {
     return ((unsigned) k) & kindMask;
@@ -223,19 +225,27 @@ public:
     return s_null;
   }
 
+  /**
+   * If this is a CONST_* Node, extract the constant from it.
+   */
+  template <class T>
+  inline const T& getConst() const;
+
+  NodeValue* getChild(int i) const;
+
 };/* class NodeValue */
 
 /**
  * For hash_maps, hash_sets, etc.. but this is for expr package
  * internal use only at present!  This is likely to be POORLY
- * PERFORMING for other uses!  NodeValue::internalHash() will lead to
+ * PERFORMING for other uses!  NodeValue::poolHash() will lead to
  * collisions for all VARIABLEs.
  */
-struct NodeValueInternalHashFunction {
+struct NodeValuePoolHashFcn {
   inline size_t operator()(const NodeValue* nv) const {
-    return (size_t) nv->internalHash();
+    return (size_t) nv->poolHash();
   }
-};/* struct NodeValueInternalHashFunction */
+};/* struct NodeValuePoolHashFcn */
 
 /**
  * For hash_maps, hash_sets, etc.
@@ -244,12 +254,14 @@ struct NodeValueIDHashFunction {
   inline size_t operator()(const NodeValue* nv) const {
     return (size_t) nv->getId();
   }
-};/* struct NodeValueHashFcn */
+};/* struct NodeValueIDHashFcn */
+
+inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv);
 
 }/* CVC4::expr namespace */
 }/* CVC4 namespace */
 
-#include "node_manager.h"
+#include "expr/node_manager.h"
 
 namespace CVC4 {
 namespace expr {
@@ -306,13 +318,34 @@ inline NodeValue::const_nv_iterator NodeValue::nv_end() const {
   return d_children + d_nchildren;
 }
 
+template <bool ref_count>
+inline NodeValue::iterator<ref_count> NodeValue::begin() const {
+  NodeValue* const* firstChild = d_children;
+  if(getMetaKind() == kind::metakind::PARAMETERIZED) {
+    ++firstChild;
+  }
+  return iterator<ref_count>(firstChild);
+}
+
+template <bool ref_count>
+inline NodeValue::iterator<ref_count> NodeValue::end() const {
+  return iterator<ref_count>(d_children + d_nchildren);
+}
 
-inline bool NodeValue::isBeingDeleted() const
-{
+inline bool NodeValue::isBeingDeleted() const {
   return NodeManager::currentNM() != NULL &&
     NodeManager::currentNM()->isCurrentlyDeleting(this);
 }
 
+inline NodeValue* NodeValue::getChild(int i) const {
+  if(getMetaKind() == kind::metakind::PARAMETERIZED) {
+    ++i;
+  }
+
+  Assert(i >= 0 && unsigned(i) < d_nchildren);
+  return d_children[i];
+}
+
 }/* CVC4::expr namespace */
 }/* CVC4 namespace */
 
@@ -326,6 +359,11 @@ inline CVC4::NodeTemplate<ref_count> NodeValue::iterator<ref_count>::operator*()
   return NodeTemplate<ref_count>(*d_i);
 }
 
+inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv) {
+  nv.toStream(out, Node::setdepth::getDepth(out));
+  return out;
+}
+
 }/* CVC4::expr namespace */
 }/* CVC4 namespace */