diff options
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 534 |
1 files changed, 94 insertions, 440 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index e2c42bccd..25fe29c67 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -26,14 +26,8 @@ #include "theory/theory.h" #include "theory/theory_engine.h" -#include "theory/builtin/theory_builtin.h" -#include "theory/booleans/theory_bool.h" -#include "theory/uf/theory_uf.h" -#include "theory/uf/morgan/theory_uf_morgan.h" -#include "theory/uf/tim/theory_uf_tim.h" -#include "theory/arith/theory_arith.h" -#include "theory/arrays/theory_arrays.h" -#include "theory/bv/theory_bv.h" +#include "theory/rewriter.h" +#include "theory/theory_traits.h" using namespace std; @@ -41,6 +35,12 @@ using namespace CVC4; using namespace CVC4::theory; namespace CVC4 { + +/** Tag for the "registerTerm()-has-been-called" flag on Nodes */ +struct Registered {}; +/** The "registerTerm()-has-been-called" flag on Nodes */ +typedef CVC4::expr::CDAttribute<Registered, bool> RegisteredAttr; + namespace theory { struct PreRegisteredTag {}; @@ -129,150 +129,101 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) { TheoryEngine::TheoryEngine(context::Context* ctxt, const Options& opts) : d_propEngine(NULL), + d_context(ctxt), d_theoryOut(this, ctxt), d_theoryRegistration(opts.theoryRegistration), d_hasShutDown(false), d_incomplete(ctxt, false), d_statistics() { - d_sharedTermManager = new SharedTermManager(this, ctxt); + Rewriter::init(); - d_builtin = new theory::builtin::TheoryBuiltin(0, ctxt, d_theoryOut); - d_bool = new theory::booleans::TheoryBool(1, ctxt, d_theoryOut); - switch(opts.uf_implementation) { - case Options::TIM: - d_uf = new theory::uf::tim::TheoryUFTim(2, ctxt, d_theoryOut); - break; - case Options::MORGAN: - d_uf = new theory::uf::morgan::TheoryUFMorgan(2, ctxt, d_theoryOut); - break; - default: - Unhandled(opts.uf_implementation); - } - d_arith = new theory::arith::TheoryArith(3, ctxt, d_theoryOut); - d_arrays = new theory::arrays::TheoryArrays(4, ctxt, d_theoryOut); - d_bv = new theory::bv::TheoryBV(5, ctxt, d_theoryOut); - - d_sharedTermManager->registerTheory(static_cast<theory::builtin::TheoryBuiltin*>(d_builtin)); - d_sharedTermManager->registerTheory(static_cast<theory::booleans::TheoryBool*>(d_bool)); - d_sharedTermManager->registerTheory(static_cast<theory::uf::TheoryUF*>(d_uf)); - d_sharedTermManager->registerTheory(static_cast<theory::arith::TheoryArith*>(d_arith)); - d_sharedTermManager->registerTheory(static_cast<theory::arrays::TheoryArrays*>(d_arrays)); - d_sharedTermManager->registerTheory(static_cast<theory::bv::TheoryBV*>(d_bv)); - - d_theoryOfTable.registerTheory(static_cast<theory::builtin::TheoryBuiltin*>(d_builtin)); - d_theoryOfTable.registerTheory(static_cast<theory::booleans::TheoryBool*>(d_bool)); - d_theoryOfTable.registerTheory(static_cast<theory::uf::TheoryUF*>(d_uf)); - d_theoryOfTable.registerTheory(static_cast<theory::arith::TheoryArith*>(d_arith)); - d_theoryOfTable.registerTheory(static_cast<theory::arrays::TheoryArrays*>(d_arrays)); - d_theoryOfTable.registerTheory(static_cast<theory::bv::TheoryBV*>(d_bv)); + d_sharedTermManager = new SharedTermManager(this, ctxt); } TheoryEngine::~TheoryEngine() { Assert(d_hasShutDown); - delete d_bv; - delete d_arrays; - delete d_arith; - delete d_uf; - delete d_bool; - delete d_builtin; - - delete d_sharedTermManager; -} - -Theory* TheoryEngine::theoryOf(TypeNode t) { - // 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 - 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); + for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++ theoryId) { + if (d_theoryTable[theoryId]) { + delete d_theoryTable[theoryId]; } } - return d_theoryOfTable[k]; + delete d_sharedTermManager; } +struct preprocess_stack_element { + TNode node; + bool children_added; + preprocess_stack_element(TNode node) + : node(node), children_added(false) {} +}; -Theory* TheoryEngine::theoryOf(TNode n) { - Kind k = n.getKind(); +Node TheoryEngine::preprocess(TNode node) { - Assert(k >= 0 && k < kind::LAST_KIND); + // Remove ITEs and rewrite the node + Node preprocessed = Rewriter::rewrite(removeITEs(node)); - if(n.getMetaKind() == kind::metakind::VARIABLE) { - return theoryOf(n.getType()); - } 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]; + // If we are pre-registered already we are done + if (preprocessed.getAttribute(PreRegistered())) { + return preprocessed; } -} - -Node TheoryEngine::preprocess(TNode t) { - Node top = rewrite(t); - Debug("rewrite") << "rewrote: " << t << endl << "to : " << top << endl; - - list<TNode> toReg; - toReg.push_back(top); - - /* Essentially this is doing a breadth-first numbering of - * non-registered subterms with children. Any non-registered - * leaves are immediately registered. */ - for(list<TNode>::iterator workp = toReg.begin(); - workp != toReg.end(); - ++workp) { - - TNode n = *workp; - for(TNode::iterator i = n.begin(); i != n.end(); ++i) { - TNode c = *i; - - if(!c.getAttribute(theory::PreRegistered())) {// c not yet registered - if(c.getNumChildren() == 0) { - c.setAttribute(theory::PreRegistered(), true); - theoryOf(c)->preRegisterTerm(c); + // Do a topological sort of the subexpressions and preregister them + vector<preprocess_stack_element> toVisit; + toVisit.push_back((TNode) preprocessed); + while (!toVisit.empty()) { + preprocess_stack_element& stackHead = toVisit.back(); + // The current node we are processing + TNode current = stackHead.node; + // If we already added all the children its time to register or just pop from the stack + if (stackHead.children_added || current.getAttribute(PreRegistered())) { + if (!current.getAttribute(PreRegistered())) { + // Mark it as registered + current.setAttribute(PreRegistered(), true); + // Register this node + if (current.getKind() == kind::EQUAL) { + TheoryId theoryLHS = Theory::theoryOf(current[0]); + Debug("register") << "preregistering " << current << " with " << theoryLHS << std::endl; + d_theoryTable[theoryLHS]->preRegisterTerm(current); +// TheoryId theoryRHS = Theory::theoryOf(current[1]); +// if (theoryLHS != theoryRHS) { +// d_theoryTable[theoryRHS]->preRegisterTerm(current); +// Debug("register") << "preregistering " << current << " with " << theoryRHS << std::endl; +// } +// TheoryId typeTheory = Theory::theoryOf(current[0].getType()); +// if (typeTheory != theoryLHS && typeTheory != theoryRHS) { +// d_theoryTable[typeTheory]->preRegisterTerm(current); +// Debug("register") << "preregistering " << current << " with " << typeTheory << std::endl; +// } } else { - toReg.push_back(c); + TheoryId theory = Theory::theoryOf(current); + Debug("register") << "preregistering " << current << " with " << theory << std::endl; + d_theoryTable[theory]->preRegisterTerm(current); + TheoryId typeTheory = Theory::theoryOf(current.getType()); + if (theory != typeTheory) { + Debug("register") << "preregistering " << current << " with " << typeTheory << std::endl; + d_theoryTable[typeTheory]->preRegisterTerm(current); + } + } + } + // Done with this node, remove from the stack + toVisit.pop_back(); + } else { + // Mark that we have added the children + stackHead.children_added = true; + // We need to add the children + for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) { + TNode childNode = *child_it; + if (!childNode.getAttribute(PreRegistered())) { + toVisit.push_back(childNode); } } } } - /* Now register the list of terms in reverse order. Between this - * and the above registration of leaves, this should ensure that - * all subterms in the entire tree were registered in - * reverse-topological order. */ - for(list<TNode>::reverse_iterator i = toReg.rbegin(); - i != toReg.rend(); - ++i) { - - TNode n = *i; - - /* Note that a shared TNode in the DAG rooted at "fact" could - * appear twice on the list, so we have to avoid hitting it - * twice. */ - // FIXME when ExprSets are online, use one of those to avoid - // duplicates in the above? - if(!n.getAttribute(theory::PreRegistered())) { - n.setAttribute(theory::PreRegistered(), true); - theoryOf(n)->preRegisterTerm(n); - } - } - - return top; + return preprocessed; } /* Our goal is to tease out any ITE's sitting under a theory operator. */ @@ -289,9 +240,9 @@ Node TheoryEngine::removeITEs(TNode node) { if(node.getKind() == kind::ITE){ Assert( node.getNumChildren() == 3 ); - TypeNode nodeType = node[1].getType(); + TypeNode nodeType = node.getType(); if(!nodeType.isBoolean()){ - Node skolem = nodeManager->mkVar(node.getType()); + Node skolem = nodeManager->mkVar(nodeType); Node newAssertion = nodeManager->mkNode(kind::ITE, node[0], @@ -299,7 +250,7 @@ Node TheoryEngine::removeITEs(TNode node) { nodeManager->mkNode(kind::EQUAL, skolem, node[2])); nodeManager->setAttribute(node, theory::IteRewriteAttr(), skolem); - Debug("ite") << "removeITEs([" << node.getId() << "," << node << "])" + Debug("ite") << "removeITEs([" << node.getId() << "," << node << "," << nodeType << "])" << "->" << "["<<newAssertion.getId() << "," << newAssertion << "]" << endl; @@ -330,277 +281,6 @@ Node TheoryEngine::removeITEs(TNode node) { } } -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 topLevel) : - d_node(n), - d_theory(thy), - d_topLevel(topLevel), - d_nextChild(0) { - } -}; - -}/* CVC4::theory::rewrite namespace */ -}/* CVC4::theory namespace */ - -Node TheoryEngine::rewrite(TNode in, bool topLevel) { - using theory::rewrite::RewriteStackElement; - - Node noItes = removeITEs(in); - Node out; - - Debug("theory-rewrite") << "removeITEs of: " << in << endl - << " is: " << noItes << endl; - - // descend top-down into the theory rewriters - vector<RewriteStackElement> stack; - stack.push_back(RewriteStackElement(noItes, theoryOf(noItes), topLevel)); - Debug("theory-rewrite") << "TheoryEngine::rewrite() starting at" << endl - << " " << noItes << " " << theoryOf(noItes) - << " " << (topLevel ? "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() ? - (response.needsFullRewriting() ? - " FULL-REWRITING" : " 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.isDone(); - } - } 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; - } - } - } - - // children - Node original = rse.d_node; - bool wasTopLevel = rse.d_topLevel; - Node cached = getPostRewriteCache(original, wasTopLevel); - - if(cached.isNull()) { - unsigned nch = rse.d_nextChild++; - - if(nch == 0 && - rse.d_node.getMetaKind() == kind::metakind::PARAMETERIZED) { - // this is an apply, so we have to push the operator - TNode op = rse.d_node.getOperator(); - Debug("theory-rewrite") << "pushing operator " << op - << " of " << rse.d_node << endl; - rse.d_builder << op; - } - - 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 - } - - // 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); - } - - // 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() ? - (response.needsFullRewriting() ? - " FULL-REWRITING" : " 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.isDone(); - } - if(response.needsFullRewriting()) { - Debug("theory-rewrite") << "full-rewrite requested for node " - << rse.d_node.getId() << ", invoking..." - << endl; - Node n = rewrite(rse.d_node, rse.d_topLevel); - Debug("theory-rewrite") << "full-rewrite finished for node " - << rse.d_node.getId() << ", got node " - << n << " output." << endl; - rse.d_node = n; - done = true; - } - } while(!done); - - /* If extra-checking is on, do _another_ rewrite before putting - * in the cache to make sure they are the same. This is - * especially necessary if a theory post-rewrites something into - * a term of another theory. */ - if(Debug.isOn("extra-checking") && - !Debug.isOn("$extra-checking:inside-rewrite")) { - ScopedDebug d("$extra-checking:inside-rewrite"); - Node rewrittenAgain = rewrite(rse.d_node, rse.d_topLevel); - Assert(rewrittenAgain == rse.d_node, - "\nExtra-checking assumption failed, " - "node is not completely rewritten.\n\n" - "Original : %s\n" - "Rewritten: %s\n" - "Again : %s\n", - original.toString().c_str(), - rse.d_node.toString().c_str(), - rewrittenAgain.toString().c_str()); - } - 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; - } - } - - 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()); - - Debug("theory-rewrite") << "DONE with theory rewriter." << endl; - Debug("theory-rewrite") << "result is:" << endl << out << endl; - - return out; -}/* TheoryEngine::rewrite(TNode in) */ - Node TheoryEngine::getValue(TNode node) { kind::MetaKind metakind = node.getMetaKind(); @@ -617,36 +297,16 @@ Node TheoryEngine::getValue(TNode node) { return theoryOf(node)->getValue(node, this); }/* TheoryEngine::getValue(TNode node) */ - bool TheoryEngine::presolve() { d_theoryOut.d_conflictNode = Node::null(); d_theoryOut.d_propagatedLiterals.clear(); try { - /* - d_builtin->presolve(); - if(!d_theoryOut.d_conflictNode.get().isNull()) { - return true; - } - d_bool->presolve(); - if(!d_theoryOut.d_conflictNode.get().isNull()) { - return true; - } - */ - d_uf->presolve(); - if(!d_theoryOut.d_conflictNode.get().isNull()) { - return true; - } - d_arith->presolve(); - /* - if(!d_theoryOut.d_conflictNode.get().isNull()) { - return true; - } - d_arrays->presolve(); - if(!d_theoryOut.d_conflictNode.get().isNull()) { - return true; - } - d_bv->presolve(); - */ + for(unsigned i = 0; i < THEORY_LAST; ++ i) { + d_theoryTable[i]->presolve(); + if(!d_theoryOut.d_conflictNode.get().isNull()) { + return true; + } + } } catch(const theory::Interrupted&) { Debug("theory") << "TheoryEngine::presolve() => interrupted" << endl; } @@ -656,26 +316,20 @@ bool TheoryEngine::presolve() { void TheoryEngine::notifyRestart() { - /* - d_builtin->notifyRestart(); - d_bool->notifyRestart(); - */ - d_uf->notifyRestart(); - /* - d_arith->notifyRestart(); - d_arrays->notifyRestart(); - d_bv->notifyRestart(); - */ + for(unsigned i = 0; i < THEORY_LAST; ++ i) { + if (d_theoryTable[i]) { + d_theoryTable[i]->notifyRestart(); + } + } } void TheoryEngine::staticLearning(TNode in, NodeBuilder<>& learned) { - d_builtin->staticLearning(in, learned); - d_bool->staticLearning(in, learned); - d_uf->staticLearning(in, learned); - d_arith->staticLearning(in, learned); - d_arrays->staticLearning(in, learned); - d_bv->staticLearning(in, learned); + for(unsigned i = 0; i < THEORY_LAST; ++ i) { + if (d_theoryTable[i]) { + d_theoryTable[i]->staticLearning(in, learned); + } + } } |