From: Tim King <taking@cs.nyu.edu>
Date: Thu, 14 Nov 2013 16:56:34 +0000 (-0500)
Subject: Adding the changes needed to delete rewriter attributes.  This includes being able... 
X-Git-Tag: cvc5-1.0.0~7246
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=91424455840a7365a328cbcc3d02ec453fe9d0ea;p=cvc5.git

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.
---

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
@@ -565,6 +565,14 @@ public:
   template <class T>
   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<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;
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<AttributeUniqueId> preids;
+  ${pre_rewrite_attribute_ids}
+
+  std::vector<AttributeUniqueId> postids;
+  ${post_rewrite_attribute_ids}
+
+  std::vector<const AttributeUniqueId*> 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<THEORY_REWRITERULES> {
 
   static void setPostRewriteCache(TNode node, TNode cache) throw() { }
 
+  typedef expr::Attribute< RewriteCacheTag<true, THEORY_REWRITERULES>, Node> pre_rewrite;
+  typedef expr::Attribute< RewriteCacheTag<false, THEORY_REWRITERULES>, Node> post_rewrite;
 };
 
 }/* CVC4::theory namespace */