diff options
author | Tim King <taking@cs.nyu.edu> | 2013-11-14 11:56:34 -0500 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2013-11-21 10:43:44 -0500 |
commit | 91424455840a7365a328cbcc3d02ec453fe9d0ea (patch) | |
tree | e8072eb0c7dda81feafb1c5f9a4ca2f0fcbc0399 /src/expr | |
parent | bd8e9319aab69db90692f72bc52288329879eefc (diff) |
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.
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/Makefile.am | 1 | ||||
-rw-r--r-- | src/expr/attribute.cpp | 63 | ||||
-rw-r--r-- | src/expr/attribute.h | 94 | ||||
-rw-r--r-- | src/expr/attribute_internals.h | 19 | ||||
-rw-r--r-- | src/expr/attribute_unique_id.h | 52 | ||||
-rw-r--r-- | src/expr/node.h | 8 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 8 | ||||
-rw-r--r-- | src/expr/node_manager.h | 13 | ||||
-rw-r--r-- | src/expr/node_value.h | 2 |
9 files changed, 260 insertions, 0 deletions
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index 16ee454c8..13358d294 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -20,6 +20,7 @@ libexpr_la_SOURCES = \ node_manager.cpp \ node_manager_attributes.h \ type_checker.h \ + attribute_unique_id.h \ attribute.h \ attribute_internals.h \ attribute.cpp \ diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp index 20d52e3cc..92a21546c 100644 --- a/src/expr/attribute.cpp +++ b/src/expr/attribute.cpp @@ -26,6 +26,15 @@ namespace CVC4 { namespace expr { namespace attr { + +void AttributeManager::debugHook(int debugFlag) { + /* DO NOT CHECK IN ANY CODE INTO THE DEBUG HOOKS! + * debugHook() is an empty function for the purpose of debugging + * the AttributeManager without recompiling all of CVC4. + * Formally this is a nop. + */ +} + void AttributeManager::deleteAllAttributes(NodeValue* nv) { d_bools.erase(nv); deleteFromTable(d_ints, nv); @@ -60,6 +69,60 @@ void AttributeManager::deleteAllAttributes() { d_cdptrs.clear(); } +void AttributeManager::deleteAttributes(const AttrIdVec& atids){ + typedef std::map<uint64_t, std::vector< uint64_t> > AttrToVecMap; + AttrToVecMap perTableIds; + + for(AttrIdVec::const_iterator it = atids.begin(), it_end = atids.end(); it != it_end; ++it){ + const AttributeUniqueId& pair = *(*it); + std::vector< uint64_t>& inTable = perTableIds[pair.getTableId()]; + inTable.push_back(pair.getWithinTypeId()); + } + AttrToVecMap::iterator it = perTableIds.begin(), it_end = perTableIds.end(); + for(; it != it_end; ++it){ + Assert(((*it).first) <= LastAttrTable); + AttrTableId tableId = (AttrTableId) ((*it).first); + std::vector< uint64_t>& ids = (*it).second; + std::sort(ids.begin(), ids.end()); + + switch(tableId){ + case AttrTableBool: + Unimplemented("delete attributes is unimplemented for bools"); + break; + case AttrTableUInt64: + deleteAttributesFromTable(d_ints, ids); + break; + case AttrTableTNode: + deleteAttributesFromTable(d_tnodes, ids); + break; + case AttrTableNode: + deleteAttributesFromTable(d_nodes, ids); + break; + case AttrTableTypeNode: + deleteAttributesFromTable(d_types, ids); + break; + case AttrTableString: + deleteAttributesFromTable(d_strings, ids); + break; + case AttrTablePointer: + deleteAttributesFromTable(d_ptrs, ids); + break; + + case AttrTableCDBool: + case AttrTableCDUInt64: + case AttrTableCDTNode: + case AttrTableCDNode: + case AttrTableCDString: + case AttrTableCDPointer: + Unimplemented("CDAttributes cannot be deleted. Contact Tim/Morgan if this behaviour is desired."); + break; + case LastAttrTable: + default: + Unreachable(); + } + } +} + }/* CVC4::expr::attr namespace */ }/* CVC4::expr namespace */ }/* CVC4 namespace */ 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 <string> #include <stdint.h> +#include "expr/attribute_unique_id.h" // include supporting templates #define CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H @@ -87,6 +88,12 @@ class AttributeManager { template <class T> void deleteAllFromTable(AttrHash<T>& table); + template <class T> + void deleteAttributesFromTable(AttrHash<T>& table, const std::vector<uint64_t>& ids); + + template <class T> + void reconstructTable(AttrHash<T>& 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 <class AttrKind> + 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<bool, false> { + static const AttrTableId id = AttrTableBool; typedef AttrHash<bool> table_type; static inline table_type& get(AttributeManager& am) { return am.d_bools; @@ -199,6 +230,7 @@ struct getTable<bool, false> { /** Access the "d_ints" member of AttributeManager. */ template <> struct getTable<uint64_t, false> { + static const AttrTableId id = AttrTableUInt64; typedef AttrHash<uint64_t> table_type; static inline table_type& get(AttributeManager& am) { return am.d_ints; @@ -211,6 +243,7 @@ struct getTable<uint64_t, false> { /** Access the "d_tnodes" member of AttributeManager. */ template <> struct getTable<TNode, false> { + static const AttrTableId id = AttrTableTNode; typedef AttrHash<TNode> table_type; static inline table_type& get(AttributeManager& am) { return am.d_tnodes; @@ -223,6 +256,7 @@ struct getTable<TNode, false> { /** Access the "d_nodes" member of AttributeManager. */ template <> struct getTable<Node, false> { + static const AttrTableId id = AttrTableNode; typedef AttrHash<Node> table_type; static inline table_type& get(AttributeManager& am) { return am.d_nodes; @@ -235,6 +269,7 @@ struct getTable<Node, false> { /** Access the "d_types" member of AttributeManager. */ template <> struct getTable<TypeNode, false> { + static const AttrTableId id = AttrTableTypeNode; typedef AttrHash<TypeNode> table_type; static inline table_type& get(AttributeManager& am) { return am.d_types; @@ -247,6 +282,7 @@ struct getTable<TypeNode, false> { /** Access the "d_strings" member of AttributeManager. */ template <> struct getTable<std::string, false> { + static const AttrTableId id = AttrTableString; typedef AttrHash<std::string> table_type; static inline table_type& get(AttributeManager& am) { return am.d_strings; @@ -259,6 +295,7 @@ struct getTable<std::string, false> { /** Access the "d_ptrs" member of AttributeManager. */ template <class T> struct getTable<T*, false> { + static const AttrTableId id = AttrTablePointer; typedef AttrHash<void*> table_type; static inline table_type& get(AttributeManager& am) { return am.d_ptrs; @@ -271,6 +308,7 @@ struct getTable<T*, false> { /** Access the "d_ptrs" member of AttributeManager. */ template <class T> struct getTable<const T*, false> { + static const AttrTableId id = AttrTablePointer; typedef AttrHash<void*> table_type; static inline table_type& get(AttributeManager& am) { return am.d_ptrs; @@ -283,6 +321,7 @@ struct getTable<const T*, false> { /** Access the "d_cdbools" member of AttributeManager. */ template <> struct getTable<bool, true> { + static const AttrTableId id = AttrTableCDBool; typedef CDAttrHash<bool> table_type; static inline table_type& get(AttributeManager& am) { return am.d_cdbools; @@ -295,6 +334,7 @@ struct getTable<bool, true> { /** Access the "d_cdints" member of AttributeManager. */ template <> struct getTable<uint64_t, true> { + static const AttrTableId id = AttrTableCDUInt64; typedef CDAttrHash<uint64_t> table_type; static inline table_type& get(AttributeManager& am) { return am.d_cdints; @@ -307,6 +347,7 @@ struct getTable<uint64_t, true> { /** Access the "d_tnodes" member of AttributeManager. */ template <> struct getTable<TNode, true> { + static const AttrTableId id = AttrTableCDTNode; typedef CDAttrHash<TNode> table_type; static inline table_type& get(AttributeManager& am) { return am.d_cdtnodes; @@ -319,6 +360,7 @@ struct getTable<TNode, true> { /** Access the "d_cdnodes" member of AttributeManager. */ template <> struct getTable<Node, true> { + static const AttrTableId id = AttrTableCDNode; typedef CDAttrHash<Node> table_type; static inline table_type& get(AttributeManager& am) { return am.d_cdnodes; @@ -331,6 +373,7 @@ struct getTable<Node, true> { /** Access the "d_cdstrings" member of AttributeManager. */ template <> struct getTable<std::string, true> { + static const AttrTableId id = AttrTableCDString; typedef CDAttrHash<std::string> table_type; static inline table_type& get(AttributeManager& am) { return am.d_cdstrings; @@ -343,6 +386,7 @@ struct getTable<std::string, true> { /** Access the "d_cdptrs" member of AttributeManager. */ template <class T> struct getTable<T*, true> { + static const AttrTableId id = AttrTableCDPointer; typedef CDAttrHash<void*> table_type; static inline table_type& get(AttributeManager& am) { return am.d_cdptrs; @@ -355,6 +399,7 @@ struct getTable<T*, true> { /** Access the "d_cdptrs" member of AttributeManager. */ template <class T> struct getTable<const T*, true> { + static const AttrTableId id = AttrTableCDPointer; typedef CDAttrHash<void*> table_type; static inline table_type& get(AttributeManager& am) { return am.d_cdptrs; @@ -584,6 +629,55 @@ inline void AttributeManager::deleteAllFromTable(AttrHash<T>& table) { table.clear(); } +template <class AttrKind> +AttributeUniqueId AttributeManager::getAttributeId(const AttrKind& attr){ + typedef typename AttrKind::value_type value_type; + AttrTableId tableId = getTable<value_type, + AttrKind::context_dependent>::id; + return AttributeUniqueId(tableId, attr.getId()); +} + +template <class T> +void AttributeManager::deleteAttributesFromTable(AttrHash<T>& table, const std::vector<uint64_t>& ids){ + typedef AttributeTraits<T, false> traits_t; + typedef AttrHash<T> hash_t; + + typename hash_t::iterator it = table.begin(); + typename hash_t::iterator tmp; + typename hash_t::iterator it_end = table.end(); + + std::vector<uint64_t>::const_iterator begin_ids = ids.begin(); + std::vector<uint64_t>::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 <class T> +void AttributeManager::reconstructTable(AttrHash<T>& table){ + typedef AttrHash<T> hash_t; + hash_t cpy; + cpy.insert(table.begin(), table.end()); + cpy.swap(table); +} + }/* CVC4::expr::attr namespace */ }/* CVC4::expr namespace */ diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h index a0086440b..fa6459481 100644 --- a/src/expr/attribute_internals.h +++ b/src/expr/attribute_internals.h @@ -357,6 +357,15 @@ public: super::clear(); } + /** Is the hash table empty? */ + bool empty() const { + return super::empty(); + } + + /** This is currently very misleading! */ + size_t size() const { + return super::size(); + } };/* class AttrHash<bool> */ /** @@ -558,6 +567,16 @@ public: super::clear(); } + /** Is the hash table empty? */ + bool empty() const { + return super::empty(); + } + + /** This is currently very misleading! */ + size_t size() const { + return super::size(); + } + };/* class CDAttrHash<bool> */ }/* CVC4::expr::attr namespace */ diff --git a/src/expr/attribute_unique_id.h b/src/expr/attribute_unique_id.h new file mode 100644 index 000000000..79c6bfd8f --- /dev/null +++ b/src/expr/attribute_unique_id.h @@ -0,0 +1,52 @@ + +#pragma once + +#include "cvc4_private.h" +#include <stdint.h> + +// ATTRIBUTE IDs ============================================================ + +namespace CVC4 { +namespace expr { +namespace attr { + +/** A unique id for each attribute table. */ +enum AttrTableId { + AttrTableBool, + AttrTableUInt64, + AttrTableTNode, + AttrTableNode, + AttrTableTypeNode, + AttrTableString, + AttrTablePointer, + AttrTableCDBool, + AttrTableCDUInt64, + AttrTableCDTNode, + AttrTableCDNode, + AttrTableCDString, + AttrTableCDPointer, + LastAttrTable +}; + +/** + * This uniquely indentifies attributes across tables. + */ +class AttributeUniqueId { + AttrTableId d_tableId; + uint64_t d_withinTypeId; + +public: + AttributeUniqueId() : d_tableId(LastAttrTable), d_withinTypeId(0){} + + AttributeUniqueId(AttrTableId tableId, uint64_t within) + : d_tableId(tableId), d_withinTypeId(within) + {} + + AttrTableId getTableId() const{ return d_tableId; } + uint64_t getWithinTypeId() const{ return d_withinTypeId; } + +};/* CVC4::expr::attr::AttributeUniqueId */ + +}/* CVC4::expr::attr namespace */ +}/* CVC4::expr namespace */ +}/* CVC4 namespace */ diff --git a/src/expr/node.h b/src/expr/node.h index 3a5b6f135..0a4b853aa 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -566,6 +566,14 @@ public: inline const T& getConst() const; /** + * Returns the reference count of this node. + * @return the refcount + */ + unsigned getRefCount() const { + return d_nv->getRefCount(); + } + + /** * Returns the value of the given attribute that this has been attached. * @param attKind the kind of the attribute * @return the value of the attribute diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index f6424cfe0..cede6ff1f 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -586,4 +586,12 @@ Node NodeManager::mkAbstractValue(const TypeNode& type) { return n; } +void NodeManager::deleteAttributes(const std::vector<const expr::attr::AttributeUniqueId*>& ids){ + d_attrManager->deleteAttributes(ids); +} + +void NodeManager::debugHook(int debugFlag){ + // For debugging purposes only, DO NOT CHECK IN ANY CODE! +} + }/* CVC4 namespace */ diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 51ed1f94d..32c492003 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -46,6 +46,7 @@ class StatisticsRegistry; namespace expr { namespace attr { + class AttributeUniqueId; class AttributeManager; }/* CVC4::expr::attr namespace */ @@ -859,6 +860,18 @@ public: */ static inline TypeNode fromType(Type t); + /** Deletes a list of attributes from the NM's AttributeManager.*/ + void deleteAttributes(const std::vector< const expr::attr::AttributeUniqueId* >& ids); + + /** + * This function gives developers a hook into the NodeManager. + * This can be changed in node_manager.cpp without recompiling most of cvc4. + * + * debugHook is a debugging only function, and should not be present in + * any published code! + */ + void debugHook(int debugFlag); + };/* class NodeManager */ /** diff --git a/src/expr/node_value.h b/src/expr/node_value.h index e9d14c38e..24132491a 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -264,6 +264,8 @@ public: : d_nchildren; } + unsigned getRefCount() const { return d_rc; } + std::string toString() const; void toStream(std::ostream& out, int toDepth = -1, bool types = false, size_t dag = 1, OutputLanguage = language::output::LANG_AST) const; |