diff options
Diffstat (limited to 'src/theory/theory_engine.cpp')
| -rw-r--r-- | src/theory/theory_engine.cpp | 338 |
1 files changed, 283 insertions, 55 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 9dfaed68b..e41df92d0 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -19,13 +19,18 @@ #include "theory/theory_engine.h" #include "expr/node.h" #include "expr/attribute.h" +#include "theory/theory.h" +#include "expr/node_builder.h" +#include <vector> #include <list> using namespace std; -namespace CVC4 { +using namespace CVC4; +using namespace CVC4::theory; +namespace CVC4 { namespace theory { struct PreRegisteredTag {}; @@ -36,6 +41,50 @@ typedef expr::Attribute<IteRewriteTag, Node> IteRewriteAttr; }/* CVC4::theory namespace */ +Theory* TheoryEngine::theoryOf(TNode n) { + Kind k = n.getKind(); + + Assert(k >= 0 && k < kind::LAST_KIND); + + if(n.getMetaKind() == kind::metakind::VARIABLE) { + 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(); + } + } else { + return theoryOf(lhs); + } + } else { + // use our Kind-to-Theory mapping + return d_theoryOfTable[k]; + } +} + Node TheoryEngine::preprocess(TNode t) { Node top = rewrite(t); Debug("rewrite") << "rewrote: " << t << endl << "to : " << top << endl; @@ -70,7 +119,7 @@ Node TheoryEngine::preprocess(TNode t) { * and the above registration of leaves, this should ensure that * all subterms in the entire tree were registered in * reverse-topological order. */ - for(std::list<TNode>::reverse_iterator i = toReg.rbegin(); + for(list<TNode>::reverse_iterator i = toReg.rbegin(); i != toReg.rend(); ++i) { @@ -128,9 +177,11 @@ Node TheoryEngine::removeITEs(TNode node) { return skolem; } } - std::vector<Node> newChildren; + vector<Node> newChildren; bool somethingChanged = false; - for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) { + for(TNode::const_iterator it = node.begin(), end = node.end(); + it != end; + ++it) { Node newChild = removeITEs(*it); somethingChanged |= (newChild != *it); newChildren.push_back(newChild); @@ -145,66 +196,243 @@ Node TheoryEngine::removeITEs(TNode node) { nodeManager->setAttribute(node, theory::IteRewriteAttr(), Node::null()); return node; } - } -Node blastDistinct(TNode in){ - Assert(in.getKind() == kind::DISTINCT); - if(in.getNumChildren() == 2){ - //If this is the case exactly 1 != pair will be generated so the AND is not required - Node eq = NodeManager::currentNM()->mkNode(CVC4::kind::EQUAL, in[0], in[1]); - Node neq = NodeManager::currentNM()->mkNode(CVC4::kind::NOT, eq); - return neq; - } - //Assume that in.getNumChildren() > 2 - // => diseqs.size() > 1 - vector<Node> diseqs; - for(TNode::iterator i = in.begin(); i != in.end(); ++i) { - TNode::iterator j = i; - while(++j != in.end()) { - Node eq = NodeManager::currentNM()->mkNode(CVC4::kind::EQUAL, *i, *j); - Node neq = NodeManager::currentNM()->mkNode(CVC4::kind::NOT, eq); - diseqs.push_back(neq); - } +namespace theory { +namespace rewrite { + +/** + * TheoryEngine::rewrite() keeps a stack of things that are being pre- + * and post-rewritten. Each element of the stack is a + * RewriteStackElement. + */ +struct RewriteStackElement { + /** + * The node at this rewrite level. For example (AND (OR x y) z) + * will have, as it's rewriting x, the stack: + * x + * (OR x y) + * (AND (OR x y) z) + */ + Node d_node; + + /** + * The theory associated to d_node. Cached here to avoid having to + * look it up again. + */ + Theory* d_theory; + + /** + * Whether or not this was a top-level rewrite. Note that at theory + * boundaries, topLevel is forced to true, so it's not the case that + * this is true only at the lowest stack level. + */ + bool d_topLevel; + + /** + * A saved index to the "next child" to pre- and post-rewrite. In + * the case when (AND (OR x y) z) is being rewritten, the AND, OR, + * and x are pre-rewritten, then (assuming they don't change), x is + * post-rewritten, then y is pre- and post-rewritten, then the OR is + * post-rewritten, then z is pre-rewritten, then the AND is + * post-rewritten. At each stack level, we need to remember the + * child index we're currently processing. + */ + int d_nextChild; + + /** + * A (re)builder for this node. As this node's children are + * post-rewritten, in order, they append to this builder. When this + * node is post-rewritten, it is reformed from d_builder since the + * children may have changed. Note Nodes aren't rebuilt if they + * have metakinds CONSTANT (which is illegal) or VARIABLE (which + * would create a fresh variable, not what we want)---which is fine, + * since those types don't have children anyway. + */ + NodeBuilder<> d_builder; + + /** + * Construct a fresh stack element. + */ + RewriteStackElement(Node n, Theory* thy, bool top) : + d_node(n), + d_theory(thy), + d_topLevel(top), + d_nextChild(0) { } - Node out = NodeManager::currentNM()->mkNode(CVC4::kind::AND, diseqs); - return out; -} +}; + +}/* CVC4::theory::rewrite namespace */ +}/* CVC4::theory namespace */ Node TheoryEngine::rewrite(TNode in) { - if(inRewriteCache(in)) { - return getRewriteCache(in); - } + using theory::rewrite::RewriteStackElement; + + Node noItes = removeITEs(in); + Node out; + + // descend top-down into the theory rewriters + vector<RewriteStackElement> stack; + stack.push_back(RewriteStackElement(noItes, theoryOf(noItes), true)); + Debug("theory-rewrite") << "TheoryEngine::rewrite() starting at" << endl + << " " << noItes << " " << theoryOf(noItes) + << " TOP-LEVEL 0" << endl; + // This whole thing is essentially recursive, but we avoid actually + // doing any recursion. + do {// do until the stack is empty.. + RewriteStackElement& rse = stack.back(); + bool done; + + Debug("theory-rewrite") << "rewriter looking at level " << stack.size() + << endl + << " " << rse.d_node << " " << rse.d_theory + << "[" << *rse.d_theory << "]" + << " " << (rse.d_topLevel ? "TOP-LEVEL " : "") + << rse.d_nextChild << endl; + + if(rse.d_nextChild == 0) { + Node original = rse.d_node; + bool wasTopLevel = rse.d_topLevel; + Node cached = getPreRewriteCache(original, wasTopLevel); + if(cached.isNull()) { + do { + Debug("theory-rewrite") << "doing pre-rewrite in " << *rse.d_theory + << " topLevel==" << rse.d_topLevel << endl; + RewriteResponse response = + rse.d_theory->preRewrite(rse.d_node, rse.d_topLevel); + rse.d_node = response.getNode(); + Assert(!rse.d_node.isNull(), "node illegally rewritten to null"); + Theory* thy2 = theoryOf(rse.d_node); + Assert(thy2 != NULL, "node illegally rewritten to null theory"); + Debug("theory-rewrite") << "got back " << rse.d_node << " " + << thy2 << "[" << *thy2 << "]" + << (response.needsMoreRewriting() ? + " MORE-REWRITING" : " DONE") + << endl; + if(rse.d_theory != thy2) { + Debug("theory-rewrite") << "pre-rewritten from " << *rse.d_theory + << " into " << *thy2 + << ", marking top-level and !done" << endl; + rse.d_theory = thy2; + done = false; + // FIXME how to handle the "top-levelness" of a node that's + // rewritten from theory T1 into T2, then back to T1 ? + rse.d_topLevel = true; + } else { + done = !response.needsMoreRewriting(); + } + } while(!done); + setPreRewriteCache(original, wasTopLevel, rse.d_node); + } else {// is in pre-rewrite cache + Debug("theory-rewrite") << "in pre-cache: " << cached << endl; + rse.d_node = cached; + Theory* thy2 = theoryOf(cached); + if(rse.d_theory != thy2) { + Debug("theory-rewrite") << "[cache-]pre-rewritten from " + << *rse.d_theory << " into " << *thy2 + << ", marking top-level" << endl; + rse.d_theory = thy2; + rse.d_topLevel = true; + } + } + } - if(in.getMetaKind() == kind::metakind::VARIABLE) { - return in; - } + // children + Node original = rse.d_node; + bool wasTopLevel = rse.d_topLevel; + Node cached = getPostRewriteCache(original, wasTopLevel); + + if(cached.isNull()) { + if(rse.d_nextChild == 0 && + rse.d_node.getMetaKind() == kind::metakind::PARAMETERIZED) { + ++rse.d_nextChild; + Node op = rse.d_node.getOperator(); + Theory* t = theoryOf(op); + Debug("theory-rewrite") << "pushing operator of " << rse.d_node << endl; + stack.push_back(RewriteStackElement(op, t, t != rse.d_theory)); + continue;// break out of this node, do its operator + } else { + unsigned nch = rse.d_nextChild++; + if(rse.d_node.getMetaKind() == kind::metakind::PARAMETERIZED) { + --nch; + } + if(nch < rse.d_node.getNumChildren()) { + Debug("theory-rewrite") << "pushing child " << nch + << " of " << rse.d_node << endl; + Node c = rse.d_node[nch]; + Theory* t = theoryOf(c); + stack.push_back(RewriteStackElement(c, t, t != rse.d_theory)); + continue;// break out of this node, do its child + } + } - Node intermediate = removeITEs(in); + // incorporate the children's rewrites + if(rse.d_node.getMetaKind() != kind::metakind::VARIABLE && + rse.d_node.getMetaKind() != kind::metakind::CONSTANT) { + Debug("theory-rewrite") << "builder here is " << &rse.d_builder + << " and it gets " << rse.d_node.getKind() + << endl; + rse.d_builder << rse.d_node.getKind(); + rse.d_node = Node(rse.d_builder); + } - // these special cases should go away when theory rewriting comes online - if(intermediate.getKind() == kind::DISTINCT) { - Node out = blastDistinct(intermediate); - //setRewriteCache(intermediate, out); - return rewrite(out); //TODO let this fall through? - } + // post-rewriting + do { + Debug("theory-rewrite") << "doing post-rewrite of " + << rse.d_node << endl + << " in " << *rse.d_theory + << " topLevel==" << rse.d_topLevel << endl; + RewriteResponse response = + rse.d_theory->postRewrite(rse.d_node, rse.d_topLevel); + rse.d_node = response.getNode(); + Assert(!rse.d_node.isNull(), "node illegally rewritten to null"); + Theory* thy2 = theoryOf(rse.d_node); + Assert(thy2 != NULL, "node illegally rewritten to null theory"); + Debug("theory-rewrite") << "got back " << rse.d_node << " " + << thy2 << "[" << *thy2 << "]" + << (response.needsMoreRewriting() ? + " MORE-REWRITING" : " DONE") + << endl; + if(rse.d_theory != thy2) { + Debug("theory-rewrite") << "post-rewritten from " << *rse.d_theory + << " into " << *thy2 + << ", marking top-level and !done" << endl; + rse.d_theory = thy2; + done = false; + // FIXME how to handle the "top-levelness" of a node that's + // rewritten from theory T1 into T2, then back to T1 ? + rse.d_topLevel = true; + } else { + done = !response.needsMoreRewriting(); + } + } while(!done); + + setPostRewriteCache(original, wasTopLevel, rse.d_node); + + out = rse.d_node; + } else { + Debug("theory-rewrite") << "in post-cache: " << cached << endl; + out = cached; + Theory* thy2 = theoryOf(cached); + if(rse.d_theory != thy2) { + Debug("theory-rewrite") << "[cache-]post-rewritten from " + << *rse.d_theory << " into " << *thy2 << endl; + rse.d_theory = thy2; + } + } - theory::Theory* thy = theoryOf(intermediate); - if(thy == NULL) { - Node out = rewriteBuiltins(intermediate); - //setRewriteCache(intermediate, out); - return out; - } else if(thy != &d_bool){ - Node out = thy->rewrite(intermediate); - //setRewriteCache(intermediate, out); - return out; - }else{ - Node out = rewriteChildren(intermediate); - //setRewriteCache(intermediate, out); - return out; - } + stack.pop_back(); + if(!stack.empty()) { + Debug("theory-rewrite") << "asserting " << out << " to previous builder " + << &stack.back().d_builder << endl; + stack.back().d_builder << out; + } + } while(!stack.empty()); - Unreachable(); -} + Debug("theory-rewrite") << "DONE with theory rewriter." << endl; + Debug("theory-rewrite") << "result is:" << endl << out << endl; + + return out; +}/* TheoryEngine::rewrite(TNode in) */ }/* CVC4 namespace */ |