From 83a143b1dd78e5d7f07666fbec1362dd60348116 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 2 Jul 2010 00:09:52 +0000 Subject: * 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 --- src/theory/theory_engine.h | 86 ++++++++++------------------------------------ 1 file changed, 19 insertions(+), 67 deletions(-) (limited to 'src/theory/theory_engine.h') diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 2575c4c2d..79eec4301 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -37,18 +37,6 @@ namespace CVC4 { -namespace theory { - -// rewrite cache support -template struct PreRewriteCacheTag {}; -typedef expr::Attribute, Node> PreRewriteCacheTop; -typedef expr::Attribute, Node> PreRewriteCache; -template struct PostRewriteCacheTag {}; -typedef expr::Attribute, Node> PostRewriteCacheTop; -typedef expr::Attribute, Node> PostRewriteCache; - -}/* CVC4::theory namespace */ - // In terms of abstraction, this is below (and provides services to) // PropEngine. @@ -136,95 +124,48 @@ class TheoryEngine { theory::arrays::TheoryArrays d_arrays; theory::bv::TheoryBV d_bv; - /** * 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(theory::PreRewriteCacheTop()); - } else { - return n.hasAttribute(theory::PreRewriteCache()); - } + return theory::Theory::inPreRewriteCache(n, topLevel); } /** * Get the value of the pre-rewrite cache (or Node::null()) if there is * none). */ - static Node getPreRewriteCache(TNode in, bool topLevel) throw() { - if(topLevel) { - Node out; - if(in.getAttribute(theory::PreRewriteCacheTop(), out)) { - return out.isNull() ? Node(in) : out; - } - } else { - Node out; - if(in.getAttribute(theory::PreRewriteCache(), out)) { - return out.isNull() ? Node(in) : out; - } - } - return Node::null(); + static Node getPreRewriteCache(TNode n, bool topLevel) throw() { + return theory::Theory::getPreRewriteCache(n, topLevel); } /** * 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(theory::PreRewriteCacheTop(), n == v ? TNode::null() : v); - } else { - n.setAttribute(theory::PreRewriteCache(), n == v ? TNode::null() : v); - } + return theory::Theory::setPreRewriteCache(n, topLevel, 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(theory::PostRewriteCacheTop()); - } else { - return n.hasAttribute(theory::PostRewriteCache()); - } + return theory::Theory::inPostRewriteCache(n, topLevel); } /** * Get the value of the post-rewrite cache (or Node::null()) if there is * none). */ - static Node getPostRewriteCache(TNode in, bool topLevel) throw() { - if(topLevel) { - Node out; - if(in.getAttribute(theory::PostRewriteCacheTop(), out)) { - return out.isNull() ? Node(in) : out; - } - } else { - Node out; - if(in.getAttribute(theory::PostRewriteCache(), out)) { - return out.isNull() ? Node(in) : out; - } - } - return Node::null(); + static Node getPostRewriteCache(TNode n, bool topLevel) throw() { + return theory::Theory::getPostRewriteCache(n, topLevel); } /** * 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(theory::PostRewriteCacheTop(), n == v ? TNode::null() : v); - } else { - n.setAttribute(theory::PostRewriteCache(), n == v ? TNode::null() : v); - } + return theory::Theory::setPostRewriteCache(n, topLevel, v); } /** @@ -233,6 +174,9 @@ class TheoryEngine { */ Node rewrite(TNode in); + /** + * Replace ITE forms in a node. + */ Node removeITEs(TNode t); public: @@ -386,6 +330,14 @@ private: StatisticsRegistry::registerStat(&d_statAugLemma); StatisticsRegistry::registerStat(&d_statExplanatation); } + + ~Statistics() { + StatisticsRegistry::unregisterStat(&d_statConflicts); + StatisticsRegistry::unregisterStat(&d_statPropagate); + StatisticsRegistry::unregisterStat(&d_statLemma); + StatisticsRegistry::unregisterStat(&d_statAugLemma); + StatisticsRegistry::unregisterStat(&d_statExplanatation); + } }; Statistics d_statistics; -- cgit v1.2.3