Consolidating the opaque pointers in SymbolTable. (#204)

* Consolidating the opaque pointers in SymbolTable. This removes details about the implementation from a public header.

* Removing the guard for SymbolTable for the move constructor.

2 files changed, 200 insertions, 117 deletions

diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp
index 7fd938a9b..ba731ec1e 100644
--- a/src/expr/symbol_table.cpp
+++ b/src/expr/symbol_table.cpp
@@ -18,6 +18,7 @@
 
 #include "expr/symbol_table.h"
 
+#include <ostream>
 #include <string>
 #include <utility>
 
@@ -28,39 +29,77 @@
 #include "expr/expr_manager_scope.h"
 #include "expr/type.h"
 
+namespace CVC4 {
 
-using namespace CVC4::context;
-using namespace std;
+using ::CVC4::context::CDHashMap;
+using ::CVC4::context::CDHashSet;
+using ::CVC4::context::Context;
+using ::std::copy;
+using ::std::endl;
+using ::std::ostream_iterator;
+using ::std::pair;
+using ::std::string;
+using ::std::vector;
 
-namespace CVC4 {
+class SymbolTable::Implementation {
+ public:
+  Implementation()
+      : d_context(),
+        d_exprMap(new (true) CDHashMap<string, Expr>(&d_context)),
+        d_typeMap(new (true) TypeMap(&d_context)),
+        d_functions(new (true) CDHashSet<Expr, ExprHashFunction>(&d_context)) {}
 
-SymbolTable::SymbolTable() :
-  d_context(new Context()),
-  d_exprMap(new(true) CDHashMap<std::string, Expr>(d_context)),
-  d_typeMap(new(true) CDHashMap<std::string, pair<vector<Type>, Type>>(d_context)),
-  d_functions(new(true) CDHashSet<Expr, ExprHashFunction>(d_context)) {
-}
+  void bind(const string& name, Expr obj, bool levelZero) throw();
+  void bindDefinedFunction(const string& name, Expr obj,
+                           bool levelZero) throw();
+  void bindType(const string& name, Type t, bool levelZero = false) throw();
+  void bindType(const string& name, const vector<Type>& params, Type t,
+                bool levelZero = false) throw();
+  bool isBound(const string& name) const throw();
+  bool isBoundDefinedFunction(const string& name) const throw();
+  bool isBoundDefinedFunction(Expr func) const throw();
+  bool isBoundType(const string& name) const throw();
+  Expr lookup(const string& name) const throw();
+  Type lookupType(const string& name) const throw();
+  Type lookupType(const string& name, const vector<Type>& params) const throw();
+  size_t lookupArity(const string& name);
+  void popScope() throw(ScopeException);
+  void pushScope() throw();
+  size_t getLevel() const throw();
+  void reset();
 
-SymbolTable::~SymbolTable() {
-  d_exprMap->deleteSelf();
-  d_typeMap->deleteSelf();
-  d_functions->deleteSelf();
-  delete d_context;
-}
+ private:
+  /** The context manager for the scope maps. */
+  Context d_context;
+
+  /** A map for expressions. */
+  CDHashMap<string, Expr>* d_exprMap;
+
+  /** A map for types. */
+  using TypeMap = CDHashMap<string, std::pair<vector<Type>, Type>>;
+  TypeMap* d_typeMap;
 
-void SymbolTable::bind(const std::string& name, Expr obj,
-                       bool levelZero) throw() {
+  /** A set of defined functions. */
+  CDHashSet<Expr, ExprHashFunction>* d_functions;
+}; /* SymbolTable::Implementation */
+
+void SymbolTable::Implementation::bind(const string& name, Expr obj,
+                                       bool levelZero) throw() {
   PrettyCheckArgument(!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);
+  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() {
+void SymbolTable::Implementation::bindDefinedFunction(const string& name,
+                                                      Expr obj,
+                                                      bool levelZero) throw() {
   PrettyCheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr");
   ExprManagerScope ems(obj);
-  if(levelZero){
+  if (levelZero) {
     d_exprMap->insertAtContextLevelZero(name, obj);
     d_functions->insertAtContextLevelZero(obj);
   } else {
@@ -69,111 +108,111 @@ void SymbolTable::bindDefinedFunction(const std::string& name, Expr obj,
   }
 }
 
-bool SymbolTable::isBound(const std::string& name) const throw() {
+bool SymbolTable::Implementation::isBound(const 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>::iterator found =
-    d_exprMap->find(name);
+bool SymbolTable::Implementation::isBoundDefinedFunction(
+    const string& name) const throw() {
+  CDHashMap<string, Expr>::iterator found = d_exprMap->find(name);
   return found != d_exprMap->end() && d_functions->contains((*found).second);
 }
 
-bool SymbolTable::isBoundDefinedFunction(Expr func) const throw() {
+bool SymbolTable::Implementation::isBoundDefinedFunction(Expr func) const
+    throw() {
   return d_functions->contains(func);
 }
 
-Expr SymbolTable::lookup(const std::string& name) const throw() {
+Expr SymbolTable::Implementation::lookup(const string& name) const throw() {
   return (*d_exprMap->find(name)).second;
 }
 
-void SymbolTable::bindType(const std::string& name, Type t,
-                           bool levelZero) throw() {
-  if(levelZero) {
+void SymbolTable::Implementation::bindType(const 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")) {
+void SymbolTable::Implementation::bindType(const string& name,
+                                           const 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"), ", ") );
+    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) {
+  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() {
+bool SymbolTable::Implementation::isBoundType(const string& name) const
+    throw() {
   return d_typeMap->find(name) != d_typeMap->end();
 }
 
-Type SymbolTable::lookupType(const std::string& name) const throw() {
+Type SymbolTable::Implementation::lookupType(const string& name) const throw() {
   pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second;
   PrettyCheckArgument(p.first.size() == 0, name,
-                "type constructor arity is wrong: "
-                "`%s' requires %u parameters but was provided 0",
-                name.c_str(), p.first.size());
+                      "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() {
+Type SymbolTable::Implementation::lookupType(const string& name,
+                                             const vector<Type>& params) const
+    throw() {
   pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second;
   PrettyCheckArgument(p.first.size() == params.size(), params,
-                "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) {
+                      "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) {
     PrettyCheckArgument(p.second.isSort(), name.c_str());
     return p.second;
   }
-  if(p.second.isSortConstructor()) {
-    if(Debug.isOn("sort")) {
+  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"), ", ") );
+      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);
+    Type instantiation = SortConstructorType(p.second).instantiate(params);
 
     Debug("sort") << "instance is  " << instantiation << endl;
 
     return instantiation;
-  } else if(p.second.isDatatype()) {
-    PrettyCheckArgument(DatatypeType(p.second).isParametric(), name, "expected parametric datatype");
+  } else if (p.second.isDatatype()) {
+    PrettyCheckArgument(DatatypeType(p.second).isParametric(), name,
+                        "expected parametric datatype");
     return DatatypeType(p.second).instantiate(params);
   } else {
-    if(Debug.isOn("sort")) {
+    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"), ", ") );
+      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;
@@ -187,29 +226,88 @@ Type SymbolTable::lookupType(const std::string& name,
   }
 }
 
-size_t SymbolTable::lookupArity(const std::string& name) {
+size_t SymbolTable::Implementation::lookupArity(const 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 ) {
+void SymbolTable::Implementation::popScope() throw(ScopeException) {
+  if (d_context.getLevel() == 0) {
     throw ScopeException();
   }
-  d_context->pop();
+  d_context.pop();
 }
 
-void SymbolTable::pushScope() throw() {
-  d_context->push();
+void SymbolTable::Implementation::pushScope() throw() { d_context.push(); }
+
+size_t SymbolTable::Implementation::getLevel() const throw() {
+  return d_context.getLevel();
 }
 
-size_t SymbolTable::getLevel() const throw() {
-  return d_context->getLevel();
+void SymbolTable::Implementation::reset() {
+  this->SymbolTable::Implementation::~Implementation();
+  new (this) SymbolTable::Implementation();
 }
 
-void SymbolTable::reset() {
-  this->SymbolTable::~SymbolTable();
-  new(this) SymbolTable();
+SymbolTable::SymbolTable()
+    : d_implementation(new SymbolTable::Implementation()) {}
+
+SymbolTable::~SymbolTable() {}
+
+void SymbolTable::bind(const string& name, Expr obj, bool levelZero) throw() {
+  d_implementation->bind(name, obj, levelZero);
+}
+
+void SymbolTable::bindDefinedFunction(const string& name, Expr obj,
+                                      bool levelZero) throw() {
+  d_implementation->bindDefinedFunction(name, obj, levelZero);
+}
+
+void SymbolTable::bindType(const string& name, Type t, bool levelZero) throw() {
+  d_implementation->bindType(name, t, levelZero);
+}
+
+void SymbolTable::bindType(const string& name, const vector<Type>& params,
+                           Type t, bool levelZero) throw() {
+  d_implementation->bindType(name, params, t, levelZero);
+}
+
+bool SymbolTable::isBound(const string& name) const throw() {
+  return d_implementation->isBound(name);
+}
+
+bool SymbolTable::isBoundDefinedFunction(const string& name) const throw() {
+  return d_implementation->isBoundDefinedFunction(name);
+}
+
+bool SymbolTable::isBoundDefinedFunction(Expr func) const throw() {
+  return d_implementation->isBoundDefinedFunction(func);
+}
+bool SymbolTable::isBoundType(const string& name) const throw() {
+  return d_implementation->isBoundType(name);
+}
+Expr SymbolTable::lookup(const string& name) const throw() {
+  return d_implementation->lookup(name);
+}
+Type SymbolTable::lookupType(const string& name) const throw() {
+  return d_implementation->lookupType(name);
+}
+
+Type SymbolTable::lookupType(const string& name,
+                             const vector<Type>& params) const throw() {
+  return d_implementation->lookupType(name, params);
+}
+size_t SymbolTable::lookupArity(const string& name) {
+  return d_implementation->lookupArity(name);
+}
+void SymbolTable::popScope() throw(ScopeException) {
+  d_implementation->popScope();
+}
+
+void SymbolTable::pushScope() throw() { d_implementation->pushScope(); }
+size_t SymbolTable::getLevel() const throw() {
+  return d_implementation->getLevel();
 }
+void SymbolTable::reset() { d_implementation->reset(); }
 
-}/* CVC4 namespace */
+}  // namespace CVC4
diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h
index 7c3b13003..e64488563 100644
--- a/src/expr/symbol_table.h
+++ b/src/expr/symbol_table.h
@@ -19,25 +19,17 @@
 #ifndef __CVC4__SYMBOL_TABLE_H
 #define __CVC4__SYMBOL_TABLE_H
 
+#include <memory>
+#include <string>
 #include <vector>
-#include <utility>
 
+#include "base/exception.h"
 #include "expr/expr.h"
-#include "util/hash.h"
-
-#include "context/cdhashset_forward.h"
-#include "context/cdhashmap_forward.h"
+#include "expr/type.h"
 
 namespace CVC4 {
 
-class Type;
-
-namespace context {
-  class Context;
-}/* CVC4::context namespace */
-
-class CVC4_PUBLIC ScopeException : public Exception {
-};/* class ScopeException */
+class CVC4_PUBLIC ScopeException : public Exception {};
 
 /**
  * A convenience class for handling scoped declarations. Implements the usual
@@ -45,24 +37,9 @@ class CVC4_PUBLIC ScopeException : public Exception {
  * and types.
  */
 class CVC4_PUBLIC SymbolTable {
-  /** The context manager for the scope maps. */
-  context::Context* d_context;
-
-  /** A map for expressions. */
-  context::CDHashMap<std::string, Expr>* d_exprMap;
-
-  /** A map for types. */
-  context::CDHashMap<std::string, std::pair<std::vector<Type>, Type> >*
-      d_typeMap;
-
-  /** A set of defined functions. */
-  context::CDHashSet<Expr, ExprHashFunction> *d_functions;
-
-public:
+ public:
   /** Create a symbol table. */
   SymbolTable();
-
-  /** Destroy a symbol table. */
   ~SymbolTable();
 
   /**
@@ -91,7 +68,8 @@ public:
    * @param obj the expression to bind to <code>name</code>
    * @param levelZero set if the binding must be done at level 0
    */
-  void bindDefinedFunction(const std::string& name, Expr obj, bool levelZero = false) throw();
+  void bindDefinedFunction(const std::string& name, Expr obj,
+                           bool levelZero = false) throw();
 
   /**
    * Bind a type to a name in the current scope.  If <code>name</code>
@@ -104,7 +82,8 @@ public:
    * @param t the type to bind to <code>name</code>
    * @param levelZero set if the binding must be done at level 0
    */
-  void bindType(const std::string& name, Type t, bool levelZero = false) throw();
+  void bindType(const std::string& name, Type t,
+                bool levelZero = false) throw();
 
   /**
    * Bind a type to a name in the current scope.  If <code>name</code>
@@ -119,8 +98,7 @@ public:
    * @param levelZero true to bind it globally (default is to bind it
    * locally within the current scope)
    */
-  void bindType(const std::string& name,
-                const std::vector<Type>& params,
+  void bindType(const std::string& name, const std::vector<Type>& params,
                 Type t, bool levelZero = false) throw();
 
   /**
@@ -201,8 +179,15 @@ public:
   /** Reset everything. */
   void reset();
 
-};/* class SymbolTable */
+ private:
+  // Copying and assignment have not yet been implemented.
+  SymbolTable(const SymbolTable&);
+  SymbolTable& operator=(SymbolTable&);
+
+  class Implementation;
+  std::unique_ptr<Implementation> d_implementation;
+}; /* class SymbolTable */
 
-}/* CVC4 namespace */
+}  // namespace CVC4
 
 #endif /* __CVC4__SYMBOL_TABLE_H */