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

22 files changed, 385 insertions, 273 deletions

diff --git a/configure.ac b/configure.ac
index 3da3671a9..8cabfe98b 100644
--- a/configure.ac
+++ b/configure.ac
@@ -164,33 +164,41 @@ case "$with_build" in
     CVC4CPPFLAGS=
     CVC4CXXFLAGS=-O3
     CVC4LDFLAGS=
-    if test -z "${enable_assertions+set}"; then enable_assertions=no             ; fi
-    if test -z "${enable_tracing+set}"   ; then enable_tracing=no                ; fi
-    if test -z "${enable_muzzle+set}"    ; then enable_muzzle=no                 ; fi
+    if test -z "${enable_optimized+set}"    ; then enable_optimized=yes             ; fi
+    if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes         ; fi
+    if test -z "${enable_assertions+set}"   ; then enable_assertions=no             ; fi
+    if test -z "${enable_tracing+set}"      ; then enable_tracing=no                ; fi
+    if test -z "${enable_muzzle+set}"       ; then enable_muzzle=no                 ; fi
     ;;
   debug) # unoptimized, debug symbols, assertions, tracing
     CVC4CPPFLAGS=-DCVC4_DEBUG
     CVC4CXXFLAGS='-O0 -fno-inline -ggdb3'
     CVC4LDFLAGS=
-    if test -z "${enable_assertions+set}"; then enable_assertions=yes            ; fi
-    if test -z "${enable_tracing+set}"   ; then enable_tracing=yes               ; fi
-    if test -z "${enable_muzzle+set}"    ; then enable_muzzle=no                 ; fi
+    if test -z "${enable_optimized+set}"    ; then enable_optimized=no              ; fi
+    if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes         ; fi
+    if test -z "${enable_assertions+set}"   ; then enable_assertions=yes            ; fi
+    if test -z "${enable_tracing+set}"      ; then enable_tracing=yes               ; fi
+    if test -z "${enable_muzzle+set}"       ; then enable_muzzle=no                 ; fi
     ;;
   default) # moderately optimized, assertions, tracing
     CVC4CPPFLAGS=
     CVC4CXXFLAGS=-O2
     CVC4LDFLAGS=
-    if test -z "${enable_assertions+set}"; then enable_assertions=yes            ; fi
-    if test -z "${enable_tracing+set}"   ; then enable_tracing=yes               ; fi
-    if test -z "${enable_muzzle+set}"    ; then enable_muzzle=no                 ; fi
+    if test -z "${enable_optimized+set}"    ; then enable_optimized=no              ; fi
+    if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes         ; fi
+    if test -z "${enable_assertions+set}"   ; then enable_assertions=yes            ; fi
+    if test -z "${enable_tracing+set}"      ; then enable_tracing=yes               ; fi
+    if test -z "${enable_muzzle+set}"       ; then enable_muzzle=no                 ; fi
     ;;
   competition) # maximally optimized, no assertions, no tracing, muzzled
     CVC4CPPFLAGS=
     CVC4CXXFLAGS='-O9 -funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs'
     CVC4LDFLAGS=
-    if test -z "${enable_assertions+set}"; then enable_assertions=no             ; fi
-    if test -z "${enable_tracing+set}"   ; then enable_tracing=no                ; fi
-    if test -z "${enable_muzzle+set}"    ; then enable_muzzle=yes                ; fi
+    if test -z "${enable_optimized+set}"    ; then enable_optimized=no              ; fi
+    if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=no          ; fi
+    if test -z "${enable_assertions+set}"   ; then enable_assertions=no             ; fi
+    if test -z "${enable_tracing+set}"      ; then enable_tracing=no                ; fi
+    if test -z "${enable_muzzle+set}"       ; then enable_muzzle=yes                ; fi
     ;;
   *)
     AC_MSG_FAILURE([unknown build profile: $with_build])
