Some items from the CVC4 public interface review:

* rename DeclarationScope to SymbolTable
* rename all HashStrategy -> HashFunction (which we often have anyways)
* remove CDCircList (no one is currently using it)

42 files changed, 230 insertions, 959 deletions

diff --git a/src/context/Makefile.am b/src/context/Makefile.am
index d979a9c16..e7f1dc68b 100644
--- a/src/context/Makefile.am
+++ b/src/context/Makefile.am
@@ -20,10 +20,8 @@ libcontext_la_SOURCES = \
 	cdhashmap_forward.h \
 	cdhashset.h \
 	cdhashset_forward.h \
-	cdcirclist.h \
-	cdcirclist_forward.h \
 	cdvector.h \
 	cdmaybe.h \
 	stacking_map.h \
 	stacking_vector.h \
-	cddense_set.h
\ No newline at end of file
+	cddense_set.h
diff --git a/src/context/cdcirclist.h b/src/context/cdcirclist.h
deleted file mode 100644
index cc6b60217..000000000
--- a/src/context/cdcirclist.h
+++ /dev/null
@@ -1,418 +0,0 @@
-/*********************                                                        */
-/*! \file cdcirclist.h
- ** \verbatim
- ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  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.\endverbatim
- **
- ** \brief Context-dependent circular list class
- **
- ** Context-dependent circular list class.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__CONTEXT__CDCIRCLIST_H
-#define __CVC4__CONTEXT__CDCIRCLIST_H
-
-#include <iterator>
-#include <memory>
-#include <string>
-#include <sstream>
-
-#include "context/context.h"
-#include "context/context_mm.h"
-#include "context/cdcirclist_forward.h"
-#include "context/cdo.h"
-#include "util/Assert.h"
-
-namespace CVC4 {
-namespace context {
-
-// CDO for pointers in particular, adds * and -> operators
-template <class T>
-class CDPtr : public CDO<T*> {
-  typedef CDO<T*> super;
-
-  // private copy ctor
-  CDPtr(const CDPtr<T>& cdptr) :
-    super(cdptr) {
-  }
-
-public:
-
-  CDPtr(Context* context, T* data = NULL) :
-    super(context, data) {
-  }
-
-  CDPtr(bool allocatedInCMM, Context* context, T* data = NULL) :
-    super(allocatedInCMM, context, data) {
-  }
-
-  // undesirable to put this here, since CDO<> does it already (?)
-  virtual ~CDPtr() throw(AssertionException) { this->destroy(); }
-
-  virtual ContextObj* save(ContextMemoryManager* pCMM) {
-    Debug("context") << "save cdptr " << this << " (value " << super::get() << ")";
-    ContextObj* p = new(pCMM) CDPtr<T>(*this);
-    Debug("context") << " to " << p << std::endl;
-    return p;
-  }
-
-  virtual void restore(ContextObj* pContextObj) {
-    Debug("context") << "restore cdptr " << this << " (using " << pContextObj << ") from " << super::get();
-    this->super::restore(pContextObj);
-    Debug("context") << " to " << super::get() << std::endl;
-  }
-
-  CDPtr<T>& operator=(T* data) {
-    Debug("context") << "set " << this << " from " << super::get();
-    super::set(data);
-    Debug("context") << " to " << super::get() << std::endl;
-    return *this;
-  }
-  // assignment is just like using the underlying ptr
-  CDPtr<T>& operator=(const CDPtr<T>& cdptr) {
-    return *this = cdptr.get();
-  }
-
-  T& operator*() { return *super::get(); }
-  T* operator->() { return super::get(); }
-  const T& operator*() const { return *super::get(); }
-  const T* operator->() const { return super::get(); }
-};/* class CDPtr<T> */
-
-
-/**
- * Class representing a single link in a CDCircList<>.
- *
- * The underlying T object is immutable, only the structure of the
- * list is mutable, so only that's backtracked.
- */
-template <class T, class AllocatorT>
-class CDCircElement {
-  typedef CDCircElement<T, AllocatorT> elt_t;
-  const T d_t;
-  CDPtr<elt_t> d_prev;
-  CDPtr<elt_t> d_next;
-  friend class CDCircList<T, AllocatorT>;
-public:
-  CDCircElement(Context* context, const T& t,
-                elt_t* prev = NULL, elt_t* next = NULL) :
-    d_t(t),
-    d_prev(true, context, prev),
-    d_next(true, context, next) {
-  }
-
-  CDPtr<elt_t>& next() { return d_next; }
-  CDPtr<elt_t>& prev() { return d_prev; }
-  elt_t* next() const { return d_next; }
-  elt_t* prev() const { return d_prev; }
-  T element() const { return d_t; }
-};/* class CDCircElement<> */
-
-
-/**
- * Generic context-dependent circular list.  Items themselves are not
- * context dependent, only the forward and backward links.  This
- * allows two lists to be spliced together in constant time (see
- * concat()).  The list *structure* is mutable (things can be spliced
- * in, removed, added, the list can be cleared, etc.) in a
- * context-dependent manner, but the list items are immutable.  To
- * replace an item A in the list with B, A must be removed and
- * B added in the same location.
- */
-template <class T, class AllocatorT>
-class CDCircList : public ContextObj {
-public:
-
-  /** List carrier element type */
-  typedef CDCircElement<T, AllocatorT> elt_t;
-  /** The value type with which this CDCircList<> was instantiated. */
-  typedef T value_type;
-  /** The allocator type with which this CDCircList<> was instantiated. */
-  typedef AllocatorT Allocator;
-
-private:
-
-  /** Head element of the circular list */
-  CDPtr<elt_t> d_head;
-  /** The context with which we're associated */
-  Context* d_context;
-  /** Our allocator */
-  typename Allocator::template rebind< CDCircElement<T, AllocatorT> >::other d_allocator;
-
-public:
-
-  CDCircList(Context* context, const Allocator& alloc = Allocator()) :
-    ContextObj(context),
-    d_head(context, NULL),
-    d_context(context),
-    d_allocator(alloc) {
-  }
-
-  CDCircList(bool allocatedInCMM, Context* context, const Allocator& alloc = Allocator()) :
-    ContextObj(allocatedInCMM, context),
-    d_head(allocatedInCMM, context, NULL),
-    d_context(context),
-    d_allocator(alloc) {
-    Debug("cdcirclist") << "head " << &d_head << " in cmm ? " << allocatedInCMM << std::endl;
-  }
-
-  ~CDCircList() throw(AssertionException) {
-    // by context contract, call destroy() here
-    destroy();
-  }
-
-  void clear() {
-    d_head = NULL;
-  }
-
-  bool empty() const {
-    return d_head == NULL;
-  }
-
-  CDPtr<elt_t>& head() {
-    return d_head;
-  }
-
-  CDPtr<elt_t>& tail() {
-    return empty() ? d_head : d_head->d_prev;
-  }
-
-  const elt_t* head() const {
-    return d_head;
-  }
-
-  const elt_t* tail() const {
-    return empty() ? d_head : d_head->d_prev;
-  }
-
-  T front() const {
-    Assert(! empty());
-    return head()->element();
-  }
-
-  T back() const {
-    Assert(! empty());
-    return tail()->element();
-  }
-
-  void push_back(const T& t) {
-    if(Debug.isOn("cdcirclist:paranoid")) {
-      debugCheck();
-    }
-    // FIXME LEAK! (should alloc in CMM, no?)
-    elt_t* x = d_allocator.allocate(1);
-    if(empty()) {
-      // zero-element case
-      new(x) elt_t(d_context, t, x, x);
-      d_head = x;
-    } else {
-      // N-element case
-      new(x) elt_t(d_context, t, d_head->d_prev, d_head);
-      d_head->d_prev->d_next = x;
-      d_head->d_prev = x;
-    }
-  }
-
-  /**
-   * Concatenate two lists.  This modifies both: afterward, the two
-   * lists might have different heads, but they will have the same
-   * elements in the same (circular) order.
-   */
-  void concat(CDCircList<T, AllocatorT>& l) {
-    Assert(this != &l, "cannot concat a list with itself");
-
-    if(d_head == NULL) {
-      d_head = l.d_head;
-      return;
-    } else if(l.d_head == NULL) {
-      l.d_head = d_head;
-      return;
-    }
-
-    // splice together the two circular lists
-    CDPtr<elt_t> &l1head = head(), &l2head = l.head();
-    CDPtr<elt_t> &l1tail = tail(), &l2tail = l.tail();
-    // l2tail will change underneath us in what's below (because it's
-    // the same as l2head->prev()), so we have to keep a regular
-    // pointer to it
-    elt_t* oldl2tail = l2tail;
-
-    Debug("cdcirclist") << "concat1 " << this << " " << &l << std::endl;
-    l1tail->next() = l2head;
-    Debug("cdcirclist") << "concat2" << std::endl;
-    l2head->prev() = l1tail;
-
-    Debug("cdcirclist") << "concat3" << std::endl;
-    oldl2tail->next() = l1head;
-    Debug("cdcirclist") << "concat4" << std::endl;
-    l1head->prev() = oldl2tail;
-    Debug("cdcirclist") << "concat5" << std::endl;
-  }
-
-  class iterator {
-    const CDCircList<T, AllocatorT>* d_list;
-    const elt_t* d_current;
-    friend class CDCircList<T, AllocatorT>;
-  public:
-    iterator(const CDCircList<T, AllocatorT>* list, const elt_t* first) :
-      d_list(list),
-      d_current(first) {
-    }
-    iterator(const iterator& other) :
-      d_list(other.d_list),
-      d_current(other.d_current) {
-    }
-
-    bool operator==(const iterator& other) const {
-      return d_list == other.d_list && d_current == other.d_current;
-    }
-    bool operator!=(const iterator& other) const {
-      return !(*this == other);
-    }
-    iterator& operator++() {
-      Assert(d_current != NULL, "iterator already off the end");
-      if(d_current == d_list->tail()) {
-        d_current = NULL;
-      } else {
-        d_current = d_current->next();
-      }
-      return *this;
-    }
-    iterator operator++(int) {
-      const elt_t* old = d_current;
-      ++*this;
-      return iterator(d_list, old);
-    }
-    iterator& operator--() {
-      // undefined to go off the beginning, but don't have a check for that
-      if(d_current == NULL) {
-        d_current = d_list->tail();
-      } else {
-        d_current = d_current->prev();
-      }
-      return *this;
-    }
-    iterator operator--(int) {
-      const elt_t* old = d_current;
-      --*this;
-      return iterator(d_list, old);
-    }
-    T operator*() {
-      Assert(d_current != NULL, "iterator already off the end");
-      return d_current->element();
-    }
-  };/* class CDCircList<>::iterator */
-
-  // list elements are immutable
-  typedef iterator const_iterator;
-
-  iterator begin() {
-    if(Debug.isOn("cdcirclist:paranoid")) {
-      debugCheck();
-    }
-    return iterator(this, head());
-  }
-
-  iterator end() {
-    if(Debug.isOn("cdcirclist:paranoid")) {
-      debugCheck();
-    }
-    return iterator(this, NULL);
-  }
-
-  const_iterator begin() const {
-    return const_iterator(this, head());
-  }
-
-  const_iterator end() const {
-    return const_iterator(this, NULL);
-  }
-
-  iterator erase(iterator pos) {
-    Assert(pos.d_current != NULL);
-    if(pos.d_current->prev() == pos.d_current) {
-      // one-elt list
-      d_head = NULL;
-      return iterator(this, NULL);
-    } else {
-      // N-elt list
-      if(pos.d_current == d_head) {
-        // removing list head
-        elt_t *pHead = head(), *pTail = tail();
-        pTail->next() = pHead->next();
-        pHead->next()->prev() = pTail;
-        d_head = pHead->next();
-        return iterator(this, d_head);
-        // can't free old head, because of backtracking
-      } else {
-        // not removing list head
-        const elt_t *elt = pos.d_current;
-        elt_t *prev = pos.d_current->prev();
-        prev->next() = elt->next();
-        elt->next()->prev() = prev;
-        return iterator(this, elt->next());
-        // can't free elt, because of backtracking
-      }
-    }
-  }
-
-private:
-
-  // do not permit copy/assignment
-  CDCircList(const CDCircList<T, AllocatorT>&) CVC4_UNUSED;
-  CDCircList<T, AllocatorT>& operator=(const CDCircList<T, AllocatorT>&) CVC4_UNUSED;
-
-public:
-  /** Check internal structure and invariants of the list */
-  void debugCheck() const {
-    elt_t* p = d_head;
-    Debug("cdcirclist") << "this is " << this << std::endl;
-    if(p == NULL) {
-      Debug("cdcirclist") << "head[" << &d_head << "] is NULL : " << d_context->getLevel() << std::endl;
-      // empty list
-      return;
-    }
-    Debug("cdcirclist") << "head[" << &d_head << "] is " << p << " next " << p->d_next << " prev " << p->d_prev << " : " << d_context->getLevel() << std::endl;//p->d_t << std::endl;
-    do {
-      elt_t* p_last = p;
-      p = p->d_next;
-      if(p == NULL) {
-        Debug("cdcirclist") << "****** ERROR ON LINE ABOVE, next == NULL ******" << std::endl;
-        break;
-      }
-      Debug("cdcirclist") << "   p is " << p << " next " << p->d_next << " prev " << p->d_prev << " : " << std::endl;//p->d_t << std::endl;
-      if(p->d_prev != p_last) {
-        Debug("cdcirclist") << "****** ERROR ON LINE ABOVE, prev != last ******" << std::endl;
-      }
-      //Assert(p->d_prev == p_last);
-      Assert(p != NULL);
-    } while(p != d_head);
-  }
-
-private:
-
-  // Nothing to save; the elements take care of themselves
-  virtual ContextObj* save(ContextMemoryManager* pCMM) {
-    Unreachable();
-  }
-
-  // Similarly, nothing to restore
-  virtual void restore(ContextObj* data) {
-    Unreachable();
-  }
-
-};/* class CDCircList<> */
-
-}/* CVC4::context namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__CONTEXT__CDCIRCLIST_H */
diff --git a/src/context/cdcirclist_forward.h b/src/context/cdcirclist_forward.h
deleted file mode 100644
index 56a39e96f..000000000
--- a/src/context/cdcirclist_forward.h
+++ /dev/null
@@ -1,45 +0,0 @@
-/*********************                                                        */
-/*! \file cdcirclist_forward.h
- ** \verbatim
- ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  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.\endverbatim
- **
- ** \brief This is a forward declaration header to declare the
- ** CDCircList<> template
- **
- ** This is a forward declaration header to declare the CDCircList<>
- ** template.  It's useful if you want to forward-declare CDCircList<>
- ** without including the full cdcirclist.h header, for example, in a
- ** public header context, or to keep compile times low when only a
- ** forward declaration is needed.
- **/
-
-#include "cvc4_public.h"
-
-#ifndef __CVC4__CONTEXT__CDCIRCLIST_FORWARD_H
-#define __CVC4__CONTEXT__CDCIRCLIST_FORWARD_H
-
-#include <memory>
-
-namespace __gnu_cxx {
-  template <class Key> struct hash;
-}/* __gnu_cxx namespace */
-
-namespace CVC4 {
-  namespace context {
-    template <class T>
-    class ContextMemoryAllocator;
-
-    template <class T, class Allocator = ContextMemoryAllocator<T> >
-    class CDCircList;
-  }/* CVC4::context namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__CONTEXT__CDCIRCLIST_FORWARD_H */
diff --git a/src/cvc4.i b/src/cvc4.i
index 08b2c509f..a4d5e1986 100644
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -112,7 +112,7 @@ using namespace CVC4;
 %include "expr/kind.i"
 %include "expr/expr.i"
 %include "expr/command.i"
-%include "expr/declaration_scope.i"
+%include "expr/symbol_table.i"
 %include "expr/expr_manager.i"
 %include "expr/expr_stream.i"
 
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index 38cb8250c..b581e8919 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -24,8 +24,8 @@ libexpr_la_SOURCES = \
 	node_value.cpp \
 	command.h \
 	command.cpp \
-	declaration_scope.h \
-	declaration_scope.cpp \
+	symbol_table.h \
+	symbol_table.cpp \
 	expr_manager_scope.h \
 	node_self_iterator.h \
 	variable_type_map.h \
@@ -62,7 +62,7 @@ EXTRA_DIST = \
 	mkexpr \
 	expr_stream.i \
 	expr_manager.i \
-	declaration_scope.i \
+	symbol_table.i \
 	command.i \
 	type.i \
 	kind.i \
diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h
index 70535cf1c..a963b9f55 100644
--- a/src/expr/attribute_internals.h
+++ b/src/expr/attribute_internals.h
@@ -40,23 +40,23 @@ namespace attr {
  * A hash function for attribute table keys.  Attribute table keys are
  * pairs, (unique-attribute-id, Node).
  */
-struct AttrHashStrategy {
+struct AttrHashFunction {
   enum { LARGE_PRIME = 32452843ul };
   std::size_t operator()(const std::pair<uint64_t, NodeValue*>& p) const {
     return p.first * LARGE_PRIME + p.second->getId();
   }
-};
+};/* struct AttrHashFunction */
 
 /**
  * A hash function for boolean-valued attribute table keys; here we
  * don't have to store a pair as the key, because we use a known bit
  * in [0..63] for each attribute
  */
-struct AttrHashBoolStrategy {
+struct AttrBoolHashFunction {
   std::size_t operator()(NodeValue* nv) const {
     return (size_t)nv->getId();
   }
-};
+};/* struct AttrBoolHashFunction */
 
 }/* CVC4::expr::attr namespace */
 
@@ -156,7 +156,7 @@ template <class value_type>
 class AttrHash :
     public __gnu_cxx::hash_map<std::pair<uint64_t, NodeValue*>,
                                value_type,
-                               AttrHashStrategy> {
+                               AttrHashFunction> {
 };/* class AttrHash<> */
 
 /**
@@ -167,10 +167,10 @@ template <>
 class AttrHash<bool> :
     protected __gnu_cxx::hash_map<NodeValue*,
                                   uint64_t,
-                                  AttrHashBoolStrategy> {
+                                  AttrBoolHashFunction> {
 
   /** A "super" type, like in Java, for easy reference below. */
-  typedef __gnu_cxx::hash_map<NodeValue*, uint64_t, AttrHashBoolStrategy> super;
+  typedef __gnu_cxx::hash_map<NodeValue*, uint64_t, AttrBoolHashFunction> super;
 
   /**
    * BitAccessor allows us to return a bit "by reference."  Of course,
@@ -367,12 +367,12 @@ template <class value_type>
 class CDAttrHash :
     public context::CDHashMap<std::pair<uint64_t, NodeValue*>,
                           value_type,
-                          AttrHashStrategy> {
+                          AttrHashFunction> {
 public:
   CDAttrHash(context::Context* ctxt) :
     context::CDHashMap<std::pair<uint64_t, NodeValue*>,
                    value_type,
-                   AttrHashStrategy>(ctxt) {
+                   AttrHashFunction>(ctxt) {
   }
 };/* class CDAttrHash<> */
 
@@ -384,10 +384,10 @@ template <>
 class CDAttrHash<bool> :
     protected context::CDHashMap<NodeValue*,
                              uint64_t,
-                             AttrHashBoolStrategy> {
+                             AttrBoolHashFunction> {
 
   /** A "super" type, like in Java, for easy reference below. */
-  typedef context::CDHashMap<NodeValue*, uint64_t, AttrHashBoolStrategy> super;
+  typedef context::CDHashMap<NodeValue*, uint64_t, AttrBoolHashFunction> super;
 
   /**
    * BitAccessor allows us to return a bit "by reference."  Of course,
diff --git a/src/expr/declaration_scope.i b/src/expr/declaration_scope.i
deleted file mode 100644
index e32c4ee4f..000000000
--- a/src/expr/declaration_scope.i
+++ /dev/null
@@ -1,5 +0,0 @@
-%{
-#include "expr/declaration_scope.h"
-%}
-
-%include "expr/declaration_scope.h"
diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h
index 6313aa30b..1acbed978 100644
--- a/src/expr/kind_template.h
+++ b/src/expr/kind_template.h
@@ -87,9 +87,11 @@ inline std::string kindToString(::CVC4::Kind k) {
   return ss.str();
 }
 
-struct KindHashStrategy {
-  static inline size_t hash(::CVC4::Kind k) { return k; }
-};/* struct KindHashStrategy */
+struct KindHashFunction {
+  inline size_t operator()(::CVC4::Kind k) const {
+    return k;
+  }
+};/* struct KindHashFunction */
 
 }/* CVC4::kind namespace */
 
@@ -104,11 +106,11 @@ ${type_constant_list}
 /**
  * We hash the constants with their values.
  */
-struct TypeConstantHashStrategy {
-  static inline size_t hash(TypeConstant tc) {
+struct TypeConstantHashFunction {
+  inline size_t operator()(TypeConstant tc) const {
     return tc;
   }
-};/* struct BoolHashStrategy */
+};/* struct TypeConstantHashFunction */
 
 inline std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant) {
   switch(typeConstant) {
diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
index 5608d2972..647c1af8e 100755
--- a/src/expr/mkmetakind
+++ b/src/expr/mkmetakind
@@ -193,7 +193,7 @@ function constant {
     fi
   fi
   if ! expr "$3" : '\(::*\)' >/dev/null; then
-    echo "$kf:$lineno: warning: constant $1 hasher \`$3' isn't fully-qualified (e.g., ::CVC4::RationalHashFcn)" >&2
+    echo "$kf:$lineno: warning: constant $1 hasher \`$3' isn't fully-qualified (e.g., ::CVC4::RationalHashFunction)" >&2
   fi
 
   if [ -n "$4" ]; then
@@ -252,7 +252,7 @@ struct ConstantMapReverse< ::CVC4::kind::$1 > {
   metakind_constHashes="${metakind_constHashes}
   case kind::$1:
 #line $lineno \"$kf\"
-    return $3::hash(nv->getConst< $2 >());
+    return $3()(nv->getConst< $2 >());
 "
   metakind_constPrinters="${metakind_constPrinters}
   case kind::$1:
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index ce6a91483..682a48bda 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -75,7 +75,7 @@ class NodeManager {
   };
 
   typedef __gnu_cxx::hash_set<expr::NodeValue*,
-                              expr::NodeValuePoolHashFcn,
+                              expr::NodeValuePoolHashFunction,
                               expr::NodeValuePoolEq> NodeValuePool;
   typedef __gnu_cxx::hash_set<expr::NodeValue*,
                               expr::NodeValueIDHashFunction,
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 657fabeb5..ae3c6beda 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -358,11 +358,11 @@ operator+(NodeValue::iterator<NodeTemplate<false> >::difference_type p,
  * PERFORMING for other uses!  NodeValue::poolHash() will lead to
  * collisions for all VARIABLEs.
  */
-struct NodeValuePoolHashFcn {
+struct NodeValuePoolHashFunction {
   inline size_t operator()(const NodeValue* nv) const {
     return (size_t) nv->poolHash();
   }
-};/* struct NodeValuePoolHashFcn */
+};/* struct NodeValuePoolHashFunction */
 
 /**
  * For hash_maps, hash_sets, etc.
@@ -371,7 +371,7 @@ struct NodeValueIDHashFunction {
   inline size_t operator()(const NodeValue* nv) const {
     return (size_t) nv->getId();
   }
-};/* struct NodeValueIDHashFcn */
+};/* struct NodeValueIDHashFunction */
 
 inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv);
 
diff --git a/src/expr/declaration_scope.cpp b/src/expr/symbol_table.cpp
index 6038fadab..c9234b5e0 100644
--- a/src/expr/declaration_scope.cpp
+++ b/src/expr/symbol_table.cpp
@@ -1,24 +1,24 @@
 /*********************                                                        */
-/*! \file declaration_scope.cpp
+/*! \file symbol_table.cpp
  ** \verbatim
  ** Original author: cconway
- ** Major contributors: mdeters
- ** Minor contributors (to current version): dejan, ajreynol
+ ** Major contributors: bobot, mdeters
+ ** Minor contributors (to current version): ajreynol, dejan
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012  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.\endverbatim
  **
  ** \brief Convenience class for scoping variable and type
- ** declarations (implementation).
+ ** declarations (implementation)
  **
  ** Convenience class for scoping variable and type declarations
  ** (implementation).
  **/
 
-#include "expr/declaration_scope.h"
+#include "expr/symbol_table.h"
 #include "expr/expr.h"
 #include "expr/type.h"
 #include "expr/expr_manager_scope.h"
@@ -35,21 +35,21 @@ using namespace std;
 
 namespace CVC4 {
 
-DeclarationScope::DeclarationScope() :
+SymbolTable::SymbolTable() :
   d_context(new Context),
   d_exprMap(new(true) CDHashMap<std::string, Expr, StringHashFunction>(d_context)),
   d_typeMap(new(true) CDHashMap<std::string, pair<vector<Type>, Type>, StringHashFunction>(d_context)),
   d_functions(new(true) CDHashSet<Expr, ExprHashFunction>(d_context)) {
 }
 
-DeclarationScope::~DeclarationScope() {
+SymbolTable::~SymbolTable() {
   d_exprMap->deleteSelf();
   d_typeMap->deleteSelf();
   d_functions->deleteSelf();
   delete d_context;
 }
 
-void DeclarationScope::bind(const std::string& name, Expr obj,
+void SymbolTable::bind(const std::string& name, Expr obj,
                             bool levelZero) throw(AssertionException) {
   CheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr");
   ExprManagerScope ems(obj);
@@ -57,7 +57,7 @@ void DeclarationScope::bind(const std::string& name, Expr obj,
   else d_exprMap->insert(name, obj);
 }
 
-void DeclarationScope::bindDefinedFunction(const std::string& name, Expr obj,
+void SymbolTable::bindDefinedFunction(const std::string& name, Expr obj,
                             bool levelZero) throw(AssertionException) {
   CheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr");
   ExprManagerScope ems(obj);
@@ -70,25 +70,25 @@ void DeclarationScope::bindDefinedFunction(const std::string& name, Expr obj,
   }
 }
 
-bool DeclarationScope::isBound(const std::string& name) const throw() {
+bool SymbolTable::isBound(const std::string& name) const throw() {
   return d_exprMap->find(name) != d_exprMap->end();
 }
 
-bool DeclarationScope::isBoundDefinedFunction(const std::string& name) const throw() {
+bool SymbolTable::isBoundDefinedFunction(const std::string& name) const throw() {
   CDHashMap<std::string, Expr, StringHashFunction>::iterator found =
     d_exprMap->find(name);
   return found != d_exprMap->end() && d_functions->contains((*found).second);
 }
 
-bool DeclarationScope::isBoundDefinedFunction(Expr func) const throw() {
+bool SymbolTable::isBoundDefinedFunction(Expr func) const throw() {
   return d_functions->contains(func);
 }
 
-Expr DeclarationScope::lookup(const std::string& name) const throw(AssertionException) {
+Expr SymbolTable::lookup(const std::string& name) const throw(AssertionException) {
   return (*d_exprMap->find(name)).second;
 }
 
-void DeclarationScope::bindType(const std::string& name, Type t,
+void SymbolTable::bindType(const std::string& name, Type t,
                                 bool levelZero) throw() {
   if(levelZero){
     d_typeMap->insertAtContextLevelZero(name, make_pair(vector<Type>(), t));
@@ -97,7 +97,7 @@ void DeclarationScope::bindType(const std::string& name, Type t,
   }
 }
 
-void DeclarationScope::bindType(const std::string& name,
+void SymbolTable::bindType(const std::string& name,
                                 const std::vector<Type>& params,
                                 Type t,
                                 bool levelZero) throw() {
@@ -117,11 +117,11 @@ void DeclarationScope::bindType(const std::string& name,
   }
 }
 
-bool DeclarationScope::isBoundType(const std::string& name) const throw() {
+bool SymbolTable::isBoundType(const std::string& name) const throw() {
   return d_typeMap->find(name) != d_typeMap->end();
 }
 
-Type DeclarationScope::lookupType(const std::string& name) const throw(AssertionException) {
+Type SymbolTable::lookupType(const std::string& name) const throw(AssertionException) {
   pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second;
   Assert(p.first.size() == 0,
          "type constructor arity is wrong: "
@@ -130,7 +130,7 @@ Type DeclarationScope::lookupType(const std::string& name) const throw(Assertion
   return p.second;
 }
 
-Type DeclarationScope::lookupType(const std::string& name,
+Type SymbolTable::lookupType(const std::string& name,
                                   const std::vector<Type>& params) const throw(AssertionException) {
   pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second;
   Assert(p.first.size() == params.size(),
@@ -188,23 +188,23 @@ Type DeclarationScope::lookupType(const std::string& name,
   }
 }
 
-size_t DeclarationScope::lookupArity(const std::string& name) {
+size_t SymbolTable::lookupArity(const std::string& name) {
   pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second;
   return p.first.size();
 }
 
-void DeclarationScope::popScope() throw(ScopeException) {
+void SymbolTable::popScope() throw(ScopeException) {
   if( d_context->getLevel() == 0 ) {
     throw ScopeException();
   }
   d_context->pop();
 }
 
-void DeclarationScope::pushScope() throw() {
+void SymbolTable::pushScope() throw() {
   d_context->push();
 }
 
-size_t DeclarationScope::getLevel() const throw() {
+size_t SymbolTable::getLevel() const throw() {
   return d_context->getLevel();
 }
 
diff --git a/src/expr/declaration_scope.h b/src/expr/symbol_table.h
index 8695d9287..ee04b17fd 100644
--- a/src/expr/declaration_scope.h
+++ b/src/expr/symbol_table.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file declaration_scope.h
+/*! \file symbol_table.h
  ** \verbatim
  ** Original author: cconway
  ** Major contributors: mdeters
- ** Minor contributors (to current version): ajreynol
+ ** Minor contributors (to current version): ajreynol, dejan, bobot
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012  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
@@ -18,8 +18,8 @@
 
 #include "cvc4_public.h"
 
-#ifndef __CVC4__DECLARATION_SCOPE_H
-#define __CVC4__DECLARATION_SCOPE_H
+#ifndef __CVC4__SYMBOL_TABLE_H
+#define __CVC4__SYMBOL_TABLE_H
 
 #include <vector>
 #include <utility>
@@ -47,7 +47,7 @@ class CVC4_PUBLIC ScopeException : public Exception {
  * nested scoping rules for declarations, with separate bindings for expressions
  * and types.
  */
-class CVC4_PUBLIC DeclarationScope {
+class CVC4_PUBLIC SymbolTable {
   /** The context manager for the scope maps. */
   context::Context* d_context;
 
@@ -62,10 +62,10 @@ class CVC4_PUBLIC DeclarationScope {
 
 public:
   /** Create a declaration scope. */
-  DeclarationScope();
+  SymbolTable();
 
   /** Destroy a declaration scope. */
-  ~DeclarationScope();
+  ~SymbolTable();
 
   /**
    * Bind an expression to a name in the current scope level.  If
@@ -188,7 +188,7 @@ public:
    * <code>pushScope</code>. Calls to <code>pushScope</code> and
    * <code>popScope</code> must be "properly nested." I.e., a call to
    * <code>popScope</code> is only legal if the number of prior calls to
-   * <code>pushScope</code> on this <code>DeclarationScope</code> is strictly
+   * <code>pushScope</code> on this <code>SymbolTable</code> is strictly
    * greater than then number of prior calls to <code>popScope</code>. */
   void popScope() throw(ScopeException);
 
@@ -198,8 +198,8 @@ public:
   /** Get the current level of this declaration scope. */
   size_t getLevel() const throw();
 
-};/* class DeclarationScope */
+};/* class SymbolTable */
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__DECLARATION_SCOPE_H */
+#endif /* __CVC4__SYMBOL_TABLE_H */
diff --git a/src/expr/symbol_table.i b/src/expr/symbol_table.i
new file mode 100644
index 000000000..7e5579c49
--- /dev/null
+++ b/src/expr/symbol_table.i
@@ -0,0 +1,5 @@
+%{
+#include "expr/symbol_table.h"
+%}
+
+%include "expr/symbol_table.h"
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index bbeee4f7f..1a85f45c3 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -1057,7 +1057,7 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t,
   std::string id;
   std::vector<Type> types;
   std::vector< std::pair<std::string, Type> > typeIds;
-  DeclarationScope* declScope;
+  //SymbolTable* symtab;
   Parser* parser;
   lhs = false;
 }
@@ -1097,11 +1097,11 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t,
      * declared in the outer context.  What follows isn't quite right,
      * though, since type aliases and function definitions should be
      * retained in the set of current declarations. */
-    { /*declScope = PARSER_STATE->getDeclarationScope();
-      PARSER_STATE->useDeclarationsFrom(new DeclarationScope());*/ }
+    { /*symtab = PARSER_STATE->getSymbolTable();
+      PARSER_STATE->useDeclarationsFrom(new SymbolTable());*/ }
     formula[f] ( COMMA formula[f2] )? RPAREN
-    { /*DeclarationScope* old = PARSER_STATE->getDeclarationScope();
-      PARSER_STATE->useDeclarationsFrom(declScope);
+    { /*SymbolTable* old = PARSER_STATE->getSymbolTable();
+      PARSER_STATE->useDeclarationsFrom(symtab);
       delete old;*/
       t = f2.isNull() ?
         EXPR_MANAGER->mkPredicateSubtype(f) :
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 44148a7f1..29db640c7 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -43,8 +43,8 @@ namespace parser {
 Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) :
   d_exprManager(exprManager),
   d_input(input),
-  d_declScopeAllocated(),
-  d_declScope(&d_declScopeAllocated),
+  d_symtabAllocated(),
+  d_symtab(&d_symtabAllocated),
   d_anonymousFunctionCount(0),
   d_done(false),
   d_checksEnabled(true),
@@ -60,7 +60,7 @@ Expr Parser::getSymbol(const std::string& name, SymbolType type) {
   switch( type ) {
 
   case SYM_VARIABLE: // Functions share var namespace
-    return d_declScope->lookup(name);
+    return d_symtab->lookup(name);
 
   default:
     Unhandled(type);
@@ -87,7 +87,7 @@ Type Parser::getType(const std::string& var_name,
 Type Parser::getSort(const std::string& name) {
   checkDeclaration(name, CHECK_DECLARED, SYM_SORT);
   Assert( isDeclared(name, SYM_SORT) );
-  Type t = d_declScope->lookupType(name);
+  Type t = d_symtab->lookupType(name);
   return t;
 }
 
@@ -95,14 +95,14 @@ Type Parser::getSort(const std::string& name,
                      const std::vector<Type>& params) {
   checkDeclaration(name, CHECK_DECLARED, SYM_SORT);
   Assert( isDeclared(name, SYM_SORT) );
-  Type t = d_declScope->lookupType(name, params);
+  Type t = d_symtab->lookupType(name, params);
   return t;
 }
 
 size_t Parser::getArity(const std::string& sort_name){
   checkDeclaration(sort_name, CHECK_DECLARED, SYM_SORT);
   Assert( isDeclared(sort_name, SYM_SORT) );
-  return d_declScope->lookupArity(sort_name);
+  return d_symtab->lookupArity(sort_name);
 }
 
 /* Returns true if name is bound to a boolean variable. */
@@ -125,14 +125,14 @@ bool Parser::isFunctionLike(const std::string& name) {
 bool Parser::isDefinedFunction(const std::string& name) {
   // more permissive in type than isFunction(), because defined
   // functions can be zero-ary and declared functions cannot.
-  return d_declScope->isBoundDefinedFunction(name);
+  return d_symtab->isBoundDefinedFunction(name);
 }
 
 /* Returns true if the Expr is a defined function. */
 bool Parser::isDefinedFunction(Expr func) {
   // more permissive in type than isFunction(), because defined
   // functions can be zero-ary and declared functions cannot.
-  return d_declScope->isBoundDefinedFunction(func);
+  return d_symtab->isBoundDefinedFunction(func);
 }
 
 /* Returns true if name is bound to a function returning boolean. */
@@ -179,20 +179,20 @@ Parser::mkVars(const std::vector<std::string> names,
 void
 Parser::defineVar(const std::string& name, const Expr& val,
                        bool levelZero) {
-  d_declScope->bind(name, val, levelZero);
+  d_symtab->bind(name, val, levelZero);
   Assert( isDeclared(name) );
 }
 
 void
 Parser::defineFunction(const std::string& name, const Expr& val,
                        bool levelZero) {
-  d_declScope->bindDefinedFunction(name, val, levelZero);
+  d_symtab->bindDefinedFunction(name, val, levelZero);
   Assert( isDeclared(name) );
 }
 
 void
 Parser::defineType(const std::string& name, const Type& type) {
-  d_declScope->bindType(name, type);
+  d_symtab->bindType(name, type);
   Assert( isDeclared(name, SYM_SORT) );
 }
 
@@ -200,7 +200,7 @@ void
 Parser::defineType(const std::string& name,
                    const std::vector<Type>& params,
                    const Type& type) {
-  d_declScope->bindType(name, params, type);
+  d_symtab->bindType(name, params, type);
   Assert( isDeclared(name, SYM_SORT) );
 }
 
@@ -369,9 +369,9 @@ DatatypeType Parser::mkTupleType(const std::vector<Type>& types) {
 bool Parser::isDeclared(const std::string& name, SymbolType type) {
   switch(type) {
   case SYM_VARIABLE:
-    return d_declScope->isBound(name);
+    return d_symtab->isBound(name);
   case SYM_SORT:
-    return d_declScope->isBoundType(name);
+    return d_symtab->isBoundType(name);
   default:
     Unhandled(type);
   }
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 635dd6b6c..f3210ae29 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -28,7 +28,7 @@
 #include "parser/input.h"
 #include "parser/parser_exception.h"
 #include "expr/expr.h"
-#include "expr/declaration_scope.h"
+#include "expr/symbol_table.h"
 #include "expr/kind.h"
 #include "expr/expr_stream.h"
 
@@ -117,15 +117,15 @@ class CVC4_PUBLIC Parser {
    * The declaration scope that is "owned" by this parser.  May or
    * may not be the current declaration scope in use.
    */
-  DeclarationScope d_declScopeAllocated;
+  SymbolTable d_symtabAllocated;
 
   /**
    * This current symbol table used by this parser.  Initially points
-   * to d_declScopeAllocated, but can be changed (making this parser
+   * to d_symtabAllocated, but can be changed (making this parser
    * delegate its definitions and lookups to another parser).
    * See useDeclarationsFrom().
    */
-  DeclarationScope* d_declScope;
+  SymbolTable* d_symtab;
 
   /** How many anonymous functions we've created. */
   size_t d_anonymousFunctionCount;
@@ -493,8 +493,8 @@ public:
     }
   }
 
-  inline void pushScope() { d_declScope->pushScope(); }
-  inline void popScope() { d_declScope->popScope(); }
+  inline void pushScope() { d_symtab->pushScope(); }
+  inline void popScope() { d_symtab->popScope(); }
 
   /**
    * Set the current symbol table used by this parser.
@@ -523,25 +523,25 @@ public:
    */
   inline void useDeclarationsFrom(Parser* parser) {
     if(parser == NULL) {
-      d_declScope = &d_declScopeAllocated;
+      d_symtab = &d_symtabAllocated;
     } else {
-      d_declScope = parser->d_declScope;
+      d_symtab = parser->d_symtab;
     }
   }
 
-  inline void useDeclarationsFrom(DeclarationScope* scope) {
-    d_declScope = scope;
+  inline void useDeclarationsFrom(SymbolTable* symtab) {
+    d_symtab = symtab;
   }
 
-  inline DeclarationScope* getDeclarationScope() const {
-    return d_declScope;
+  inline SymbolTable* getSymbolTable() const {
+    return d_symtab;
   }
 
   /**
    * Gets the current declaration level.
    */
   inline size_t getDeclarationLevel() const throw() {
-    return d_declScope->getLevel();
+    return d_symtab->getLevel();
   }
 
   /**
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index 7883bd92b..b9fac6e20 100644
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -38,7 +38,7 @@ sort INTEGER_TYPE \
 
 constant SUBRANGE_TYPE \
     ::CVC4::SubrangeBounds \
-    ::CVC4::SubrangeBoundsHashStrategy \
+    ::CVC4::SubrangeBoundsHashFunction \
     "util/subrange_bound.h" \
     "the type of an integer subrange"
 cardinality SUBRANGE_TYPE \
@@ -51,7 +51,7 @@ well-founded SUBRANGE_TYPE \
 
 constant CONST_RATIONAL \
     ::CVC4::Rational \
-    ::CVC4::RationalHashStrategy \
+    ::CVC4::RationalHashFunction \
     "util/rational.h" \
     "a multiple-precision rational constant"
 
diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h
index b34232b8f..e847a238d 100644
--- a/src/theory/arrays/array_info.h
+++ b/src/theory/arrays/array_info.h
@@ -2,28 +2,10 @@
 /*! \file array_info.h
  ** \verbatim
  ** Original author: lianah
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): dejan, barrett
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  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.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-/*! \file array_info.h
- ** \verbatim
- ** Original author: lianah
- ** 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)
+ ** Copyright (c) 2009-2012  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
@@ -31,14 +13,13 @@
  **
  ** \brief Contains additional classes to store context dependent information
  ** for each term of type array
- **
- **
  **/
 
 #include "cvc4_private.h"
 
 #ifndef __CVC4__THEORY__ARRAYS__ARRAY_INFO_H
 #define __CVC4__THEORY__ARRAYS__ARRAY_INFO_H
+
 #include "util/backtrackable.h"
 #include "context/cdlist.h"
 #include "context/cdhashmap.h"
@@ -58,7 +39,7 @@ typedef context::CDList<TNode> CTNodeList;
 typedef quad<TNode, TNode, TNode, TNode> RowLemmaType;
 
 struct RowLemmaTypeHashFunction {
-  size_t operator()(const RowLemmaType& q ) const {
+  size_t operator()(const RowLemmaType& q) const {
     TNode n1 = q.first;
     TNode n2 = q.second;
     TNode n3 = q.third;
@@ -92,7 +73,6 @@ public:
     indices = new(true)CTNodeList(c);
     stores = new(true)CTNodeList(c);
     in_stores = new(true)CTNodeList(c);
-
   }
 
   ~Info() {
@@ -115,7 +95,7 @@ public:
     Trace("arrays-info")<<"  in_stores ";
     printList(in_stores);
   }
-};
+};/* class Info */
 
 
 typedef __gnu_cxx::hash_map<Node, Info*, NodeHashFunction> CNodeInfoMap;
@@ -202,7 +182,7 @@ public:
     StatisticsRegistry::registerStat(&d_tableSize);
   }
 
-  ~ArrayInfo(){
+  ~ArrayInfo() {
     CNodeInfoMap::iterator it = info_map.begin();
     for( ; it != info_map.end(); it++ ) {
       if((*it).second!= emptyInfo) {
@@ -255,8 +235,7 @@ public:
    *  a should be the canonical representative of b
    */
   void mergeInfo(const TNode a, const TNode b);
-};
-
+};/* class ArrayInfo */
 
 }/* CVC4::theory::arrays namespace */
 }/* CVC4::theory namespace */
diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds
index 7386ec5c2..ef237e351 100644
--- a/src/theory/arrays/kinds
+++ b/src/theory/arrays/kinds
@@ -32,7 +32,7 @@ operator STORE 3 "array store"
 # storeall t e  is  \all i in indexType(t) <= e
 constant STORE_ALL \
     ::CVC4::ArrayStoreAll \
-    ::CVC4::ArrayStoreAllHashStrategy \
+    ::CVC4::ArrayStoreAllHashFunction \
     "util/array_store_all.h" \
     "array store-all"
 
diff --git a/src/theory/booleans/kinds b/src/theory/booleans/kinds
index 92a9a937f..4d748ca59 100644
--- a/src/theory/booleans/kinds
+++ b/src/theory/booleans/kinds
@@ -20,7 +20,7 @@ sort BOOLEAN_TYPE \
 
 constant CONST_BOOLEAN \
     bool \
-    ::CVC4::BoolHashStrategy \
+    ::CVC4::BoolHashFunction \
     "util/bool.h" \
     "truth and falsity"
 
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index 57baa82cd..6bb175db3 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -122,7 +122,7 @@
 #     to define it.  Hasher is a hash functor type defined like this:
 #
 #       struct MyHashFcn {
-#         static size_t hash(const T& val);
+#         size_t operator()(const T& val) const;
 #       };
 #
 #     For consistency, constants taking a non-void payload should
@@ -267,7 +267,7 @@ well-founded SORT_TYPE \
 
 constant UNINTERPRETED_CONSTANT \
     ::CVC4::UninterpretedConstant \
-    ::CVC4::UninterpretedConstantHashStrategy \
+    ::CVC4::UninterpretedConstantHashFunction \
     "util/uninterpreted_constant.h" \
     "The kind of nodes representing uninterpreted constants"
 typerule UNINTERPRETED_CONSTANT ::CVC4::theory::builtin::UninterpretedConstantTypeRule
@@ -281,7 +281,7 @@ enumerator SORT_TYPE \
 # you'll get a special, singleton (BUILTIN EQUAL) Node.
 constant BUILTIN \
     ::CVC4::Kind \
-    ::CVC4::kind::KindHashStrategy \
+    ::CVC4::kind::KindHashFunction \
     "expr/kind.h" \
     "The kind of nodes representing built-in operators"
 
@@ -296,7 +296,7 @@ operator TUPLE 2: "a tuple"
 
 constant TYPE_CONSTANT \
     ::CVC4::TypeConstant \
-    ::CVC4::TypeConstantHashStrategy \
+    ::CVC4::TypeConstantHashFunction \
     "expr/kind.h" \
     "basic types"
 operator FUNCTION_TYPE 2: "function type"
@@ -325,7 +325,7 @@ sort STRING_TYPE \
     "String type"
 constant CONST_STRING \
     ::std::string \
-    ::CVC4::StringHashStrategy \
+    ::CVC4::StringHashFunction \
     "util/hash.h" \
     "a string of characters"
 typerule CONST_STRING ::CVC4::theory::builtin::StringConstantTypeRule
@@ -337,7 +337,7 @@ typerule TUPLE ::CVC4::theory::builtin::TupleTypeRule
 
 constant SUBTYPE_TYPE \
     ::CVC4::Predicate \
-    ::CVC4::PredicateHashStrategy \
+    ::CVC4::PredicateHashFunction \
     "util/predicate.h" \
     "predicate subtype"
 cardinality SUBTYPE_TYPE \
diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds
index 36e27c66c..765f6bc59 100644
--- a/src/theory/bv/kinds
+++ b/src/theory/bv/kinds
@@ -14,7 +14,7 @@ rewriter ::CVC4::theory::bv::TheoryBVRewriter "theory/bv/theory_bv_rewriter.h"
 
 constant BITVECTOR_TYPE \
 	::CVC4::BitVectorSize \
-	"::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorSize >" \
+	"::CVC4::UnsignedHashFunction< ::CVC4::BitVectorSize >" \
 	"util/bitvector.h" \
 	"bit-vector type"
 cardinality BITVECTOR_TYPE \
@@ -23,7 +23,7 @@ cardinality BITVECTOR_TYPE \
 
 constant CONST_BITVECTOR \
     ::CVC4::BitVector \
-    ::CVC4::BitVectorHashStrategy \
+    ::CVC4::BitVectorHashFunction \
     "util/bitvector.h" \
     "a fixed-width bit-vector constant"
 
@@ -63,43 +63,43 @@ operator BITVECTOR_SGE 2 "signed greater than or equal"
 
 constant BITVECTOR_BITOF_OP \
 	::CVC4::BitVectorBitOf \
-	::CVC4::BitVectorBitOfHashStrategy \
+	::CVC4::BitVectorBitOfHashFunction \
 	"util/bitvector.h" \
 	"operator for the bit-vector boolean bit extract"
 
 constant BITVECTOR_EXTRACT_OP \
 	::CVC4::BitVectorExtract \
-	::CVC4::BitVectorExtractHashStrategy \
+	::CVC4::BitVectorExtractHashFunction \
 	"util/bitvector.h" \
 	"operator for the bit-vector extract"
 
 constant BITVECTOR_REPEAT_OP \
 	::CVC4::BitVectorRepeat \
-	"::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorRepeat >" \
+	"::CVC4::UnsignedHashFunction< ::CVC4::BitVectorRepeat >" \
 	"util/bitvector.h" \
 	"operator for the bit-vector repeat"
 
 constant BITVECTOR_ZERO_EXTEND_OP \
 	::CVC4::BitVectorZeroExtend \
-	"::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorZeroExtend >" \
+	"::CVC4::UnsignedHashFunction< ::CVC4::BitVectorZeroExtend >" \
 	"util/bitvector.h" \
 	"operator for the bit-vector zero-extend"
 
 constant BITVECTOR_SIGN_EXTEND_OP \
 	::CVC4::BitVectorSignExtend \
-	"::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorSignExtend >" \
+	"::CVC4::UnsignedHashFunction< ::CVC4::BitVectorSignExtend >" \
 	"util/bitvector.h" \
 	"operator for the bit-vector sign-extend"
 
 constant BITVECTOR_ROTATE_LEFT_OP \
 	::CVC4::BitVectorRotateLeft \
-	"::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorRotateLeft >" \
+	"::CVC4::UnsignedHashFunction< ::CVC4::BitVectorRotateLeft >" \
 	"util/bitvector.h" \
 	"operator for the bit-vector rotate left"
 
 constant BITVECTOR_ROTATE_RIGHT_OP \
 	::CVC4::BitVectorRotateRight \
-	"::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorRotateRight >" \
+	"::CVC4::UnsignedHashFunction< ::CVC4::BitVectorRotateRight >" \
 	"util/bitvector.h" \
 	"operator for the bit-vector rotate right"
 
diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index e66cc3454..58c8fb5d2 100644
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -44,7 +44,7 @@ parameterized APPLY_TESTER TESTER_TYPE 1: "tester application"
 
 constant DATATYPE_TYPE \
     ::CVC4::Datatype \
-    "::CVC4::DatatypeHashStrategy" \
+    "::CVC4::DatatypeHashFunction" \
     "util/datatype.h" \
     "datatype type"
 cardinality DATATYPE_TYPE \
@@ -72,7 +72,7 @@ parameterized APPLY_TYPE_ASCRIPTION ASCRIPTION_TYPE 1 \
     "type ascription, for datatype constructor applications"
 constant ASCRIPTION_TYPE \
     ::CVC4::AscriptionType \
-    ::CVC4::AscriptionTypeHashStrategy \
+    ::CVC4::AscriptionTypeHashFunction \
     "util/ascription_type.h" \
     "a type parameter for type ascription"
 
diff --git a/src/theory/ite_simplifier.h b/src/theory/ite_simplifier.h
index fb42909e0..cba5c7051 100644
--- a/src/theory/ite_simplifier.h
+++ b/src/theory/ite_simplifier.h
@@ -69,7 +69,7 @@ class ITESimplifier {
       hash ^= 0x9e3779b9 + NodeHashFunction().operator()(pair.second) + (hash << 6) + (hash >> 2);
       return hash;
     }
-  };
+  };/* struct ITESimplifier::NodePairHashFunction */
 
   typedef std::hash_map<NodePair, Node, NodePairHashFunction> NodePairMap;
 
diff --git a/src/util/array_store_all.h b/src/util/array_store_all.h
index 834eec2c3..277422ecf 100644
--- a/src/util/array_store_all.h
+++ b/src/util/array_store_all.h
@@ -88,12 +88,12 @@ public:
 std::ostream& operator<<(std::ostream& out, const ArrayStoreAll& asa) CVC4_PUBLIC;
 
 /**
- * Hash function for the BitVector constants.
+ * Hash function for the ArrayStoreAll constants.
  */
-struct CVC4_PUBLIC ArrayStoreAllHashStrategy {
-  static inline size_t hash(const ArrayStoreAll& asa) {
+struct CVC4_PUBLIC ArrayStoreAllHashFunction {
+  inline size_t operator()(const ArrayStoreAll& asa) const {
     return TypeHashFunction()(asa.getType()) * ExprHashFunction()(asa.getExpr());
   }
-};/* struct ArrayStoreAllHashStrategy */
+};/* struct ArrayStoreAllHashFunction */
 
 }/* CVC4 namespace */
diff --git a/src/util/ascription_type.h b/src/util/ascription_type.h
index 81289572c..579746332 100644
--- a/src/util/ascription_type.h
+++ b/src/util/ascription_type.h
@@ -48,11 +48,11 @@ public:
 /**
  * A hash strategy for type ascription operators.
  */
-struct CVC4_PUBLIC AscriptionTypeHashStrategy {
-  static inline size_t hash(const AscriptionType& at) {
+struct CVC4_PUBLIC AscriptionTypeHashFunction {
+  inline size_t operator()(const AscriptionType& at) const {
     return TypeHashFunction()(at.getType());
   }
-};/* struct AscriptionTypeHashStrategy */
+};/* struct AscriptionTypeHashFunction */
 
 /** An output routine for AscriptionTypes */
 inline std::ostream& operator<<(std::ostream& out, AscriptionType at) {
diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index 5d0c301d4..185bb55d9 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -375,11 +375,11 @@ inline BitVector::BitVector(const std::string& num, unsigned base) {
 /**
  * Hash function for the BitVector constants.
  */
-struct CVC4_PUBLIC BitVectorHashStrategy {
-  static inline size_t hash(const BitVector& bv) {
+struct CVC4_PUBLIC BitVectorHashFunction {
+  inline size_t operator()(const BitVector& bv) const {
     return bv.hash();
   }
-};/* struct BitVectorHashStrategy */
+};/* struct BitVectorHashFunction */
 
 /**
  * The structure representing the extraction operation for bit-vectors. The
@@ -403,14 +403,13 @@ struct CVC4_PUBLIC BitVectorExtract {
 /**
  * Hash function for the BitVectorExtract objects.
  */
-class CVC4_PUBLIC BitVectorExtractHashStrategy {
-public:
-  static size_t hash(const BitVectorExtract& extract) {
+struct CVC4_PUBLIC BitVectorExtractHashFunction {
+  size_t operator()(const BitVectorExtract& extract) const {
     size_t hash = extract.low;
     hash ^= extract.high + 0x9e3779b9 + (hash << 6) + (hash >> 2);
     return hash;
   }
-};/* class BitVectorExtractHashStrategy */
+};/* struct BitVectorExtractHashFunction */
 
 
 /**
@@ -430,12 +429,11 @@ struct CVC4_PUBLIC BitVectorBitOf {
 /**
  * Hash function for the BitVectorBitOf objects.
  */
-class CVC4_PUBLIC BitVectorBitOfHashStrategy {
-public:
-  static size_t hash(const BitVectorBitOf& b) {
+struct CVC4_PUBLIC BitVectorBitOfHashFunction {
+  size_t operator()(const BitVectorBitOf& b) const {
     return b.bitIndex;
   }
-};/* class BitVectorBitOfHashStrategy */
+};/* struct BitVectorBitOfHashFunction */
 
 
 
@@ -482,11 +480,11 @@ struct CVC4_PUBLIC BitVectorRotateRight {
 };/* struct BitVectorRotateRight */
 
 template <typename T>
-struct CVC4_PUBLIC UnsignedHashStrategy {
-  static inline size_t hash(const T& x) {
+struct CVC4_PUBLIC UnsignedHashFunction {
+  inline size_t operator()(const T& x) const {
     return (size_t)x;
   }
-};/* struct UnsignedHashStrategy */
+};/* struct UnsignedHashFunction */
 
 inline std::ostream& operator <<(std::ostream& os, const BitVector& bv) CVC4_PUBLIC;
 inline std::ostream& operator <<(std::ostream& os, const BitVector& bv) {
@@ -503,8 +501,6 @@ inline std::ostream& operator <<(std::ostream& os, const BitVectorBitOf& bv) {
   return os << "[" << bv.bitIndex << "]";
 }
 
-
-
 }/* CVC4 namespace */
 
 #endif /* __CVC4__BITVECTOR_H */
diff --git a/src/util/bool.h b/src/util/bool.h
index a4d33ca61..9985395e3 100644
--- a/src/util/bool.h
+++ b/src/util/bool.h
@@ -29,11 +29,11 @@
 
 namespace CVC4 {
 
-struct BoolHashStrategy {
-  static inline size_t hash(bool b) {
+struct BoolHashFunction {
+  inline size_t operator()(bool b) const {
     return b;
   }
-};/* struct BoolHashStrategy */
+};/* struct BoolHashFunction */
 
 }/* CVC4 namespace */
 
diff --git a/src/util/datatype.h b/src/util/datatype.h
index b701073c7..c7631ae7b 100644
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -560,17 +560,6 @@ public:
 };/* class Datatype */
 
 /**
- * A hash strategy for Datatypes.  Needed because Datatypes are used
- * as the constant payload in CONSTANT-kinded TypeNodes (for
- * DATATYPE_TYPE expressions).
- */
-struct CVC4_PUBLIC DatatypeHashStrategy {
-  static inline size_t hash(const Datatype& dt) {
-    return StringHashFunction()(dt.getName());
-  }
-};/* struct DatatypeHashStrategy */
-
-/**
  * A hash function for Datatypes.  Needed to store them in hash sets
  * and hash maps.
  */
diff --git a/src/util/hash.h b/src/util/hash.h
index 6fb20dab0..2420b7acd 100644
--- a/src/util/hash.h
+++ b/src/util/hash.h
@@ -54,12 +54,6 @@ struct StringHashFunction {
   }
 };/* struct StringHashFunction */
 
-struct StringHashStrategy {
-  static size_t hash(const std::string& str) {
-    return std::hash<const char*>()(str.c_str());
-  }
-};/* struct StringHashStrategy */
-
 }/* CVC4 namespace */
 
 #endif /* __CVC4__HASH_H */
diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index 43b77df6a..71d6d5b6d 100644
--- a/src/util/integer_cln_imp.h
+++ b/src/util/integer_cln_imp.h
@@ -460,11 +460,11 @@ public:
   friend class CVC4::Rational;
 };/* class Integer */
 
-struct IntegerHashStrategy {
-  static inline size_t hash(const CVC4::Integer& i) {
+struct IntegerHashFunction {
+  inline size_t operator()(const CVC4::Integer& i) const {
     return i.hash();
   }
-};/* struct IntegerHashStrategy */
+};/* struct IntegerHashFunction */
 
 inline std::ostream& operator<<(std::ostream& os, const Integer& n) {
   return os << n.toString();
diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
index dfd6c0599..ea7967023 100644
--- a/src/util/integer_gmp_imp.h
+++ b/src/util/integer_gmp_imp.h
@@ -418,11 +418,11 @@ public:
   friend class CVC4::Rational;
 };/* class Integer */
 
-struct IntegerHashStrategy {
-  static inline size_t hash(const CVC4::Integer& i) {
+struct IntegerHashFunction {
+  inline size_t operator()(const CVC4::Integer& i) const {
     return i.hash();
   }
-};/* struct IntegerHashStrategy */
+};/* struct IntegerHashFunction */
 
 inline std::ostream& operator<<(std::ostream& os, const Integer& n) {
   return os << n.toString();
diff --git a/src/util/predicate.cpp b/src/util/predicate.cpp
index 1868f557d..748e818c3 100644
--- a/src/util/predicate.cpp
+++ b/src/util/predicate.cpp
@@ -49,7 +49,7 @@ operator<<(std::ostream& out, const Predicate& p) {
   return out;
 }
 
-size_t PredicateHashStrategy::hash(const Predicate& p) {
+size_t PredicateHashFunction::operator()(const Predicate& p) const {
   ExprHashFunction h;
   return h(p.d_witness) * 5039 + h(p.d_predicate);
 }
diff --git a/src/util/predicate.h b/src/util/predicate.h
index 94a685177..18e0b8b70 100644
--- a/src/util/predicate.h
+++ b/src/util/predicate.h
@@ -31,9 +31,9 @@ class Predicate;
 
 std::ostream& operator<<(std::ostream& out, const Predicate& p) CVC4_PUBLIC;
 
-struct CVC4_PUBLIC PredicateHashStrategy {
-  static size_t hash(const Predicate& p);
-};/* class PredicateHashStrategy */
+struct CVC4_PUBLIC PredicateHashFunction {
+  size_t operator()(const Predicate& p) const;
+};/* class PredicateHashFunction */
 
 }/* CVC4 namespace */
 
@@ -55,7 +55,7 @@ public:
   bool operator==(const Predicate& p) const;
 
   friend std::ostream& operator<<(std::ostream& out, const Predicate& p);
-  friend size_t PredicateHashStrategy::hash(const Predicate& p);
+  friend size_t PredicateHashFunction::operator()(const Predicate& p) const;
 
 };/* class Predicate */
 
diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h
index ea9f7d055..258060e02 100644
--- a/src/util/rational_cln_imp.h
+++ b/src/util/rational_cln_imp.h
@@ -314,11 +314,11 @@ public:
 
 };/* class Rational */
 
-struct RationalHashStrategy {
-  static inline size_t hash(const CVC4::Rational& r) {
+struct RationalHashFunction {
+  inline size_t operator()(const CVC4::Rational& r) const {
     return r.hash();
   }
-};/* struct RationalHashStrategy */
+};/* struct RationalHashFunction */
 
 CVC4_PUBLIC std::ostream& operator<<(std::ostream& os, const Rational& n);
 
diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h
index ed9c57a80..22f1e91b2 100644
--- a/src/util/rational_gmp_imp.h
+++ b/src/util/rational_gmp_imp.h
@@ -296,11 +296,11 @@ public:
 
 };/* class Rational */
 
-struct RationalHashStrategy {
-  static inline size_t hash(const CVC4::Rational& r) {
+struct RationalHashFunction {
+  inline size_t operator()(const CVC4::Rational& r) const {
     return r.hash();
   }
-};/* struct RationalHashStrategy */
+};/* struct RationalHashFunction */
 
 CVC4_PUBLIC std::ostream& operator<<(std::ostream& os, const Rational& n);
 
diff --git a/src/util/subrange_bound.h b/src/util/subrange_bound.h
index 063e59a0f..5de17106d 100644
--- a/src/util/subrange_bound.h
+++ b/src/util/subrange_bound.h
@@ -230,15 +230,15 @@ public:
 
 };/* class SubrangeBounds */
 
-struct CVC4_PUBLIC SubrangeBoundsHashStrategy {
-  static inline size_t hash(const SubrangeBounds& bounds) {
+struct CVC4_PUBLIC SubrangeBoundsHashFunction {
+  inline size_t operator()(const SubrangeBounds& bounds) const {
     // We use Integer::hash() rather than Integer::getUnsignedLong()
     // because the latter might overflow and throw an exception
     size_t l = bounds.lower.hasBound() ? bounds.lower.getBound().hash() : std::numeric_limits<size_t>::max();
     size_t u = bounds.upper.hasBound() ? bounds.upper.getBound().hash() : std::numeric_limits<size_t>::max();
     return l + 0x9e3779b9 + (u << 6) + (u >> 2);
   }
-};/* struct SubrangeBoundsHashStrategy */
+};/* struct SubrangeBoundsHashFunction */
 
 inline std::ostream&
 operator<<(std::ostream& out, const SubrangeBound& bound) throw() CVC4_PUBLIC;
diff --git a/src/util/uninterpreted_constant.h b/src/util/uninterpreted_constant.h
index 418b8d333..792da178e 100644
--- a/src/util/uninterpreted_constant.h
+++ b/src/util/uninterpreted_constant.h
@@ -77,10 +77,10 @@ std::ostream& operator<<(std::ostream& out, const UninterpretedConstant& uc) CVC
 /**
  * Hash function for the BitVector constants.
  */
-struct CVC4_PUBLIC UninterpretedConstantHashStrategy {
-  static inline size_t hash(const UninterpretedConstant& uc) {
-    return TypeHashFunction()(uc.getType()) * IntegerHashStrategy::hash(uc.getIndex());
+struct CVC4_PUBLIC UninterpretedConstantHashFunction {
+  inline size_t operator()(const UninterpretedConstant& uc) const {
+    return TypeHashFunction()(uc.getType()) * IntegerHashFunction()(uc.getIndex());
   }
-};/* struct UninterpretedConstantHashStrategy */
+};/* struct UninterpretedConstantHashFunction */
 
 }/* CVC4 namespace */
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index 88d21cac5..470fdac3d 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -17,7 +17,7 @@ UNIT_TESTS = \
 	expr/node_manager_white \
 	expr/attribute_white \
 	expr/attribute_black \
-	expr/declaration_scope_black \
+	expr/symbol_table_black \
 	expr/node_self_iterator_black \
 	expr/type_cardinality_public \
 	expr/type_node_white \
@@ -30,7 +30,6 @@ UNIT_TESTS = \
 	context/cdo_black \
 	context/cdlist_black \
 	context/cdlist_context_memory_black \
-	context/cdcirclist_white \
 	context/cdmap_black \
 	context/cdmap_white \
 	context/cdvector_black \
diff --git a/test/unit/context/cdcirclist_white.h b/test/unit/context/cdcirclist_white.h
deleted file mode 100644
index b03a850a8..000000000
--- a/test/unit/context/cdcirclist_white.h
+++ /dev/null
@@ -1,223 +0,0 @@
-/*********************                                                        */
-/*! \file cdcirclist_white.h
- ** \verbatim
- ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  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.\endverbatim
- **
- ** \brief White box testing of CVC4::context::CDCircList<>.
- **
- ** White box testing of CVC4::context::CDCircList<>.
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include <vector>
-#include <iostream>
-
-#include <limits.h>
-
-#include "context/context.h"
-#include "context/cdcirclist.h"
-
-#include "util/output.h"
-
-using namespace std;
-using namespace CVC4::context;
-using namespace CVC4;
-
-class CDCircListWhite : public CxxTest::TestSuite {
-private:
-
-  Context* d_context;
-
-public:
-
-  void setUp() {
-    d_context = new Context();
-  }
-
-  void tearDown() {
-    delete d_context;
-  }
-
-  void testSimple() {
-    //Debug.on("cdcirclist");
-    CDCircList<int> l(d_context, ContextMemoryAllocator<int>(d_context->getCMM()));
-
-    TS_ASSERT_THROWS_NOTHING( l.debugCheck() );
-
-    d_context->push();
-    {
-      TS_ASSERT(l.empty());
-      l.push_back(1);
-      TS_ASSERT(!l.empty());
-      TS_ASSERT_EQUALS(l.front(), 1);
-      TS_ASSERT_EQUALS(l.back(), 1);
-      TS_ASSERT_THROWS_NOTHING( l.debugCheck() );
-
-      l.push_back(2);
-      TS_ASSERT(!l.empty());
-      TS_ASSERT_EQUALS(l.front(), 1);
-      TS_ASSERT_EQUALS(l.back(), 2);
-      TS_ASSERT_THROWS_NOTHING( l.debugCheck() );
-
-      l.push_back(3);
-      TS_ASSERT(!l.empty());
-      TS_ASSERT_EQUALS(l.front(), 1);
-      TS_ASSERT_EQUALS(l.back(), 3);
-      TS_ASSERT_THROWS_NOTHING( l.debugCheck() );
-
-#ifdef CVC4_ASSERTIONS
-      TS_ASSERT_THROWS( l.concat(l), AssertionException );
-#endif /* CVC4_ASSERTIONS */
-
-      CDCircList<int> l2(d_context, ContextMemoryAllocator<int>(d_context->getCMM()));
-      l2.push_back(4);
-      l2.push_back(5);
-      l2.push_back(6);
-      TS_ASSERT_EQUALS(l2.front(), 4);
-      TS_ASSERT_EQUALS(l2.back(), 6);
-      TS_ASSERT_THROWS_NOTHING( l2.debugCheck() );
-
-      d_context->push();
-      {
-        l.concat(l2);
-
-        TS_ASSERT_EQUALS(l.front(), 1);
-        TS_ASSERT_EQUALS(l.back(), 6);
-        TS_ASSERT_THROWS_NOTHING( l.debugCheck() );
-
-        TS_ASSERT_EQUALS(l2.front(), 4);
-        TS_ASSERT_EQUALS(l2.back(), 3);
-        TS_ASSERT_THROWS_NOTHING( l2.debugCheck() );
-
-        d_context->push();
-        {
-          CDCircList<int>::iterator i = l.begin();
-          CDCircList<int>::iterator j = l.begin();
-          TS_ASSERT_EQUALS(i, j);
-          TS_ASSERT_EQUALS(i++, j);
-          TS_ASSERT_EQUALS(i, ++j);
-          TS_ASSERT_EQUALS(l.erase(l.begin()), i);
-
-          i = l.begin();
-          TS_ASSERT_EQUALS(i, j); TS_ASSERT_DIFFERS(i, l.end());
-          TS_ASSERT_EQUALS(*i, l.front()); TS_ASSERT_DIFFERS(i, l.end());
-          TS_ASSERT_EQUALS(*i, 2); TS_ASSERT_DIFFERS(i, l.end());
-          TS_ASSERT_EQUALS(*i++, 2); TS_ASSERT_DIFFERS(i, l.end()); TS_ASSERT_DIFFERS(i, j);
-          TS_ASSERT_EQUALS(*i++, 3); TS_ASSERT_DIFFERS(i, l.end()); TS_ASSERT_DIFFERS(i, j);
-          TS_ASSERT_EQUALS(*i++, 4); TS_ASSERT_DIFFERS(i, l.end()); TS_ASSERT_DIFFERS(i, j);
-          TS_ASSERT_EQUALS(*i++, 5); TS_ASSERT_DIFFERS(i, l.end()); TS_ASSERT_DIFFERS(i, j);
-          TS_ASSERT_EQUALS(*i++, 6); TS_ASSERT_EQUALS(i, l.end()); TS_ASSERT_DIFFERS(i, j);
-          TS_ASSERT_EQUALS(*--i, 6); TS_ASSERT_DIFFERS(i, l.end()); TS_ASSERT_DIFFERS(i, j);
-          TS_ASSERT_EQUALS(*--i, 5); TS_ASSERT_DIFFERS(i, l.end()); TS_ASSERT_DIFFERS(i, j);
-          TS_ASSERT_EQUALS(*--i, 4); TS_ASSERT_DIFFERS(i, l.end()); TS_ASSERT_DIFFERS(i, j);
-          TS_ASSERT_EQUALS(*--i, 3); TS_ASSERT_DIFFERS(i, l.end()); TS_ASSERT_DIFFERS(i, j);
-          TS_ASSERT_EQUALS(*--i, 2); TS_ASSERT_DIFFERS(i, l.end());
-          TS_ASSERT_EQUALS(i, l.begin()); TS_ASSERT_EQUALS(i, j);
-
-          TS_ASSERT_THROWS_NOTHING( l.debugCheck() );
-          TS_ASSERT_THROWS_NOTHING( l2.debugCheck() );
-        }
-        d_context->pop();
-
-        CDCircList<int>::iterator i = l.begin();
-        TS_ASSERT_EQUALS(*i, l.front()); TS_ASSERT_DIFFERS(i, l.end());
-        TS_ASSERT_EQUALS(*i++, 1); TS_ASSERT_DIFFERS(i, l.end());
-        TS_ASSERT_EQUALS(*i++, 2); TS_ASSERT_DIFFERS(i, l.end());
-        TS_ASSERT_EQUALS(*i++, 3); TS_ASSERT_DIFFERS(i, l.end());
-        TS_ASSERT_EQUALS(*i++, 4); TS_ASSERT_DIFFERS(i, l.end());
-        TS_ASSERT_EQUALS(*i++, 5); TS_ASSERT_DIFFERS(i, l.end());
-        TS_ASSERT_EQUALS(*i++, 6); TS_ASSERT_EQUALS(i, l.end());
-        TS_ASSERT_EQUALS(*--i, 6); TS_ASSERT_DIFFERS(i, l.end());
-        TS_ASSERT_EQUALS(*--i, 5); TS_ASSERT_DIFFERS(i, l.end());
-        TS_ASSERT_EQUALS(*--i, 4); TS_ASSERT_DIFFERS(i, l.end());
-        TS_ASSERT_EQUALS(*--i, 3); TS_ASSERT_DIFFERS(i, l.end());
-        TS_ASSERT_EQUALS(*--i, 2); TS_ASSERT_DIFFERS(i, l.end());
-        TS_ASSERT_EQUALS(*--i, 1); TS_ASSERT_DIFFERS(i, l.end());
-        TS_ASSERT_EQUALS(i, l.begin());
-
-        i = l2.begin();
-        TS_ASSERT_EQUALS(*i, l2.front()); TS_ASSERT_DIFFERS(i, l2.end());
-        TS_ASSERT_EQUALS(*i++, 4); TS_ASSERT_DIFFERS(i, l2.end());
-        TS_ASSERT_EQUALS(*i++, 5); TS_ASSERT_DIFFERS(i, l2.end());
-        TS_ASSERT_EQUALS(*i++, 6); TS_ASSERT_DIFFERS(i, l2.end());
-        TS_ASSERT_EQUALS(*i++, 1); TS_ASSERT_DIFFERS(i, l2.end());
-        TS_ASSERT_EQUALS(*i++, 2); TS_ASSERT_DIFFERS(i, l2.end());
-        TS_ASSERT_EQUALS(*i++, 3); TS_ASSERT_EQUALS(i, l2.end());
-        TS_ASSERT_EQUALS(*--i, 3); TS_ASSERT_DIFFERS(i, l2.end());
-        TS_ASSERT_EQUALS(*--i, 2); TS_ASSERT_DIFFERS(i, l2.end());
-        TS_ASSERT_EQUALS(*--i, 1); TS_ASSERT_DIFFERS(i, l2.end());
-        TS_ASSERT_EQUALS(*--i, 6); TS_ASSERT_DIFFERS(i, l2.end());
-        TS_ASSERT_EQUALS(*--i, 5); TS_ASSERT_DIFFERS(i, l2.end());
-        TS_ASSERT_EQUALS(*--i, 4); TS_ASSERT_DIFFERS(i, l2.end());
-        TS_ASSERT_EQUALS(i, l2.begin());
-
-        TS_ASSERT_THROWS_NOTHING( l.debugCheck() );
-        TS_ASSERT_THROWS_NOTHING( l2.debugCheck() );
-      }
-      d_context->pop();
-
-      TS_ASSERT(! l.empty());
-      TS_ASSERT(! l2.empty());
-
-      CDCircList<int>::iterator i = l.begin();
-      TS_ASSERT_EQUALS(*i, l.front()); TS_ASSERT_DIFFERS(i, l.end());
-      TS_ASSERT_EQUALS(*i++, 1); TS_ASSERT_DIFFERS(i, l.end());
-      TS_ASSERT_EQUALS(*i++, 2); TS_ASSERT_DIFFERS(i, l.end());
-      TS_ASSERT_EQUALS(*i++, 3); TS_ASSERT_EQUALS(i, l.end());
-      TS_ASSERT_EQUALS(*--i, 3); TS_ASSERT_DIFFERS(i, l.end());
-      TS_ASSERT_EQUALS(*--i, 2); TS_ASSERT_DIFFERS(i, l.end());
-      TS_ASSERT_EQUALS(*--i, 1); TS_ASSERT_DIFFERS(i, l.end());
-      TS_ASSERT_EQUALS(i, l.begin());
-
-      i = l2.begin();
-      TS_ASSERT_EQUALS(*i, l2.front()); TS_ASSERT_DIFFERS(i, l2.end());
-      TS_ASSERT_EQUALS(*i++, 4); TS_ASSERT_DIFFERS(i, l2.end());
-      TS_ASSERT_EQUALS(*i++, 5); TS_ASSERT_DIFFERS(i, l2.end());
-      TS_ASSERT_EQUALS(*i++, 6); TS_ASSERT_EQUALS(i, l2.end());
-      TS_ASSERT_EQUALS(*--i, 6); TS_ASSERT_DIFFERS(i, l2.end());
-      TS_ASSERT_EQUALS(*--i, 5); TS_ASSERT_DIFFERS(i, l2.end());
-      TS_ASSERT_EQUALS(*--i, 4); TS_ASSERT_DIFFERS(i, l2.end());
-      TS_ASSERT_EQUALS(i, l2.begin());
-
-      TS_ASSERT_THROWS_NOTHING( l.debugCheck() );
-      TS_ASSERT_THROWS_NOTHING( l2.debugCheck() );
-    }
-    d_context->pop();
-
-    TS_ASSERT(l.empty());
-    TS_ASSERT_THROWS_NOTHING( l.debugCheck() );
-  }
-
-  void testCDPtr() {
-    int* x = (int*)0x12345678;
-    int* y = (int*)0x87654321;
-    CDPtr<int> p(d_context, NULL);
-    TS_ASSERT(p == NULL);
-    d_context->push();
-    TS_ASSERT(p == NULL);
-    d_context->push();
-    TS_ASSERT(p == NULL);
-    p = x;
-    TS_ASSERT(p == x);
-    d_context->push();
-    TS_ASSERT(p == x);
-    p = y;
-    TS_ASSERT(p == y);
-    d_context->pop();
-    TS_ASSERT(p == x);
-    d_context->pop();
-    TS_ASSERT(p == NULL);
-    d_context->pop();
-    TS_ASSERT(p == NULL);
-  }
-
-};/* class CDCircListWhite */
diff --git a/test/unit/expr/declaration_scope_black.h b/test/unit/expr/symbol_table_black.h
index bde04157c..89fbf42e8 100644
--- a/test/unit/expr/declaration_scope_black.h
+++ b/test/unit/expr/symbol_table_black.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file declaration_scope_black.h
+/*! \file symbol_table_black.h
  ** \verbatim
  ** Original author: cconway
  ** Major contributors: none
@@ -11,9 +11,9 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief Black box testing of CVC4::DeclarationScope.
+ ** \brief Black box testing of CVC4::SymbolTable
  **
- ** Black box testing of CVC4::DeclarationScope.
+ ** Black box testing of CVC4::SymbolTable.
  **/
 
 #include <cxxtest/TestSuite.h>
@@ -22,7 +22,7 @@
 #include <string>
 
 #include "context/context.h"
-#include "expr/declaration_scope.h"
+#include "expr/symbol_table.h"
 #include "expr/expr_manager.h"
 #include "expr/expr.h"
 #include "expr/type.h"
@@ -34,7 +34,7 @@ using namespace CVC4::kind;
 using namespace CVC4::context;
 using namespace std;
 
-class DeclarationScopeBlack : public CxxTest::TestSuite {
+class SymbolTableBlack : public CxxTest::TestSuite {
 private:
 
   ExprManager* d_exprManager;
@@ -60,104 +60,104 @@ public:
   }
 
   void testBind() {
-    DeclarationScope declScope;
+    SymbolTable symtab;
     Type booleanType = d_exprManager->booleanType();
     Expr x = d_exprManager->mkVar(booleanType);
-    declScope.bind("x",x);
-    TS_ASSERT( declScope.isBound("x") );
-    TS_ASSERT_EQUALS( declScope.lookup("x"), x );
+    symtab.bind("x",x);
+    TS_ASSERT( symtab.isBound("x") );
+    TS_ASSERT_EQUALS( symtab.lookup("x"), x );
   }
 
   void testBind2() {
-    DeclarationScope declScope;
+    SymbolTable symtab;
     Type booleanType = d_exprManager->booleanType();
     // var name attribute shouldn't matter
     Expr y = d_exprManager->mkVar("y", booleanType);
-    declScope.bind("x",y);
-    TS_ASSERT( declScope.isBound("x") );
-    TS_ASSERT_EQUALS( declScope.lookup("x"), y );
+    symtab.bind("x",y);
+    TS_ASSERT( symtab.isBound("x") );
+    TS_ASSERT_EQUALS( symtab.lookup("x"), y );
   }
 
   void testBind3() {
-    DeclarationScope declScope;
+    SymbolTable symtab;
     Type booleanType = d_exprManager->booleanType();
     Expr x = d_exprManager->mkVar(booleanType);
-    declScope.bind("x",x);
+    symtab.bind("x",x);
     Expr y = d_exprManager->mkVar(booleanType);
     // new binding covers old
-    declScope.bind("x",y);
-    TS_ASSERT( declScope.isBound("x") );
-    TS_ASSERT_EQUALS( declScope.lookup("x"), y );
+    symtab.bind("x",y);
+    TS_ASSERT( symtab.isBound("x") );
+    TS_ASSERT_EQUALS( symtab.lookup("x"), y );
   }
 
   void testBind4() {
-    DeclarationScope declScope;
+    SymbolTable symtab;
     Type booleanType = d_exprManager->booleanType();
     Expr x = d_exprManager->mkVar(booleanType);
-    declScope.bind("x",x);
+    symtab.bind("x",x);
 
     Type t = d_exprManager->mkSort("T");
     // duplicate binding for type is OK
-    declScope.bindType("x",t);
+    symtab.bindType("x",t);
 
-    TS_ASSERT( declScope.isBound("x") );
-    TS_ASSERT_EQUALS( declScope.lookup("x"), x );
-    TS_ASSERT( declScope.isBoundType("x") );
-    TS_ASSERT_EQUALS( declScope.lookupType("x"), t );
+    TS_ASSERT( symtab.isBound("x") );
+    TS_ASSERT_EQUALS( symtab.lookup("x"), x );
+    TS_ASSERT( symtab.isBoundType("x") );
+    TS_ASSERT_EQUALS( symtab.lookupType("x"), t );
   }
 
   void testBindType() {
-    DeclarationScope declScope;
+    SymbolTable symtab;
     Type s = d_exprManager->mkSort("S");
-    declScope.bindType("S",s);
-    TS_ASSERT( declScope.isBoundType("S") );
-    TS_ASSERT_EQUALS( declScope.lookupType("S"), s );
+    symtab.bindType("S",s);
+    TS_ASSERT( symtab.isBoundType("S") );
+    TS_ASSERT_EQUALS( symtab.lookupType("S"), s );
   }
 
   void testBindType2() {
-    DeclarationScope declScope;
+    SymbolTable symtab;
     // type name attribute shouldn't matter
     Type s = d_exprManager->mkSort("S");
-    declScope.bindType("T",s);
-    TS_ASSERT( declScope.isBoundType("T") );
-    TS_ASSERT_EQUALS( declScope.lookupType("T"), s );
+    symtab.bindType("T",s);
+    TS_ASSERT( symtab.isBoundType("T") );
+    TS_ASSERT_EQUALS( symtab.lookupType("T"), s );
   }
 
   void testBindType3() {
-    DeclarationScope declScope;
+    SymbolTable symtab;
     Type s = d_exprManager->mkSort("S");
-    declScope.bindType("S",s);
+    symtab.bindType("S",s);
     Type t = d_exprManager->mkSort("T");
     // new binding covers old
-    declScope.bindType("S",t);
-    TS_ASSERT( declScope.isBoundType("S") );
-    TS_ASSERT_EQUALS( declScope.lookupType("S"), t );
+    symtab.bindType("S",t);
+    TS_ASSERT( symtab.isBoundType("S") );
+    TS_ASSERT_EQUALS( symtab.lookupType("S"), t );
   }
 
   void testPushScope() {
-    DeclarationScope declScope;
+    SymbolTable symtab;
     Type booleanType = d_exprManager->booleanType();
     Expr x = d_exprManager->mkVar(booleanType);
-    declScope.bind("x",x);
-    declScope.pushScope();
+    symtab.bind("x",x);
+    symtab.pushScope();
 
-    TS_ASSERT( declScope.isBound("x") );
-    TS_ASSERT_EQUALS( declScope.lookup("x"), x );
+    TS_ASSERT( symtab.isBound("x") );
+    TS_ASSERT_EQUALS( symtab.lookup("x"), x );
 
     Expr y = d_exprManager->mkVar(booleanType);
-    declScope.bind("x",y);
+    symtab.bind("x",y);
 
-    TS_ASSERT( declScope.isBound("x") );
-    TS_ASSERT_EQUALS( declScope.lookup("x"), y );
+    TS_ASSERT( symtab.isBound("x") );
+    TS_ASSERT_EQUALS( symtab.lookup("x"), y );
 
-    declScope.popScope();
-    TS_ASSERT( declScope.isBound("x") );
-    TS_ASSERT_EQUALS( declScope.lookup("x"), x );
+    symtab.popScope();
+    TS_ASSERT( symtab.isBound("x") );
+    TS_ASSERT_EQUALS( symtab.lookup("x"), x );
   }
 
   void testBadPop() {
-    DeclarationScope declScope;
+    SymbolTable symtab;
     // TODO: What kind of exception gets thrown here?
-    TS_ASSERT_THROWS( declScope.popScope(), ScopeException );
+    TS_ASSERT_THROWS( symtab.popScope(), ScopeException );
   }
-};
+};/* class SymbolTableBlack */