From 4cab39bd4f166716cd3d357a175c346afb838137 Mon Sep 17 00:00:00 2001 From: Tim King Date: Sat, 22 Jul 2017 19:56:49 -0700 Subject: [PATCH] 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. --- src/expr/symbol_table.cpp | 262 ++++++++++++++++++++++++++------------ src/expr/symbol_table.h | 55 +++----- 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 #include #include @@ -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(&d_context)), + d_typeMap(new (true) TypeMap(&d_context)), + d_functions(new (true) CDHashSet(&d_context)) {} -SymbolTable::SymbolTable() : - d_context(new Context()), - d_exprMap(new(true) CDHashMap(d_context)), - d_typeMap(new(true) CDHashMap, Type>>(d_context)), - d_functions(new(true) CDHashSet(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& 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& 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* d_exprMap; + + /** A map for types. */ + using TypeMap = CDHashMap, Type>>; + TypeMap* d_typeMap; -void SymbolTable::bind(const std::string& name, Expr obj, - bool levelZero) throw() { + /** A set of defined functions. */ + CDHashSet* 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::iterator found = - d_exprMap->find(name); +bool SymbolTable::Implementation::isBoundDefinedFunction( + const string& name) const throw() { + CDHashMap::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(), t)); } else { d_typeMap->insert(name, make_pair(vector(), t)); } } -void SymbolTable::bindType(const std::string& name, - const std::vector& params, - Type t, - bool levelZero) throw() { - if(Debug.isOn("sort")) { +void SymbolTable::Implementation::bindType(const string& name, + const vector& 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(Debug("sort"), ", ") ); + if (params.size() > 0) { + copy(params.begin(), params.end() - 1, + ostream_iterator(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, 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& params) const throw() { +Type SymbolTable::Implementation::lookupType(const string& name, + const vector& params) const + throw() { pair, 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(Debug("sort"), ", ") ); - Debug("sort") << p.first.back() << "]" << endl - << "parameters ["; - copy( params.begin(), params.end() - 1, - ostream_iterator(Debug("sort"), ", ") ); + copy(p.first.begin(), p.first.end() - 1, + ostream_iterator(Debug("sort"), ", ")); + Debug("sort") << p.first.back() << "]" << endl << "parameters ["; + copy(params.begin(), params.end() - 1, + ostream_iterator(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(Debug("sort"), ", ") ); - Debug("sort") << p.first.back() << "]" << endl - << "parameters ["; - copy( params.begin(), params.end() - 1, - ostream_iterator(Debug("sort"), ", ") ); + copy(p.first.begin(), p.first.end() - 1, + ostream_iterator(Debug("sort"), ", ")); + Debug("sort") << p.first.back() << "]" << endl << "parameters ["; + copy(params.begin(), params.end() - 1, + ostream_iterator(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, 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& 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& 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 +#include #include -#include +#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* d_exprMap; - - /** A map for types. */ - context::CDHashMap, Type> >* - d_typeMap; - - /** A set of defined functions. */ - context::CDHashSet *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 name * @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 name @@ -104,7 +82,8 @@ public: * @param t the type to bind to name * @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 name @@ -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& params, + void bindType(const std::string& name, const std::vector& 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 d_implementation; +}; /* class SymbolTable */ -}/* CVC4 namespace */ +} // namespace CVC4 #endif /* __CVC4__SYMBOL_TABLE_H */ -- 2.30.2