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 | |
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')
-rw-r--r-- | src/theory/builtin/kinds | 1 | ||||
-rw-r--r-- | src/theory/theory.h | 98 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 54 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 86 | ||||
-rw-r--r-- | src/theory/uf/kinds | 1 |
5 files changed, 141 insertions, 99 deletions
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index 1f22ebef1..dfa94a66d 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -127,4 +127,3 @@ constant TYPE_CONSTANT \ "expr/type_constant.h" \ "basic types" operator FUNCTION_TYPE 2: "function type" -variable SORT_TYPE "sort type" 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); diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index e41df92d0..f496f1fd5 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -47,38 +47,30 @@ Theory* TheoryEngine::theoryOf(TNode n) { Assert(k >= 0 && k < kind::LAST_KIND); if(n.getMetaKind() == kind::metakind::VARIABLE) { + // FIXME: we don't yet have a Type-to-Theory map. When we do, + // look up the type of the var and return that Theory (?) + + //The following JUST hacks around this lack of a table TypeNode t = n.getType(); - if(t.isBoolean()) { - return &d_bool; - } else if(t.isReal()) { - return &d_arith; - } else if(t.isArray()) { - return &d_arrays; - } else { - return &d_uf; - } - //Unimplemented(); - } else if(k == kind::EQUAL) { - // if LHS is a variable, use theoryOf(LHS.getType()) - // otherwise, use theoryOf(LHS) - TNode lhs = n[0]; - if(lhs.getMetaKind() == kind::metakind::VARIABLE) { - // FIXME: we don't yet have a Type-to-Theory map. When we do, - // look up the type of the LHS and return that Theory (?) - - //The following JUST hacks around this lack of a table - TypeNode type_of_n = lhs.getType(); - if(type_of_n.isReal()) { - return &d_arith; - } else if(type_of_n.isArray()) { - return &d_arrays; - } else { - return &d_uf; - //Unimplemented(); + Kind k = t.getKind(); + if(k == kind::TYPE_CONSTANT) { + switch(TypeConstant tc = t.getConst<TypeConstant>()) { + case BOOLEAN_TYPE: + return d_theoryOfTable[kind::CONST_BOOLEAN]; + case INTEGER_TYPE: + return d_theoryOfTable[kind::CONST_INTEGER]; + case REAL_TYPE: + return d_theoryOfTable[kind::CONST_RATIONAL]; + case KIND_TYPE: + default: + Unhandled(tc); } - } else { - return theoryOf(lhs); } + + return d_theoryOfTable[k]; + } else if(k == kind::EQUAL) { + // equality is special: use LHS + return theoryOf(n[0]); } else { // use our Kind-to-Theory mapping return d_theoryOfTable[k]; @@ -141,7 +133,7 @@ Node TheoryEngine::preprocess(TNode t) { /* Our goal is to tease out any ITE's sitting under a theory operator. */ Node TheoryEngine::removeITEs(TNode node) { - Debug("ite") << "handleNonAtomicNode(" << node << ")" << endl; + Debug("ite") << "removeITEs(" << node << ")" << endl; /* The result may be cached already */ Node cachedRewrite; @@ -155,7 +147,7 @@ Node TheoryEngine::removeITEs(TNode node) { TypeNode nodeType = node[1].getType(); if(!nodeType.isBoolean()){ - Node skolem = nodeManager->mkVar(node.getType()); + Node skolem = nodeManager->mkSkolem(node.getType()); Node newAssertion = nodeManager->mkNode( kind::ITE, 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 <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; - -}/* 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; diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds index f95bfb582..4bfba382c 100644 --- a/src/theory/uf/kinds +++ b/src/theory/uf/kinds @@ -7,3 +7,4 @@ theory ::CVC4::theory::uf::TheoryUF "theory_uf.h" parameterized APPLY_UF VARIABLE 1: "uninterpreted function application" +variable SORT_TYPE "sort type" |