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)

10 files changed, 67 insertions, 65 deletions

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"