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/Makefile.am | 1 + src/expr/attribute.cpp | 63 +++++++++++++++ src/expr/attribute.h | 94 ++++++++++++++++++++++ src/expr/attribute_internals.h | 19 +++++ src/expr/attribute_unique_id.h | 52 ++++++++++++ src/expr/node.h | 8 ++ src/expr/node_manager.cpp | 8 ++ src/expr/node_manager.h | 13 +++ src/expr/node_value.h | 2 + src/theory/mkrewriter | 9 +++ src/theory/rewriter.h | 5 ++ src/theory/rewriter_tables_template.h | 20 +++++ .../rewriterules/theory_rewriterules_rewriter.h | 2 + 13 files changed, 296 insertions(+) create mode 100644 src/expr/attribute_unique_id.h (limited to 'src') 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 > 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 #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 */ 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 */ /** @@ -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 */ }/* 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 + +// 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 @@ -565,6 +565,14 @@ public: template 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 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& 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; diff --git a/src/theory/mkrewriter b/src/theory/mkrewriter index 084a624f7..0a21a1fe4 100755 --- a/src/theory/mkrewriter +++ b/src/theory/mkrewriter @@ -48,6 +48,9 @@ post_rewrite_calls= post_rewrite_get_cache= post_rewrite_set_cache= +pre_rewrite_attribute_ids= +post_rewrite_attribute_ids= + seen_theory=false seen_theory_builtin=false @@ -144,6 +147,10 @@ function rewriter { " rewrite_shutdown="${rewrite_shutdown} ${class}::shutdown(); " + pre_rewrite_attribute_ids="${pre_rewrite_attribute_ids} preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<${theory_id}>::pre_rewrite())); +" + post_rewrite_attribute_ids="${post_rewrite_attribute_ids} postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<${theory_id}>::post_rewrite())); +" pre_rewrite_calls="${pre_rewrite_calls} case ${theory_id}: return ${class}::preRewrite(node); " @@ -256,6 +263,8 @@ for var in \ pre_rewrite_set_cache \ post_rewrite_set_cache \ rewrite_init rewrite_shutdown \ + pre_rewrite_attribute_ids \ + post_rewrite_attribute_ids \ template \ ; do eval text="\${text//\\\$\\{$var\\}/\${$var}}" diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h index e05d97c05..24f09e62d 100644 --- a/src/theory/rewriter.h +++ b/src/theory/rewriter.h @@ -109,6 +109,11 @@ public: */ static Node rewrite(TNode node); + /** + * Garbage collects the rewrite caches. + */ + static void garbageCollect(); + };/* class Rewriter */ }/* CVC4::theory namespace */ diff --git a/src/theory/rewriter_tables_template.h b/src/theory/rewriter_tables_template.h index 408bdec1a..17aed4e42 100644 --- a/src/theory/rewriter_tables_template.h +++ b/src/theory/rewriter_tables_template.h @@ -21,6 +21,8 @@ #include "theory/rewriter.h" #include "theory/rewriter_attributes.h" +#include "expr/attribute_unique_id.h" +#include "expr/attribute.h" ${rewriter_includes} @@ -83,5 +85,23 @@ void Rewriter::shutdown() { ${rewrite_shutdown} } +void Rewriter::garbageCollect() { + typedef CVC4::expr::attr::AttributeUniqueId AttributeUniqueId; + std::vector preids; + ${pre_rewrite_attribute_ids} + + std::vector postids; + ${post_rewrite_attribute_ids} + + std::vector allids; + for(unsigned i = 0; i < preids.size(); ++i){ + allids.push_back(&preids[i]); + } + for(unsigned i = 0; i < postids.size(); ++i){ + allids.push_back(&postids[i]); + } + NodeManager::currentNM()->deleteAttributes(allids); +} + }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/rewriterules/theory_rewriterules_rewriter.h b/src/theory/rewriterules/theory_rewriterules_rewriter.h index 2c90f063a..f49471407 100644 --- a/src/theory/rewriterules/theory_rewriterules_rewriter.h +++ b/src/theory/rewriterules/theory_rewriterules_rewriter.h @@ -105,6 +105,8 @@ struct RewriteAttibute { static void setPostRewriteCache(TNode node, TNode cache) throw() { } + typedef expr::Attribute< RewriteCacheTag, Node> pre_rewrite; + typedef expr::Attribute< RewriteCacheTag, Node> post_rewrite; }; }/* CVC4::theory namespace */ -- cgit v1.2.3