* src/context/cdmap.h: rename orderedIterator to iterator, do away

  with old iterator (closes bug #47).

* src/context/cdset.h: implemented.

* src/expr/node_builder.h: fixed all the strict-aliasing warnings.

* Remove Node::hash() and Expr::hash() (they had been aliases for
  getId()).  There's now a NodeValue::internalHash(), for internal
  expr package purposes only, that doesn't depend on the ID.  That's
  the only hashing of Nodes or Exprs.

* Automake-quiet generation of kind.h, theoryof_table.h, and CVC and
  SMT parsers.

* various minor code cleanups.

9 files changed, 100 insertions, 91 deletions

diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index 3deed9a52..6d041814f 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -34,7 +34,7 @@ EXTRA_DIST = \
 
 @srcdir@/kind.h: mkkind kind_prologue.h kind_middle.h kind_epilogue.h builtin_kinds @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds
 	chmod +x @srcdir@/mkkind
-	(@srcdir@/mkkind \
+	$(AM_V_GEN)(@srcdir@/mkkind \
 		@srcdir@/kind_prologue.h \
 		@srcdir@/kind_middle.h \
 		@srcdir@/kind_epilogue.h \
diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp
index b6348394c..2f84f018b 100644
--- a/src/expr/expr.cpp
+++ b/src/expr/expr.cpp
@@ -81,11 +81,6 @@ bool Expr::operator<(const Expr& e) const {
   return *d_node < *e.d_node;
 }
 
-size_t Expr::hash() const {
-  Assert(d_node != NULL, "Unexpected NULL expression pointer!");
-  return (d_node->hash());
-}
-
 Kind Expr::getKind() const {
   Assert(d_node != NULL, "Unexpected NULL expression pointer!");
   return d_node->getKind();
diff --git a/src/expr/expr.h b/src/expr/expr.h
index 6c615d391..b297be6fb 100644
--- a/src/expr/expr.h
+++ b/src/expr/expr.h
@@ -92,12 +92,6 @@ public:
   operator bool() const;
 
   /**
-   * Returns the hash value of the expression. Equal expression will have the
-   * same hash value.
-   */
-  size_t hash() const;
-
-  /**
    * Returns the kind of the expression (AND, PLUS ...).
    * @return the kind of the expression
    */
diff --git a/src/expr/node.h b/src/expr/node.h
index c1df399a1..d1bb8f3b3 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -219,14 +219,6 @@ public:
   bool isAtomic() const;
 
   /**
-   * Returns the hash value of this node.
-   * @return the hash value
-   */
-  size_t hash() const {
-    return d_nv->getId();
-  }
-
-  /**
    * Returns the unique id of this node
    * @return the ud
    */
@@ -420,7 +412,7 @@ namespace CVC4 {
 // for hash_maps, hash_sets..
 struct NodeHashFcn {
   size_t operator()(const CVC4::Node& node) const {
-    return (size_t) node.hash();
+    return (size_t) node.getId();
   }
 };
 
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index a92c3a872..76307a525 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -421,9 +421,9 @@ protected:
 
 protected:
 
-  inline NodeBuilderBase(char* buf, unsigned maxChildren,
+  inline NodeBuilderBase(expr::NodeValue* buf, unsigned maxChildren,
                          Kind k = kind::UNDEFINED_KIND);
-  inline NodeBuilderBase(char* buf, unsigned maxChildren,
+  inline NodeBuilderBase(expr::NodeValue* buf, unsigned maxChildren,
                          NodeManager* nm, Kind k = kind::UNDEFINED_KIND);
 
 private:
@@ -575,24 +575,24 @@ public:
  */
 class BackedNodeBuilder : public NodeBuilderBase<BackedNodeBuilder> {
 public:
-  inline BackedNodeBuilder(char* buf, unsigned maxChildren) :
+  inline BackedNodeBuilder(expr::NodeValue* buf, unsigned maxChildren) :
     NodeBuilderBase<BackedNodeBuilder>(buf, maxChildren) {
   }
 
-  inline BackedNodeBuilder(char* buf, unsigned maxChildren, Kind k) :
+  inline BackedNodeBuilder(expr::NodeValue* buf, unsigned maxChildren, Kind k) :
     NodeBuilderBase<BackedNodeBuilder>(buf, maxChildren) {
   }
 
-  inline BackedNodeBuilder(char* buf, unsigned maxChildren, NodeManager* nm) :
+  inline BackedNodeBuilder(expr::NodeValue* buf, unsigned maxChildren, NodeManager* nm) :
     NodeBuilderBase<BackedNodeBuilder>(buf, maxChildren) {
   }
 
-  inline BackedNodeBuilder(char* buf, unsigned maxChildren, NodeManager* nm, Kind k) :
+  inline BackedNodeBuilder(expr::NodeValue* buf, unsigned maxChildren, NodeManager* nm, Kind k) :
     NodeBuilderBase<BackedNodeBuilder>(buf, maxChildren) {
   }
 
   // we don't want a vtable, so do not declare a dtor!
-  //inline ~NodeBuilder();
+  //inline ~BackedNodeBuilder();
 
 private:
   // disallow copy or assignment (there would be no backing store!)
@@ -610,13 +610,15 @@ private:
  * declarations are permitted.
  */
 #define makeStackNodeBuilder(__v, __n)                                  \
-  size_t __cvc4_backednodebuilder_nchildren__ ## __v = (__n);           \
-  char __cvc4_backednodebuilder_buf__ ## __v                            \
-  [ sizeof(NodeValue) +                                                 \
-    sizeof(NodeValue*) * __cvc4_backednodebuilder_nchildren__ ## __v ]  \
-    __attribute__((aligned(__WORDSIZE / 8)));                           \
-  BackedNodeBuilder __v(__cvc4_backednodebuilder_buf__ ## __v,          \
-                        __cvc4_backednodebuilder_nchildren__ ## __v)
+  const size_t __cvc4_backednodebuilder_nchildren__ ## __v = (__n);     \
+  ::CVC4::expr::NodeValue __cvc4_backednodebuilder_buf__ ## __v[1 + (((sizeof(::CVC4::expr::NodeValue) + sizeof(::CVC4::expr::NodeValue*) + 1) / sizeof(::CVC4::expr::NodeValue*)) * __cvc4_backednodebuilder_nchildren__ ## __v)]; \
+  ::CVC4::BackedNodeBuilder __v(__cvc4_backednodebuilder_buf__ ## __v, \
+                                __cvc4_backednodebuilder_nchildren__ ## __v)
+// IF THE ABOVE ASSERTION FAILS, write another compiler-specific
+// version of makeStackNodeBuilder() that works for your compiler
+// (even if it's suboptimal, ignoring its __n argument, and just
+// creates a NodeBuilder<10>).
+
 
 /**
  * Simple NodeBuilder interface.  This is a template that requires
@@ -626,9 +628,18 @@ private:
  */
 template <unsigned nchild_thresh = default_nchild_thresh>
 class NodeBuilder : public NodeBuilderBase<NodeBuilder<nchild_thresh> > {
-  char d_backingStore[ sizeof(expr::NodeValue)
-                       + (sizeof(expr::NodeValue*) * nchild_thresh) ]
-    __attribute__((aligned(__WORDSIZE / 8)));
+  // This is messy:
+  // 1. This (anonymous) struct here must be a POD to avoid the
+  //    compiler laying out things in a different way.
+  // 2. The layout is engineered carefully.  We can't just
+  //    stack-allocate enough bytes as a char[] because we break
+  //    strict-aliasing rules.  The first thing in the struct is a
+  //    "NodeValue" so a pointer to this struct should be safely
+  //    castable to a pointer to a NodeValue (same alignment).
+  struct BackingStore {
+    expr::NodeValue n;
+    expr::NodeValue* c[nchild_thresh];
+  } d_backingStore;
 
   typedef NodeBuilderBase<NodeBuilder<nchild_thresh> > super;
 
@@ -637,19 +648,31 @@ class NodeBuilder : public NodeBuilderBase<NodeBuilder<nchild_thresh> > {
 
 public:
   inline NodeBuilder() :
-    NodeBuilderBase<NodeBuilder<nchild_thresh> >(d_backingStore, nchild_thresh) {
+    NodeBuilderBase<NodeBuilder<nchild_thresh> >
+      (reinterpret_cast<expr::NodeValue*>(&d_backingStore),
+       nchild_thresh) {
   }
 
   inline NodeBuilder(Kind k) :
-    NodeBuilderBase<NodeBuilder<nchild_thresh> >(d_backingStore, nchild_thresh, k) {
+    NodeBuilderBase<NodeBuilder<nchild_thresh> >
+      (reinterpret_cast<expr::NodeValue*>(&d_backingStore),
+       nchild_thresh,
+       k) {
   }
 
   inline NodeBuilder(NodeManager* nm) :
-    NodeBuilderBase<NodeBuilder<nchild_thresh> >(d_backingStore, nchild_thresh, nm) {
+    NodeBuilderBase<NodeBuilder<nchild_thresh> >
+      (reinterpret_cast<expr::NodeValue*>(&d_backingStore),
+       nchild_thresh,
+       nm) {
   }
 
   inline NodeBuilder(NodeManager* nm, Kind k) :
-    NodeBuilderBase<NodeBuilder<nchild_thresh> >(d_backingStore, nchild_thresh, nm, k) {
+    NodeBuilderBase<NodeBuilder<nchild_thresh> >
+      (reinterpret_cast<expr::NodeValue*>(&d_backingStore),
+       nchild_thresh,
+       nm,
+       k) {
   }
 
   // These implementations are identical, but we need to have both of
@@ -657,20 +680,22 @@ public:
   // generalization of a copy constructor (and a default copy
   // constructor will be generated [?])
   inline NodeBuilder(const NodeBuilder& nb) :
-    NodeBuilderBase<NodeBuilder<nchild_thresh> >(d_backingStore,
-                                                 nchild_thresh,
-                                                 nb.d_nm,
-                                                 nb.getKind()) {
+    NodeBuilderBase<NodeBuilder<nchild_thresh> >
+      (reinterpret_cast<expr::NodeValue*>(&d_backingStore),
+       nchild_thresh,
+       nb.d_nm,
+       nb.getKind()) {
     internalCopy(nb);
   }
 
   // technically this is a conversion, not a copy
   template <unsigned N>
   inline NodeBuilder(const NodeBuilder<N>& nb) :
-    NodeBuilderBase<NodeBuilder<nchild_thresh> >(d_backingStore,
-                                                 nchild_thresh,
-                                                 nb.d_nm,
-                                                 nb.getKind()) {
+    NodeBuilderBase<NodeBuilder<nchild_thresh> >
+      (reinterpret_cast<expr::NodeValue*>(&d_backingStore),
+       nchild_thresh,
+       nb.d_nm,
+       nb.getKind()) {
     internalCopy(nb);
   }
 
@@ -1019,8 +1044,8 @@ inline NodeTemplate<true> operator-(const NodeTemplate<rc>& a) {
 namespace CVC4 {
 
 template <class Builder>
-inline NodeBuilderBase<Builder>::NodeBuilderBase(char* buf, unsigned maxChildren, Kind k) :
-  d_inlineNv(*reinterpret_cast<expr::NodeValue*>(buf)),
+inline NodeBuilderBase<Builder>::NodeBuilderBase(expr::NodeValue* buf, unsigned maxChildren, Kind k) :
+  d_inlineNv(*buf),
   d_nv(&d_inlineNv),
   d_nm(NodeManager::currentNM()),
   d_inlineNvMaxChildren(maxChildren),
@@ -1033,8 +1058,8 @@ inline NodeBuilderBase<Builder>::NodeBuilderBase(char* buf, unsigned maxChildren
 }
 
 template <class Builder>
-inline NodeBuilderBase<Builder>::NodeBuilderBase(char* buf, unsigned maxChildren, NodeManager* nm, Kind k) :
-  d_inlineNv(*reinterpret_cast<expr::NodeValue*>(buf)),
+inline NodeBuilderBase<Builder>::NodeBuilderBase(expr::NodeValue* buf, unsigned maxChildren, NodeManager* nm, Kind k) :
+  d_inlineNv(*buf),
   d_nv(&d_inlineNv),
   d_nm(nm),
   d_inlineNvMaxChildren(maxChildren),
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 98171cb2e..7be593575 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -52,24 +52,6 @@ struct Reclaim {
   }
 };
 
-/**
- * Reclaim a particular zombie.
- */
-void NodeManager::reclaimZombie(expr::NodeValue* nv) {
-  Debug("gc") << "deleting node value " << nv
-              << " [" << nv->d_id << "]: " << nv->toString() << "\n";
-
-  if(nv->getKind() != kind::VARIABLE) {
-    poolRemove(nv);
-  }
-
-  d_attrManager.deleteAllAttributes(nv);
-
-  // dtor decr's ref counts of children
-  // FIXME: NOT  ACTUALLY GARBAGE COLLECTING  YET (DUE TO  ISSUES WITH
-  // CDMAPs (?) ) delete nv;
-}
-
 void NodeManager::reclaimZombies() {
   // FIXME multithreading
 
@@ -102,9 +84,25 @@ void NodeManager::reclaimZombies() {
   for(vector<NodeValue*>::iterator i = zombies.begin();
       i != zombies.end();
       ++i) {
+    NodeValue* nv = *i;
+
     // collect ONLY IF still zero
     if((*i)->d_rc == 0) {
-      reclaimZombie(*i);
+      Debug("gc") << "deleting node value " << nv
+                  << " [" << nv->d_id << "]: " << nv->toString() << "\n";
+
+      // remove from the pool
+      if(nv->getKind() != kind::VARIABLE) {
+        poolRemove(nv);
+      }
+
+      // remove attributes
+      d_attrManager.deleteAllAttributes(nv);
+
+      // decr ref counts of children
+      nv->decrRefCounts();
+      //free(nv);
+#warning NOT FREEING NODEVALUES
     }
   }
 }
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 32c1cd210..b40ec2978 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -100,11 +100,6 @@ class NodeManager {
    */
   void reclaimZombies();
 
-  /**
-   * Reclaim a particular zombie.
-   */
-  void reclaimZombie(expr::NodeValue* nv);
-
 public:
 
   NodeManager(context::Context* ctxt) :
diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp
index 5dbfac169..7a4263d8a 100644
--- a/src/expr/node_value.cpp
+++ b/src/expr/node_value.cpp
@@ -28,7 +28,7 @@ namespace expr {
 
 size_t NodeValue::next_id = 1;
 
-NodeValue NodeValue::s_null;
+NodeValue NodeValue::s_null(0);
 
 string NodeValue::toString() const {
   stringstream ss;
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index a5f68babf..cbe4e718a 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -75,17 +75,13 @@ class NodeValue {
   unsigned d_nchildren : 16;
 
   /** Variable number of child nodes */
-  NodeValue *d_children[0];
+  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 N> friend class CVC4::NodeBuilder;
-  friend class CVC4::AndNodeBuilder;
-  friend class CVC4::OrNodeBuilder;
-  friend class CVC4::PlusNodeBuilder;
-  friend class CVC4::MultNodeBuilder;
+  template <unsigned nchild_thresh> friend class CVC4::NodeBuilder;
   friend class CVC4::NodeManager;
 
   void inc();
@@ -93,11 +89,17 @@ class NodeValue {
 
   static size_t next_id;
 
-  /** Private default constructor for the null value. */
-  NodeValue();
+public:
+  /**
+   * Uninitializing constructor for NodeBuilder's use.  This is
+   * somewhat dangerous, but must also be public for the
+   * makeStackNodeBuilder() macro to work.
+   */
+  NodeValue() { /* do not initialize! */ }
 
-  /** Destructor decrements the ref counts of its children */
-  ~NodeValue();
+private:
+  /** Private constructor for the null value. */
+  NodeValue(int);
 
   typedef NodeValue** nv_iterator;
   typedef NodeValue const* const* const_nv_iterator;
@@ -136,6 +138,9 @@ class NodeValue {
     typedef std::input_iterator_tag iterator_category;
   };
 
+  /** Decrement ref counts of children */
+  inline void decrRefCounts();
+
 public:
 
   template <bool ref_count>
@@ -211,6 +216,11 @@ public:
   static inline Kind dKindToKind(unsigned d) {
     return (d == kindMask) ? kind::UNDEFINED_KIND : Kind(d);
   }
+
+  static inline const NodeValue& null() {
+    return s_null;
+  }
+
 };/* class NodeValue */
 
 /**
@@ -242,14 +252,14 @@ struct NodeValueIDHashFcn {
 namespace CVC4 {
 namespace expr {
 
-inline NodeValue::NodeValue() :
+inline NodeValue::NodeValue(int) :
   d_id(0),
   d_rc(MAX_RC),
   d_kind(kind::NULL_EXPR),
   d_nchildren(0) {
 }
 
-inline NodeValue::~NodeValue() {
+inline void NodeValue::decrRefCounts() {
   for(nv_iterator i = nv_begin(); i != nv_end(); ++i) {
     (*i)->dec();
   }