diff --git a/src/context/cdlist.h b/src/context/cdlist.h
index 5b4ba639a..fd50d4149 100644
--- a/src/context/cdlist.h
+++ b/src/context/cdlist.h
@@ -56,6 +56,8 @@ class CDList : public ContextObj {
    */
   unsigned d_sizeAlloc;
 
+protected:
+
   /**
    * Implementation of mandatory ContextObj method save: simply copies the
    * current size to a copy using the copy constructor (the pointer and the
@@ -83,8 +85,10 @@ class CDList : public ContextObj {
     }
   }
 
+private:
+
   /**
-   * Privae copy constructor used only by save above.  d_list and d_sizeAlloc
+   * Private copy constructor used only by save above.  d_list and d_sizeAlloc
    * are not copied: only the base class information and d_size are needed in
    * restore.
    */
@@ -122,14 +126,18 @@ public:
   /**
    * Main constructor: d_list starts as NULL, size is 0
    */
- CDList(Context* context, bool callDestructor = true)
-   : ContextObj(context), d_list(NULL), d_callDestructor(callDestructor),
-    d_size(0), d_sizeAlloc(0) { }
+ CDList(Context* context, bool callDestructor = true) :
+   ContextObj(context),
+   d_list(NULL),
+   d_callDestructor(callDestructor),
+   d_size(0),
+   d_sizeAlloc(0) {
+ }
 
   /**
    * Destructor: delete the list
    */
-  ~CDList() throw() {
+  ~CDList() throw(AssertionException) {
     if(d_list != NULL) {
       if(d_callDestructor) {
         while(d_size != 0) {
@@ -144,26 +152,33 @@ public:
   /**
    * Return the current size of (i.e. valid number of objects in) the list
    */
-  unsigned size() const { return d_size; }
-
+  unsigned size() const {
+    return d_size;
+  }
 
   /**
    * Return true iff there are no valid objects in the list.
    */
-  bool empty() const { return d_size == 0; }
+  bool empty() const {
+    return d_size == 0;
+  }
 
   /**
    * Add an item to the end of the list.
    */
   void push_back(const T& data) {
     makeCurrent();
-    if(d_size == d_sizeAlloc) grow();
+
+    if(d_size == d_sizeAlloc) {
+      grow();
+    }
+
     ::new((void*)(d_list + d_size)) T(data);
-    ++ d_size;
+    ++d_size;
   }
 
   /**
-   * operator[]: return the ith item in the list
+   * Access to the ith item in the list.
    */
   const T& operator[](unsigned i) const {
     Assert(i < d_size, "index out of bounds in CDList::operator[]");
@@ -171,11 +186,11 @@ public:
   }
 
   /**
-   * return the most recent item added to the list
+   * Returns the most recent item added to the list.
    */
   const T& back() const {
     Assert(d_size > 0, "CDList::back() called on empty list");
-    return d_list[d_size-1];
+    return d_list[d_size - 1];
   }
 
   /**
@@ -186,19 +201,66 @@ public:
    * uninitialized list, as begin() and end() will have the same value (NULL).
    */
   class const_iterator {
-    friend class CDList<T>;
     T* d_it;
-    const_iterator(T* it) : d_it(it) {};
+
+    const_iterator(T* it) : d_it(it) {}
+
+    friend class CDList<T>;
+
   public:
+
     const_iterator() : d_it(NULL) {}
-    bool operator==(const const_iterator& i) const { return d_it == i.d_it; }
-    bool operator!=(const const_iterator& i) const { return d_it != i.d_it; }
-    const T& operator*() const { return *d_it; }
+
+    inline bool operator==(const const_iterator& i) const {
+      return d_it == i.d_it;
+    }
+
+    inline bool operator!=(const const_iterator& i) const {
+      return d_it != i.d_it;
+    }
+
+    inline const T& operator*() const {
+      return *d_it;
+    }
+
     /** Prefix increment */
-    const_iterator& operator++() { ++d_it; return *this; }
+    const_iterator& operator++() {
+      ++d_it;
+      return *this;
+    }
+
     /** Prefix decrement */
     const_iterator& operator--() { --d_it; return *this; }
-  }; /* class const_iterator */
+
+    // Postfix operations on iterators: requires a Proxy object to
+    // hold the intermediate value for dereferencing
+    class Proxy {
+      const T* d_t;
+
+    public:
+
+      Proxy(const T& p): d_t(&p) {}
+
+      T& operator*() {
+        return *d_t;
+      }
+    };/* class CDList<>::const_iterator::Proxy */
+
+    /** Postfix increment: returns Proxy with the old value. */
+    Proxy operator++(int) {
+      Proxy e(*(*this));
+      ++(*this);
+      return e;
+    }
+
+    /** Postfix decrement: returns Proxy with the old value. */
+    Proxy operator--(int) {
+      Proxy e(*(*this));
+      --(*this);
+      return e;
+    }
+
+  };/* class CDList<>::const_iterator */
 
   /**
    * Returns an iterator pointing to the first item in the list.
diff --git a/src/context/cdmap.h b/src/context/cdmap.h
index dc3448e52..b1bb47c4c 100644
--- a/src/context/cdmap.h
+++ b/src/context/cdmap.h
@@ -163,7 +163,8 @@ class CDMap : public ContextObj {
 
   friend class CDOmap<Key, Data, HashFcn>;
 
-  __gnu_cxx::hash_map<Key, CDOmap<Key, Data, HashFcn>*, HashFcn> d_map;
+  typedef __gnu_cxx::hash_map<Key, CDOmap<Key, Data, HashFcn>*, HashFcn> table_type;
+  table_type d_map;
 
   // The vector of CDOmap objects to be destroyed
   std::vector<CDOmap<Key, Data, HashFcn>*> d_trash;
@@ -200,7 +201,7 @@ public:
 
   ~CDMap() throw(AssertionException) {
     // Delete all the elements and clear the map
-    for(typename __gnu_cxx::hash_map<Key, CDOmap<Key, Data, HashFcn>*, HashFcn>::iterator
+    for(typename table_type::iterator
 	  i = d_map.begin(), iend = d_map.end(); i != iend; ++i) {
       /*
         delete (*i).second;
@@ -227,11 +228,10 @@ public:
   CDOmap<Key, Data, HashFcn>& operator[](const Key& k) {
     emptyTrash();
 
-    typename __gnu_cxx::hash_map<Key, CDOmap<Key, Data, HashFcn>*, HashFcn>::iterator
-      i(d_map.find(k));
+    typename table_type::iterator i = d_map.find(k);
 
     CDOmap<Key, Data, HashFcn>* obj;
-    if(i == d_map.end()) { // Create new object
+    if(i == d_map.end()) {// create new object
       obj = new(true) CDOmap<Key, Data, HashFcn>(d_context, this, k, Data());
       d_map[k] = obj;
     } else {
@@ -243,8 +243,7 @@ public:
   void insert(const Key& k, const Data& d) {
     emptyTrash();
 
-    typename __gnu_cxx::hash_map<Key, CDOmap<Key, Data, HashFcn>*, HashFcn>::iterator
-      i = d_map.find(k);
+    typename table_type::iterator i = d_map.find(k);
 
     if(i == d_map.end()) {// create new object
       CDOmap<Key, Data, HashFcn>*
@@ -257,19 +256,12 @@ public:
 
   // FIXME: no erase(), too much hassle to implement efficiently...
 
-  // Iterator for CDMap: points to pair<const Key, CDOMap<Key, Data, HashFcn>&>;
-  // in most cases, this will be functionally similar to pair<const Key, Data>.
-  class iterator : public std::iterator<std::input_iterator_tag, std::pair<const Key, Data>, std::ptrdiff_t> {
-
-    // Private members
-    typename __gnu_cxx::hash_map<Key, CDOmap<Key, Data, HashFcn>*, HashFcn>::const_iterator d_it;
+  class iterator {
+    const CDOmap<Key, Data, HashFcn>* d_it;
 
   public:
 
-    // Constructor from __gnu_cxx::hash_map
-    iterator(const typename __gnu_cxx::hash_map<Key, CDOmap<Key, Data, HashFcn>*, HashFcn>::const_iterator& i) : d_it(i) {}
-
-    // Copy constructor
+    iterator(const CDOmap<Key, Data, HashFcn>* p) : d_it(p) {}
     iterator(const iterator& i) : d_it(i.d_it) {}
 
     // Default constructor
@@ -285,80 +277,11 @@ public:
 
     // Dereference operators.
     std::pair<const Key, Data> operator*() const {
-      const std::pair<const Key, CDOmap<Key, Data, HashFcn>*>& p(*d_it);
-      return std::pair<const Key, Data>(p.first, *p.second);
-    }
-
-    // Who needs an operator->() for maps anyway?...
-    // It'd be nice, but not possible by design.
-    //std::pair<const Key, Data>* operator->() const {
-    //  return &(operator*());
-    //}
-
-    // Prefix and postfix increment
-    iterator& operator++() {
-      ++d_it;
-      return *this;
-    }
-
-    // Postfix increment: requires a Proxy object to hold the
-    // intermediate value for dereferencing
-    class Proxy {
-      const std::pair<const Key, Data>* d_pair;
-    public:
-      Proxy(const std::pair<const Key, Data>& p): d_pair(&p) {}
-      std::pair<const Key, Data>& operator*() {
-        return *d_pair;
-      }
-    };/* class CDMap<>::iterator::Proxy */
-
-    // Actual postfix increment: returns Proxy with the old value.
-    // Now, an expression like *i++ will return the current *i, and
-    // then advance the iterator.  However, don't try to use Proxy for
-    // anything else.
-    Proxy operator++(int) {
-      Proxy e(*(*this));
-      ++(*this);
-      return e;
-    }
-  };/* class CDMap<>::iterator */
-
-  typedef iterator const_iterator;
-
-  iterator begin() const {
-    return iterator(d_map.begin());
-  }
-
-  iterator end() const {
-    return iterator(d_map.end());
-  }
-
-  class orderedIterator {
-    const CDOmap<Key, Data, HashFcn>* d_it;
-
-  public:
-
-    orderedIterator(const CDOmap<Key, Data, HashFcn>* p) : d_it(p) {}
-    orderedIterator(const orderedIterator& i) : d_it(i.d_it) {}
-
-    // Default constructor
-    orderedIterator() {}
-
-    // (Dis)equality
-    bool operator==(const orderedIterator& i) const {
-      return d_it == i.d_it;
-    }
-    bool operator!=(const orderedIterator& i) const {
-      return d_it != i.d_it;
-    }
-
-    // Dereference operators.
-    std::pair<const Key, Data> operator*() const {
       return std::pair<const Key, Data>(d_it->getKey(), d_it->get());
     }
 
-    // Prefix and postfix increment
-    orderedIterator& operator++() {
+    // Prefix increment
+    iterator& operator++() {
       d_it = d_it->next();
       return *this;
     }
@@ -370,34 +293,41 @@ public:
 
     public:
 
-      Proxy(const std::pair<const Key, Data>& p): d_pair(&p) {}
+      Proxy(const std::pair<const Key, Data>& p) : d_pair(&p) {}
 
-      std::pair<const Key, Data>& operator*() {
+      const std::pair<const Key, Data>& operator*() const {
         return *d_pair;
       }
-    };/* class CDMap<>::orderedIterator::Proxy */
+    };/* class CDMap<>::iterator::Proxy */
 
     // Actual postfix increment: returns Proxy with the old value.
     // Now, an expression like *i++ will return the current *i, and
     // then advance the orderedIterator.  However, don't try to use
     // Proxy for anything else.
-    Proxy operator++(int) {
+    const Proxy operator++(int) {
       Proxy e(*(*this));
       ++(*this);
       return e;
     }
-  };/* class CDMap<>::orderedIterator */
+  };/* class CDMap<>::iterator */
+
+  typedef iterator const_iterator;
 
-  orderedIterator orderedBegin() const {
-    return orderedIterator(d_first);
+  iterator begin() const {
+    return iterator(d_first);
   }
 
-  orderedIterator orderedEnd() const {
-    return orderedIterator(NULL);
+  iterator end() const {
+    return iterator(NULL);
   }
 
   iterator find(const Key& k) const {
-    return iterator(d_map.find(k));
+    typename table_type::const_iterator i = d_map.find(k);
+    if(i == d_map.end()) {
+      return end();
+    } else {
+      return iterator((*i).second);
+    }
   }
 
 };/* class CDMap<> */
diff --git a/src/context/cdo.h b/src/context/cdo.h
index 6c30a70f4..aca48d264 100644
--- a/src/context/cdo.h
+++ b/src/context/cdo.h
@@ -63,7 +63,7 @@ class CDO : public ContextObj {
   /**
    * operator= for CDO is private to ensure CDO object is not copied.
    */
-  CDO<T>& operator=(const CDO<T>& cdo) {}
+  CDO<T>& operator=(const CDO<T>& cdo);
 
 public:
   /**
diff --git a/src/context/cdset.h b/src/context/cdset.h
index 48ad12daa..f51e689d5 100644
--- a/src/context/cdset.h
+++ b/src/context/cdset.h
@@ -24,8 +24,100 @@
 namespace CVC4 {
 namespace context {
 
-template <class K, class HashFcn>
-class CDSet;
+template <class V, class HashFcn>
+class CDSet : protected CDMap<V, V, HashFcn> {
+  typedef CDMap<V, V, HashFcn> super;
+
+public:
+
+  CDSet(Context* context) :
+    super(context) {
+  }
+
+  size_t size() const {
+    return super::size();
+  }
+
+  size_t count(const V& v) const {
+    return super::count(v);
+  }
+
+  void insert(const V& v) {
+    super::insert(v, v);
+  }
+
+  // FIXME: no erase(), too much hassle to implement efficiently...
+
+  class iterator {
+    typename super::iterator d_it;
+
+  public:
+
+    iterator(const typename super::iterator& it) : d_it(it) {}
+    iterator(const iterator& it) : d_it(it.d_it) {}
+
+    // Default constructor
+    iterator() {}
+
+    // (Dis)equality
+    bool operator==(const iterator& i) const {
+      return d_it == i.d_it;
+    }
+    bool operator!=(const iterator& i) const {
+      return d_it != i.d_it;
+    }
+
+    // Dereference operators.
+    V operator*() const {
+      return (*d_it).first;
+    }
+
+    // Prefix increment
+    iterator& operator++() {
+      ++d_it;
+      return *this;
+    }
+
+    // Postfix increment: requires a Proxy object to hold the
+    // intermediate value for dereferencing
+    class Proxy {
+      const V& d_val;
+
+    public:
+
+      Proxy(const V& v) : d_val(v) {}
+
+      V operator*() const {
+        return d_val;
+      }
+    };/* class CDSet<>::iterator::Proxy */
+
+    // Actual postfix increment: returns Proxy with the old value.
+    // Now, an expression like *i++ will return the current *i, and
+    // then advance the orderedIterator.  However, don't try to use
+    // Proxy for anything else.
+    const Proxy operator++(int) {
+      Proxy e(*(*this));
+      ++(*this);
+      return e;
+    }
+  };/* class CDSet<>::iterator */
+
+  typedef iterator const_iterator;
+
+  const_iterator begin() const {
+    return iterator(super::begin());
+  }
+
+  const_iterator end() const {
+    return iterator(super::end());
+  }
+
+  const_iterator find(const V& v) const {
+    return iterator(super::find(v));
+  }
+
+};/* class CDSet */
 
 }/* CVC4::context namespace */
 }/* CVC4 namespace */
diff --git a/src/context/context.h b/src/context/context.h
index 4e10347d7..69e8fe776 100644
--- a/src/context/context.h
+++ b/src/context/context.h
@@ -134,23 +134,23 @@ public:
    */
   void addNotifyObjPost(ContextNotifyObj* pCNO);
 
-}; /* class Context */
-
-  /**
-   * Conceptually, a Scope encapsulates that portion of the context that
-   * changes after a call to push() and must be undone on a subsequent call to
-   * pop().  In particular, each call to push() creates a new Scope object .
-   * This new Scope object becomes the top scope and it points (via the
-   * d_pScopePrev member) to the previous top Scope.  Each call to pop()
-   * deletes the current top scope and restores the previous one.  The main
-   * purpose of a Scope is to maintain a linked list of ContexObj objects which
-   * change while the Scope is the top scope and which must be restored when
-   * the Scope is deleted.
-   *
-   * A Scope is also associated with a ContextMemoryManager.  All memory
-   * allocated by the Scope is allocated in a single region using the
-   * ContextMemoryManager and released all at once when the Scope is popped.
-   */
+};/* class Context */
+
+/**
+ * Conceptually, a Scope encapsulates that portion of the context that
+ * changes after a call to push() and must be undone on a subsequent call to
+ * pop().  In particular, each call to push() creates a new Scope object .
+ * This new Scope object becomes the top scope and it points (via the
+ * d_pScopePrev member) to the previous top Scope.  Each call to pop()
+ * deletes the current top scope and restores the previous one.  The main
+ * purpose of a Scope is to maintain a linked list of ContexObj objects which
+ * change while the Scope is the top scope and which must be restored when
+ * the Scope is deleted.
+ *
+ * A Scope is also associated with a ContextMemoryManager.  All memory
+ * allocated by the Scope is allocated in a single region using the
+ * ContextMemoryManager and released all at once when the Scope is popped.
+ */
 class Scope {
 
   /**
@@ -432,14 +432,14 @@ public:
 
 };/* class ContextObj */
 
-  /**
-   * For more flexible context-dependent behavior than that provided
-   * by ContextObj, objects may implement the ContextNotifyObj
-   * interface and simply get a notification when a pop has occurred.
-   * See Context class for how to register a ContextNotifyObj with the
-   * Context (you can choose to have notification come before or after
-   * the ContextObj objects have been restored).
-   */
+/**
+ * For more flexible context-dependent behavior than that provided by
+ * ContextObj, objects may implement the ContextNotifyObj interface
+ * and simply get a notification when a pop has occurred.  See
+ * Context class for how to register a ContextNotifyObj with the
+ * Context (you can choose to have notification come before or after
+ * the ContextObj objects have been restored).
+ */
 class ContextNotifyObj {
   /**
    * Context is our friend so that when the Context is deleted, any
@@ -490,7 +490,7 @@ public:
    * implemented by the subclass.
    */
   virtual void notify() = 0;
-}; /* class ContextNotifyObj */
+};/* class ContextNotifyObj */
 
 // Inline functions whose definitions had to be delayed:
 
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();
   }
diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp
index b319b7293..df94ef9ab 100644
--- a/src/main/getopt.cpp
+++ b/src/main/getopt.cpp
@@ -107,7 +107,7 @@ const char *progPath;
 const char *progName;
 
 /** Parse argc/argv and put the result into a CVC4::Options struct. */
-int parseOptions(int argc, char** argv, CVC4::Options* opts)
+int parseOptions(int argc, char* argv[], CVC4::Options* opts)
 throw(OptionException) {
   progPath = progName = argv[0];
   int c;
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 1da56b9f9..f5e53f34a 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -39,7 +39,7 @@ using namespace CVC4::main;
 static Result lastResult;
 static struct Options options;
 
-int runCvc4(int argc, char *argv[]);
+int runCvc4(int argc, char* argv[]);
 void doCommand(SmtEngine&, Command*);
 
 /**
@@ -49,7 +49,7 @@ void doCommand(SmtEngine&, Command*);
  * problems.  That's why main() wraps runCvc4() in the first place.
  * Put everything in runCvc4().
  */
-int main(int argc, char *argv[]) {
+int main(int argc, char* argv[]) {
   try {
     return runCvc4(argc, argv);
   } catch(OptionException& e) {
@@ -80,7 +80,7 @@ int main(int argc, char *argv[]) {
   }
 }
 
-int runCvc4(int argc, char *argv[]) {
+int runCvc4(int argc, char* argv[]) {
 
   // Initialize the signal handlers
   cvc4_init();
diff --git a/src/parser/cvc/Makefile.am b/src/parser/cvc/Makefile.am
index ad0eb70d8..c1b5f752e 100644
--- a/src/parser/cvc/Makefile.am
+++ b/src/parser/cvc/Makefile.am
@@ -38,14 +38,14 @@ maintainer-clean-local:
 	touch @srcdir@/stamp-generated
 # antlr doesn't overwrite output files, it just leaves them.  So we have to delete them first.
 @srcdir@/generated/AntlrCvcLexer.hpp: cvc_lexer.g @srcdir@/stamp-generated
-	-rm -f $(ANTLR_LEXER_STUFF)
-	$(ANTLR) -o "@srcdir@/generated" "@srcdir@/cvc_lexer.g"
+	$(AM_V_at)-rm -f $(ANTLR_LEXER_STUFF)
+	$(AM_V_GEN)$(ANTLR) -o "@srcdir@/generated" "@srcdir@/cvc_lexer.g"
 @srcdir@/generated/AntlrCvcLexer.cpp $(ANTLR_TOKEN_STUFF): @srcdir@/generated/AntlrCvcLexer.hpp
 # doesn't actually depend on the lexer, but if we're doing parallel
 # make and the lexer needs to be rebuilt, we have to keep the rules
 # from running in parallel (since the token files will be deleted &
 # recreated)
 @srcdir@/generated/AntlrCvcParser.hpp: cvc_parser.g cvc_lexer.g $(ANTLR_TOKEN_STUFF) @srcdir@/stamp-generated
-	-rm -f $(ANTLR_PARSER_STUFF)
-	$(ANTLR) -o "@srcdir@/generated" "@srcdir@/cvc_parser.g"
+	$(AM_V_at)-rm -f $(ANTLR_PARSER_STUFF)
+	$(AM_V_GEN)$(ANTLR) -o "@srcdir@/generated" "@srcdir@/cvc_parser.g"
 @srcdir@/generated/AntlrCvcParser.cpp: @srcdir@/generated/AntlrCvcParser.hpp
diff --git a/src/parser/smt/Makefile.am b/src/parser/smt/Makefile.am
index 96ad9c27f..7fe235002 100644
--- a/src/parser/smt/Makefile.am
+++ b/src/parser/smt/Makefile.am
@@ -38,14 +38,14 @@ maintainer-clean-local:
 	touch @srcdir@/stamp-generated
 # antlr doesn't overwrite output files, it just leaves them.  So we have to delete them first.
 @srcdir@/generated/AntlrSmtLexer.hpp: smt_lexer.g @srcdir@/stamp-generated
-	-rm -f $(ANTLR_LEXER_STUFF)
-	$(ANTLR) -o "@srcdir@/generated" "@srcdir@/smt_lexer.g"
+	$(AM_V_at)-rm -f $(ANTLR_LEXER_STUFF)
+	$(AM_V_GEN)$(ANTLR) -o "@srcdir@/generated" "@srcdir@/smt_lexer.g"
 @srcdir@/generated/AntlrSmtLexer.cpp $(ANTLR_TOKEN_STUFF): @srcdir@/generated/AntlrSmtLexer.hpp
 # doesn't actually depend on the lexer, but if we're doing parallel
 # make and the lexer needs to be rebuilt, we have to keep the rules
 # from running in parallel (since the token files will be deleted &
 # recreated)
 @srcdir@/generated/AntlrSmtParser.hpp: smt_parser.g smt_lexer.g $(ANTLR_TOKEN_STUFF) @srcdir@/stamp-generated
-	-rm -f $(ANTLR_PARSER_STUFF)
-	$(ANTLR) -o "@srcdir@/generated" "@srcdir@/smt_parser.g"
+	$(AM_V_at)-rm -f $(ANTLR_PARSER_STUFF)
+	$(AM_V_GEN)$(ANTLR) -o "@srcdir@/generated" "@srcdir@/smt_parser.g"
 @srcdir@/generated/AntlrSmtParser.cpp: @srcdir@/generated/AntlrSmtParser.hpp
diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am
index d71ae842f..43ed0574a 100644
--- a/src/theory/Makefile.am
+++ b/src/theory/Makefile.am
@@ -27,7 +27,7 @@ EXTRA_DIST = \
 
 @srcdir@/theoryof_table.h: @srcdir@/mktheoryof theoryof_table_prologue.h theoryof_table_middle.h theoryof_table_epilogue.h @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds
 	chmod +x @srcdir@/mktheoryof
-	(@srcdir@/mktheoryof \
+	$(AM_V_GEN)(@srcdir@/mktheoryof \
 		@srcdir@/theoryof_table_prologue.h \
 		@srcdir@/theoryof_table_middle.h \
 		@srcdir@/theoryof_table_epilogue.h \
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index 96f02c489..c1ece1145 100644
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -258,16 +258,6 @@ public:
     
   }
 
-  void testHash() {
-    /* Not sure how to test this except survial... */
-    Node a = d_nodeManager->mkNode(ITE);
-    Node b = d_nodeManager->mkNode(ITE);
-    
-    TS_ASSERT(b.hash() == a.hash());
-  }
-
-  
-
   void testEqNode() {
     /*Node eqNode(const Node& right) const;*/
 
diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h
index ab3c1c842..46e524f59 100644
--- a/test/unit/expr/node_builder_black.h
+++ b/test/unit/expr/node_builder_black.h
@@ -647,4 +647,25 @@ public:
     TS_ASSERT_EQUALS(Node(- a + b), d_nm->mkNode(PLUS, d_nm->mkNode(UMINUS, a), b));
     TS_ASSERT_EQUALS(Node(- a * b), d_nm->mkNode(MULT, d_nm->mkNode(UMINUS, a), b));
   }
+
+  /**
+   * This tests the "stack builder"
+   */
+  void testStackBuilder() {
+    try {
+      for(unsigned i = 0; i < 100; ++i) {
+        size_t n = 1 + (rand() % 50);
+
+        // make a builder "b" with a backing store for n children
+        makeStackNodeBuilder(b, n);
+
+        // build one-past-the-end
+        for(size_t j = 0; j <= n; ++j) {
+          b << Node::null();
+        }
+      }
+    } catch(Exception e) {
+      std::cout << e;
+    }
+  }
 };