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

5 files changed, 231 insertions, 147 deletions

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: