* public/private code untangled (smt/smt_engine.h no longer #includes

  expr/node.h).  This removes the warnings we had during compilation,
  and heads off a number of potential linking errors due to improper
  inlining of private (library-only) stuff in client (out-of-library)
  code.

* "configure" now takes some options as part of a "bare-option" build
  type (e.g., "./configure debug-coverage" or "./configure production-muzzle").

* split cdo.h, cdlist.h, cdmap.h, and cdset.h from context.h

* split cdlist_black unit test from context_black

* implement CDMap<>.

* give ExprManagers ownership of the context (and have SmtEngine share
  that one)

* fix main driver to properly report file-not-found

* fix MemoryMappedInputBuffer class to report reasons for
  "errno"-returned system errors

* src/expr/attribute.h: context-dependent attribute kinds now
  supported

* test/unit/expr/node_white.h: context-dependent attribute tests

* src/prop/cnf_conversion.h and associated parts of src/util/options.h
  and src/main/getopt.cpp: obsolete command-line option, removed.

* src/util/Assert.h: assertions are now somewhat more useful (in debug
  builds, anyway) during stack unwinding.

* test/unit/theory/theory_black.h: test context-dependent behavior of
  registerTerm() attribute for theories

* src/expr/node_builder.h: formatting, fixes for arithmetic
  convenience node builders, check memory allocations

* test/unit/expr/node_builder_black.h: add tessts for addition,
  subtraction, unary minus, and multiplication convenience node
  builders

* src/expr/attribute.h: more comments

* (various) code formatting, comment cleanup, added throws specifier
  to some destructors

* contrib/code-checker: prototype perl script to test (some) code policy

* contrib/indent-settings: command line for GNU indent to indent using
  CVC4 style (sort of; this is a work in progress)

* COPYING: legal stuff

* DESIGN_QUESTIONS: obsolete, removed

9 files changed, 973 insertions, 451 deletions

diff --git a/src/context/Makefile.am b/src/context/Makefile.am
index b36d5e69c..54accdd6e 100644
--- a/src/context/Makefile.am
+++ b/src/context/Makefile.am
@@ -9,5 +9,8 @@ libcontext_la_SOURCES = \
 	context.cpp \
 	context.h \
 	context_mm.cpp \
-	context_mm.h
-
+	context_mm.h \
+	cdo.h \
+	cdlist.h \
+	cdmap.h \
+	cdset.h
diff --git a/src/context/cdlist.h b/src/context/cdlist.h
new file mode 100644
index 000000000..5b4ba639a
--- /dev/null
+++ b/src/context/cdlist.h
@@ -0,0 +1,222 @@
+/*********************                                                        */
+/** cdlist.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** Context-dependent list class.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__CONTEXT__CDLIST_H
+#define __CVC4__CONTEXT__CDLIST_H
+
+#include "context/context.h"
+#include "util/Assert.h"
+
+namespace CVC4 {
+namespace context {
+
+/**
+ * Generic context-dependent dynamic array.  Note that for efficiency, this
+ * implementation makes the following assumptions:
+ * 1. Over time, objects are only added to the list.  Objects are only
+ *    removed when a pop restores the list to a previous state.
+ * 2. T objects can safely be copied using their copy constructor,
+ *    operator=, and memcpy.
+ */
+template <class T>
+class CDList : public ContextObj {
+  /**
+   * d_list is a dynamic array of objects of type T.
+   */
+  T* d_list;
+
+  /**
+   * Whether to call the destructor when items are popped from the
+   * list.  True by default, but can be set to false by setting the
+   * second argument in the constructor to false.
+   */
+  bool d_callDestructor;
+
+  /**
+   * Number of objects in d_list
+   */
+  unsigned d_size;
+
+  /**
+   * Allocated size of d_list.
+   */
+  unsigned d_sizeAlloc;
+
+  /**
+   * Implementation of mandatory ContextObj method save: simply copies the
+   * current size 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) {
+    return new(pCMM) CDList<T>(*this);
+  }
+
+  /**
+   * 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) {
+    if(d_callDestructor) {
+      unsigned size = ((CDList<T>*)data)->d_size;
+      while(d_size != size) {
+        --d_size;
+        d_list[d_size].~T();
+      }
+    } else {
+      d_size = ((CDList<T>*)data)->d_size;
+    }
+  }
+
+  /**
+   * Privae 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.
+   */
+  CDList(const CDList<T>& l) :
+    ContextObj(l),
+    d_list(NULL),
+    d_size(l.d_size),
+    d_sizeAlloc(0) {
+  }
+
+  /**
+   * Reallocate the array with more space.
+   * Throws bad_alloc if memory allocation fails.
+   */
+  void grow() {
+    if(d_list == NULL) {
+      // Allocate an initial list if one does not yet exist
+      d_sizeAlloc = 10;
+      d_list = (T*) malloc(sizeof(T) * d_sizeAlloc);
+      if(d_list == NULL) {
+        throw std::bad_alloc();
+      }
+    } else {
+      // Allocate a new array with double the size
+      d_sizeAlloc *= 2;
+      T* tmpList = (T*) realloc(d_list, sizeof(T) * d_sizeAlloc);
+      if(tmpList == NULL) {
+        throw std::bad_alloc();
+      }
+      d_list = tmpList;
+    }
+  }
+
+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) { }
+
+  /**
+   * Destructor: delete the list
+   */
+  ~CDList() throw() {
+    if(d_list != NULL) {
+      if(d_callDestructor) {
+        while(d_size != 0) {
+          --d_size;
+          d_list[d_size].~T();
+        }
+      }
+      free(d_list);
+    }
+  }
+
+  /**
+   * Return the current size of (i.e. valid number of objects in) the list
+   */
+  unsigned size() const { return d_size; }
+
+
+  /**
+   * Return true iff there are no valid objects in the list.
+   */
+  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();
+    ::new((void*)(d_list + d_size)) T(data);
+    ++ d_size;
+  }
+
+  /**
+   * operator[]: return the ith item in the list
+   */
+  const T& operator[](unsigned i) const {
+    Assert(i < d_size, "index out of bounds in CDList::operator[]");
+    return d_list[i];
+  }
+
+  /**
+   * return 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];
+  }
+
+  /**
+   * Iterator for CDList class.  It has to be const because we don't allow
+   * items in the list to be changed.  It's a straightforward wrapper around a
+   * pointer.  Note that for efficiency, we implement only prefix increment and
+   * decrement.  Also note that it's OK to create an iterator from an empty,
+   * 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) {};
+  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; }
+    /** Prefix increment */
+    const_iterator& operator++() { ++d_it; return *this; }
+    /** Prefix decrement */
+    const_iterator& operator--() { --d_it; return *this; }
+  }; /* class const_iterator */
+
+  /**
+   * Returns an iterator pointing to the first item in the list.
+   */
+  const_iterator begin() const {
+    return const_iterator(d_list);
+  }
+
+  /**
+   * Returns an iterator pointing one past the last item in the list.
+   */
+  const_iterator end() const {
+    return const_iterator(d_list + d_size);
+  }
+
+};/* class CDList */
+
+}/* CVC4::context namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__CONTEXT__CDLIST_H */
diff --git a/src/context/cdmap.h b/src/context/cdmap.h
new file mode 100644
index 000000000..994ff76b4
--- /dev/null
+++ b/src/context/cdmap.h
@@ -0,0 +1,407 @@
+/*********************                                                        */
+/** cdmap.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** Context-dependent map class.  Generic templated class for a map
+ ** which must be saved and restored as contexts are pushed and
+ ** popped.  Requires that operator= be defined for the data class,
+ ** and operator== for the key class.  For key types that don't have a
+ ** __gnu_cxx::hash<>, you should provide an explicit HashFcn.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__CONTEXT__CDMAP_H
+#define __CVC4__CONTEXT__CDMAP_H
+
+#include "context/context.h"
+#include "util/Assert.h"
+
+#include <iterator>
+#include <ext/hash_map>
+
+namespace CVC4 {
+namespace context {
+
+// Auxiliary class: almost the same as CDO (see cdo.h), but on
+// setNull() call it erases itself from the map.
+
+template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> > class CDMap;
+
+template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> >
+class CDOmap : public ContextObj {
+  Key d_key;
+  Data d_data;
+  bool d_inMap; // whether the data must be in the map
+  CDMap<Key, Data, HashFcn>* d_cdmap;
+
+  // Doubly-linked list for keeping track of elements in order of insertion
+  CDOmap<Key, Data, HashFcn>* d_prev;
+  CDOmap<Key, Data, HashFcn>* d_next;
+
+  virtual ContextObj* save(ContextMemoryManager* pCMM) {
+    return new(pCMM) CDOmap<Key, Data, HashFcn>(*this);
+  }
+
+  virtual void restore(ContextObj* data) {
+    CDOmap<Key, Data, HashFcn>* p((CDOmap<Key, Data, HashFcn>*) data);
+    if(p->d_inMap) {
+      d_data = p->d_data;
+      d_inMap = true;
+    } else {
+      // Erase itself from the map and put itself into trash.  We cannot
+      // "delete this" here, because it will break context operations in
+      // a non-trivial way.
+      if(d_cdmap->d_map.count(d_key) > 0) {
+        d_cdmap->d_map.erase(d_key);
+        d_cdmap->d_trash.push_back(this);
+      }
+
+      d_prev->d_next = d_next;
+      d_next->d_prev = d_prev;
+
+      if(d_cdmap->d_first == this) {
+        d_cdmap->d_first = d_next;
+
+        if(d_next == this) {
+          d_cdmap->d_first = NULL;
+        }
+      }
+    }
+  }
+
+public:
+
+  CDOmap(Context* context,
+         CDMap<Key, Data, HashFcn>* cdmap,
+	 const Key& key,
+         const Data& data) :
+    ContextObj(context),
+    d_key(key),
+    d_inMap(false),
+    d_cdmap(cdmap) {
+
+    set(data);
+
+    CDOmap<Key, Data, HashFcn>*& first = d_cdmap->d_first;
+    if(first == NULL) {
+      first = d_next = d_prev = this;
+    } else {
+      d_prev = first->d_prev;
+      d_next = first;
+      d_prev->d_next = first->d_prev = this;
+    }
+  }
+
+  ~CDOmap() throw(AssertionException) {}
+
+  void set(const Data& data) {
+    makeCurrent();
+    d_data = data;
+    d_inMap = true;
+  }
+
+  const Key& getKey() const {
+    return d_key;
+  }
+
+  const Data& get() const {
+    return d_data;
+  }
+
+  operator Data() {
+    return get();
+  }
+
+  CDOmap<Key, Data, HashFcn>& operator=(const Data& data) {
+    set(data);
+    return *this;
+  }
+
+  CDOmap<Key, Data, HashFcn>* next() const {
+    if(d_next == d_cdmap->d_first) {
+      return NULL;
+    } else {
+      return d_next;
+    }
+  }
+};/* class CDOmap */
+
+// Dummy subclass of ContextObj to serve as our data class
+class CDMapData : public ContextObj {
+  // befriend CDMap<> so that it can allocate us
+  template <class Key, class Data, class HashFcn>
+  friend class CDMap;
+
+  ContextObj* save(ContextMemoryManager* pCMM) {
+    return new(pCMM) CDMapData(*this);
+  }
+
+  void restore(ContextObj* data) {}
+
+public:
+
+  CDMapData(Context* context) : ContextObj(context) {}
+  CDMapData(const ContextObj& co) : ContextObj(co) {}
+};
+
+/**
+ * Generic templated class for a map which must be saved and restored
+ * as contexts are pushed and popped.  Requires that operator= be
+ * defined for the data class, and operator== for the key class.
+ */
+template <class Key, class Data, class HashFcn>
+class CDMap : public ContextObj {
+
+  friend class CDOmap<Key, Data, HashFcn>;
+
+  __gnu_cxx::hash_map<Key, CDOmap<Key, Data, HashFcn>*, HashFcn> d_map;
+
+  // The vector of CDOmap objects to be destroyed
+  std::vector<CDOmap<Key, Data, HashFcn>*> d_trash;
+  CDOmap<Key, Data, HashFcn>* d_first;
+  Context* d_context;
+
+  // Nothing to save; the elements take care of themselves
+  virtual ContextObj* save(ContextMemoryManager* pCMM) {
+    return new(pCMM) CDMapData(*this);
+  }
+
+  // Similarly, nothing to restore
+  virtual void restore(ContextObj* data) {}
+
+  // Destroy stale CDOmap objects from trash
+  void emptyTrash() {
+    for(typename std::vector<CDOmap<Key, Data, HashFcn>*>::iterator
+          i = d_trash.begin(), iend = d_trash.end(); i != iend; ++i) {
+      /*
+        delete *i;
+        free(*i);
+      */
+    }
+    d_trash.clear();
+  }
+
+public:
+
+  CDMap(Context* context) :
+    ContextObj(context),
+    d_first(NULL),
+    d_context(context) {
+  }
+
+  ~CDMap() throw(AssertionException) {
+    // Delete all the elements and clear the map
+    for(typename __gnu_cxx::hash_map<Key, CDOmap<Key, Data, HashFcn>*, HashFcn>::iterator
+	  i = d_map.begin(), iend = d_map.end(); i != iend; ++i) {
+      /*
+        delete (*i).second;
+        free((*i).second);
+      */
+    }
+    d_map.clear();
+    emptyTrash();
+  }
+
+  // The usual operators of map
+
+  size_t size() const {
+    return d_map.size();
+  }
+
+  size_t count(const Key& k) const {
+    return d_map.count(k);
+  }
+
+  typedef CDOmap<Key, Data, HashFcn>& ElementReference;
+
+  // If a key is not present, a new object is created and inserted
+  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));
+
+    CDOmap<Key, Data, HashFcn>* obj;
+    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 {
+      obj = (*i).second;
+    }
+    return *obj;
+  }
+
+  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));
+
+    if(i == d_map.end()) { // Create new object
+      CDOmap<Key, Data, HashFcn>*
+	obj(new(true) CDOmap<Key, Data, HashFcn>(d_context, this, k, d));
+      d_map[k] = obj;
+    } else {
+      (*i).second->set(d);
+    }
+  }
+  // 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;
+
+  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 iterator& i) : d_it(i.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.
+    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++() {
+      d_it = d_it->next();
+      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<>::orderedIterator::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) {
+      Proxy e(*(*this));
+      ++(*this);
+      return e;
+    }
+  };/* class CDMap<>::orderedIterator */
+
+  orderedIterator orderedBegin() const {
+    return orderedIterator(d_first);
+  }
+
+  orderedIterator orderedEnd() const {
+    return orderedIterator(NULL);
+  }
+
+  iterator find(const Key& k) const {
+    return iterator(d_map.find(k));
+  }
+
+};/* class CDMap<> */
+
+}/* CVC4::context namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__CONTEXT__CDMAP_H */
diff --git a/src/context/cdo.h b/src/context/cdo.h
new file mode 100644
index 000000000..6c30a70f4
--- /dev/null
+++ b/src/context/cdo.h
@@ -0,0 +1,122 @@
+/*********************                                                        */
+/** cdo.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** A context-dependent object.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__CONTEXT__CDO_H
+#define __CVC4__CONTEXT__CDO_H
+
+#include "context/context.h"
+#include "util/Assert.h"
+
+namespace CVC4 {
+namespace context {
+
+/**
+ * Most basic template for context-dependent objects.  Simply makes a copy
+ * (using the copy constructor) of class T when saving, and copies it back
+ * (using operator=) during restore.
+ */
+template <class T>
+class CDO : public ContextObj {
+
+  /**
+   * The data of type T being stored in this context-dependent object.
+   */
+  T d_data;
+
+  /**
+   * Implementation of mandatory ContextObj method save: simply copies the
+   * current data to a copy using the copy constructor.  Memory is allocated
+   * using the ContextMemoryManager.
+   */
+  virtual ContextObj* save(ContextMemoryManager* pCMM) {
+    return new(pCMM) CDO<T>(*this);
+  }
+
+  /**
+   * Implementation of mandatory ContextObj method restore: simply copies the
+   * saved data back from the saved copy using operator= for T.
+   */
+  virtual void restore(ContextObj* pContextObj) {
+    d_data = ((CDO<T>*) pContextObj)->d_data;
+  }
+
+  /**
+   * Copy constructor - it's private to ensure it is only used by save().
+   * Basic CDO objects, cannot be copied-they have to be unique.
+   */
+  CDO(const CDO<T>& cdo) : ContextObj(cdo), d_data(cdo.d_data) {}
+
+  /**
+   * operator= for CDO is private to ensure CDO object is not copied.
+   */
+  CDO<T>& operator=(const CDO<T>& cdo) {}
+
+public:
+  /**
+   * Main constructor - uses default constructor for T to create the initial
+   * value of d_data.
+   */
+  CDO(Context* context) : ContextObj(context) {}
+
+  /**
+   * Constructor from object of type T.  Creates a ContextObj and sets the data
+   * to the given data value.  Note that this value is only valid in the
+   * current Scope.  If the Scope is popped, the value will revert to whatever
+   * is assigned by the default constructor for T
+   */
+  CDO(Context* context, const T& data) : ContextObj(context) {
+    makeCurrent();
+    d_data = data;
+  }
+
+  /**
+   * Destructor - no need to do anything.
+   */
+  ~CDO() throw() {}
+
+  /**
+   * Set the data in the CDO.  First call makeCurrent.
+   */
+  void set(const T& data) {
+    makeCurrent();
+    d_data = data;
+  }
+
+  /**
+   * Get the current data from the CDO.  Read-only.
+   */
+  const T& get() const { return d_data; }
+
+  /**
+   * For convenience, define operator T to be the same as get().
+   */
+  operator T() { return get(); }
+
+  /**
+   * For convenience, define operator= that takes an object of type T.
+   */
+  CDO<T>& operator=(const T& data) {
+    set(data);
+    return *this;
+  }
+
+};/* class CDO */
+
+}/* CVC4::context namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__CONTEXT__CDO_H */
diff --git a/src/context/cdset.h b/src/context/cdset.h
new file mode 100644
index 000000000..48ad12daa
--- /dev/null
+++ b/src/context/cdset.h
@@ -0,0 +1,33 @@
+/*********************                                                        */
+/** cdset.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** Context-dependent set class.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__CONTEXT__CDSET_H
+#define __CVC4__CONTEXT__CDSET_H
+
+#include "context/context.h"
+#include "util/Assert.h"
+
+namespace CVC4 {
+namespace context {
+
+template <class K, class HashFcn>
+class CDSet;
+
+}/* CVC4::context namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__CONTEXT__CDSET_H */
diff --git a/src/context/context.cpp b/src/context/context.cpp
index 5ff377194..8e87741b5 100644
--- a/src/context/context.cpp
+++ b/src/context/context.cpp
@@ -29,7 +29,7 @@ Context::Context() : d_pCNOpre(NULL), d_pCNOpost(NULL) {
 }
 
 
-Context::~Context() {
+Context::~Context() throw(AssertionException) {
   // Delete all Scopes
   popto(0);
 
@@ -38,13 +38,13 @@ Context::~Context() {
 
   // Clear ContextNotifyObj lists so there are no dangling pointers
   ContextNotifyObj* pCNO;
-  while (d_pCNOpre != NULL) {
+  while(d_pCNOpre != NULL) {
     pCNO = d_pCNOpre;
     pCNO->d_ppCNOprev = NULL;
     d_pCNOpre = pCNO->d_pCNOnext;
     pCNO->d_pCNOnext = NULL;
   }
-  while (d_pCNOpost != NULL) {
+  while(d_pCNOpost != NULL) {
     pCNO = d_pCNOpost;
     pCNO->d_ppCNOprev = NULL;
     d_pCNOpost = pCNO->d_pCNOnext;
@@ -69,7 +69,7 @@ void Context::pop() {
 
   // Notify the (pre-pop) ContextNotifyObj objects
   ContextNotifyObj* pCNO = d_pCNOpre;
-  while (pCNO != NULL) {
+  while(pCNO != NULL) {
     pCNO->notify();
     pCNO = pCNO->d_pCNOnext;
   }
@@ -88,7 +88,7 @@ void Context::pop() {
 
   // Notify the (post-pop) ContextNotifyObj objects
   pCNO = d_pCNOpost;
-  while (pCNO != NULL) {
+  while(pCNO != NULL) {
     pCNO->notify();
     pCNO = pCNO->d_pCNOnext;
   }
@@ -99,8 +99,8 @@ void Context::pop() {
 
 void Context::popto(int toLevel) {
   // Pop scopes until there are none left or toLevel is reached
-  if (toLevel < 0) toLevel = 0;
-  while (toLevel < getLevel()) pop();
+  if(toLevel < 0) toLevel = 0;
+  while(toLevel < getLevel()) pop();
 }
 
 
@@ -147,19 +147,17 @@ void ContextObj::update() {
 }
 
 
-ContextObj* ContextObj::restoreAndContinue()
-{
+ContextObj* ContextObj::restoreAndContinue() {
   // Variable to hold next object in list
   ContextObj* pContextObjNext;
 
   // Check the restore pointer.  If NULL, this must be the bottom Scope
-  if (d_pContextObjRestore == NULL) {
+  if(d_pContextObjRestore == NULL) {
     Assert(d_pScope == d_pScope->getContext()->getBottomScope(),
            "Expected bottom scope");
     pContextObjNext = d_pContextObjNext;
     // Nothing else to do
-  }
-  else {
+  } else {
     // Call restore to update the subclass data
     restore(d_pContextObjRestore);
 
@@ -177,48 +175,48 @@ ContextObj* ContextObj::restoreAndContinue()
 }
 
 
-ContextObj::ContextObj(Context* pContext)
-  : d_pContextObjRestore(NULL)
-{
+ContextObj::ContextObj(Context* pContext) :
+  d_pContextObjRestore(NULL) {
+
   Assert(pContext != NULL, "NULL context pointer");
+
   d_pScope = pContext->getBottomScope();
   d_pScope->addToChain(this);
 }
 
 
-ContextObj::~ContextObj()
-{
+ContextObj::~ContextObj() throw(AssertionException) {
   for(;;) {
-    if (next() != NULL) {
+    if(next() != NULL) {
       next()->prev() = prev();
     }
     *(prev()) = next();
-    if (d_pContextObjRestore == NULL) break;
+    if(d_pContextObjRestore == NULL) {
+      break;
+    }
     restoreAndContinue();
   }
 }
 
 
 ContextNotifyObj::ContextNotifyObj(Context* pContext, bool preNotify) {
-  if (preNotify) {
+  if(preNotify) {
     pContext->addNotifyObjPre(this);
-  }
-  else {
+  } else {
     pContext->addNotifyObjPost(this);
   }
 }
 
-ContextNotifyObj::~ContextNotifyObj()
-{
-  if (d_pCNOnext != NULL) {
+
+ContextNotifyObj::~ContextNotifyObj() throw(AssertionException) {
+  if(d_pCNOnext != NULL) {
     d_pCNOnext->d_ppCNOprev = d_ppCNOprev;
   }
-  if (d_ppCNOprev != NULL) {
+  if(d_ppCNOprev != NULL) {
     *(d_ppCNOprev) = d_pCNOnext;
   }
 }
 
-} /* CVC4::context namespace */
-
 
+} /* CVC4::context namespace */
 } /* CVC4 namespace */
diff --git a/src/context/context.h b/src/context/context.h
index 6a35945b7..4e10347d7 100644
--- a/src/context/context.h
+++ b/src/context/context.h
@@ -20,6 +20,7 @@
 
 #include "context/context_mm.h"
 #include "util/Assert.h"
+
 #include <cstdlib>
 #include <cstring>
 #include <new>
@@ -32,28 +33,27 @@ class Scope;
 class ContextObj;
 class ContextNotifyObj;
 
-  /**
-   * A Context encapsulates all of the dynamic state of the system.  Its main
-   * methods are push() and pop().  A call to push() saves the current state,
-   * and a call to pop() restores the state saved by the most recent call to
-   * push().
-   *
-   * Objects which want to participate in this global save and restore
-   * mechanism must inherit from ContextObj (see below).
-   *
-   * For more flexible context-dependent behavior, objects may implement the
-   * ContextNotifyObj interface and simply get a notification when a pop has
-   * occurred.
-   *
-   * Context also uses a helper class called Scope which stores information
-   * specific to the portion of the Context since the last call to push() (see
-   * below).
-   *
-   * Memory allocation in Contexts is done with the help of the
-   * ContextMemoryManager.  A copy is stored in each Scope object for quick
-   * access.
-   *
-   */
+/**
+ * A Context encapsulates all of the dynamic state of the system.  Its main
+ * methods are push() and pop().  A call to push() saves the current state,
+ * and a call to pop() restores the state saved by the most recent call to
+ * push().
+ *
+ * Objects which want to participate in this global save and restore
+ * mechanism must inherit from ContextObj (see below).
+ *
+ * For more flexible context-dependent behavior, objects may implement the
+ * ContextNotifyObj interface and simply get a notification when a pop has
+ * occurred.
+ *
+ * Context also uses a helper class called Scope which stores information
+ * specific to the portion of the Context since the last call to push() (see
+ * below).
+ *
+ * Memory allocation in Contexts is done with the help of the
+ * ContextMemoryManager.  A copy is stored in each Scope object for quick
+ * access.
+ */
 class Context {
 
   /**
@@ -87,7 +87,7 @@ public:
   /**
    * Destructor: pop all scopes, delete ContextMemoryManager
    */
-  ~Context();
+  ~Context() throw(AssertionException);
 
   /**
    * Return the current (top) scope
@@ -107,7 +107,7 @@ public:
   /**
    * Return the ContextMemoryManager associated with the context.
    */
-  ContextMemoryManager* getCMM(){ return d_pCMM; }
+  ContextMemoryManager* getCMM() { return d_pCMM; }
 
   /**
    * Save the current state, create a new Scope
@@ -182,15 +182,18 @@ public:
    * Constructor: Create a new Scope; set the level and the previous Scope
    * if any.
    */
-  Scope(Context* pContext, ContextMemoryManager* pCMM, int level)
-    : d_pContext(pContext), d_pCMM(pCMM), d_level(level),
-      d_pContextObjList(NULL) { }
+  Scope(Context* pContext, ContextMemoryManager* pCMM, int level) :
+    d_pContext(pContext),
+    d_pCMM(pCMM),
+    d_level(level),
+    d_pContextObjList(NULL) {
+  }
 
   /**
    * Destructor: Restore all of the objects in ContextObjList.  Defined inline
    * below.
    */
-  ~Scope();
+  ~Scope() throw();
 
   /**
    * Get the Context for this Scope
@@ -223,8 +226,9 @@ public:
    * Overload operator new for use with ContextMemoryManager to allow creation
    * of new Scope objects in the current memory region.
    */
-  static void* operator new(size_t size, ContextMemoryManager* pCMM)
-    { return pCMM->newData(size); }
+  static void* operator new(size_t size, ContextMemoryManager* pCMM) {
+    return pCMM->newData(size);
+  }
 
   /**
    * Overload operator delete for Scope objects allocated using
@@ -232,44 +236,44 @@ public:
    * automatically when the ContextMemoryManager pop() method is called.
    * Include both placement and standard delete for completeness.
    */
-  static void operator delete(void* pMem, ContextMemoryManager* pCMM) { }
-  static void operator delete(void* pMem) { }
+  static void operator delete(void* pMem, ContextMemoryManager* pCMM) {}
+  static void operator delete(void* pMem) {}
 
   //FIXME:  //! Check for memory leaks
   //  void check(void);
 
-}; /* class Scope */
-
-  /**
-   * This is an abstract base class from which all objects that are context-dependent
-   * should inherit.  For any data structure that you want to have be
-   * automatically backtracked, do the following:
-   * 1. Create a class for the data structure that inherits from ContextObj
-   * 2. Implement save()
-   *    The role of save() is to create a new ContexObj object that contains
-   *    enough information to restore the object to its current state, even if
-   *    it gets changed later.  Note that save should call the (default)
-   *    ContextObj Copy Constructor to copy the information in the base class.
-   *    It is recommended that any memory allocated by save() should be done
-   *    through the ContextMemoryManager.  This way, it does not need to be
-   *    explicitly freed when restore is called.  However, it is only required
-   *    that the ContextObj itself be allocated using the
-   *    ContextMemoryManager.  If other memory is allocated not using the
-   *    ContextMemoryManager, it should be freed when restore() is called.  In
-   *    fact, any clean-up work on a saved object must be done by restore().
-   *    This is because the destructor is never called explicitly on saved
-   *    objects.
-   * 3. Implement restore()
-   *    The role of restore() is, given the ContextObj returned by a previous
-   *    call to save(), to restore the current object to the state it was in
-   *    when save() was called.  Note that the implementation of restore does
-   *    *not* need to worry about restoring the base class data.  This is done
-   *    automatically.  Ideally, restore() should not have to free any memory
-   *    as any memory allocated by save() should have been done using the
-   *    ContextMemoryManager (see item 2 above).
-   * 4. In the subclass implementation, any time the state is about to be
-   *    changed, first call makeCurrent().
-   */
+};/* class Scope */
+
+/**
+ * This is an abstract base class from which all objects that are context-dependent
+ * should inherit.  For any data structure that you want to have be
+ * automatically backtracked, do the following:
+ * 1. Create a class for the data structure that inherits from ContextObj
+ * 2. Implement save()
+ *    The role of save() is to create a new ContexObj object that contains
+ *    enough information to restore the object to its current state, even if
+ *    it gets changed later.  Note that save should call the (default)
+ *    ContextObj Copy Constructor to copy the information in the base class.
+ *    It is recommended that any memory allocated by save() should be done
+ *    through the ContextMemoryManager.  This way, it does not need to be
+ *    explicitly freed when restore is called.  However, it is only required
+ *    that the ContextObj itself be allocated using the
+ *    ContextMemoryManager.  If other memory is allocated not using the
+ *    ContextMemoryManager, it should be freed when restore() is called.  In
+ *    fact, any clean-up work on a saved object must be done by restore().
+ *    This is because the destructor is never called explicitly on saved
+ *    objects.
+ * 3. Implement restore()
+ *    The role of restore() is, given the ContextObj returned by a previous
+ *    call to save(), to restore the current object to the state it was in
+ *    when save() was called.  Note that the implementation of restore does
+ *    *not* need to worry about restoring the base class data.  This is done
+ *    automatically.  Ideally, restore() should not have to free any memory
+ *    as any memory allocated by save() should have been done using the
+ *    ContextMemoryManager (see item 2 above).
+ * 4. In the subclass implementation, any time the state is about to be
+ *    changed, first call makeCurrent().
+ */
 class ContextObj {
   /**
    * Pointer to Scope in which this object was last modified.
@@ -325,6 +329,7 @@ class ContextObj {
   ContextObj* restoreAndContinue();
 
 protected:
+
   /**
    * This is a method that must be implemented by all classes inheriting from
    * ContextObj.  See the comment before the class declaration.
@@ -341,57 +346,70 @@ protected:
    * This method checks if the object has been modified in this Scope yet.  If
    * not, it calls update().
    */
-  void makeCurrent() { if (!(d_pScope->isCurrent())) update(); }
+  void makeCurrent() {
+    if(!(d_pScope->isCurrent())) {
+      update();
+    }
+  }
 
   /**
-   * operator new using ContextMemoryManager (common case used by subclasses
-   * during save() ).  No delete is required for memory allocated this way,
-   * since it is automatically released when the context is popped.  Also note
-   * that allocations using this operator never have their destructor called,
-   * so any clean-up has to be done using the restore method.
+   * operator new using ContextMemoryManager (common case used by
+   * subclasses during save() ).  No delete is required for memory
+   * allocated this way, since it is automatically released when the
+   * context is popped.  Also note that allocations using this
+   * operator never have their destructor called, so any clean-up has
+   * to be done using the restore method.
    */
   static void* operator new(size_t size, ContextMemoryManager* pCMM) {
     return pCMM->newData(size);
   }
 
   /**
-   * Corresponding placement delete.  Note that this is provided just to
-   * satisfy the requirement that a placement delete should be provided for
-   * every placement new.  It would only be called if a ContextObj Constructor
-   * throws an exception after a successful call to the above new operator.
+   * Corresponding placement delete.  Note that this is provided just
+   * to satisfy the requirement that a placement delete should be
+   * provided for every placement new.  It would only be called if a
+   * ContextObj constructor throws an exception after a successful
+   * call to the above new operator.
    */
-  static void operator delete(void* pMem, ContextMemoryManager* pCMM) { }
+  static void operator delete(void* pMem, ContextMemoryManager* pCMM) {}
 
 public:
+
   /**
    * Create a new ContextObj.  The initial scope is set to the bottom
-   * scope of the Context.  Note that in the common case, the copy constructor
-   * is called to create new ContextObj objects.  The default copy constructor
-   * does the right thing, so we do not explicitly define it.
+   * scope of the Context.  Note that in the common case, the copy
+   * constructor is called to create new ContextObj objects.  The
+   * default copy constructor does the right thing, so we do not
+   * explicitly define it.
    */
   ContextObj(Context* context);
 
   /**
-   * Destructor: Calls restore until restored to initial version.  Also removes
-   * object from all Scope lists.  Note that this doesn't actually free the
-   * memory allocated by the ContextMemoryManager for this object.  This isn't
-   * done until the corresponding Scope is popped.
+   * Destructor: Calls restore until restored to initial version.
+   * Also removes object from all Scope lists.  Note that this doesn't
+   * actually free the memory allocated by the ContextMemoryManager
+   * for this object.  This isn't done until the corresponding Scope
+   * is popped.
    */
-  virtual ~ContextObj();
+  virtual ~ContextObj() throw(AssertionException);
 
   /**
-   * If you want to allocate a ContextObj object on the heap, use this special
-   * new operator.  To free this memory, instead of "delete p", use
-   * "p->deleteSelf()".
+   * If you want to allocate a ContextObj object on the heap, use this
+   * special new operator.  To free this memory, instead of
+   * "delete p", use "p->deleteSelf()".
    */
-  static void* operator new(size_t size, bool) { return ::operator new(size); }
+  static void* operator new(size_t size, bool) {
+    return ::operator new(size);
+  }
 
   /**
-   * Corresponding placement delete.  Note that this is provided for the
-   * compiler in case the ContextObj constructor throws an exception.  The
-   * client can't call it.
+   * Corresponding placement delete.  Note that this is provided for
+   * the compiler in case the ContextObj constructor throws an
+   * exception.  The client can't call it.
    */
-  static void operator delete(void* pMem, bool) { ::operator delete(pMem); }
+  static void operator delete(void* pMem, bool) {
+    ::operator delete(pMem);
+  }
 
   /**
    * Use this instead of delete to delete memory allocated using the special
@@ -399,7 +417,9 @@ public:
    * function on memory allocated using the new that takes a
    * ContextMemoryManager as an argument.
    */
-  void deleteSelf() { ::operator delete(this); }
+  void deleteSelf() {
+    ::operator delete(this);
+  }
 
   /**
    * Disable delete: objects allocated with new(ContextMemorymanager) should
@@ -407,23 +427,23 @@ public:
    * calling deleteSelf().
    */
   static void operator delete(void* pMem) {
-    AlwaysAssert(false, "Not Allowed!");
+    AlwaysAssert(false, "It is not allowed to delete a ContextObj this way!");
   }
 
-}; /* class ContextObj */
+};/* 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 remaining
-   * ContextNotifyObj can be removed from the Context list.
+   * Context is our friend so that when the Context is deleted, any
+   * remaining ContextNotifyObj can be removed from the Context list.
    */
   friend class Context;
 
@@ -451,18 +471,19 @@ class ContextNotifyObj {
 
 public:
   /**
-   * Constructor for ContextNotifyObj.  Parameters are the context to which
-   * this notify object will be added, and a flag which, if true, tells the
-   * context to notify this object *before* the ContextObj objects are
-   * restored.  Otherwise, the context notifies the object after the ContextObj
-   * objects are restored.  The default is for notification after.
+   * Constructor for ContextNotifyObj.  Parameters are the context to
+   * which this notify object will be added, and a flag which, if
+   * true, tells the context to notify this object *before* the
+   * ContextObj objects are restored.  Otherwise, the context notifies
+   * the object after the ContextObj objects are restored.  The
+   * default is for notification after.
    */
   ContextNotifyObj(Context* pContext, bool preNotify = false);
 
   /**
    * Destructor: removes object from list
    */
-  virtual ~ContextNotifyObj();
+  virtual ~ContextNotifyObj() throw(AssertionException);
 
   /**
    * This is the method called to notify the object of a pop.  It must be
@@ -473,11 +494,11 @@ public:
 
 // Inline functions whose definitions had to be delayed:
 
-inline Scope::~Scope() {
+inline Scope::~Scope() throw() {
   // Call restore() method on each ContextObj object in the list.
-  // Note that it is the responsibility of restore() to return the next item in
-  // the list.
-  while (d_pContextObjList != NULL) {
+  // Note that it is the responsibility of restore() to return the
+  // next item in the list.
+  while(d_pContextObjList != NULL) {
     d_pContextObjList = d_pContextObjList->restoreAndContinue();
   }
 }
@@ -490,290 +511,7 @@ inline void Scope::addToChain(ContextObj* pContextObj) {
   d_pContextObjList = pContextObj;
 }
 
-  /**
-   * Most basic template for context-dependent objects.  Simply makes a copy
-   * (using the copy constructor) of class T when saving, and copies it back
-   * (using operator=) during restore.
-   */
-template <class T>
-class CDO :public ContextObj {
-
-  /**
-   * The data of type T being stored in this context-dependent object.
-   */
-  T d_data;
-
-  /**
-   * Implementation of mandatory ContextObj method save: simply copies the
-   * current data to a copy using the copy constructor.  Memory is allocated
-   * using the ContextMemoryManager.
-   */
-  virtual ContextObj* save(ContextMemoryManager* pCMM) {
-    return new(pCMM) CDO<T>(*this);
-  }
-
-  /**
-   * Implementation of mandatory ContextObj method restore: simply copies the
-   * saved data back from the saved copy using operator= for T.
-   */
-  virtual void restore(ContextObj* pContextObj) {
-    d_data = ((CDO<T>*)pContextObj)->d_data;
-  }
-
-  /**
-   * Copy constructor - it's private to ensure it is only used by save().
-   * Basic CDO objects, cannot be copied-they have to be unique.
-   */
-  CDO(const CDO<T>& cdo): ContextObj(cdo), d_data(cdo.d_data) { }
-
-  /**
-   * operator= for CDO is private to ensure CDO object is not copied.
-   */
-  CDO<T>& operator=(const CDO<T>& cdo) {}
-
-public:
-  /**
-   * Main constructor - uses default constructor for T to create the initial
-   * value of d_data.
-   */
-  CDO(Context* context) : ContextObj(context) {}
-
-  /**
-   * Constructor from object of type T.  Creates a ContextObj and sets the data
-   * to the given data value.  Note that this value is only valid in the
-   * current Scope.  If the Scope is popped, the value will revert to whatever
-   * is assigned by the default constructor for T
-   */
-  CDO(Context* context, const T& data) : ContextObj(context) {
-    makeCurrent(); d_data = data;
-  }
-
-  /**
-   * Destructor - no need to do anything.
-   */
-  ~CDO() {}
-
-  /**
-   * Set the data in the CDO.  First call makeCurrent.
-   */
-  void set(const T& data) { makeCurrent(); d_data = data; }
-
-  /**
-   * Get the current data from the CDO.  Read-only.
-   */
-  const T& get() const { return d_data; }
-
-  /**
-   * For convenience, define operator T to be the same as get().
-   */
-  operator T() { return get(); }
-
-  /**
-   * For convenience, define operator= that takes an object of type T.
-   */
-  CDO<T>& operator=(const T& data) { set(data); return *this; }
-
-}; /* class CDO */
-
-  /**
-   * Generic context-dependent dynamic array.  Note that for efficiency, this
-   * implementation makes the following assumptions:
-   * 1. Over time, objects are only added to the list.  Objects are only
-   *    removed when a pop restores the list to a previous state.
-   * 2. T objects can safely be copied using their copy constructor,
-   *    operator=, and memcpy.
-   */
-template <class T>
-class CDList :public ContextObj {
-  /**
-   * d_list is a dynamic array of objects of type T.
-   */
-  T* d_list;
-
-  /**
-   * Whether to call the destructor when items are popped from the
-   * list.  True by default, but can be set to false by setting the
-   * second argument in the constructor to false.
-   */
-  bool d_callDestructor;
-
-  /**
-   * Number of objects in d_list
-   */
-  unsigned d_size;
-
-  /**
-   * Allocated size of d_list.
-   */
-  unsigned d_sizeAlloc;
-
-  /**
-   * Implementation of mandatory ContextObj method save: simply copies the
-   * current size 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) {
-    return new(pCMM) CDList<T>(*this);
-  }
-
-  /**
-   * 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) {
-    if (d_callDestructor) {
-      unsigned size = ((CDList<T>*)data)->d_size;
-      while (d_size != size) {
-        --d_size;
-        d_list[d_size].~T();
-      }
-    }
-    else {
-      d_size = ((CDList<T>*)data)->d_size;
-    }
-  }
-
-  /**
-   * Privae 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.
-   */
-  CDList(const CDList<T>& l): ContextObj(l), d_list(NULL),
-                              d_size(l.d_size), d_sizeAlloc(0) { }
-
-  /**
-   * Reallocate the array with more space.
-   * Throws bad_alloc if memory allocation fails.
-   */
-  void grow() {
-    if (d_list == NULL) {
-      // Allocate an initial list if one does not yet exist
-      d_sizeAlloc = 10;
-      d_list = (T*)malloc(sizeof(T)*d_sizeAlloc);
-      if(d_list == NULL){
-        throw std::bad_alloc();
-      }
-    }
-    else {
-      // Allocate a new array with double the size
-      d_sizeAlloc *= 2;
-      T* tmpList = (T*)realloc(d_list, sizeof(T)*d_sizeAlloc);
-      if(tmpList == NULL){
-        throw std::bad_alloc();
-      }
-      d_list = tmpList;
-    }
-  }
-
-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) { }
-
-  /**
-   * Destructor: delete the list
-   */
-  ~CDList() {
-    if(d_list != NULL) {
-      if (d_callDestructor) {
-        while (d_size != 0) {
-          --d_size;
-          d_list[d_size].~T();
-        }
-      }
-      delete d_list;
-    }
-  }
-
-  /**
-   * Return the current size of (i.e. valid number of objects in) the list
-   */
-  unsigned size() const { return d_size; }
-
-
-  /**
-   * Return true iff there are no valid objects in the list.
-   */
-  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();
-    ::new((void*)(d_list + d_size)) T(data);
-    ++ d_size;
-  }
-
-  /**
-   * operator[]: return the ith item in the list
-   */
-  const T& operator[](unsigned i) const {
-    Assert(i < d_size, "index out of bounds in CDList::operator[]");
-    return d_list[i];
-  }
-
-  /**
-   * return 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];
-  }
-
-  /**
-   * Iterator for CDList class.  It has to be const because we don't allow
-   * items in the list to be changed.  It's a straightforward wrapper around a
-   * pointer.  Note that for efficiency, we implement only prefix increment and
-   * decrement.  Also note that it's OK to create an iterator from an empty,
-   * 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) {};
-  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; }
-    /** Prefix increment */
-    const_iterator& operator++() { ++d_it; return *this; }
-    /** Prefix decrement */
-    const_iterator& operator--() { --d_it; return *this; }
-  }; /* class const_iterator */
-
-  /**
-   * Returns an iterator pointing to the first item in the list.
-   */
-  const_iterator begin() const {
-    return const_iterator(d_list);
-  }
-
-  /**
-   * Returns an iterator pointing one past the last item in the list.
-   */
-  const_iterator end() const {
-    return const_iterator(d_list + d_size);
-  }
-
-}; /* class CDList */
-
-template <class T>
-class CDMap;
-
-template <class T>
-class CDSet;
-
-} /* CVC4::context namespace */
-
-} /* CVC4 namespace */
+}/* CVC4::context namespace */
+}/* CVC4 namespace */
 
 #endif /* __CVC4__CONTEXT__CONTEXT_H */
-
diff --git a/src/context/context_mm.cpp b/src/context/context_mm.cpp
index df7d82987..ab81c7486 100644
--- a/src/context/context_mm.cpp
+++ b/src/context/context_mm.cpp
@@ -32,9 +32,9 @@ void ContextMemoryManager::newChunk() {
          "Index should be at the end of the list");
 
   // Create new chunk if no free chunk available
-  if (d_freeChunks.empty()) {
+  if(d_freeChunks.empty()) {
     d_chunkList.push_back((char*)malloc(chunkSizeBytes));
-    if (d_chunkList.back() == NULL) {
+    if(d_chunkList.back() == NULL) {
       throw std::bad_alloc();
     }
   }
@@ -53,31 +53,32 @@ ContextMemoryManager::ContextMemoryManager() : d_indexChunkList(0) {
   // Create initial chunk
   d_chunkList.push_back((char*)malloc(chunkSizeBytes));
   d_nextFree = d_chunkList.back();
-  if (d_nextFree == NULL) {
+  if(d_nextFree == NULL) {
     throw std::bad_alloc();
   }
   d_endChunk = d_nextFree + chunkSizeBytes;
 }
 
 
-ContextMemoryManager::~ContextMemoryManager() {
+ContextMemoryManager::~ContextMemoryManager() throw() {
   // Delete all chunks
-  while (!d_chunkList.empty()) {
+  while(!d_chunkList.empty()) {
     free(d_chunkList.back());
     d_chunkList.pop_back();
   }
-  while (!d_freeChunks.empty()) {
+  while(!d_freeChunks.empty()) {
     free(d_freeChunks.back());
     d_freeChunks.pop_back();
   }
 }
 
+
 void* ContextMemoryManager::newData(size_t size) {
   // Use next available free location in current chunk
   void* res = (void*)d_nextFree;
   d_nextFree += size;
   // Check if the request is too big for the chunk
-  if (d_nextFree > d_endChunk) {
+  if(d_nextFree > d_endChunk) {
     newChunk();
     res = (void*)d_nextFree;
     d_nextFree += size;
@@ -104,7 +105,7 @@ void ContextMemoryManager::pop() {
   d_endChunkStack.pop_back();
 
   // Free all the new chunks since the last push
-  while (d_indexChunkList > d_indexChunkListStack.back()) {
+  while(d_indexChunkList > d_indexChunkListStack.back()) {
     d_freeChunks.push_back(d_chunkList.back());
     d_chunkList.pop_back();
     --d_indexChunkList;
@@ -112,7 +113,7 @@ void ContextMemoryManager::pop() {
   d_indexChunkListStack.pop_back();
 
   // Delete excess free chunks
-  while (d_freeChunks.size() > maxFreeChunks) {
+  while(d_freeChunks.size() > maxFreeChunks) {
     free(d_freeChunks.front());
     d_freeChunks.pop_front();
   }
@@ -120,6 +121,4 @@ void ContextMemoryManager::pop() {
 
 
 } /* CVC4::context namespace */
-
-
 } /* CVC4 namespace */
diff --git a/src/context/context_mm.h b/src/context/context_mm.h
index c4e5aba4f..04b0c8167 100644
--- a/src/context/context_mm.h
+++ b/src/context/context_mm.h
@@ -25,17 +25,16 @@
 namespace CVC4 {
 namespace context {
 
-
-  /**
-   * Region-based memory manager for contexts.  Calls to newData provide memory
-   * from the current region.  This memory will persist until the entire
-   * region is deallocated (by calling pop).
-   *
-   * If push is called, the current region is deactivated and pushed on a
-   * stack, and a new current region is created.  A subsequent call to pop
-   * releases the new region and restores the top region from the stack.
-   *
-   */
+/**
+ * Region-based memory manager for contexts.  Calls to newData provide memory
+ * from the current region.  This memory will persist until the entire
+ * region is deallocated (by calling pop).
+ *
+ * If push is called, the current region is deactivated and pushed on a
+ * stack, and a new current region is created.  A subsequent call to pop
+ * releases the new region and restores the top region from the stack.
+ *
+ */
 class ContextMemoryManager {
 
   /**
@@ -102,6 +101,7 @@ class ContextMemoryManager {
   void newChunk();
 
  public:
+
   /**
    * Constructor - creates an initial region and an empty stack
    */
@@ -110,7 +110,7 @@ class ContextMemoryManager {
   /**
    * Destructor - deletes all memory in all regions
    */
-  ~ContextMemoryManager();
+  ~ContextMemoryManager() throw();
 
   /**
    * Allocate size bytes from the current region
@@ -128,7 +128,7 @@ class ContextMemoryManager {
    */
   void pop();
 
-}; /* class ContextMemoryManager */
+};/* class ContextMemoryManager */
 
 }/* CVC4::context namespace */
 }/* CVC4 namespace */