From d8c692850d8d7d9963c9c207e1b20cac1ec24635 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 2 Nov 2020 07:01:19 -0600 Subject: [PATCH] Avoid dynamic allocation in symbol table implementation (#5368) Encountered this while debugging the new symbol manager. This is not essential but probably a good idea to refactor. --- src/expr/symbol_table.cpp | 55 +++++++++++++++++++-------------------- 1 file changed, 27 insertions(+), 28 deletions(-) diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp index 888434665..3d01b778c 100644 --- a/src/expr/symbol_table.cpp +++ b/src/expr/symbol_table.cpp @@ -342,16 +342,13 @@ class SymbolTable::Implementation { public: Implementation() : d_context(), - d_exprMap(new (true) CDHashMap(&d_context)), - d_typeMap(new (true) TypeMap(&d_context)) + d_exprMap(&d_context), + d_typeMap(&d_context), + d_overload_trie(&d_context) { - d_overload_trie = new OverloadedTypeTrie(&d_context); } ~Implementation() { - d_exprMap->deleteSelf(); - d_typeMap->deleteSelf(); - delete d_overload_trie; } bool bind(const string& name, api::Term obj, bool levelZero, bool doOverload); @@ -388,17 +385,17 @@ class SymbolTable::Implementation { Context d_context; /** A map for expressions. */ - CDHashMap* d_exprMap; + CDHashMap d_exprMap; /** A map for types. */ using TypeMap = CDHashMap, api::Sort>>; - TypeMap* d_typeMap; + TypeMap d_typeMap; //------------------------ operator overloading // the null expression api::Term d_nullTerm; // 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 @@ -420,21 +417,21 @@ bool SymbolTable::Implementation::bind(const string& name, } } if (levelZero) { - d_exprMap->insertAtContextLevelZero(name, obj); + d_exprMap.insertAtContextLevelZero(name, obj); } else { - d_exprMap->insert(name, obj); + d_exprMap.insert(name, obj); } return true; } bool SymbolTable::Implementation::isBound(const string& name) const { - return d_exprMap->find(name) != d_exprMap->end(); + return d_exprMap.find(name) != d_exprMap.end(); } api::Term SymbolTable::Implementation::lookup(const string& name) const { Assert(isBound(name)); - api::Term expr = (*d_exprMap->find(name)).second; + api::Term expr = (*d_exprMap.find(name)).second; if (isOverloadedFunction(expr)) { return d_nullTerm; } else { @@ -447,10 +444,9 @@ void SymbolTable::Implementation::bindType(const string& name, bool levelZero) { if (levelZero) { - d_typeMap->insertAtContextLevelZero(name, - make_pair(vector(), t)); + d_typeMap.insertAtContextLevelZero(name, make_pair(vector(), t)); } else { - d_typeMap->insert(name, make_pair(vector(), t)); + d_typeMap.insert(name, make_pair(vector(), t)); } } @@ -470,19 +466,20 @@ void SymbolTable::Implementation::bindType(const string& name, Debug("sort") << "], " << t << ")" << endl; } if (levelZero) { - d_typeMap->insertAtContextLevelZero(name, make_pair(params, t)); + d_typeMap.insertAtContextLevelZero(name, make_pair(params, t)); } else { - d_typeMap->insert(name, make_pair(params, t)); + d_typeMap.insert(name, make_pair(params, t)); } } bool SymbolTable::Implementation::isBoundType(const string& name) const { - return d_typeMap->find(name) != d_typeMap->end(); + return d_typeMap.find(name) != d_typeMap.end(); } api::Sort SymbolTable::Implementation::lookupType(const string& name) const { - pair, api::Sort> p = (*d_typeMap->find(name)).second; + std::pair, api::Sort> 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", @@ -494,7 +491,7 @@ api::Sort SymbolTable::Implementation::lookupType( const string& name, const vector& params) const { std::pair, api::Sort> p = - (*d_typeMap->find(name)).second; + (*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", @@ -535,7 +532,8 @@ api::Sort SymbolTable::Implementation::lookupType( } size_t SymbolTable::Implementation::lookupArity(const string& name) { - pair, api::Sort> p = (*d_typeMap->find(name)).second; + std::pair, api::Sort> p = + (*d_typeMap.find(name)).second; return p.first.size(); } @@ -559,29 +557,30 @@ void SymbolTable::Implementation::reset() { bool SymbolTable::Implementation::isOverloadedFunction(api::Term fun) const { - return d_overload_trie->isOverloadedFunction(fun); + return d_overload_trie.isOverloadedFunction(fun); } api::Term SymbolTable::Implementation::getOverloadedConstantForType( const std::string& name, api::Sort t) const { - return d_overload_trie->getOverloadedConstantForType(name, t); + return d_overload_trie.getOverloadedConstantForType(name, t); } api::Term SymbolTable::Implementation::getOverloadedFunctionForTypes( const std::string& name, const std::vector& argTypes) const { - return d_overload_trie->getOverloadedFunctionForTypes(name, argTypes); + return d_overload_trie.getOverloadedFunctionForTypes(name, argTypes); } bool SymbolTable::Implementation::bindWithOverloading(const string& name, api::Term obj) { - CDHashMap::const_iterator it = d_exprMap->find(name); - if (it != d_exprMap->end()) { + CDHashMap::const_iterator it = d_exprMap.find(name); + if (it != d_exprMap.end()) + { const api::Term& prev_bound_obj = (*it).second; if (prev_bound_obj != obj) { - return d_overload_trie->bind(name, prev_bound_obj, obj); + return d_overload_trie.bind(name, prev_bound_obj, obj); } } return true; -- 2.30.2