diff options
Diffstat (limited to 'src/theory/rewriter_attributes.h')
-rw-r--r-- | src/theory/rewriter_attributes.h | 86 |
1 files changed, 86 insertions, 0 deletions
diff --git a/src/theory/rewriter_attributes.h b/src/theory/rewriter_attributes.h new file mode 100644 index 000000000..d33d7314e --- /dev/null +++ b/src/theory/rewriter_attributes.h @@ -0,0 +1,86 @@ +/* + * rewriter_attributes.h + * + * Created on: Dec 27, 2010 + * Author: dejan + */ + +#pragma once + +namespace CVC4 { +namespace theory { + +template <bool pre, theory::TheoryId theoryId> +struct RewriteCacheTag {}; + +template <theory::TheoryId theoryId> +struct RewriteAttibute { + + typedef expr::Attribute< RewriteCacheTag<true, theoryId>, Node> pre_rewrite; + typedef expr::Attribute< RewriteCacheTag<false, theoryId>, Node> post_rewrite; + + /** + * Get the value of the pre-rewrite cache. + */ + static Node getPreRewriteCache(TNode node) throw() { + Node cache; + if (node.hasAttribute(pre_rewrite())) { + node.getAttribute(pre_rewrite(), cache); + } else { + return Node::null(); + } + if (cache.isNull()) { + return node; + } else { + return cache; + } + } + + /** + * Set the value of the pre-rewrite cache. + */ + static void setPreRewriteCache(TNode node, TNode cache) throw() { + Debug("rewriter") << "setting pre-rewrite of " << node << " to " << cache << std::endl; + Assert(!cache.isNull()); + if (node == cache) { + node.setAttribute(pre_rewrite(), Node::null()); + } else { + node.setAttribute(pre_rewrite(), cache); + } + } + + /** + * Get the value of the post-rewrite cache. + * none). + */ + static Node getPostRewriteCache(TNode node) throw() { + Node cache; + if (node.hasAttribute(post_rewrite())) { + node.getAttribute(post_rewrite(), cache); + } else { + return Node::null(); + } + if (cache.isNull()) { + return node; + } else { + return cache; + } + } + + /** + * Set the value of the post-rewrite cache. v cannot be a null Node. + */ + static void setPostRewriteCache(TNode node, TNode cache) throw() { + Assert(!cache.isNull()); + Debug("rewriter") << "setting rewrite of " << node << " to " << cache << std::endl; + if (node == cache) { + node.setAttribute(post_rewrite(), Node::null()); + } else { + node.setAttribute(post_rewrite(), cache); + } + } +}; + +} // Namespace CVC4 +} // Namespace theory + |