From: Tim King <taking@cs.nyu.edu>
Date: Wed, 5 Dec 2012 19:06:21 +0000 (+0000)
Subject: This commit merges in CDTrailHashMap and CDInsertHashMap. CDHashSet now uses CDInsert... 
X-Git-Tag: cvc5-1.0.0~7481
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7f52115ab0dcba4c8ba9403a5f25b8e8c588911a;p=cvc5.git

This commit merges in CDTrailHashMap and CDInsertHashMap. CDHashSet now uses CDInsertHashMap. CDHashSet<TNode> have been changed to CDHashSet<Node>.  Switching CnfStream to use CDInsertSet. Switches a few CDHashMaps in arithmetic to use CDTrailHashMap. Documentation changes to CDHashMap.
---

diff --git a/src/context/Makefile.am b/src/context/Makefile.am
index e7f1dc68b..a63c990cc 100644
--- a/src/context/Makefile.am
+++ b/src/context/Makefile.am
@@ -16,6 +16,10 @@ libcontext_la_SOURCES = \
 	cdlist_forward.h \
 	cdqueue.h \
 	cdtrail_queue.h \
+	cdtrail_hashmap.h \
+	cdtrail_hashmap_forward.h \
+	cdinsert_hashmap.h \
+	cdinsert_hashmap_forward.h \
 	cdhashmap.h \
 	cdhashmap_forward.h \
 	cdhashset.h \
diff --git a/src/context/cdhashmap.h b/src/context/cdhashmap.h
index a37fd2f23..e2ede0603 100644
--- a/src/context/cdhashmap.h
+++ b/src/context/cdhashmap.h
@@ -17,14 +17,19 @@
  ** and operator== for the key class.  For key types that don't have a
  ** __gnu_cxx::hash<>, you should provide an explicit HashFcn.
  **
+ ** See also:
+ **  CDInsertHashMap : An "insert-once" CD hash map.
+ **  CDTrailHashMap : A lightweight CD hash map with poor iteration
+ **    characteristics and some quirks in usage.
+ **
  ** Internal documentation:
  **
- ** CDMap<> is something of a work in progress at present (26 May
+ ** CDHashMap<> is something of a work in progress at present (26 May
  ** 2010), due to some recent discoveries of problems with its
  ** internal state.  Here are some notes on the internal use of
  ** CDOhash_maps that may be useful in figuring out this mess:
  **
- **     So you have a CDMap<>.
+ **     So you have a CDHashMap<>.
  **
  **     You insert some (key,value) pairs.  Each allocates a CDOhash_map<>
  **     and goes on a doubly-linked list headed by map.d_first and
@@ -36,7 +41,7 @@
  **     map pointer at level 0, and a non-NULL map pointer in the
  **     current context level.  (Remember that for later.)
  **
- **     When a key is associated to a new value in a CDMap, its
+ **     When a key is associated to a new value in a CDHashMap, its
  **     associated CDOhash_map calls makeCurrent(), then sets the new
  **     value.  The save object is also a CDOhash_map (allocated in context
  **     memory).
@@ -62,21 +67,21 @@
  **     obliterate() removes it from the map and frees the CDOhash_map's
  **     memory.
  **
- **     Fourth, you might delete the cdhashmap(calling CDMap::~CDMap()).
+ **     Fourth, you might delete the cdhashmap(calling CDHashMap::~CDHashMap()).
  **     This first calls destroy(), as per ContextObj contract, but
  **     cdhashmapdoesn't save/restore itself, so that does nothing at the
- **     CDMap-level.  Then it empties the trash.  Then, for each
+ **     CDHashMap-level.  Then it empties the trash.  Then, for each
  **     element in the map, it marks it as being "part of a complete
  **     map destruction", which essentially short-circuits
  **     CDOhash_map::restore() (see CDOhash_map::restore()), then deallocates
  **     it.  Finally it asserts that the trash is empty (which it
  **     should be, since restore() was short-circuited).
  **
- **     Fifth, you might clear() the CDMap.  This does exactly the
- **     same as CDMap::~CDMap(), except that it doesn't call destroy()
+ **     Fifth, you might clear() the CDHashMap.  This does exactly the
+ **     same as CDHashMap::~CDHashMap(), except that it doesn't call destroy()
  **     on itself.
  **
- **     CDMap::emptyTrash() simply goes through and calls
+ **     CDHashMap::emptyTrash() simply goes through and calls
  **     ->deleteSelf() on all elements in the trash.
  **     ContextObj::deleteSelf() calls the CDOhash_map destructor, then
  **     frees the memory associated to the CDOhash_map.  CDOhash_map::~CDOhash_map()
@@ -87,8 +92,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__CONTEXT__CDMAP_H
-#define __CVC4__CONTEXT__CDMAP_H
+#ifndef __CVC4__CONTEXT__CDHASHMAP_H
+#define __CVC4__CONTEXT__CDHASHMAP_H
 
 #include <vector>
 #include <iterator>
@@ -148,9 +153,9 @@ class CDOhash_map : public ContextObj {
         d_next->d_prev = d_prev;
         d_prev->d_next = d_next;
         if(d_noTrash) {
-          Debug("gc") << "CDMap<> no-trash " << this << std::endl;
+          Debug("gc") << "CDHashMap<> no-trash " << this << std::endl;
         } else {
-          Debug("gc") << "CDMap<> trash push_back " << this << std::endl;
+          Debug("gc") << "CDHashMap<> trash push_back " << this << std::endl;
           //this->deleteSelf();
           d_map->d_trash.push_back(this);
         }
@@ -190,7 +195,7 @@ public:
       // "Initializing" map insertion: this entry will never be
       // removed from the map, it's inserted at level 0 as an
       // "initializing" element.  See
-      // CDMap<>::insertAtContextLevelZero().
+      // CDHashMap<>::insertAtContextLevelZero().
       d_data = data;
     } else {
       // Normal map insertion: first makeCurrent(), then set the data
@@ -417,7 +422,7 @@ public:
   }
 
   /**
-   * Version of insert() for CDMap<> that inserts data value d at
+   * Version of insert() for CDHashMap<> that inserts data value d at
    * context level zero.  This is a special escape hatch for inserting
    * "initializing" data into the map.  Imagine something happens at a
    * deep context level L that causes insertion into a map, such that
@@ -538,7 +543,7 @@ public:
       const std::pair<const Key, Data>& operator*() const {
         return *d_pair;
       }
-    };/* class CDMap<>::iterator::Proxy */
+    };/* class CDHashMap<>::iterator::Proxy */
 
     // Actual postfix increment: returns Proxy with the old value.
     // Now, an expression like *i++ will return the current *i, and
@@ -549,7 +554,7 @@ public:
       ++(*this);
       return e;
     }
-  };/* class CDMap<>::iterator */
+  };/* class CDHashMap<>::iterator */
 
   typedef iterator const_iterator;
 
@@ -576,9 +581,9 @@ public:
     return const_cast<const CDHashMap*>(this)->find(k);
   }
 
-};/* class CDMap<> */
+};/* class CDHashMap<> */
 
 }/* CVC4::context namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__CONTEXT__CDMAP_H */
+#endif /* __CVC4__CONTEXT__CDHashMAP_H */
diff --git a/src/context/cdhashmap_forward.h b/src/context/cdhashmap_forward.h
index d81f5345d..60291af07 100644
--- a/src/context/cdhashmap_forward.h
+++ b/src/context/cdhashmap_forward.h
@@ -9,22 +9,22 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief This is a forward declaration header to declare the CDMap<>
+ ** \brief This is a forward declaration header to declare the CDHashMap<>
  ** template
  **
- ** This is a forward declaration header to declare the CDMap<>
- ** template.  It's useful if you want to forward-declare CDMap<>
- ** without including the full cdmap.h header, for example, in a
+ ** This is a forward declaration header to declare the CDHashMap<>
+ ** template.  It's useful if you want to forward-declare CDHashMap<>
+ ** without including the full cdhashmap.h header, for example, in a
  ** public header context.
  **
