diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-07-02 00:09:52 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-07-02 00:09:52 +0000 |
commit | 83a143b1dd78e5d7f07666fbec1362dd60348116 (patch) | |
tree | 08400222d94f4760c7155fea787ac7e78b7b0dfc /src/theory/theory.h | |
parent | a8566c313e9b5eb8248eaeea642a9c72c803dcfa (diff) |
* Added white-box TheoryEngine test that tests the rewriter
* Added regression documentation to test/regress/README
* Added ability to print types of vars in expr printouts
with iomanipulator Node::printtypes(true)... for example,
Warning() << Node::printtypes(true) << n << std::endl;
* Types-printing can be specified on the command line with
--print-expr-types
* Improved type handling facilities and theoryOf().
For now, SORT_TYPE moved from builtin theory to UF theory
to match old behavior.
* Additional gdb debug functionality. Now we have:
debugPrintNode(Node) debugPrintRawNode(Node)
debugPrintTNode(TNode) debugPrintRawTNode(TNode)
debugPrintTypeNode(TypeNode) debugPrintRawTypeNode(TypeNode)
debugPrintNodeValue(NodeValue*) debugPrintRawNodeValue(NodeValue*)
they all print a {Node,TNode,NodeValue*} from the debugger.
The "Raw" versions print a very low-level AST-like form.
The regular versions do the same as operator<<, but force
full printing on (no depth-limiting).
* Other trivial fixes
Diffstat (limited to 'src/theory/theory.h')
-rw-r--r-- | src/theory/theory.h | 98 |
1 files changed, 98 insertions, 0 deletions
diff --git a/src/theory/theory.h b/src/theory/theory.h index bb598d410..8481aa5ff 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -38,6 +38,14 @@ class TheoryEngine; namespace theory { +// rewrite cache support +template <bool topLevel> struct PreRewriteCacheTag {}; +typedef expr::Attribute<PreRewriteCacheTag<true>, Node> PreRewriteCacheTop; +typedef expr::Attribute<PreRewriteCacheTag<false>, Node> PreRewriteCache; +template <bool topLevel> struct PostRewriteCacheTag {}; +typedef expr::Attribute<PostRewriteCacheTag<true>, Node> PostRewriteCacheTop; +typedef expr::Attribute<PostRewriteCacheTag<false>, Node> PostRewriteCache; + /** * Instances of this class serve as response codes from * Theory::preRewrite() and Theory::postRewrite(). Instances of @@ -374,6 +382,96 @@ protected: return true; } + /** + * Check whether a node is in the pre-rewrite cache or not. + */ + static bool inPreRewriteCache(TNode n, bool topLevel) throw() { + if(topLevel) { + return n.hasAttribute(PreRewriteCacheTop()); + } else { + return n.hasAttribute(PreRewriteCache()); + } + } + + /** + * Get the value of the pre-rewrite cache (or Node::null()) if there is + * none). + */ + static Node getPreRewriteCache(TNode n, bool topLevel) throw() { + if(topLevel) { + Node out; + if(n.getAttribute(PreRewriteCacheTop(), out)) { + return out.isNull() ? Node(n) : out; + } + } else { + Node out; + if(n.getAttribute(PreRewriteCache(), out)) { + return out.isNull() ? Node(n) : out; + } + } + return Node::null(); + } + + /** + * Set the value of the pre-rewrite cache. v cannot be a null Node. + */ + static void setPreRewriteCache(TNode n, bool topLevel, TNode v) throw() { + AssertArgument(!n.isNull(), n, "n cannot be null in setPostRewriteCache()"); + AssertArgument(!v.isNull(), v, "v cannot be null in setPreRewriteCache()"); + // mappings from n -> n are actually stored as n -> null as a + // special case, to avoid cycles in the reference-counting of Nodes + if(topLevel) { + n.setAttribute(PreRewriteCacheTop(), n == v ? TNode::null() : v); + } else { + n.setAttribute(PreRewriteCache(), n == v ? TNode::null() : v); + } + } + + /** + * Check whether a node is in the post-rewrite cache or not. + */ + static bool inPostRewriteCache(TNode n, bool topLevel) throw() { + if(topLevel) { + return n.hasAttribute(PostRewriteCacheTop()); + } else { + return n.hasAttribute(PostRewriteCache()); + } + } + + /** + * Get the value of the post-rewrite cache (or Node::null()) if there is + * none). + */ + static Node getPostRewriteCache(TNode n, bool topLevel) throw() { + if(topLevel) { + Node out; + if(n.getAttribute(PostRewriteCacheTop(), out)) { + return out.isNull() ? Node(n) : out; + } + } else { + Node out; + if(n.getAttribute(PostRewriteCache(), out)) { + return out.isNull() ? Node(n) : out; + } + } + return Node::null(); + } + + /** + * Set the value of the post-rewrite cache. v cannot be a null Node. + */ + static void setPostRewriteCache(TNode n, bool topLevel, TNode v) throw() { + AssertArgument(!n.isNull(), n, "n cannot be null in setPostRewriteCache()"); + AssertArgument(!v.isNull(), v, "v cannot be null in setPostRewriteCache()"); + // mappings from n -> n are actually stored as n -> null as a + // special case, to avoid cycles in the reference-counting of Nodes + if(topLevel) { + n.setAttribute(PostRewriteCacheTop(), n == v ? TNode::null() : v); + } else { + n.setAttribute(PostRewriteCache(), n == v ? TNode::null() : v); + } + } + };/* class Theory */ std::ostream& operator<<(std::ostream& os, Theory::Effort level); |