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, 285 insertions, 0 deletions

diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
new file mode 100644
index 000000000..95e107313
--- /dev/null
+++ b/src/expr/metakind_template.h
@@ -0,0 +1,285 @@
+/*********************                                                        */
+/** metakind_template.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** Template for the metakind header.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__KIND__METAKIND_H
+#define __CVC4__KIND__METAKIND_H
+
+#include <iostream>
+
+#include "expr/kind.h"
+#include "util/Assert.h"
+
+${metakind_includes}
+
+namespace CVC4 {
+
+namespace expr {
+  class NodeValue;
+}/* CVC4::expr namespace */
+
+namespace kind {
+namespace metakind {
+
+/**
+ * Static, compile-time information about types T representing CVC4
+ * constants:
+ *
+ *   typename ConstantMap<T>::OwningTheory
+ *
+ *     The theory in charge of constructing T when constructing Nodes
+ *     with NodeManager::mkConst(T).
+ *
+ *   typename ConstantMap<T>::kind
+ *
+ *     The kind to use when constructing Nodes with
+ *     NodeManager::mkConst(T).
+ */
+template <class T>
+struct ConstantMap;
+
+/**
+ * Static, compile-time information about kinds k and what type their
+ * corresponding CVC4 constants are:
+ *
+ *   typename ConstantMapReverse<k>::T
+ *
+ *     Constant type for kind k.
+ */
+template <Kind k>
+struct ConstantMapReverse;
+
+/**
+ * Static, compile-time mapping from CONSTANT kinds to comparison
+ * functors on NodeValue*.  The single element of this structure is:
+ *
+ *   static bool NodeValueCompare<K, pool>::compare(NodeValue* x, NodeValue* y)
+ *
+ *     Compares x and y, given that they are both K-kinded (and the
+ *     meta-kind of K is CONSTANT).  If pool == true, one of x and y
+ *     (but not both) may be a "non-inlined" NodeValue.  If pool ==
+ *     false, neither x nor y may be a "non-inlined" NodeValue.
+ */
+template <Kind k, bool pool>
+struct NodeValueConstCompare {
+  inline static bool compare(const ::CVC4::expr::NodeValue* x,
+                             const ::CVC4::expr::NodeValue* y);
+  inline static size_t constHash(const ::CVC4::expr::NodeValue* nv);
+};/* NodeValueConstCompare<k, pool> */
+
+struct NodeValueCompare {
+  template <bool pool>
+  inline static bool compare(const ::CVC4::expr::NodeValue* nv1,
+                             const ::CVC4::expr::NodeValue* nv2);
+  inline static size_t constHash(const ::CVC4::expr::NodeValue* nv);
+};/* struct NodeValueCompare */
+
+struct NodeValueConstPrinter {
+  inline static void toStream(std::ostream& out,
+                              const ::CVC4::expr::NodeValue* nv);
+};
+
+/**
+ * "metakinds" represent the "kinds" of kinds at the meta-level.
+ * "metakind" is an ugly name but it's not used by client code, just
+ * by the expr package, and the intent here is to keep it from
+ * polluting the kind namespace.  For more documentation on what these
+ * mean, see src/expr/builtin_kinds.
+ */
+enum MetaKind_t {
+  INVALID = -1, /*! special node non-kinds like NULL_EXPR or LAST_KIND */
+  VARIABLE, /*! special node kinds: no operator */
+  OPERATOR, /*! operators that get "inlined" */
+  PARAMETERIZED, /*! parameterized ops (like APPLYs) that carry extra data */
+  CONSTANT /*! constants */
+};/* enum MetaKind_t */
+
+}/* CVC4::kind::metakind namespace */
+
+// import MetaKind into the "CVC4::kind" namespace but keep the
+// individual MetaKind constants under kind::metakind::
+typedef ::CVC4::kind::metakind::MetaKind_t MetaKind;
+
+static inline MetaKind metaKindOf(Kind k) {
+  static const MetaKind metaKinds[] = {
+    metakind::INVALID, /* NULL_EXPR */
+${metakind_kinds}
+    metakind::INVALID /* LAST_KIND */
+  };/* metaKinds[] */
+
+  return metaKinds[k];
+}/* metaKindOf(k) */
+
+}/* CVC4::kind namespace */
+
+namespace expr {
+  class NodeValue;
+}/* CVC4::expr namespace */
+
+namespace kind {
+namespace metakind {
+
+/* these are #defines so their sum can be #if-checked in node_value.h */
+#define __CVC4__EXPR__NODE_VALUE__NBITS__REFCOUNT 8
+#define __CVC4__EXPR__NODE_VALUE__NBITS__KIND 8
+#define __CVC4__EXPR__NODE_VALUE__NBITS__ID 32
+#define __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN 16
+
+static const unsigned MAX_CHILDREN =
+  (1u << __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN) - 1;
+
+}/* CVC4::kind::metakind namespace */
+}/* CVC4::kind namespace */
+
+namespace expr {
+
+// Comparison predicate
+struct NodeValueEq {
+  inline bool operator()(const NodeValue* nv1, const NodeValue* nv2) const {
+    return ::CVC4::kind::metakind::NodeValueCompare::compare<false>(nv1, nv2);
+  }
+};
+
+// Comparison predicate
+struct NodeValuePoolEq {
+  inline bool operator()(const NodeValue* nv1, const NodeValue* nv2) const {
+    return ::CVC4::kind::metakind::NodeValueCompare::compare<true>(nv1, nv2);
+  }
+};
+
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */
+
+#include "expr/node_value.h"
+
+#endif /* __CVC4__KIND__METAKIND_H */
+
+#ifdef __CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP
+
+namespace CVC4 {
+namespace kind {
+namespace metakind {
+
+template <Kind k, bool pool>
+inline bool NodeValueConstCompare<k, pool>::compare(const ::CVC4::expr::NodeValue* x,
+                                                    const ::CVC4::expr::NodeValue* y) {
+  typedef typename ConstantMapReverse<k>::T T;
+  if(pool) {
+    if(x->d_nchildren == 1) {
+      Assert(y->d_nchildren == 0);
+      return compare(y, x);
+      return *reinterpret_cast<T*>(x->d_children[0]) == y->getConst<T>();
+    } else if(y->d_nchildren == 1) {
+      Assert(x->d_nchildren == 0);
+      return x->getConst<T>() == *reinterpret_cast<T*>(y->d_children[0]);
+    }
+  }
+
+  Assert(x->d_nchildren == 0);
+  Assert(y->d_nchildren == 0);
+  return x->getConst<T>() == y->getConst<T>();
+}
+
+template <Kind k, bool pool>
+inline size_t NodeValueConstCompare<k, pool>::constHash(const ::CVC4::expr::NodeValue* nv) {
+  typedef typename ConstantMapReverse<k>::T T;
+  return nv->getConst<T>().hash();
+}
+
+${metakind_constantMaps}
+
+template <bool pool>
+inline bool NodeValueCompare::compare(const ::CVC4::expr::NodeValue* nv1,
+                                      const ::CVC4::expr::NodeValue* nv2) {
+  if(nv1->d_kind != nv2->d_kind) {
+    return false;
+  }
+
+  if(nv1->getMetaKind() == kind::metakind::CONSTANT) {
+    switch(nv1->d_kind) {
+${metakind_compares}
+    default:
+      Unhandled(::CVC4::expr::NodeValue::dKindToKind(nv1->d_kind));
+    }
+  }
+
+  if(nv1->d_nchildren != nv2->d_nchildren) {
+    return false;
+  }
+
+  ::CVC4::expr::NodeValue::const_nv_iterator i = nv1->nv_begin();
+  ::CVC4::expr::NodeValue::const_nv_iterator j = nv2->nv_begin();
+  ::CVC4::expr::NodeValue::const_nv_iterator i_end = nv1->nv_end();
+
+  while(i != i_end) {
+    if((*i) != (*j)) {
+      return false;
+    }
+    ++i;
+    ++j;
+  }
+
+  return true;
+}
+
+inline size_t NodeValueCompare::constHash(const ::CVC4::expr::NodeValue* nv) {
+  Assert(nv->getMetaKind() == kind::metakind::CONSTANT);
+
+  switch(nv->d_kind) {
+${metakind_constHashes}
+  default:
+    Unhandled(::CVC4::expr::NodeValue::dKindToKind(nv->d_kind));
+  }
+}
+
+inline void NodeValueConstPrinter::toStream(std::ostream& out,
+                                            const ::CVC4::expr::NodeValue* nv) {
+  Assert(nv->getMetaKind() == kind::metakind::CONSTANT);
+
+  switch(nv->d_kind) {
+${metakind_constPrinters}
+  default:
+    Unhandled(::CVC4::expr::NodeValue::dKindToKind(nv->d_kind));
+  }
+}
+
+inline unsigned getLowerBoundForKind(::CVC4::Kind k) {
+  static const unsigned lbs[] = {
+    0, /* NULL_EXPR */
+${metakind_lbchildren}
+
+    0 /* LAST_KIND */
+  };
+
+  return lbs[k];
+}
+
+inline unsigned getUpperBoundForKind(::CVC4::Kind k) {
+  static const unsigned ubs[] = {
+    0, /* NULL_EXPR */
+${metakind_ubchildren}
+
+    0, /* LAST_KIND */
+  };
+
+  return ubs[k];
+}
+
+}/* CVC4::kind::metakind namespace */
+}/* CVC4::kind namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP */