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)

3 files changed, 53 insertions, 277 deletions

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