- ** For CDMap<> in particular, it's difficult to forward-declare it
+ ** For CDHashMap<> in particular, it's difficult to forward-declare it
  ** yourself, because it has a default template argument.
  **/
 
 #include "cvc4_public.h"
 
-#ifndef __CVC4__CONTEXT__CDMAP_FORWARD_H
-#define __CVC4__CONTEXT__CDMAP_FORWARD_H
+#ifndef __CVC4__CONTEXT__CDHASHMAP_FORWARD_H
+#define __CVC4__CONTEXT__CDHASHMAP_FORWARD_H
 
 /// \cond internals
 
@@ -41,4 +41,4 @@ namespace CVC4 {
 
 /// \endcond
 
-#endif /* __CVC4__CONTEXT__CDMAP_FORWARD_H */
+#endif /* __CVC4__CONTEXT__CDHASHMAP_FORWARD_H */
diff --git a/src/context/cdhashset.h b/src/context/cdhashset.h
index e885b7729..d7957cf3f 100644
--- a/src/context/cdhashset.h
+++ b/src/context/cdhashset.h
@@ -20,16 +20,15 @@
 #define __CVC4__CONTEXT__CDSET_H
 
 #include "context/context.h"
-#include "context/cdhashset_forward.h"
-#include "context/cdhashmap.h"
+#include "context/cdinsert_hashmap.h"
 #include "util/cvc4_assert.h"
 
 namespace CVC4 {
 namespace context {
 
 template <class V, class HashFcn>
-class CDHashSet : protected CDHashMap<V, V, HashFcn> {
-  typedef CDHashMap<V, V, HashFcn> super;
+class CDHashSet : protected CDInsertHashMap<V, bool, HashFcn> {
+  typedef CDInsertHashMap<V, bool, HashFcn> super;
 
 public:
 
@@ -58,40 +57,30 @@ public:
     return super::size();
   }
 
-  size_t count(const V& v) const {
-    return super::count(v);
-  }
-
   bool insert(const V& v) {
-    return super::insert(v, v);
-  }
-
-  void insertAtContextLevelZero(const V& v) {
-    return super::insertAtContextLevelZero(v, v);
+    return super::insert_safe(v, true);
   }
 
   bool contains(const V& v) {
-    return find(v) != end();
+    return super::contains(v);
   }
 
-  // FIXME: no erase(), too much hassle to implement efficiently...
-
-  class iterator {
-    typename super::iterator d_it;
+  class const_iterator {
+    typename super::const_iterator d_it;
 
   public:
 
-    iterator(const typename super::iterator& it) : d_it(it) {}
-    iterator(const iterator& it) : d_it(it.d_it) {}
+    const_iterator(const typename super::const_iterator& it) : d_it(it) {}
+    const_iterator(const const_iterator& it) : d_it(it.d_it) {}
 
     // Default constructor
-    iterator() {}
+    const_iterator() {}
 
     // (Dis)equality
-    bool operator==(const iterator& i) const {
+    bool operator==(const const_iterator& i) const {
       return d_it == i.d_it;
     }
-    bool operator!=(const iterator& i) const {
+    bool operator!=(const const_iterator& i) const {
       return d_it != i.d_it;
     }
 
@@ -101,7 +90,7 @@ public:
     }
 
     // Prefix increment
-    iterator& operator++() {
+    const_iterator& operator++() {
       ++d_it;
       return *this;
     }
@@ -131,18 +120,28 @@ public:
     }
   };/* class CDSet<>::iterator */
 
-  typedef iterator const_iterator;
-
   const_iterator begin() const {
-    return iterator(super::begin());
+    return const_iterator(super::begin());
   }
 
   const_iterator end() const {
-    return iterator(super::end());
+    return const_iterator(super::end());
   }
 
   const_iterator find(const V& v) const {
-    return iterator(super::find(v));
+    return const_iterator(super::find(v));
+  }
+
+  typedef typename super::key_iterator key_iterator;
+  key_iterator key_begin() const {
+    return super::key_begin();
+  }
+  key_iterator key_end() const {
+    return super::key_end();
+  }
+
+  void insertAtContextLevelZero(const V& v) {
+    return super::insertAtContextLevelZero(v, true);
   }
 
 };/* class CDSet */
diff --git a/src/context/cdinsert_hashmap.h b/src/context/cdinsert_hashmap.h
new file mode 100644
index 000000000..0c84eda80
--- /dev/null
+++ b/src/context/cdinsert_hashmap.h
@@ -0,0 +1,402 @@
+/*********************                                                        */
+/*! \file cdinsert_hashmap.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Context-dependent insert only hashmap built using trail of edits
+ **
+ ** Context-dependent hashmap that only allows for one insertion per element.
+ ** This can be viewed as a highly restricted version of CDHashMap.
+ ** It is significantly lighter in memory usage than CDHashMap.
+ **
+ ** See also:
+ **  CDTrailHashMap : A lightweight CD hash map with poor iteration
+ **    characteristics and some quirks in usage.
+ **  CDHashMap : A fully featured CD hash map. (The closest to <ext/hash_map>)
+ **
+ ** Notes:
+ ** - To iterate efficiently over the elements use the key_iterators.
+ ** - operator[] is only supported as a const derefence (must succeed).
+ ** - insert(k) must always work.
+ ** - Use insert_safe if you want to check if the element has been inserted
+ **   and only insert if it has not yet been.
+ ** - Does not accept TNodes as keys.
+ ** - Supports insertAtContextLevelZero() if the element is not in the map.
+ **/
+
+
+#include "cvc4_private.h"
+
+#include "context/context.h"
+#include "context/cdinsert_hashmap_forward.h"
+#include <utility>
+#include <ext/hash_map>
+#include <deque>
+#include "util/cvc4_assert.h"
+#include "util/output.h"
+
+#include "expr/node.h"
+#include <boost/static_assert.hpp>
+
+#pragma once
+
+namespace CVC4 {
+namespace context {
+
+
+template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> >
+class InsertHashMap {
+private:
+  typedef std::deque<Key> KeyVec;
+  /** A list of the keys in the map maintained as a stack. */
+  KeyVec d_keys;
+
+  typedef __gnu_cxx::hash_map<Key, Data, HashFcn> HashMap;
+  /** The hash_map used for element lookup. */
+  HashMap d_hashMap;
+
+public:
+  /**
+   * An iterator over a list of keys.
+   * Use this to efficiently iterate over the elements.
+   * (See std::deque<>::iterator).
+   */
+  typedef typename KeyVec::const_iterator key_iterator;
+
+  /**An iterator over the elements in the hash_map. */
+  typedef typename HashMap::const_iterator const_iterator;
+
+
+  /**
+   * Returns an iterator to the begining of the HashMap.
+   * Acts like a hash_map::const_iterator.
+   */
+  const_iterator begin() const{
+    return d_hashMap.begin();
+  }
+  /**
+   * Returns an iterator to the end of the HashMap.
+   * Acts like a hash_map::const_iterator.
+   */
+  const_iterator end() const{
+    return d_hashMap.end();
+  }
+
+  /**
+   * Returns an iterator to the Key k of the map.
+   * See hash_map::find()
+   */
+  const_iterator find(const Key& k) const{
+    return d_hashMap.find(k);
+  }
+
+  /** Returns an iterator to the start of the set of keys. */
+  key_iterator key_begin() const{
+    return d_keys.begin();
+  }
+  /** Returns an iterator to the end of the set of keys. */
+  key_iterator key_end() const{
+    return d_keys.end();
+  }
+
+  /** Returns true if the map is empty. */
+  bool empty() const { return d_keys.empty(); }
+  /** Returns the number of elements in the map. */
+  size_t size() const { return d_keys.size(); }
+
+  /** Returns true if k is a mapped key. */
+  bool contains(const Key& k) const {
+    return find(k) != end();
+  }
+
+  /**
+   * Returns a reference the data mapped by k.
+   * This must succeed.
+   */
+  const Data& operator[](const Key& k) const {
+    const_iterator ci = find(k);
+    Assert(ci != end());
+    return (*ci).second;
+  }
+
+  /**
+   * Inserts an element into the map, and pushes its key to the front
+   * of the stack. The key inserted must be not be currently mapped.
+   */
+  void push_front(const Key& k, const Data& d){
+    Assert(!contains(k));
+    d_hashMap.insert(std::make_pair(k, d));
+    d_keys.push_front(k);
+  }
+
+  /**
+   * Inserts an element into the map, and pushes its key onto the
+   * back on the stack.  The key inserted must be not be currently mapped.
+   */
+  void push_back(const Key& k, const Data& d){
+    Assert(!contains(k));
+    d_hashMap.insert(std::make_pair(k, d));
+    d_keys.push_back(k);
+  }
+
+  /**
+   * Pops the key at the front of the list off and removes its key from the map.
+   */
+  void pop_front(){
+    Assert(!empty());
+    const Key& front = d_keys.front();
+    d_hashMap.erase(front);
+
+    Debug("TrailHashMap") <<"TrailHashMap pop_front " << size() << std::endl;
+    d_keys.pop_front();
+  }
+
+  /**
+   * Pops the key at the back of the stack off and removes its key from the map.
+   */
+  void pop_back(){
+    Assert(!empty());
+    const Key& back = d_keys.back();
+    d_hashMap.erase(back);
+
+    Debug("TrailHashMap") <<"TrailHashMap pop_back " << size() << std::endl;
+    d_keys.pop_back();
+  }
+
+  /**
+   * Pops the back of the stack until the size is below s.
+   */
+  void pop_to_size(size_t s){
+    while(size() > s){
+      pop_back();
+    }
+  }
+};/* class TrailHashMap<> */
+
+template <class Key, class Data, class HashFcn >
+class CDInsertHashMap : public ContextObj {
+private:
+  typedef InsertHashMap<Key, Data, HashFcn> IHM;
+
+  /** An InsertHashMap that backs all of the data. */
+  IHM* d_insertMap;
+
+  /** For restores, we need to keep track of the previous size. */
+  size_t d_size;
+
+  /**
+   * To support insertAtContextLevelZero() and restores,
+   * we have called d_insertMap->d_pushFront().
+   */
+  size_t d_pushFronts;
+
+  /**
+   * Private copy constructor used only by save().  d_insertMap is
+   * not copied: only the base class information and
+   * d_size and d_pushFronts are needed in restore.
+   */
+  CDInsertHashMap(const CDInsertHashMap<Key, Data, HashFcn>& l) :
+    ContextObj(l),
+    d_insertMap(NULL),
+    d_size(l.d_size),
+    d_pushFronts(l.d_pushFronts)
+  {
+    Debug("CDInsertHashMap") << "copy ctor: " << this
+                    << " from " << &l
+                    << " size " << d_size << std::endl;
+  }
+
+  /**
+   * Implementation of mandatory ContextObj method save: simply copies
+   * the current size information to a copy using the copy constructor (the
+   * pointer and the allocated size are *not* copied as they are not
+   * restored on a pop).  The saved information is allocated using the
+   * ContextMemoryManager.
+   */
+  ContextObj* save(ContextMemoryManager* pCMM) {
+    ContextObj* data = new(pCMM) CDInsertHashMap<Key, Data, HashFcn>(*this);
+    Debug("CDInsertHashMap") << "save " << this
+                            << " at level " << this->getContext()->getLevel()
+                            << " size at " << this->d_size
+                            << " d_list is " << this->d_insertMap
+                            << " data:" << data << std::endl;
+    return data;
+  }
+protected:
+  /**
+   * Implementation of mandatory ContextObj method restore:
+   * restore to the previous size taking into account the number
+   * of new pushFront calls have happened since saving.
+   * The d_insertMap is untouched and d_pushFronts is also kept.
+   */
+  void restore(ContextObj* data) {
+    Debug("CDInsertHashMap") << "restore " << this
+                            << " level " << this->getContext()->getLevel()
+                            << " data == " << data
+                            << " d_insertMap == " << this->d_insertMap << std::endl;
+    size_t oldSize = ((CDInsertHashMap<Key, Data, HashFcn>*)data)->d_size;
+    size_t oldPushFronts = ((CDInsertHashMap<Key, Data, HashFcn>*)data)->d_pushFronts;
+    Assert(oldPushFronts <= d_pushFronts);
+
+    // The size to restore to.
+    size_t restoreSize = oldSize + (d_pushFronts - oldPushFronts);
+    d_insertMap->pop_to_size(restoreSize);
+    d_size = restoreSize;
+    Assert(d_insertMap->size() == d_size);
+    Debug("CDInsertHashMap") << "restore " << this
+                            << " level " << this->getContext()->getLevel()
+                            << " size back to " << this->d_size << std::endl;
+  }
+public:
+
+ /**
+   * Main constructor: d_insertMap starts as an empty map, with the size is 0
+   */
+  CDInsertHashMap(Context* context) :
+    ContextObj(context),
+    d_insertMap(new IHM()),
+    d_size(0),
+    d_pushFronts(0){
+    Assert(d_insertMap->size() == d_size);
+  }
+
+  /**
+   * Destructor: delete the d_insertMap
+   */
+  ~CDInsertHashMap() throw(AssertionException) {
+    this->destroy();
+    delete d_insertMap;
+  }
+
+  /** An iterator over the elements in the hash_map. */
+  typedef typename IHM::const_iterator const_iterator;
+
+  /**
+   * An iterator over a list of keys.
+   * Use this to efficiently iterate over the elements.
+   * (See std::deque<>::iterator).
+   */
+  typedef typename IHM::key_iterator key_iterator;
+
+  /** Returns true if the map is empty in the current context. */
+  bool empty() const{
+    return d_size == 0;
+  }
+
+  /** Returns true the size of the map in the current context. */
+  size_t size() const {
+    return d_size;
+  }
+
+  /**
+   * Inserts an element into the map.
+   * The key inserted must be not be currently mapped.
+   * This is implemented using d_insertMap.push_back().
+   */
+  void insert(const Key& k, const Data& d){
+    makeCurrent();
+    ++d_size;
+    d_insertMap->push_back(k, d);
+    Assert(d_insertMap->size() == d_size);
+  }
+
+  /**
+   * Checks if the key k is mapped already.
+   * If it is, this returns false.
+   * Otherwise it is inserted and this returns true.
+   */
+  bool insert_safe(const Key& k, const Data& d){
+    if(contains(k)){
+      return false;
+    }else{
+      insert(k,d);
+      return true;
+    }
+  }
+
+  /**
+   * Version of insert() for CDMap<> that inserts data value d at
+   * context level zero.
+   *
+   * It is an error to insertAtContextLevelZero()
+   * a key that already is in the map.
+   */
+  void insertAtContextLevelZero(const Key& k, const Data& d){
+    makeCurrent();
+    ++d_size;
+    ++d_pushFronts;
+    d_insertMap->push_front(k, d);
+  }
+
+  /** Returns true if k is a mapped key in the context. */
+  bool contains(const Key& k) const {
+    return d_insertMap->contains(k);
+  }
+
+  /**
+   * Returns a reference the data mapped by k.
+   * k must be in the map in this context.
+   */
+  const Data& operator[](const Key& k) const {
+    return (*d_insertMap)[k];
+  }
+
+   /**
+    * Returns a const_iterator to the value_type if k is a mapped key in
+    * the context.
+    */
+  const_iterator find(const Key& k) const {
+    return d_insertMap->find(k);
+  }
+
+  /**
+   * Returns an iterator to the begining of the map.
+   * Acts like a hash_map::const_iterator.
+   */
+  const_iterator begin() const{
+    return d_insertMap->begin();
+  }
+
+  /**
+   * Returns an iterator to the end of the map.
+   * Acts like a hash_map::const_iterator.
+   */
+  const_iterator end() const{
+    return d_insertMap->end();
+  }
+
+  /** Returns an iterator to the start of the set of keys. */
+  key_iterator key_begin() const{
+    return d_insertMap->key_begin();
+  }
+  /** Returns an iterator to the end of the set of keys. */
+  key_iterator key_end() const{
+    return d_insertMap->key_end();
+  }
+};/* class CDInsertHashMap<> */
+
+
+template <class Data, class HashFcn>
+class CDInsertHashMap <TNode, Data, HashFcn > : public ContextObj {
+  /* CDInsertHashMap is challenging to get working with TNode.
+   * Consider using CDHashMap<TNode,...> instead.
+   *
+   * Explanation:
+   * CDInsertHashMap uses keys for deallocation.
+   * If the key is a TNode and the backing (the hard node reference)
+   * for the key in another data structure removes the key at the same context
+   * the ref count could drop to 0.  The key would then not be eligible to be
+   * hashed. Getting the order right with a guarentee is to hard.
+   */
+
+  BOOST_STATIC_ASSERT(sizeof(Data) == 0);
+};
+
+}/* CVC4::context namespace */
+}/* CVC4 namespace */
diff --git a/src/context/cdinsert_hashmap_forward.h b/src/context/cdinsert_hashmap_forward.h
new file mode 100644
index 000000000..638607840
--- /dev/null
+++ b/src/context/cdinsert_hashmap_forward.h
@@ -0,0 +1,38 @@
+/*********************                                                        */
+/*! \file cdinsert_hashmap_forward.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief This is a forward declaration header to declare the CDInsertHashMap<>
+ ** template
+ **
+ ** This is a forward declaration header to declare the CDInsertHashMap<>
+ ** template.  It's useful if you want to forward-declare CDInsertHashMap<>
+ ** without including the full cdinsert_hashmap.h header, for example, in a
+ ** public header context.
+ **
+ ** For CDInsertHashMap<> in particular, it's difficult to forward-declare it
+ ** yourself, because it has a default template argument.
+ **/
+
+#include "cvc4_public.h"
+
+#pragma once
+
+namespace __gnu_cxx {
+  template <class Key> struct hash;
+}/* __gnu_cxx namespace */
+
+namespace CVC4 {
+  namespace context {
+    template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> >
+    class CDInsertHashMap;
+  }/* CVC4::context namespace */
+}/* CVC4 namespace */
+
diff --git a/src/context/cdtrail_hashmap.h b/src/context/cdtrail_hashmap.h
new file mode 100644
index 000000000..5f090341d
--- /dev/null
+++ b/src/context/cdtrail_hashmap.h
@@ -0,0 +1,571 @@
+/*********************                                                        */
+/*! \file cdtrail_hashmap.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Context-dependent hashmap built using trail of elements
+ **
+ ** Context-dependent hashmap that explicitly keeps track of its edit history.
+ ** This is similar in functionality to CDHashMap with fewer capabilites and
+ ** slight changes in the interface. It has the advantage of being lighter in
+ ** memory usage.
+ **
+ ** See also:
+ **  CDInsertHashMap : An "insert-once" CD hash map.
+ **  CDHashMap : A fully featured CD hash map. (The closest to <ext/hash_map>)
+ **
+ ** Notes:
+ ** - To iterate efficiently over the elements use the key_iterators.
+ ** - operator[] is only supported as a const derefence (must succeed).
+ ** - Insertions to the map are done with respect to a context.
+ ** - Insertions can be done in two manors either with insert() or
+ **   insert_no_overwrite().
+ ** - insert(k,d) inserts the key data pair into the hashtable and returns a
+ **   false if it overwrote the previous value.
+ ** - insert_no_overwrite(k,d) inserts key data pair into the hashtable only
+ **   if the value is not already there. It returns true, if an element was
+ **   added. This conditionally extends the trail length if it returns true.
+ ** - inserts are compacting.  If there is another insert to the same key
+ **   at the same context, the memory is reused.
+ ** - Iterating over const_iterators has amortized time proportional to
+ **   O(trail length). (If this needs to be improved, please bug Tim.)
+ ** - contains() and operator[] are slightly faster than using stl style
+ **   iterator comparisons: find(), end(), etc.
+ **/
+
+
+#include "cvc4_private.h"
+
+#pragma once
+
+#include "context/context.h"
+#include "context/cdtrail_hashmap_forward.h"
+#include <utility>
+#include <ext/hash_map>
+#include <deque>
+#include "util/cvc4_assert.h"
+#include "util/output.h"
+
+#include "expr/node.h"
+#include <boost/static_assert.hpp>
+
+
+namespace CVC4 {
+namespace context {
+
+
+template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> >
+class TrailHashMap {
+public:
+  /** A pair of Key and Data that mirrors hash_map::value_type. */
+  typedef std::pair<Key, Data> value_type;
+
+private:
+
+  /** The trail information from an insert. */
+  struct KDT {
+    /** The Key Data pair. */
+    value_type d_kd;
+
+    /**
+     * The previous trail entry with the same key.
+     * On a pop, this is the element to revert to.
+     * This value is a self loop if there is no previous entry.
+     */
+    size_t d_prevKey;
+
+    /**  The whether the trail element is current. */
+    bool d_current;
+
+    KDT(const Key& key, const Data& data, size_t prev, bool cur = true):
+      d_kd(std::make_pair(key, data)), d_prevKey(prev), d_current(cur){ }
+    KDT(){}
+  };
+
+  typedef std::deque<KDT> KDTVec;
+  typedef typename KDTVec::const_iterator KDTVec_const_iterator;
+  /** The trail of elements. */
+  KDTVec d_kdts;
+
+
+  typedef __gnu_cxx::hash_map<Key, size_t, HashFcn> PositionMap;
+  typedef typename PositionMap::iterator PM_iterator;
+  typedef typename PositionMap::const_iterator PM_const_iterator;
+
+  /** A map of keys to their positions in the trail. */
+  PositionMap d_posMap;
+
+
+  /** The number of unique keys in the map. */
+  size_t d_uniqueKeys;
+
+  /** Internal utility class. NonConstant find on the position map.*/
+  inline PM_iterator ncfind(const Key& k) {
+    return d_posMap.find(k);
+  }
+
+  /** Internal utility class. Position Map Find.*/
+  inline PM_const_iterator pmfind(const Key& k) const{
+    return d_posMap.find(k);
+  }
+  /** Internal utility class. Position Map End.*/
+  inline PM_const_iterator pmend() const{
+    return d_posMap.end();
+  }
+
+  /** This is true if the previous entry in the trail points at itself.*/
+  inline bool selfLoop(size_t pos, const KDT& kdt) const {
+    return pos == kdt.d_prevKey;
+  }
+
+public:
+  /**
+   * Constant iterator for TrailHashMap.
+   * Only supports forward iteration.
+   * This always points at the end or a current element in the trail.
+   * This is done by iterating over the trail.
+   */
+  class const_iterator {
+  private:
+    /** A vector iterator. */
+    KDTVec_const_iterator d_it;
+
+    /** A pointer to the end of the vector.*/
+    KDTVec_const_iterator d_end;
+
+    /** Move the iterator to the end or the next current element.*/
+    void findCurrent(){
+      while(d_it != d_end && !(*d_it).d_current){
+        ++d_it;
+      }
+    }
+
+  public:
+
+    /** Constructs an iterator for a TrailHashMap. */
+    const_iterator(KDTVec_const_iterator it, KDTVec_const_iterator end) :
+      d_it(it),
+      d_end(end){
+      findCurrent();
+    }
+
+    /** Copy constructor for an iterator for a TrailHashMap. */
+    const_iterator(const const_iterator& other) :
+      d_it(other.d_it), d_end(other.d_end){
+      // Do not need to findCurrent()
+    }
+
+    /** Returns true if the iterators are the same. */
+    inline bool operator==(const const_iterator& other) const {
+      return d_it == other.d_it;
+    }
+
+    /** Returns true if the iterators are the same. */
+    inline bool operator!=(const const_iterator& other) const {
+      return d_it != other.d_it;
+    }
+
+    /** Returns a pair<Key,Data>. */
+    inline const value_type& operator*() const {
+      return (*d_it).d_kd;
+    }
+
+    /** Prefix increment */
+    const_iterator& operator++() {
+      ++d_it;
+      findCurrent();
+      return *this;
+    }
+  };
+
+  /** Returns a beginning iterator.*/
+  inline const_iterator begin() const{
+    return const_iterator(d_kdts.begin(), d_kdts.end());
+  }
+
+  /** Returns an end iterator.*/
+  inline const_iterator end() const{
+    return const_iterator(d_kdts.end(), d_kdts.end());
+  }
+
+  /** Returns true if the trail is empty.*/
+  inline bool empty() const { return d_kdts.empty(); }
+
+  /** Returns the size of the trail.*/
+  inline size_t trailSize() const { return d_kdts.size(); }
+
+  /** Returns the number of unique keys in the map.*/
+  inline size_t uniqueKeys() const { return d_uniqueKeys; }
+
+  /** Returns true if the key is in the map.*/
+  inline bool contains(const Key& k) const {
+    return pmfind(k) != pmend();
+  }
+
+  /**
+   * Returns a NON const reference to an element in the Map.
+   * k must be a key in the Map.
+   * DO NOT USE THIS UNLESS YOU ARE CONFIDENT THE CHANGES MAKE SENSE.
+   */
+  Data& lookup(const Key& k){
+    Assert(contains(k));
+    PM_iterator ci = ncfind(k);
+    KDT& kdt = d_kdts[(*ci).second];
+    return kdt.d_kd.second;
+  }
+
+  /**
+   * Returns a const reference to an element mapped by a Key k.
+   * k must be a key in the Map.
+   */
+  const Data& operator[](const Key& k) const {
+    PM_const_iterator pci = pmfind(k);
+    Assert(pci != pmend());
+    return d_kdts[(*pci).second].d_kd.second;
+  }
+
+  /**
+   * If the key k is in the map, this returns a const_iterator pointing at this
+   * element.  Otherwise, this returns end().
+   */
+  const_iterator find(const Key& k) const {
+    PM_const_iterator pci = pmfind(k);
+    if(pci == pmend()){
+      return end();
+    }else{
+      size_t pos = (*pci).second;
+      return const_iterator(d_kdts.begin() + pos, d_kdts.end());
+    }
+  }
+
+  /**
+   * Similar to contains, but includes a notion of trail position.
+   * Returns <true, true> if contains(k) and the current position of k
+   *  in the map is greater than or equal to pos.
+   * Returns <true, false> if it contains(k) but not the previous condition.
+   * Returns <false, false> if it does not contains(k).
+   */
+  std::pair<bool, bool> hasAfter(const Key& k, size_t pos) {
+    PM_iterator it = ncfind(k);
+    if(it != d_posMap.end()){
+      return std::make_pair(true, (*it).second >= pos );
+    }
+    return std::make_pair(false, false);
+  }
+
+  /**
+   * Inserts an element unconditionally.
+   * Always increases the trail size.
+   * Returns true if the key count increased.
+   */
+  bool push_back(const Key& k, const Data& d){
+    std::pair<bool, bool> res = compacting_push_back(k, d, trailSize());
+    return res.first;
+  }
+
+  /**
+   * This inserts an element into the trail.
+   * This insert can reuse the same trail element if the postion of the element
+   * is >= threshold.
+   *
+   * Return values:
+   * If pair<bool, bool> res = compacting_push_back(..),
+   * then res.first is true if this is a new unique key, and
+   * res.second is true if the trail length increased.
+   * 
+   */
+  std::pair<bool, bool> compacting_push_back(const Key& k, const Data& d, size_t threshold){
+    size_t backPos = d_kdts.size();
+    std::pair<PM_iterator, bool> res = d_posMap.insert(std::make_pair(k, backPos));
+    if(!res.second){
+      size_t& prevPosInPM = (*res.first).second;
+
+      Assert(d_kdts[prevPosInPM].d_current);
+
+      if(prevPosInPM < threshold){
+        d_kdts.push_back(KDT(k,d, prevPosInPM));
+        d_kdts[prevPosInPM].d_current = false;
+        prevPosInPM = backPos;
+
+        return std::make_pair(false, true);
+      }else{
+        d_kdts[prevPosInPM].d_kd.second = d;
+        return std::make_pair(false, false);
+      }
+    }else{
+      d_kdts.push_back(KDT(k,d, backPos));
+      ++d_uniqueKeys;
+      return std::make_pair(true, true);
+    }
+  }
+
+  /**
+   * Inserts an element if the key is not already in the map.
+   * Returns true if the element was inserted.
+   */
+  bool insert_no_overwrite(const Key& k, const Data& d){
+    size_t backPos = d_kdts.size();
+    std::pair<PM_iterator, bool> res = d_posMap.insert(std::make_pair(k, backPos));
+    if(res.second){
+      d_kdts.push_back(KDT(k,d, backPos));
+      ++d_uniqueKeys;
+    }
+    Debug("TrailHashMap") <<"TrailHashMap insert" << k << " d " << d << " " << backPos << std::endl;
+    return res.second;
+  }
+
+  /** Pops the element at the back of the trail. */
+  void pop_back(){
+    Assert(!empty());
+    const KDT& back = d_kdts.back();
+    const Key& k = back.d_kd.first;
+    if(selfLoop(trailSize()-1, back)){
+      d_posMap.erase(k);
+      --d_uniqueKeys;
+      Debug("TrailHashMap") <<"TrailHashMap pop_back erase " << trailSize() <<" " << std::endl;
+
+    }else{
+      Debug("TrailHashMap") <<"TrailHashMap reset " << trailSize() <<" " << " " << back.d_prevKey << std::endl;
+      d_posMap[k] = back.d_prevKey;
+      d_kdts[back.d_prevKey].d_current = true;
+    }
+    d_kdts.pop_back();
+  }
+
+  /** Pops the element at the back of the trail until the trailSize is <= s. */
+  void pop_to_size(size_t s){
+    while(trailSize() > s){
+      pop_back();
+    }
+  }
+};/* class TrailHashMap<> */
+
+template <class Key, class Data, class HashFcn >
+class CDTrailHashMap : public ContextObj {
+private:
+  /** A short name for the templatized TrailMap that backs the CDTrailMap. */
+  typedef TrailHashMap<Key, Data, HashFcn> THM;
+
+  /** The trail map that backs the CDTrailMap. */
+  THM* d_trailMap;
+public:
+  /** Iterator for the CDTrailHashMap. */
+  typedef typename THM::const_iterator const_iterator;
+
+  /** Return value of operator* on a const_iterator (pair<Key,Data>).*/
+  typedef typename THM::value_type value_type;
+
+private:
+  /**
+   * The length of the trail in the current context.
+   * This is used to support reverting.
+   */
+  size_t d_trailSize;
+
+  /**
+   * The length of the trail immediately after the previous makeCurrent().
+   * This is used to support compacting inserts.
+   */
+  size_t d_prevTrailSize;
+
+  /**
+   * Private copy constructor used only by save().  d_trailMap is not copied:
+   * only the base class information, d_trailSize, and d_prevTrailSize
+   * are needed in restore.
+   */
+  CDTrailHashMap(const CDTrailHashMap<Key, Data, HashFcn>& l) :
+    ContextObj(l),
+    d_trailMap(NULL),
+    d_trailSize(l.d_trailSize),
+    d_prevTrailSize(l.d_prevTrailSize){
+    Debug("CDTrailHashMap") << "copy ctor: " << this
+                    << " from " << &l
+                    << " size " << d_trailSize << std::endl;
+  }
+
+  /**
+   * Implementation of mandatory ContextObj method save: simply copies
+   * the current sizes to a copy using the copy constructor,
+   * The saved information is allocated using the ContextMemoryManager.
+   */
+  ContextObj* save(ContextMemoryManager* pCMM) {
+    ContextObj* data = new(pCMM) CDTrailHashMap<Key, Data, HashFcn>(*this);
+    Debug("CDTrailHashMap") << "save " << this
+                            << " at level " << this->getContext()->getLevel()
+                            << " size at " << this->d_trailSize
+                            << " d_list is " << this->d_trailMap
+                            << " data:" << data << std::endl;
+    return data;
+  }
+protected:
+  /**
+   * Implementation of mandatory ContextObj method restore: simply
+   * restores the previous size.  Note that the list pointer and the
+   * allocated size are not changed.
+   */
+  void restore(ContextObj* data) {
+    Debug("CDTrailHashMap") << "restore " << this
+                            << " level " << this->getContext()->getLevel()
+                            << " data == " << data
+                            << " d_trailMap == " << this->d_trailMap << std::endl;
+    size_t oldSize = ((CDTrailHashMap<Key, Data, HashFcn>*)data)->d_trailSize;
+    d_trailMap->pop_to_size(oldSize);
+    d_trailSize = oldSize;
+    Assert(d_trailMap->trailSize() == d_trailSize);
+
+    d_prevTrailSize = ((CDTrailHashMap<Key, Data, HashFcn>*)data)->d_prevTrailSize;
+    Debug("CDTrailHashMap") << "restore " << this
+                            << " level " << this->getContext()->getLevel()
+                            << " size back to " << this->d_trailSize << std::endl;
+  }
+
+  /**
+   * We need to save the d_trailSize immediately after a successful makeCurrent.
+   * So this version needs to be used everywhere instead of maekCurrent()
+   * internally.
+   */
+  void internalMakeCurrent () {
+    if(!isCurrent()){
+      makeCurrent();
+      d_prevTrailSize = d_trailSize;
+    }
+  }
+
+public:
+
+  /**
+   * Main constructor: d_trailMap starts as an empty map, with the sizes are 0
+   */
+  CDTrailHashMap(Context* context) :
+    ContextObj(context),
+    d_trailMap(new THM()),
+    d_trailSize(0),
+    d_prevTrailSize(0){
+    Assert(d_trailMap->trailSize() == d_trailSize);
+  }
+
+  /**
+   * Destructor: delete the map
+   */
+  ~CDTrailHashMap() throw(AssertionException) {
+    this->destroy();
+    delete d_trailMap;
+  }
+
+  /** Returns true if the map is empty in the current context. */
+  bool empty() const{
+    return d_trailSize == 0;
+  }
+
+  /** Returns true the size of the map in the current context. */
+  size_t size() const {
+    return d_trailMap->uniqueKeys();
+  }
+
+  /**
+   * Inserts an element into the map.
+   * This always succeeds.
+   * Returns true if the key is new.
+   */
+  bool insert(const Key& k, const Data& d){
+    internalMakeCurrent();
+    std::pair<bool, bool> res = d_trailMap->compacting_push_back(k, d, d_prevTrailSize);
+    if(res.second){
+      ++d_trailSize;
+    }
+    Assert(d_trailMap->trailSize() == d_trailSize);
+    return res.first;
+  }
+
+  /**
+   * Inserts an element into the map if the key is not already there.
+   * This has no side effects if the insert does not happen.
+   * Returns true if the element was inserted.
+   */
+  bool insert_no_overwrite(const Key& k, const Data& d){
+    bool res = d_trailMap->insert_no_overwrite(k, d);
+    if(res){
+      internalMakeCurrent();
+      ++d_trailSize;
+    }
+    Assert(d_trailMap->trailSize() == d_trailSize);
+    return res;
+  }
+
+  /** Returns true if k is a mapped key in the context. */
+  bool contains(const Key& k) const {
+    return d_trailMap->contains(k);
+  }
+
+  /**
+   * Returns a reference the data mapped by k.
+   * k must be in the map in this context.
+   */
+  const Data& operator[](const Key& k) const {
+    return (*d_trailMap)[k];
+  }
+ /*
+// While the following code "works", I wonder if it is not better to disable it?
+// Non-const operator[] has strange semantics for a context-dependent
+// data structure.
+  Data& operator[](const Key& k) {
+    internalMakeCurrent();
+    std::pair<bool, bool> res = d_trailMap->hasAfter(k, d_prevTrailSize);
+    if(!res.first){
+      std::pair<bool, bool> res = d_trailMap->compacting_push_back(k, Data(), d_prevTrailSize);
+      if(res.second){
+        ++d_trailSize;
+      }
+    }else if(!res.second){
+      std::pair<bool, bool> res = d_trailMap->compacting_push_back(k, (*d_trailMap)[k], d_prevTrailSize);
+      if(res.second){
+        ++d_trailSize;
+      }
+    }
+    return d_trailMap->lookup(k);
+  }
+ */
+
+  /**
+   * Returns a const_iterator to the value_type if k is a mapped key in
+   * the context.
+   */
+  const_iterator find(const Key& k) const {
+    return d_trailMap->find(k);
+  }
+
+  /** Returns an iterator to the begining of the map.  */
+  const_iterator begin() const{
+    return d_trailMap->begin();
+  }
+  /** Returns an iterator to the end of the map.  */
+  const_iterator end() const{
+    return d_trailMap->end();
+  }
+
+};/* class CDTrailHashMap<> */
+
+template <class Data, class HashFcn>
+class CDTrailHashMap <TNode, Data, HashFcn > : public ContextObj {
+  /* CDTrailHashMap is challenging to get working with TNode.
+   * Consider using CDHashMap<TNode,...> instead.
+   *
+   * Explanation:
+   * CDTrailHashMap uses keys during deallocation.
+   * If the key is a TNode and the backing (the hard node reference)
+   * for the key in another data structure removes the key at the same context
+   * the ref count could drop to 0.  The key would then not be eligible to be
+   * hashed. Getting the order right with a guarentee is to hard.
+   */
+
+  BOOST_STATIC_ASSERT(sizeof(Data) == 0);
+};
+
+}/* CVC4::context namespace */
+}/* CVC4 namespace */
diff --git a/src/context/cdtrail_hashmap_forward.h b/src/context/cdtrail_hashmap_forward.h
new file mode 100644
index 000000000..549ecd738
--- /dev/null
+++ b/src/context/cdtrail_hashmap_forward.h
@@ -0,0 +1,38 @@
+/*********************                                                        */
+/*! \file cdtrail_hashmap_forward.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief This is a forward declaration header to declare the
+ ** CDTrailHashMap<> template
+ **
+ ** This is a forward declaration header to declare the CDTrailHashMap<>
+ ** template.  It's useful if you want to forward-declare CDTrailHashMap<>
+ ** without including the full cdtrail_hash_map.h header, for example, in a
+ ** public header context.
+ **
+ ** For CDTrailHashMap<> in particular, it's difficult to forward-declare it
+ ** yourself, because it has a default template argument.
+ **/
+
+#include "cvc4_public.h"
+
+#pragma once
+
+namespace __gnu_cxx {
+  template <class Key> struct hash;
+}/* __gnu_cxx namespace */
+
+namespace CVC4 {
+  namespace context {
+    template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> >
+    class CDTrailHashMap;
+  }/* CVC4::context namespace */
+}/* CVC4 namespace */
+
diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h
index adccc0d55..a1b29ed47 100644
--- a/src/decision/justification_heuristic.h
+++ b/src/decision/justification_heuristic.h
@@ -49,7 +49,7 @@ class JustificationHeuristic : public ITEDecisionStrategy {
   typedef context::CDHashMap<TNode,TNode,TNodeHashFunction> SkolemMap;
 
   // being 'justified' is monotonic with respect to decisions
-  typedef context::CDHashSet<TNode,TNodeHashFunction> JustifiedSet;
+  typedef context::CDHashSet<Node,NodeHashFunction> JustifiedSet;
   JustifiedSet d_justified;
   context::CDO<unsigned>  d_prvsIndex;
 
@@ -107,8 +107,8 @@ public:
     d_visited.clear();
 
     if(Trace.isOn("justified")) {
-      for(JustifiedSet::iterator i = d_justified.begin();
-          i != d_justified.end(); ++i) {
+      for(JustifiedSet::key_iterator i = d_justified.key_begin();
+          i != d_justified.key_end(); ++i) {
         TNode n = *i;
         SatLiteral l = d_decisionEngine->hasSatLiteral(n) ?
           d_decisionEngine->getSatLiteral(n) : -1;
diff --git a/src/decision/relevancy.h b/src/decision/relevancy.h
index 8a6eb54ef..bfd30ddde 100644
--- a/src/decision/relevancy.h
+++ b/src/decision/relevancy.h
@@ -60,7 +60,7 @@ class Relevancy : public RelevancyStrategy {
   typedef hash_map<TNode,SatValue,TNodeHashFunction> PolarityCache;
 
   // being 'justified' is monotonic with respect to decisions
-  context::CDHashSet<TNode,TNodeHashFunction> d_justified;
+  context::CDHashSet<Node, NodeHashFunction> d_justified;
   context::CDO<unsigned>  d_prvsIndex;
 
   IntStat d_helfulness;
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 9f2138e9d..89cd731e9 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -108,11 +108,10 @@ void TseitinCnfStream::ensureLiteral(TNode n) {
   Debug("cnf") << "ensureLiteral(" << n << ")" << endl;
   if(hasLiteral(n)) {
     SatLiteral lit = getLiteral(n);
-    LiteralToNodeMap::iterator i = d_literalToNodeMap.find(lit);
-    if(i == d_literalToNodeMap.end()) {
+    if(!d_literalToNodeMap.contains(lit)){
       // Store backward-mappings
-      d_literalToNodeMap[lit] = n;
-      d_literalToNodeMap[~lit] = n.notNode();
+      d_literalToNodeMap.insert(lit, n);
+      d_literalToNodeMap.insert(~lit, n.notNode());
     }
     return;
   }
@@ -140,8 +139,9 @@ void TseitinCnfStream::ensureLiteral(TNode n) {
     lit = toCNF(n, false);
 
     // Store backward-mappings
-    d_literalToNodeMap[lit] = n;
-    d_literalToNodeMap[~lit] = n.notNode();
+    // These may already exist
+    d_literalToNodeMap.insert_safe(lit, n);
+    d_literalToNodeMap.insert_safe(~lit, n.notNode());
   } else {
     // We have a theory atom or variable.
     lit = convertAtom(n);
@@ -168,8 +168,8 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) {
     } else {
       lit = SatLiteral(d_satSolver->newVar(theoryLiteral));
     }
-    d_nodeToLiteralMap[node] = lit;
-    d_nodeToLiteralMap[node.notNode()] = ~lit;
+    d_nodeToLiteralMap.insert(node, lit);
+    d_nodeToLiteralMap.insert(node.notNode(), ~lit);
   } else {
     lit = getLiteral(node);
   }
@@ -178,8 +178,9 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) {
   if ( theoryLiteral || d_fullLitToNodeMap ||
        ( CVC4_USE_REPLAY && options::replayLog() != NULL ) ||
        (Dump.isOn("clauses")) ) {
-    d_literalToNodeMap[lit] = node;
-    d_literalToNodeMap[~lit] = node.notNode();
+
+    d_literalToNodeMap.insert_safe(lit, node);
+    d_literalToNodeMap.insert_safe(~lit, node.notNode());
   }
 
   // If a theory literal, we pre-register it
@@ -197,11 +198,8 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) {
 
 TNode CnfStream::getNode(const SatLiteral& literal) {
   Debug("cnf") << "getNode(" << literal << ")" << endl;
-  LiteralToNodeMap::iterator find = d_literalToNodeMap.find(literal);
-  Assert(find != d_literalToNodeMap.end());
-  Assert(d_nodeToLiteralMap.find((*find).second) != d_nodeToLiteralMap.end());
-  Debug("cnf") << "getNode(" << literal << ") => " << (*find).second << endl;
-  return (*find).second;
+  Debug("cnf") << "getNode(" << literal << ") => " << d_literalToNodeMap[literal] << endl;
+  return d_literalToNodeMap[literal];
 }
 
 void CnfStream::getBooleanVariables(std::vector<TNode>& outputVariables) const {
@@ -229,10 +227,9 @@ SatLiteral CnfStream::convertAtom(TNode node) {
 }
 
 SatLiteral CnfStream::getLiteral(TNode node) {
-  NodeToLiteralMap::iterator find = d_nodeToLiteralMap.find(node);
   Assert(!node.isNull(), "CnfStream: can't getLiteral() of null node");
-  Assert(find != d_nodeToLiteralMap.end(), "Literal not in the CNF Cache: %s\n", node.toString().c_str());
-  SatLiteral literal = (*find).second;
+  Assert(d_nodeToLiteralMap.contains(node), "Literal not in the CNF Cache: %s\n", node.toString().c_str());
+  SatLiteral literal = d_nodeToLiteralMap[node];
   Debug("cnf") << "CnfStream::getLiteral(" << node << ") => " << literal << std::endl;
   return literal;
 }
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 6ab639712..042cccd56 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -29,6 +29,7 @@
 #include "prop/theory_proxy.h"
 #include "prop/registrar.h"
 #include "context/cdlist.h"
+#include "context/cdinsert_hashmap.h"
 
 #include <ext/hash_map>
 
@@ -47,10 +48,10 @@ class CnfStream {
 public:
 
   /** Cache of what nodes have been registered to a literal. */
-  typedef context::CDHashMap<SatLiteral, TNode, SatLiteralHashFunction> LiteralToNodeMap;
+  typedef context::CDInsertHashMap<SatLiteral, TNode, SatLiteralHashFunction> LiteralToNodeMap;
 
   /** Cache of what literals have been registered to a node. */
-  typedef context::CDHashMap<Node, SatLiteral, NodeHashFunction> NodeToLiteralMap;
+  typedef context::CDInsertHashMap<Node, SatLiteral, NodeHashFunction> NodeToLiteralMap;
 
 protected:
 
diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp
index 5b8d3befc..9ae7cd1c2 100644
--- a/src/theory/arith/arith_static_learner.cpp
+++ b/src/theory/arith/arith_static_learner.cpp
@@ -145,8 +145,8 @@ void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet
     break;
   case CONST_RATIONAL:
     // Mark constants as minmax
-    d_minMap[n] = n.getConst<Rational>();
-    d_maxMap[n] = n.getConst<Rational>();
+    d_minMap.insert(n, n.getConst<Rational>());
+    d_maxMap.insert(n, n.getConst<Rational>());
     break;
   case OR: {
     // Look for things like "x = 0 OR x = 1" (that are defTrue) and
@@ -248,7 +248,7 @@ void ArithStaticLearner::iteConstant(TNode n, NodeBuilder<>& learned){
     DeltaRational min = std::min(first, second);
     CDNodeToMinMaxMap::const_iterator minFind = d_minMap.find(n);
     if (minFind == d_minMap.end() || (*minFind).second < min) {
-      d_minMap[n] = min;
+      d_minMap.insert(n, min);
       Node nGeqMin;
       if (min.getInfinitesimalPart() == 0) {
         nGeqMin = NodeBuilder<2>(kind::GEQ) << n << mkRationalNode(min.getNoninfinitesimalPart());
@@ -267,7 +267,7 @@ void ArithStaticLearner::iteConstant(TNode n, NodeBuilder<>& learned){
     DeltaRational max = std::max(first, second);
     CDNodeToMinMaxMap::const_iterator maxFind = d_maxMap.find(n);
     if (maxFind == d_maxMap.end() || (*maxFind).second > max) {
-      d_maxMap[n] = max;
+      d_maxMap.insert(n, max);
       Node nLeqMax;
       if (max.getInfinitesimalPart() == 0) {
         nLeqMax = NodeBuilder<2>(kind::LEQ) << n << mkRationalNode(max.getNoninfinitesimalPart());
@@ -398,7 +398,7 @@ void ArithStaticLearner::addBound(TNode n) {
     /* fall through */
   case kind::LEQ:
     if (maxFind == d_maxMap.end() || (*maxFind).second > bound) {
-      d_maxMap[n[0]] = bound;
+      d_maxMap.insert(n[0], bound);
       Debug("arith::static") << "adding bound " << n << endl;
     }
     break;
@@ -407,7 +407,7 @@ void ArithStaticLearner::addBound(TNode n) {
     /* fall through */
   case kind::GEQ:
     if (minFind == d_minMap.end() || (*minFind).second < bound) {
-      d_minMap[n[0]] = bound;
+      d_minMap.insert(n[0], bound);
       Debug("arith::static") << "adding bound " << n << endl;
     }
     break;
diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h
index b047018e8..0de28c5ab 100644
--- a/src/theory/arith/arith_static_learner.h
+++ b/src/theory/arith/arith_static_learner.h
@@ -27,7 +27,7 @@
 
 #include "context/context.h"
 #include "context/cdlist.h"
-#include "context/cdhashmap.h"
+#include "context/cdtrail_hashmap.h"
 #include <set>
 
 namespace CVC4 {
@@ -41,8 +41,7 @@ private:
    *  (=> _ (= x c))
    * where c is a constant.
    */
-  //typedef __gnu_cxx::hash_map<Node, std::set<Node>, NodeHashFunction> VarToNodeSetMap;
-  typedef context::CDHashMap<Node, Node, NodeHashFunction> CDNodeToNodeListMap;
+  typedef context::CDTrailHashMap<Node, Node, NodeHashFunction> CDNodeToNodeListMap;
   // The domain is an implicit list OR(x, OR(y, ..., FALSE ))
   // or FALSE
   CDNodeToNodeListMap d_miplibTrick;
@@ -50,8 +49,7 @@ private:
   /**
    * Map from a node to it's minimum and maximum.
    */
-  //typedef __gnu_cxx::hash_map<Node, DeltaRational, NodeHashFunction> NodeToMinMaxMap;
-  typedef context::CDHashMap<Node, DeltaRational, NodeHashFunction> CDNodeToMinMaxMap;
+  typedef context::CDTrailHashMap<Node, DeltaRational, NodeHashFunction> CDNodeToMinMaxMap;
   CDNodeToMinMaxMap d_minMap;
   CDNodeToMinMaxMap d_maxMap;
 
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 6ec6c7090..d2814348a 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -1369,7 +1369,7 @@ Constraint TheoryArith::constraintFromFactQueue(){
     if(assertion != reAssertion){
       Debug("arith::nf") << "getting non-nf assertion " << assertion << " |-> " <<  reAssertion << endl;
       Assert(constraint != NullConstraint);
-      d_assertionsThatDoNotMatchTheirLiterals[assertion] = constraint;
+      d_assertionsThatDoNotMatchTheirLiterals.insert(assertion, constraint);
     }
   }
 
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 6a83c501b..b791186cf 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -22,6 +22,7 @@
 #include "context/context.h"
 #include "context/cdlist.h"
 #include "context/cdhashset.h"
+#include "context/cdinsert_hashmap.h"
 #include "context/cdqueue.h"
 #include "expr/node.h"
 
@@ -135,7 +136,7 @@ private:
    * A superset of all of the assertions that currently are not the literal for
    * their constraint do not match constraint literals. Not just the witnesses.
    */
-  context::CDHashMap<TNode, Constraint, TNodeHashFunction> d_assertionsThatDoNotMatchTheirLiterals;
+  context::CDInsertHashMap<Node, Constraint, NodeHashFunction> d_assertionsThatDoNotMatchTheirLiterals;
 
   /**
    * (For the moment) the type hierarchy goes as:
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index a05d30517..aabd3a62d 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -537,7 +537,7 @@ EqualityStatus TheoryArrays::getEqualityStatus(TNode a, TNode b) {
 void TheoryArrays::computeCareGraph()
 {
   if (d_sharedArrays.size() > 0) {
-    context::CDHashSet<TNode, TNodeHashFunction>::iterator it1 = d_sharedArrays.begin(), it2, iend = d_sharedArrays.end();
+    CDNodeSet::key_iterator it1 = d_sharedArrays.key_begin(), it2, iend = d_sharedArrays.key_end();
     for (; it1 != iend; ++it1) {
       for (it2 = it1, ++it2; it2 != iend; ++it2) {
         if ((*it1).getType() != (*it2).getType()) {
@@ -1261,7 +1261,7 @@ void TheoryArrays::checkRowLemmas(TNode a, TNode b)
 
 void TheoryArrays::queueRowLemma(RowLemmaType lem)
 {
-  if (d_conflict || d_RowAlreadyAdded.count(lem) != 0) {
+  if (d_conflict || d_RowAlreadyAdded.contains(lem)) {
     return;
   }
   TNode a = lem.first;
@@ -1407,7 +1407,7 @@ void TheoryArrays::dischargeLemmas()
   for (unsigned count = 0; count < sz; ++count) {
     RowLemmaType l = d_RowQueue.front();
     d_RowQueue.pop();
-    if (d_RowAlreadyAdded.count(l) != 0) {
+    if (d_RowAlreadyAdded.contains(l)) {
       continue;
     }
 
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 240cfad9a..172482e71 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -333,8 +333,10 @@ class TheoryArrays : public Theory {
   context::CDQueue<RowLemmaType> d_RowQueue;
   context::CDHashSet<RowLemmaType, RowLemmaTypeHashFunction > d_RowAlreadyAdded;
 
-  context::CDHashSet<TNode, TNodeHashFunction> d_sharedArrays;
-  context::CDHashSet<TNode, TNodeHashFunction> d_sharedOther;
+  typedef context::CDHashSet<Node, NodeHashFunction> CDNodeSet;
+
+  CDNodeSet d_sharedArrays;
+  CDNodeSet d_sharedOther;
   context::CDO<bool> d_sharedTerms;
   context::CDList<TNode> d_reads;
   std::hash_map<TNode, Node, TNodeHashFunction> d_diseqCache;
diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h
index e62f9b7a1..aec0cff58 100644
--- a/src/theory/booleans/circuit_propagator.h
+++ b/src/theory/booleans/circuit_propagator.h
@@ -118,7 +118,7 @@ private:
 
   /** Nodes that have been attached already (computed forward edges for) */
   // All the nodes we've visited so far
-  context::CDHashSet<TNode, TNodeHashFunction> d_seen;
+  context::CDHashSet<Node, NodeHashFunction> d_seen;
 
   /**
    * Assignment status of each node.
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 0c8df3fca..e38f3568c 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -40,8 +40,8 @@ class TheoryBV : public Theory {
   context::Context* d_context;
 
   /** Context dependent set of atoms we already propagated */
-  context::CDHashSet<TNode, TNodeHashFunction> d_alreadyPropagatedSet;
-  context::CDHashSet<TNode, TNodeHashFunction> d_sharedTermsSet;
+  context::CDHashSet<Node, NodeHashFunction> d_alreadyPropagatedSet;
+  context::CDHashSet<Node, NodeHashFunction> d_sharedTermsSet;
 
   BitblastSolver d_bitblastSolver;
   EqualitySolver d_equalitySolver;
diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h
index 655918986..c7036a9ad 100644
--- a/src/theory/shared_terms_database.h
+++ b/src/theory/shared_terms_database.h
@@ -66,7 +66,7 @@ private:
   AlreadyNotifiedMap d_alreadyNotifiedMap;
 
   /** The registered equalities for propagation */
-  typedef context::CDHashSet<TNode, TNodeHashFunction> RegisteredEqualitiesSet;
+  typedef context::CDHashSet<Node, NodeHashFunction> RegisteredEqualitiesSet;
   RegisteredEqualitiesSet d_registeredEqualities;
 
 private:
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 063943056..27371eac3 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -190,7 +190,7 @@ class TheoryEngine {
    * context-dependent set of those theory-propagable literals that
    * have been propagated.
    */
-  context::CDHashSet<TNode, TNodeHashFunction> d_hasPropagated;
+  context::CDHashSet<Node, NodeHashFunction> d_hasPropagated;
 
   /**
    * Statistics for a particular theory.