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/theory | |
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/theory')
-rwxr-xr-x | src/theory/mkrewriter | 9 | ||||
-rw-r--r-- | src/theory/rewriter.h | 5 | ||||
-rw-r--r-- | src/theory/rewriter_tables_template.h | 20 | ||||
-rw-r--r-- | src/theory/rewriterules/theory_rewriterules_rewriter.h | 2 |
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 */ |