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.

4 files changed, 36 insertions, 0 deletions

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 */