From f1c7be3a9b96f1a949f127344ecc775680da2c8e Mon Sep 17 00:00:00 2001 From: Tim King Date: Mon, 2 Oct 2017 09:11:49 -0700 Subject: Removing throw specifiers from SymbolTable::Implementation. (#1183) --- src/expr/symbol_table.cpp | 275 ++++++++++++++++++++++++---------------------- src/expr/symbol_table.h | 49 +++++---- 2 files changed, 168 insertions(+), 156 deletions(-) (limited to 'src/expr') diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp index b411d8dfb..33046be7a 100644 --- a/src/expr/symbol_table.cpp +++ b/src/expr/symbol_table.cpp @@ -20,8 +20,8 @@ #include #include -#include #include +#include #include "context/cdhashmap.h" #include "context/cdhashset.h" @@ -45,82 +45,84 @@ using ::std::vector; // This data structure stores a trie of expressions with // the same name, and must be distinguished by their argument types. // It is context-dependent. -class OverloadedTypeTrie -{ -public: - OverloadedTypeTrie(Context * c ) : - d_overloaded_symbols(new (true) CDHashSet(c)) { - } - ~OverloadedTypeTrie() { - d_overloaded_symbols->deleteSelf(); - } +class OverloadedTypeTrie { + public: + OverloadedTypeTrie(Context* c) + : d_overloaded_symbols(new (true) CDHashSet(c)) {} + ~OverloadedTypeTrie() { d_overloaded_symbols->deleteSelf(); } + /** is this function overloaded? */ bool isOverloadedFunction(Expr fun) const; - + /** Get overloaded constant for type. * If possible, it returns a defined symbol with name * that has type t. Otherwise returns null expression. - */ + */ Expr getOverloadedConstantForType(const std::string& name, Type t) const; - + /** * If possible, returns a defined function for a name * and a vector of expected argument types. Otherwise returns * null expression. */ - Expr getOverloadedFunctionForTypes(const std::string& name, const std::vector< Type >& argTypes) const; - /** called when obj is bound to name, and prev_bound_obj was already bound to name - * Returns false if the binding is invalid. - */ + Expr getOverloadedFunctionForTypes(const std::string& name, + const std::vector& argTypes) const; + /** called when obj is bound to name, and prev_bound_obj was already bound to + * name Returns false if the binding is invalid. + */ bool bind(const string& name, Expr prev_bound_obj, Expr obj); -private: - /** Marks expression obj with name as overloaded. + + private: + /** Marks expression obj with name as overloaded. * Adds relevant information to the type arg trie data structure. * It returns false if there is already an expression bound to that name - * whose type expects the same arguments as the type of obj but is not identical - * to the type of obj. For example, if we declare : + * whose type expects the same arguments as the type of obj but is not + * identical to the type of obj. For example, if we declare : * * (declare-datatypes () ((List (cons (hd Int) (tl List)) (nil)))) * (declare-fun cons (Int List) List) * * cons : constructor_type( Int, List, List ) * cons : function_type( Int, List, List ) - * + * * These are put in the same place in the trie but do not have identical type, * hence we return false. - */ + */ bool markOverloaded(const string& name, Expr obj); /** the null expression */ Expr d_nullExpr; // The (context-independent) trie storing that maps expected argument - // vectors to symbols. All expressions stored in d_symbols are only + // vectors to symbols. All expressions stored in d_symbols are only // interpreted as active if they also appear in the context-dependent // set d_overloaded_symbols. class TypeArgTrie { - public: + public: // children of this node - std::map< Type, TypeArgTrie > d_children; + std::map d_children; // symbols at this node - std::map< Type, Expr > d_symbols; + std::map d_symbols; }; - /** for each string with operator overloading, this stores the data structure above. */ - std::unordered_map< std::string, TypeArgTrie > d_overload_type_arg_trie; + /** for each string with operator overloading, this stores the data structure + * above. */ + std::unordered_map d_overload_type_arg_trie; /** The set of overloaded symbols. */ CDHashSet* d_overloaded_symbols; }; bool OverloadedTypeTrie::isOverloadedFunction(Expr fun) const { - return d_overloaded_symbols->find(fun)!=d_overloaded_symbols->end(); + return d_overloaded_symbols->find(fun) != d_overloaded_symbols->end(); } -Expr OverloadedTypeTrie::getOverloadedConstantForType(const std::string& name, Type t) const { - std::unordered_map< std::string, TypeArgTrie >::const_iterator it = d_overload_type_arg_trie.find(name); - if(it!=d_overload_type_arg_trie.end()) { - std::map< Type, Expr >::const_iterator its = it->second.d_symbols.find(t); - if(its!=it->second.d_symbols.end()) { +Expr OverloadedTypeTrie::getOverloadedConstantForType(const std::string& name, + Type t) const { + std::unordered_map::const_iterator it = + d_overload_type_arg_trie.find(name); + if (it != d_overload_type_arg_trie.end()) { + std::map::const_iterator its = it->second.d_symbols.find(t); + if (its != it->second.d_symbols.end()) { Expr expr = its->second; // must be an active symbol - if(isOverloadedFunction(expr)) { + if (isOverloadedFunction(expr)) { return expr; } } @@ -128,28 +130,31 @@ Expr OverloadedTypeTrie::getOverloadedConstantForType(const std::string& name, T return d_nullExpr; } -Expr OverloadedTypeTrie::getOverloadedFunctionForTypes(const std::string& name, - const std::vector< Type >& argTypes) const { - std::unordered_map< std::string, TypeArgTrie >::const_iterator it = d_overload_type_arg_trie.find(name); - if(it!=d_overload_type_arg_trie.end()) { - const TypeArgTrie * tat = &it->second; - for(unsigned i=0; i::const_iterator itc = tat->d_children.find(argTypes[i]); - if(itc!=tat->d_children.end()) { +Expr OverloadedTypeTrie::getOverloadedFunctionForTypes( + const std::string& name, const std::vector& argTypes) const { + std::unordered_map::const_iterator it = + d_overload_type_arg_trie.find(name); + if (it != d_overload_type_arg_trie.end()) { + const TypeArgTrie* tat = &it->second; + for (unsigned i = 0; i < argTypes.size(); i++) { + std::map::const_iterator itc = + tat->d_children.find(argTypes[i]); + if (itc != tat->d_children.end()) { tat = &itc->second; - }else{ - // no functions match + } else { + // no functions match return d_nullExpr; } } // now, we must ensure that there is *only* one active symbol at this node Expr retExpr; - for(std::map< Type, Expr >::const_iterator its = tat->d_symbols.begin(); its != tat->d_symbols.end(); ++its) { + for (std::map::const_iterator its = tat->d_symbols.begin(); + its != tat->d_symbols.end(); ++its) { Expr expr = its->second; - if(isOverloadedFunction(expr)) { - if(retExpr.isNull()) { + if (isOverloadedFunction(expr)) { + if (retExpr.isNull()) { retExpr = expr; - }else{ + } else { // multiple functions match return d_nullExpr; } @@ -160,9 +165,10 @@ Expr OverloadedTypeTrie::getOverloadedFunctionForTypes(const std::string& name, return d_nullExpr; } -bool OverloadedTypeTrie::bind(const string& name, Expr prev_bound_obj, Expr obj) { +bool OverloadedTypeTrie::bind(const string& name, Expr prev_bound_obj, + Expr obj) { bool retprev = true; - if(!isOverloadedFunction(prev_bound_obj)) { + if (!isOverloadedFunction(prev_bound_obj)) { // mark previous as overloaded retprev = markOverloaded(name, prev_bound_obj); } @@ -177,56 +183,58 @@ bool OverloadedTypeTrie::markOverloaded(const string& name, Expr obj) { // get the argument types Type t = obj.getType(); Type rangeType = t; - std::vector< Type > argTypes; - if(t.isFunction()) { + std::vector argTypes; + if (t.isFunction()) { argTypes = static_cast(t).getArgTypes(); rangeType = static_cast(t).getRangeType(); - }else if(t.isConstructor()) { + } else if (t.isConstructor()) { argTypes = static_cast(t).getArgTypes(); rangeType = static_cast(t).getRangeType(); - }else if(t.isTester()) { - argTypes.push_back( static_cast(t).getDomain() ); + } else if (t.isTester()) { + argTypes.push_back(static_cast(t).getDomain()); rangeType = static_cast(t).getRangeType(); - }else if(t.isSelector()) { - argTypes.push_back( static_cast(t).getDomain() ); + } else if (t.isSelector()) { + argTypes.push_back(static_cast(t).getDomain()); rangeType = static_cast(t).getRangeType(); } // add to the trie - TypeArgTrie * tat = &d_overload_type_arg_trie[name]; - for(unsigned i=0; id_children[argTypes[i]]); } - - // types can be identical but vary on the kind of the type, thus we must distinguish based on this - std::map< Type, Expr >::iterator it = tat->d_symbols.find( rangeType ); - if( it!=tat->d_symbols.end() ){ + + // types can be identical but vary on the kind of the type, thus we must + // distinguish based on this + std::map::iterator it = tat->d_symbols.find(rangeType); + if (it != tat->d_symbols.end()) { Expr prev_obj = it->second; - // if there is already an active function with the same name and expects the same argument types - if( isOverloadedFunction(prev_obj) ){ - if( prev_obj.getType()==obj.getType() ){ - //types are identical, simply ignore it + // if there is already an active function with the same name and expects the + // same argument types + if (isOverloadedFunction(prev_obj)) { + if (prev_obj.getType() == obj.getType()) { + // types are identical, simply ignore it return true; - }else{ - //otherwise there is no way to distinguish these types, we return an error + } else { + // otherwise there is no way to distinguish these types, we return an + // error return false; } } } - + // otherwise, update the symbols d_overloaded_symbols->insert(obj); tat->d_symbols[rangeType] = obj; return true; } - 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)){ + d_functions(new (true) CDHashSet(&d_context)) { d_overload_trie = new OverloadedTypeTrie(&d_context); } @@ -237,33 +245,34 @@ class SymbolTable::Implementation { delete d_overload_trie; } - bool bind(const string& name, Expr obj, bool levelZero, bool doOverload) throw(); - bool bindDefinedFunction(const string& name, Expr obj, - bool levelZero, bool doOverload) throw(); - void bindType(const string& name, Type t, bool levelZero = false) throw(); + bool bind(const string& name, Expr obj, bool levelZero, bool doOverload); + bool bindDefinedFunction(const string& name, Expr obj, bool levelZero, + bool doOverload); + void bindType(const string& name, Type t, bool levelZero = false); 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(); + bool levelZero = false); + bool isBound(const string& name) const; + bool isBoundDefinedFunction(const string& name) const; + bool isBoundDefinedFunction(Expr func) const; + bool isBoundType(const string& name) const; + Expr lookup(const string& name) const; + Type lookupType(const string& name) const; + Type lookupType(const string& name, const vector& params) const; size_t lookupArity(const string& name); - void popScope() throw(ScopeException); - void pushScope() throw(); - size_t getLevel() const throw(); + void popScope(); + void pushScope(); + size_t getLevel() const; void reset(); //------------------------ operator overloading /** implementation of function from header */ bool isOverloadedFunction(Expr fun) const; - + /** implementation of function from header */ Expr getOverloadedConstantForType(const std::string& name, Type t) const; - + /** implementation of function from header */ - Expr getOverloadedFunctionForTypes(const std::string& name, const std::vector< Type >& argTypes) const; + Expr getOverloadedFunctionForTypes(const std::string& name, + const std::vector& argTypes) const; //------------------------ end operator overloading private: /** The context manager for the scope maps. */ @@ -278,27 +287,27 @@ class SymbolTable::Implementation { /** A set of defined functions. */ CDHashSet* d_functions; - + //------------------------ operator overloading // the null expression Expr d_nullExpr; // overloaded type trie, stores all information regarding overloading - OverloadedTypeTrie * d_overload_trie; + OverloadedTypeTrie* d_overload_trie; /** bind with overloading - * This is called whenever obj is bound to name where overloading symbols is allowed. - * If a symbol is previously bound to that name, it marks both as overloaded. - * Returns false if the binding was invalid. - */ + * This is called whenever obj is bound to name where overloading symbols is + * allowed. If a symbol is previously bound to that name, it marks both as + * overloaded. Returns false if the binding was invalid. + */ bool bindWithOverloading(const string& name, Expr obj); //------------------------ end operator overloading }; /* SymbolTable::Implementation */ bool SymbolTable::Implementation::bind(const string& name, Expr obj, - bool levelZero, bool doOverload) throw() { + bool levelZero, bool doOverload) { PrettyCheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr"); ExprManagerScope ems(obj); if (doOverload) { - if( !bindWithOverloading(name, obj) ){ + if (!bindWithOverloading(name, obj)) { return false; } } @@ -311,13 +320,12 @@ bool SymbolTable::Implementation::bind(const string& name, Expr obj, } bool SymbolTable::Implementation::bindDefinedFunction(const string& name, - Expr obj, - bool levelZero, - bool doOverload) throw() { + Expr obj, bool levelZero, + bool doOverload) { PrettyCheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr"); ExprManagerScope ems(obj); if (doOverload) { - if( !bindWithOverloading(name, obj) ){ + if (!bindWithOverloading(name, obj)) { return false; } } @@ -331,32 +339,32 @@ bool SymbolTable::Implementation::bindDefinedFunction(const string& name, return true; } -bool SymbolTable::Implementation::isBound(const string& name) const throw() { +bool SymbolTable::Implementation::isBound(const string& name) const { return d_exprMap->find(name) != d_exprMap->end(); } bool SymbolTable::Implementation::isBoundDefinedFunction( - const string& name) const throw() { + const string& name) const { CDHashMap::iterator found = d_exprMap->find(name); return found != d_exprMap->end() && d_functions->contains((*found).second); } -bool SymbolTable::Implementation::isBoundDefinedFunction(Expr func) const - throw() { +bool SymbolTable::Implementation::isBoundDefinedFunction(Expr func) const { return d_functions->contains(func); } -Expr SymbolTable::Implementation::lookup(const string& name) const throw() { +Expr SymbolTable::Implementation::lookup(const string& name) const { + Assert(isBound(name)); Expr expr = (*d_exprMap->find(name)).second; - if(isOverloadedFunction(expr)) { + if (isOverloadedFunction(expr)) { return d_nullExpr; - }else{ + } else { return expr; } } void SymbolTable::Implementation::bindType(const string& name, Type t, - bool levelZero) throw() { + bool levelZero) { if (levelZero) { d_typeMap->insertAtContextLevelZero(name, make_pair(vector(), t)); } else { @@ -366,7 +374,7 @@ void SymbolTable::Implementation::bindType(const string& name, Type t, void SymbolTable::Implementation::bindType(const string& name, const vector& params, Type t, - bool levelZero) throw() { + bool levelZero) { if (Debug.isOn("sort")) { Debug("sort") << "bindType(" << name << ", ["; if (params.size() > 0) { @@ -383,12 +391,11 @@ void SymbolTable::Implementation::bindType(const string& name, } } -bool SymbolTable::Implementation::isBoundType(const string& name) const - throw() { +bool SymbolTable::Implementation::isBoundType(const string& name) const { return d_typeMap->find(name) != d_typeMap->end(); } -Type SymbolTable::Implementation::lookupType(const string& name) const throw() { +Type SymbolTable::Implementation::lookupType(const string& name) const { pair, Type> p = (*d_typeMap->find(name)).second; PrettyCheckArgument(p.first.size() == 0, name, "type constructor arity is wrong: " @@ -398,8 +405,7 @@ Type SymbolTable::Implementation::lookupType(const string& name) const throw() { } Type SymbolTable::Implementation::lookupType(const string& name, - const vector& params) const - throw() { + const vector& params) const { pair, Type> p = (*d_typeMap->find(name)).second; PrettyCheckArgument(p.first.size() == params.size(), params, "type constructor arity is wrong: " @@ -459,16 +465,16 @@ size_t SymbolTable::Implementation::lookupArity(const string& name) { return p.first.size(); } -void SymbolTable::Implementation::popScope() throw(ScopeException) { +void SymbolTable::Implementation::popScope() { if (d_context.getLevel() == 0) { throw ScopeException(); } d_context.pop(); } -void SymbolTable::Implementation::pushScope() throw() { d_context.push(); } +void SymbolTable::Implementation::pushScope() { d_context.push(); } -size_t SymbolTable::Implementation::getLevel() const throw() { +size_t SymbolTable::Implementation::getLevel() const { return d_context.getLevel(); } @@ -481,20 +487,22 @@ bool SymbolTable::Implementation::isOverloadedFunction(Expr fun) const { return d_overload_trie->isOverloadedFunction(fun); } -Expr SymbolTable::Implementation::getOverloadedConstantForType(const std::string& name, Type t) const { +Expr SymbolTable::Implementation::getOverloadedConstantForType( + const std::string& name, Type t) const { return d_overload_trie->getOverloadedConstantForType(name, t); } -Expr SymbolTable::Implementation::getOverloadedFunctionForTypes(const std::string& name, - const std::vector< Type >& argTypes) const { +Expr SymbolTable::Implementation::getOverloadedFunctionForTypes( + const std::string& name, const std::vector& argTypes) const { return d_overload_trie->getOverloadedFunctionForTypes(name, argTypes); } -bool SymbolTable::Implementation::bindWithOverloading(const string& name, Expr obj){ +bool SymbolTable::Implementation::bindWithOverloading(const string& name, + Expr obj) { CDHashMap::const_iterator it = d_exprMap->find(name); - if(it != d_exprMap->end()) { + if (it != d_exprMap->end()) { const Expr& prev_bound_obj = (*it).second; - if(prev_bound_obj!=obj) { + if (prev_bound_obj != obj) { return d_overload_trie->bind(name, prev_bound_obj, obj); } } @@ -505,12 +513,13 @@ bool SymbolTable::isOverloadedFunction(Expr fun) const { return d_implementation->isOverloadedFunction(fun); } -Expr SymbolTable::getOverloadedConstantForType(const std::string& name, Type t) const { +Expr SymbolTable::getOverloadedConstantForType(const std::string& name, + Type t) const { return d_implementation->getOverloadedConstantForType(name, t); } -Expr SymbolTable::getOverloadedFunctionForTypes(const std::string& name, - const std::vector< Type >& argTypes) const { +Expr SymbolTable::getOverloadedFunctionForTypes( + const std::string& name, const std::vector& argTypes) const { return d_implementation->getOverloadedFunctionForTypes(name, argTypes); } @@ -519,13 +528,15 @@ SymbolTable::SymbolTable() SymbolTable::~SymbolTable() {} -bool SymbolTable::bind(const string& name, Expr obj, bool levelZero, bool doOverload) throw() { +bool SymbolTable::bind(const string& name, Expr obj, bool levelZero, + bool doOverload) throw() { return d_implementation->bind(name, obj, levelZero, doOverload); } bool SymbolTable::bindDefinedFunction(const string& name, Expr obj, bool levelZero, bool doOverload) throw() { - return d_implementation->bindDefinedFunction(name, obj, levelZero, doOverload); + return d_implementation->bindDefinedFunction(name, obj, levelZero, + doOverload); } void SymbolTable::bindType(const string& name, Type t, bool levelZero) throw() { diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h index b6ca7a76f..854e8a04e 100644 --- a/src/expr/symbol_table.h +++ b/src/expr/symbol_table.h @@ -43,13 +43,13 @@ class CVC4_PUBLIC SymbolTable { ~SymbolTable(); /** - * Bind an expression to a name in the current scope level. + * Bind an expression to a name in the current scope level. * * When doOverload is false: * if name is already bound to an expression in the current * level, then the binding is replaced. If name is bound * in a previous level, then the binding is "covered" by this one - * until the current scope is popped. + * until the current scope is popped. * If levelZero is true the name shouldn't be already bound. * * When doOverload is true: @@ -64,17 +64,17 @@ class CVC4_PUBLIC SymbolTable { * * Returns false if the binding was invalid. */ - bool bind(const std::string& name, Expr obj, bool levelZero = false, + bool bind(const std::string& name, Expr obj, bool levelZero = false, bool doOverload = false) throw(); /** - * Bind a function body to a name in the current scope. + * Bind a function body to a name in the current scope. * * When doOverload is false: * if name is already bound to an expression in the current * level, then the binding is replaced. If name is bound * in a previous level, then the binding is "covered" by this one - * until the current scope is popped. + * until the current scope is popped. * If levelZero is true the name shouldn't be already bound. * * When doOverload is true: @@ -82,7 +82,7 @@ class CVC4_PUBLIC SymbolTable { * level, then we mark the previous bound expression and obj as overloaded * functions. * - * Same as bind() but registers this as a function (so that + * Same as bind() but registers this as a function (so that * isBoundDefinedFunction() returns true). * * @param name an identifier @@ -93,7 +93,7 @@ class CVC4_PUBLIC SymbolTable { * Returns false if the binding was invalid. */ bool bindDefinedFunction(const std::string& name, Expr obj, - bool levelZero = false, + bool levelZero = false, bool doOverload = false) throw(); /** @@ -158,8 +158,9 @@ class CVC4_PUBLIC SymbolTable { * Lookup a bound expression. * * @param name the identifier to lookup - * @returns the unique expression bound to name in the current scope. - * It returns the null expression if there is not a unique expression bound to + * @returns the unique expression bound to name in the current + * scope. + * It returns the null expression if there is not a unique expression bound to * name in the current scope (i.e. if there is not exactly one). */ Expr lookup(const std::string& name) const throw(); @@ -189,15 +190,14 @@ class CVC4_PUBLIC SymbolTable { size_t lookupArity(const std::string& name); /** - * Pop a scope level. Deletes all bindings since the last call to - * pushScope. Calls to pushScope and - * popScope must be "properly nested." I.e., a call to - * popScope is only legal if the number of prior calls to - * pushScope on this SymbolTable is strictly - * greater than then number of prior calls to popScope. */ + * Pop a scope level, deletes all bindings since the last call to pushScope, + * and decreases the level by 1. + * + * @throws ScopeException if the scope level is 0. + */ void popScope() throw(ScopeException); - /** Push a scope level. */ + /** Push a scope level and increase the scope level by 1. */ void pushScope() throw(); /** Get the current level of this symbol table. */ @@ -205,31 +205,32 @@ class CVC4_PUBLIC SymbolTable { /** Reset everything. */ void reset(); - + //------------------------ operator overloading /** is this function overloaded? */ bool isOverloadedFunction(Expr fun) const; - + /** Get overloaded constant for type. * If possible, it returns the defined symbol with name * that has type t. Otherwise returns null expression. */ Expr getOverloadedConstantForType(const std::string& name, Type t) const; - + /** * If possible, returns the unique defined function for a name * that expects arguments with types "argTypes". - * For example, if argTypes = ( T1, ..., Tn ), then this may return - * an expression with type function( T1, ..., Tn ), or constructor( T1, ...., Tn ). - * + * For example, if argTypes = (T1, ..., Tn), then this may return an + * expression with type function(T1, ..., Tn), or constructor(T1, ...., Tn). + * * If there is not a unique defined function for the name and argTypes, * this returns the null expression. This can happen either if there are * no functions with name and expected argTypes, or alternatively there is * more than one function with name and expected argTypes. */ - Expr getOverloadedFunctionForTypes(const std::string& name, const std::vector< Type >& argTypes) const; + Expr getOverloadedFunctionForTypes(const std::string& name, + const std::vector< Type >& argTypes) const; //------------------------ end operator overloading - + private: // Copying and assignment have not yet been implemented. SymbolTable(const SymbolTable&); -- cgit v1.2.3