diff options
Diffstat (limited to 'src/expr')
| -rw-r--r-- | src/expr/attribute.h | 16 | ||||
| -rw-r--r-- | src/expr/attribute_internals.h | 28 |
2 files changed, 21 insertions, 23 deletions
diff --git a/src/expr/attribute.h b/src/expr/attribute.h index 70f04be85..969843ddd 100644 --- a/src/expr/attribute.h +++ b/src/expr/attribute.h @@ -522,14 +522,14 @@ AttributeManager::setAttribute(NodeValue* nv, template <class T> inline void AttributeManager::deleteFromTable(AttrHash<T>& table, NodeValue* nv) { - for(uint64_t id = 0; id < attr::LastAttributeId<T, false>::s_id; ++id) { + for(uint64_t id = 0; id < attr::LastAttributeId<T, false>::getId(); ++id) { typedef AttributeTraits<T, false> traits_t; typedef AttrHash<T> hash_t; std::pair<uint64_t, NodeValue*> pr = std::make_pair(id, nv); - if(traits_t::cleanup[id] != NULL) { + if(traits_t::getCleanup()[id] != NULL) { typename hash_t::iterator i = table.find(pr); if(i != table.end()) { - traits_t::cleanup[id]((*i).second); + traits_t::getCleanup()[id]((*i).second); table.erase(pr); } } else { @@ -544,7 +544,7 @@ inline void AttributeManager::deleteFromTable(AttrHash<T>& table, template <class T> inline void AttributeManager::deleteFromTable(CDAttrHash<T>& table, NodeValue* nv) { - for(unsigned id = 0; id < attr::LastAttributeId<T, true>::s_id; ++id) { + for(unsigned id = 0; id < attr::LastAttributeId<T, true>::getId(); ++id) { table.obliterate(std::make_pair(id, nv)); } } @@ -558,8 +558,8 @@ inline void AttributeManager::deleteAllFromTable(AttrHash<T>& table) { bool anyRequireClearing = false; typedef AttributeTraits<T, false> traits_t; typedef AttrHash<T> hash_t; - for(uint64_t id = 0; id < attr::LastAttributeId<T, false>::s_id; ++id) { - if(traits_t::cleanup[id] != NULL) { + for(uint64_t id = 0; id < attr::LastAttributeId<T, false>::getId(); ++id) { + if(traits_t::getCleanup()[id] != NULL) { anyRequireClearing = true; } } @@ -575,8 +575,8 @@ inline void AttributeManager::deleteAllFromTable(AttrHash<T>& table) { << " node_value: " << ((*it).first.second) << std::endl; */ - if(traits_t::cleanup[id] != NULL) { - traits_t::cleanup[id]((*it).second); + if(traits_t::getCleanup()[id] != NULL) { + traits_t::getCleanup()[id]((*it).second); } ++it; } diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h index 4893075c3..a0086440b 100644 --- a/src/expr/attribute_internals.h +++ b/src/expr/attribute_internals.h @@ -679,13 +679,12 @@ namespace attr { */ template <class T, bool context_dep> struct LastAttributeId { - static uint64_t s_id; + static uint64_t& getId() { + static uint64_t s_id = 0; + return s_id; + } }; -/** Initially zero. */ -template <class T, bool context_dep> -uint64_t LastAttributeId<T, context_dep>::s_id = 0; - }/* CVC4::expr::attr namespace */ // ATTRIBUTE TRAITS ============================================================ @@ -699,13 +698,12 @@ namespace attr { template <class T, bool context_dep> struct AttributeTraits { typedef void (*cleanup_t)(T); - static std::vector<cleanup_t> cleanup; + static std::vector<cleanup_t>& getCleanup() { + static std::vector<cleanup_t> cleanup; + return cleanup; + } }; -template <class T, bool context_dep> -std::vector<typename AttributeTraits<T, context_dep>::cleanup_t> - AttributeTraits<T, context_dep>::cleanup; - }/* CVC4::expr::attr namespace */ // ATTRIBUTE DEFINITION ======================================================== @@ -765,9 +763,9 @@ public: typedef typename attr::KindValueToTableValueMapping<value_t>:: table_value_type table_value_type; typedef attr::AttributeTraits<table_value_type, context_dep> traits; - uint64_t id = attr::LastAttributeId<table_value_type, context_dep>::s_id++; - //Assert(traits::cleanup.size() == id);// sanity check - traits::cleanup.push_back(attr::getCleanupStrategy<value_t, + uint64_t id = attr::LastAttributeId<table_value_type, context_dep>::getId()++; + Assert(traits::getCleanup().size() == id);// sanity check + traits::getCleanup().push_back(attr::getCleanupStrategy<value_t, CleanupStrategy>::fn); return id; } @@ -827,7 +825,7 @@ public: * return the id. */ static inline uint64_t registerAttribute() { - uint64_t id = attr::LastAttributeId<bool, context_dep>::s_id++; + uint64_t id = attr::LastAttributeId<bool, context_dep>::getId()++; AlwaysAssert( id <= 63, "Too many boolean node attributes registered " "during initialization !" ); @@ -876,7 +874,7 @@ template <class T, class value_t, class CleanupStrategy, bool context_dep> const uint64_t Attribute<T, value_t, CleanupStrategy, context_dep>::s_id = ( attr::AttributeTraits<typename attr::KindValueToTableValueMapping<value_t>:: table_value_type, - context_dep>::cleanup.size(), + context_dep>::getCleanup().size(), Attribute<T, value_t, CleanupStrategy, context_dep>::registerAttribute() ); /** Assign unique IDs to attributes at load time. */ |