From 91424455840a7365a328cbcc3d02ec453fe9d0ea Mon Sep 17 00:00:00 2001 From: Tim King Date: Thu, 14 Nov 2013 11:56:34 -0500 Subject: Adding the changes needed to delete rewriter attributes. This includes being able to list attributes. Additionally, added debugging hooks to node manager and attribute manager. --- src/expr/attribute.h | 94 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 94 insertions(+) (limited to 'src/expr/attribute.h') diff --git a/src/expr/attribute.h b/src/expr/attribute.h index f9939fa90..605427190 100644 --- a/src/expr/attribute.h +++ b/src/expr/attribute.h @@ -26,6 +26,7 @@ #include #include +#include "expr/attribute_unique_id.h" // include supporting templates #define CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H @@ -87,6 +88,12 @@ class AttributeManager { template void deleteAllFromTable(AttrHash& table); + template + void deleteAttributesFromTable(AttrHash& table, const std::vector& ids); + + template + void reconstructTable(AttrHash& table); + /** * getTable<> is a helper template that gets the right table from an * AttributeManager given its type. @@ -169,6 +176,29 @@ public: * Remove all attributes from the tables. */ void deleteAllAttributes(); + + + /** + * Determines the AttrTableId of an attribute. + * + * @param attr the attribute + * @return the id of the attribute table. + */ + template + static AttributeUniqueId getAttributeId(const AttrKind& attr); + + /** A list of attributes. */ + typedef std::vector< const AttributeUniqueId* > AttrIdVec; + + /** Deletes a list of attributes. */ + void deleteAttributes(const AttrIdVec& attributeIds); + + /** + * debugHook() is an empty function for the purpose of debugging + * the AttributeManager without recompiling all of CVC4. + * Formally this is a nop. + */ + void debugHook(int debugFlag); }; }/* CVC4::expr::attr namespace */ @@ -187,6 +217,7 @@ struct getTable; /** Access the "d_bools" member of AttributeManager. */ template <> struct getTable { + static const AttrTableId id = AttrTableBool; typedef AttrHash table_type; static inline table_type& get(AttributeManager& am) { return am.d_bools; @@ -199,6 +230,7 @@ struct getTable { /** Access the "d_ints" member of AttributeManager. */ template <> struct getTable { + static const AttrTableId id = AttrTableUInt64; typedef AttrHash table_type; static inline table_type& get(AttributeManager& am) { return am.d_ints; @@ -211,6 +243,7 @@ struct getTable { /** Access the "d_tnodes" member of AttributeManager. */ template <> struct getTable { + static const AttrTableId id = AttrTableTNode; typedef AttrHash table_type; static inline table_type& get(AttributeManager& am) { return am.d_tnodes; @@ -223,6 +256,7 @@ struct getTable { /** Access the "d_nodes" member of AttributeManager. */ template <> struct getTable { + static const AttrTableId id = AttrTableNode; typedef AttrHash table_type; static inline table_type& get(AttributeManager& am) { return am.d_nodes; @@ -235,6 +269,7 @@ struct getTable { /** Access the "d_types" member of AttributeManager. */ template <> struct getTable { + static const AttrTableId id = AttrTableTypeNode; typedef AttrHash table_type; static inline table_type& get(AttributeManager& am) { return am.d_types; @@ -247,6 +282,7 @@ struct getTable { /** Access the "d_strings" member of AttributeManager. */ template <> struct getTable { + static const AttrTableId id = AttrTableString; typedef AttrHash table_type; static inline table_type& get(AttributeManager& am) { return am.d_strings; @@ -259,6 +295,7 @@ struct getTable { /** Access the "d_ptrs" member of AttributeManager. */ template struct getTable { + static const AttrTableId id = AttrTablePointer; typedef AttrHash table_type; static inline table_type& get(AttributeManager& am) { return am.d_ptrs; @@ -271,6 +308,7 @@ struct getTable { /** Access the "d_ptrs" member of AttributeManager. */ template struct getTable { + static const AttrTableId id = AttrTablePointer; typedef AttrHash table_type; static inline table_type& get(AttributeManager& am) { return am.d_ptrs; @@ -283,6 +321,7 @@ struct getTable { /** Access the "d_cdbools" member of AttributeManager. */ template <> struct getTable { + static const AttrTableId id = AttrTableCDBool; typedef CDAttrHash table_type; static inline table_type& get(AttributeManager& am) { return am.d_cdbools; @@ -295,6 +334,7 @@ struct getTable { /** Access the "d_cdints" member of AttributeManager. */ template <> struct getTable { + static const AttrTableId id = AttrTableCDUInt64; typedef CDAttrHash table_type; static inline table_type& get(AttributeManager& am) { return am.d_cdints; @@ -307,6 +347,7 @@ struct getTable { /** Access the "d_tnodes" member of AttributeManager. */ template <> struct getTable { + static const AttrTableId id = AttrTableCDTNode; typedef CDAttrHash table_type; static inline table_type& get(AttributeManager& am) { return am.d_cdtnodes; @@ -319,6 +360,7 @@ struct getTable { /** Access the "d_cdnodes" member of AttributeManager. */ template <> struct getTable { + static const AttrTableId id = AttrTableCDNode; typedef CDAttrHash table_type; static inline table_type& get(AttributeManager& am) { return am.d_cdnodes; @@ -331,6 +373,7 @@ struct getTable { /** Access the "d_cdstrings" member of AttributeManager. */ template <> struct getTable { + static const AttrTableId id = AttrTableCDString; typedef CDAttrHash table_type; static inline table_type& get(AttributeManager& am) { return am.d_cdstrings; @@ -343,6 +386,7 @@ struct getTable { /** Access the "d_cdptrs" member of AttributeManager. */ template struct getTable { + static const AttrTableId id = AttrTableCDPointer; typedef CDAttrHash table_type; static inline table_type& get(AttributeManager& am) { return am.d_cdptrs; @@ -355,6 +399,7 @@ struct getTable { /** Access the "d_cdptrs" member of AttributeManager. */ template struct getTable { + static const AttrTableId id = AttrTableCDPointer; typedef CDAttrHash table_type; static inline table_type& get(AttributeManager& am) { return am.d_cdptrs; @@ -584,6 +629,55 @@ inline void AttributeManager::deleteAllFromTable(AttrHash& table) { table.clear(); } +template +AttributeUniqueId AttributeManager::getAttributeId(const AttrKind& attr){ + typedef typename AttrKind::value_type value_type; + AttrTableId tableId = getTable::id; + return AttributeUniqueId(tableId, attr.getId()); +} + +template +void AttributeManager::deleteAttributesFromTable(AttrHash& table, const std::vector& ids){ + typedef AttributeTraits traits_t; + typedef AttrHash hash_t; + + typename hash_t::iterator it = table.begin(); + typename hash_t::iterator tmp; + typename hash_t::iterator it_end = table.end(); + + std::vector::const_iterator begin_ids = ids.begin(); + std::vector::const_iterator end_ids = ids.end(); + + size_t initialSize = table.size(); + while (it != it_end){ + uint64_t id = (*it).first.first; + + if(std::binary_search(begin_ids, end_ids, id)){ + tmp = it; + ++it; + if(traits_t::getCleanup()[id] != NULL) { + traits_t::getCleanup()[id]((*tmp).second); + } + table.erase(tmp); + }else{ + ++it; + } + } + static const size_t ReconstructShrinkRatio = 8; + if(initialSize/ReconstructShrinkRatio > table.size()){ + reconstructTable(table); + } +} + +template +void AttributeManager::reconstructTable(AttrHash& table){ + typedef AttrHash hash_t; + hash_t cpy; + cpy.insert(table.begin(), table.end()); + cpy.swap(table); +} + }/* CVC4::expr::attr namespace */ }/* CVC4::expr namespace */ -- cgit v1.2.3