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)

1 files changed, 211 insertions, 0 deletions

diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp
new file mode 100644
index 000000000..c9234b5e0
--- /dev/null
+++ b/src/expr/symbol_table.cpp
@@ -0,0 +1,211 @@
+/*********************                                                        */
+/*! \file symbol_table.cpp
+ ** \verbatim
+ ** Original author: cconway
+ ** Major contributors: bobot, mdeters
+ ** Minor contributors (to current version): ajreynol, dejan
+ ** This file is part of the CVC4 prototype.
+ ** 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)
+ **
+ ** Convenience class for scoping variable and type declarations
+ ** (implementation).
+ **/
+
+#include "expr/symbol_table.h"
+#include "expr/expr.h"
+#include "expr/type.h"
+#include "expr/expr_manager_scope.h"
+#include "context/cdhashmap.h"
+#include "context/cdhashset.h"
+#include "context/context.h"
+
+#include <string>
+#include <utility>
+
+using namespace CVC4;
+using namespace CVC4::context;
+using namespace std;
+
+namespace CVC4 {
+
+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)) {
+}
+
+SymbolTable::~SymbolTable() {
+  d_exprMap->deleteSelf();
+  d_typeMap->deleteSelf();
+  d_functions->deleteSelf();
+  delete d_context;
+}
+
+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);
+  if(levelZero) d_exprMap->insertAtContextLevelZero(name, obj);
+  else d_exprMap->insert(name, 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);
+  if(levelZero){
+    d_exprMap->insertAtContextLevelZero(name, obj);
+    d_functions->insertAtContextLevelZero(obj);
+  } else {
+    d_exprMap->insert(name, obj);
+    d_functions->insert(obj);
+  }
+}
+
+bool SymbolTable::isBound(const std::string& name) const throw() {
+  return d_exprMap->find(name) != d_exprMap->end();
+}
+
+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 SymbolTable::isBoundDefinedFunction(Expr func) const throw() {
+  return d_functions->contains(func);
+}
+
+Expr SymbolTable::lookup(const std::string& name) const throw(AssertionException) {
+  return (*d_exprMap->find(name)).second;
+}
+
+void SymbolTable::bindType(const std::string& name, Type t,
+                                bool levelZero) throw() {
+  if(levelZero){
+    d_typeMap->insertAtContextLevelZero(name, make_pair(vector<Type>(), t));
+  }else{
+    d_typeMap->insert(name, make_pair(vector<Type>(), t));
+  }
+}
+
+void SymbolTable::bindType(const std::string& name,
+                                const std::vector<Type>& params,
+                                Type t,
+                                bool levelZero) throw() {
+  if(Debug.isOn("sort")) {
+    Debug("sort") << "bindType(" << name << ", [";
+    if(params.size() > 0) {
+      copy( params.begin(), params.end() - 1,
+            ostream_iterator<Type>(Debug("sort"), ", ") );
+      Debug("sort") << params.back();
+    }
+    Debug("sort") << "], " << t << ")" << endl;
+  }
+  if(levelZero){
+    d_typeMap->insertAtContextLevelZero(name, make_pair(params, t));
+  } else {
+    d_typeMap->insert(name, make_pair(params, t));
+  }
+}
+
+bool SymbolTable::isBoundType(const std::string& name) const throw() {
+  return d_typeMap->find(name) != d_typeMap->end();
+}
+
+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: "
+         "`%s' requires %u parameters but was provided 0",
+         name.c_str(), p.first.size());
+  return p.second;
+}
+
+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(),
+         "type constructor arity is wrong: "
+         "`%s' requires %u parameters but was provided %u",
+         name.c_str(), p.first.size(), params.size());
+  if(p.first.size() == 0) {
+    Assert(p.second.isSort());
+    return p.second;
+  }
+  if(p.second.isSortConstructor()) {
+    if(Debug.isOn("sort")) {
+      Debug("sort") << "instantiating using a sort constructor" << endl;
+      Debug("sort") << "have formals [";
+      copy( p.first.begin(), p.first.end() - 1,
+            ostream_iterator<Type>(Debug("sort"), ", ") );
+      Debug("sort") << p.first.back() << "]" << endl
+                    << "parameters   [";
+      copy( params.begin(), params.end() - 1,
+            ostream_iterator<Type>(Debug("sort"), ", ") );
+      Debug("sort") << params.back() << "]" << endl
+                    << "type ctor    " << name << endl
+                    << "type is      " << p.second << endl;
+    }
+
+    Type instantiation =
+      SortConstructorType(p.second).instantiate(params);
+
+    Debug("sort") << "instance is  " << instantiation << endl;
+
+    return instantiation;
+  } else if(p.second.isDatatype()) {
+    Assert( DatatypeType(p.second).isParametric() );
+    return DatatypeType(p.second).instantiate(params);
+  } else {
+    if(Debug.isOn("sort")) {
+      Debug("sort") << "instantiating using a sort substitution" << endl;
+      Debug("sort") << "have formals [";
+      copy( p.first.begin(), p.first.end() - 1,
+            ostream_iterator<Type>(Debug("sort"), ", ") );
+      Debug("sort") << p.first.back() << "]" << endl
+                    << "parameters   [";
+      copy( params.begin(), params.end() - 1,
+            ostream_iterator<Type>(Debug("sort"), ", ") );
+      Debug("sort") << params.back() << "]" << endl
+                    << "type ctor    " << name << endl
+                    << "type is      " << p.second << endl;
+    }
+
+    Type instantiation = p.second.substitute(p.first, params);
+
+    Debug("sort") << "instance is  " << instantiation << endl;
+
+    return instantiation;
+  }
+}
+
+size_t SymbolTable::lookupArity(const std::string& name) {
+  pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second;
+  return p.first.size();
+}
+
+void SymbolTable::popScope() throw(ScopeException) {
+  if( d_context->getLevel() == 0 ) {
+    throw ScopeException();
+  }
+  d_context->pop();
+}
+
+void SymbolTable::pushScope() throw() {
+  d_context->push();
+}
+
+size_t SymbolTable::getLevel() const throw() {
+  return d_context->getLevel();
+}
+
+}/* CVC4 namespace */