diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2010-07-07 21:55:11 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2010-07-07 21:55:11 +0000 |
commit | 5b4b7727433f06c1788647b08e7da1ee1cc37bc9 (patch) | |
tree | 065c5cf1f4257bf6e406336f0c57367055ffddf9 /src | |
parent | 97eb2d77fddb9c690cc2ebc2caff98d62467b671 (diff) |
Shared term manager tested and working
It is currently tracking all asserted equalities for simplicity.
Might want to check if this is a performance hit
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 4 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 2 | ||||
-rw-r--r-- | src/theory/shared_data.cpp | 18 | ||||
-rw-r--r-- | src/theory/shared_data.h | 28 | ||||
-rw-r--r-- | src/theory/shared_term_manager.cpp | 131 | ||||
-rw-r--r-- | src/theory/shared_term_manager.h | 60 | ||||
-rw-r--r-- | src/theory/theory.h | 12 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 8 |
8 files changed, 206 insertions, 57 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index b84b1e507..8b5f7d3e7 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -45,9 +45,9 @@ void TheoryArrays::addSharedTerm(TNode t) { } -void TheoryArrays::notifyEq(TNode eq) { +void TheoryArrays::notifyEq(TNode lhs, TNode rhs) { Debug("arrays") << "TheoryArrays::notifyEq(): " - << eq << endl; + << lhs << " = " << rhs << endl; } diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 3cb050287..cb738d085 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -49,7 +49,7 @@ public: } void addSharedTerm(TNode t); - void notifyEq(TNode eq); + void notifyEq(TNode lhs, TNode rhs); void check(Effort e); void propagate(Effort e) { } void explain(TNode n, Effort e) { } diff --git a/src/theory/shared_data.cpp b/src/theory/shared_data.cpp index 7a8970c29..50e916832 100644 --- a/src/theory/shared_data.cpp +++ b/src/theory/shared_data.cpp @@ -33,6 +33,7 @@ SharedData::SharedData(Context * context, TNode n, uint64_t theories) : d_size(1), d_find(this), d_proofNext(this), + d_edgeReversed(false), d_explainingTheory(NULL), d_rep(n) { } @@ -49,7 +50,7 @@ void SharedData::restore(ContextObj* pContextObj) { d_size = data->d_size; d_find = data->d_find; d_proofNext = data->d_proofNext; - d_equality = data->d_equality; + d_edgeReversed = data->d_edgeReversed; d_explainingTheory = data->d_explainingTheory; d_rep = data->d_rep; } @@ -60,20 +61,23 @@ void SharedData::reverseEdges() { SharedData* parent = this; SharedData* current = d_proofNext; - Node equality = d_equality; + bool reversed = d_edgeReversed; Theory* explainingTheory = d_explainingTheory; makeCurrent(); + + // Make this the proof root d_proofNext = this; - Node tmpNode; + // Reverse the edges from here to the former root + bool tmpReversed; Theory* tmpTheory; SharedData* tmpData; while (!current->isProofRoot()) { - tmpNode = current->getEquality(); - current->setEquality(equality); - equality = tmpNode; + tmpReversed = current->getEdgeReversed(); + current->setEdgeReversed(!reversed); + reversed = tmpReversed; tmpTheory = current->getExplainingTheory(); current->setExplainingTheory(explainingTheory); @@ -84,7 +88,7 @@ void SharedData::reverseEdges() { parent = current; current = tmpData; } - current->setEquality(equality); + current->setEdgeReversed(!reversed); current->setExplainingTheory(explainingTheory); current->setProofNext(parent); } diff --git a/src/theory/shared_data.h b/src/theory/shared_data.h index 64b7f5ab1..0b21eedae 100644 --- a/src/theory/shared_data.h +++ b/src/theory/shared_data.h @@ -72,13 +72,15 @@ private: SharedData* d_proofNext; /** - * The equality that justifies this node being equal to - * the node at d_proofNext. Not valid if this is proof root. + * In order to precisely reconstruct the equality that justifies this node + * being equal to the node at d_proofNext, we need to know whether this edge + * has been switched. Value is meaningless at the proof root. */ - Node d_equality; + bool d_edgeReversed; /** - * The theory that can explain d_equality. Not valid if this is proof root. + * The theory that can explain the equality of this node and the node at + * d_proofNext. Not valid if this is proof root. */ theory::Theory* d_explainingTheory; @@ -157,14 +159,24 @@ public: void setProofNext(SharedData* pData) { makeCurrent(); d_proofNext = pData; } /** - * Get the equality associated with the link in the proof tree. + * Get the edge reversed property of this node */ - Node getEquality() const { return d_equality; } + bool getEdgeReversed() const { return d_edgeReversed; } /** - * Set the equality associated with the link in the proof tree. + * Set the edge reversed flag to value */ - void setEquality(TNode eq) { makeCurrent(); d_equality = eq; } + void setEdgeReversed(bool value) { makeCurrent(); d_edgeReversed = value; } + + /** + * Get the original equality that created the link from this node to the next + * proof node. + */ + Node getEquality() const { + return d_edgeReversed + ? NodeManager::currentNM()->mkNode(kind::EQUAL, d_proofNext->getRep(), d_rep) + : NodeManager::currentNM()->mkNode(kind::EQUAL, d_rep, d_proofNext->getRep()); + } /** * Get the explaining theory diff --git a/src/theory/shared_term_manager.cpp b/src/theory/shared_term_manager.cpp index 55087ecbd..564fb776f 100644 --- a/src/theory/shared_term_manager.cpp +++ b/src/theory/shared_term_manager.cpp @@ -31,11 +31,16 @@ SharedTermManager::SharedTermManager(TheoryEngine* engine, } -SharedData* SharedTermManager::find(SharedData* pData) { +SharedData* SharedTermManager::find(SharedData* pData) const { + // Check if pData is the representative SharedData* next = pData->getFind(); if (next == pData) return pData; + + // Check if its successor is the representative SharedData* nextNext = next->getFind(); if (nextNext == next) return next; + + // Otherwise, recurse and do find path-compression next = find(nextNext); pData->setFind(next); return next; @@ -59,23 +64,49 @@ void SharedTermManager::addTerm(TNode n, Theory* parent, Theory* child) { // theory id uint64_t parentTag = (1 << parent->getId()); uint64_t childTag = (1 << child->getId()); - uint64_t newTags = parentTag | childTag; + uint64_t bothTags = parentTag | childTag; + + // Create or update the SharedData for n SharedData* pData; if(n.getAttribute(SharedAttr(), pData)) { // The attribute already exists, just update it if necessary uint64_t tags = pData->getTheories(); - newTags |= tags; + uint64_t newTags = tags | bothTags; if (tags == newTags) return; + + // Get the equivalence class representative -- if this is different from + // the current node, then we will need to notify the theories of that and + // update the theory tags on the representative node + SharedData* pDataFind = find(pData); + + // Notify parent theory if necessary if (!(tags & parentTag)) { parent->addSharedTerm(n); + if (pData != pDataFind) { + parent->notifyEq(n, pDataFind->getRep()); + } } + + // Notify child theory if necessary if (!(tags & childTag)) { child->addSharedTerm(n); + if (pData != pDataFind) { + child->notifyEq(n, pDataFind->getRep()); + } } + + // Update theory tags pData->setTheories(newTags); + if (pData != pDataFind) { + tags = pDataFind->getTheories(); + newTags = tags | bothTags; + if (tags != newTags) { + pDataFind->setTheories(newTags); + } + } } else { // The attribute does not exist, so it is created and set - pData = new (true) SharedData(d_context, n, newTags); + pData = new (true) SharedData(d_context, n, bothTags); n.setAttribute(SharedAttr(), pData); parent->addSharedTerm(n); child->addSharedTerm(n); @@ -83,22 +114,35 @@ void SharedTermManager::addTerm(TNode n, Theory* parent, Theory* child) { } -void SharedTermManager::addEq(Theory* thReason, TNode eq) { - Assert(eq.getKind() == kind::EQUAL && - eq[0].hasAttribute(SharedAttr()) && eq[1].hasAttribute(SharedAttr()), +void SharedTermManager::addEq(TNode eq, Theory* thReason) { + Assert(eq.getKind() == kind::EQUAL, "SharedTermManager::addEq precondition violated"); TNode x = eq[0]; TNode y = eq[1]; - SharedData* pDataX = x.getAttribute(SharedAttr()); - SharedData* pDataY = y.getAttribute(SharedAttr()); + SharedData* pDataX; + SharedData* pDataY; + + // Grab the SharedData for each side of the equality, create if necessary + if(!x.getAttribute(SharedAttr(), pDataX)) { + pDataX = new (true) SharedData(d_context, x, 0); + x.setAttribute(SharedAttr(), pDataX); + } + if(!y.getAttribute(SharedAttr(), pDataY)) { + pDataY = new (true) SharedData(d_context, y, 0); + y.setAttribute(SharedAttr(), pDataY); + } + // Get the representatives SharedData* pDataXX = find(pDataX); SharedData* pDataYY = find(pDataY); + // If already in the same equivalence class, nothing to do if(pDataXX == pDataYY) return; + // Make sure we reverse the edges in the smaller tree + bool switched = false; if(pDataXX->getSize() > pDataYY->getSize()) { SharedData* tmp = pDataXX; pDataXX = pDataYY; @@ -107,17 +151,27 @@ void SharedTermManager::addEq(Theory* thReason, TNode eq) { tmp = pDataX; pDataX = pDataY; pDataY = tmp; + + switched = true; } - pDataX->reverseEdges(); - pDataX->setEquality(eq); + // Reverse the edges in the left proof tree and link the two trees + if(!pDataX->isProofRoot()) { + pDataX->reverseEdges(); + } + pDataX->setEdgeReversed(switched); pDataX->setExplainingTheory(thReason); pDataX->setProofNext(pDataY); + // Set the equivalence class representative for the left node to be the right node pDataXX->setFind(pDataYY); pDataYY->setSize(pDataYY->getSize() + pDataXX->getSize()); + + // Update the theory tags for the new representative uint64_t tags = pDataXX->getTheories(); pDataYY->setTheories(pDataYY->getTheories() | tags); + + // Notify the theories that care about the left node int id = 0; while (tags != 0) { if (tags & 1) { @@ -129,8 +183,29 @@ void SharedTermManager::addEq(Theory* thReason, TNode eq) { } +void SharedTermManager::collectExplanations(SharedData* pData, set<Node>& s) const { + Theory* expTh = pData->getExplainingTheory(); + if(expTh == NULL) { + // This equality is directly from SAT, no need to ask a theory for an explanation + s.insert(pData->getEquality()); + } + else { + // This equality was sent by a theory - ask the theory for the explanation + Node n = d_engine->getExplanation(pData->getEquality(), expTh); + if(n.getKind() == kind::AND) { + for (Node::iterator it = n.begin(), iend = n.end(); it != iend; ++it) { + s.insert(*it); + } + } + else { + s.insert(n); + } + } +} + + // Explain this equality -Node SharedTermManager::explain(TNode eq) { +Node SharedTermManager::explain(TNode eq) const { Assert(eq.getKind() == kind::EQUAL && eq[0].hasAttribute(SharedAttr()) && eq[1].hasAttribute(SharedAttr()), "SharedTermManager::explain precondition violated"); @@ -138,14 +213,15 @@ Node SharedTermManager::explain(TNode eq) { TNode x = eq[0]; TNode y = eq[1]; + // Get the SharedData for both sides of the equality SharedData* pDataX = x.getAttribute(SharedAttr()); SharedData* pDataY = y.getAttribute(SharedAttr()); Assert(find(pDataX) == find(pDataY), "invalid equality input to SharedTermManager::explain"); + // Find the path between the two nodes and build up the explanation std::set<Node> s; - Node n; SharedData* tmp = pDataX; // Check to see if Y is on path from X to root @@ -155,39 +231,27 @@ Node SharedTermManager::explain(TNode eq) { if (tmp == pDataY) { // Y is on path from X to root, just traverse that path while (pDataX != pDataY) { - n = d_engine->getExplanation(pDataX->getEquality(), - pDataX->getExplainingTheory()); - for (Node::iterator it = n.begin(), iend = n.end(); it != iend; ++it) { - s.insert(*it); - } + collectExplanations(pDataX, s); pDataX = pDataX->getProofNext(); } } else { // Y is not on path from X to root, so traverse from Y to root instead while (!pDataY->isProofRoot() && pDataX != pDataY) { - n = d_engine->getExplanation(pDataY->getEquality(), - pDataY->getExplainingTheory()); - for (Node::iterator it = n.begin(), iend = n.end(); it != iend; ++it) { - s.insert(*it); - } + collectExplanations(pDataY, s); pDataY = pDataY->getProofNext(); } } if (pDataX != pDataY) { // X and Y are on different branches - have to traverse both while (!pDataX->isProofRoot()) { - n = d_engine->getExplanation(pDataX->getEquality(), - pDataX->getExplainingTheory()); - for (Node::iterator it = n.begin(), iend = n.end(); it != iend; ++it) { - s.insert(*it); - } + collectExplanations(pDataX, s); pDataX = pDataX->getProofNext(); } } // Build explanation from s - NodeBuilder<kind::AND> nb; + NodeBuilder<> nb(kind::AND); set<Node>::iterator it = s.begin(), iend = s.end(); for (; it != iend; ++it) { nb << *it; @@ -196,4 +260,13 @@ Node SharedTermManager::explain(TNode eq) { } +Node SharedTermManager::getRep(TNode n) const { + Assert(n.hasAttribute(SharedAttr()), + "SharedTermManager::getRep precondition violated"); + + SharedData* pData = n.getAttribute(SharedAttr()); + return find(pData)->getRep(); +} + + }/* CVC4 namespace */ diff --git a/src/theory/shared_term_manager.h b/src/theory/shared_term_manager.h index e6a58cdc9..8b5567e4e 100644 --- a/src/theory/shared_term_manager.h +++ b/src/theory/shared_term_manager.h @@ -39,25 +39,77 @@ namespace theory { */ class SharedTermManager { + /** + * Pointer back to theory engine + */ TheoryEngine* d_engine; + /** + * Pointer to context + */ context::Context* d_context; + /** + * List of all theories indexed by theory id (built by calls to registerTheory) + */ std::vector<theory::Theory*> d_theories; - SharedData* find(SharedData* pData); + /** + * Private method to find equivalence class representative in union-find data + * structure. + */ + SharedData* find(SharedData* pData) const; + + /** + * Helper function for explain: add all reasons for equality at pData to set s + */ + void collectExplanations(SharedData* pData, std::set<Node>& s) const; public: + /** + * Constructor + */ SharedTermManager(TheoryEngine* engine, context::Context* context); + /** + * Should be called once for each theory at setup time + */ void registerTheory(theory::Theory* th); + /** + * Called by theory engine to indicate that node n is shared by theories + * parent and child. + */ void addTerm(TNode n, theory::Theory* parent, theory::Theory* child); - void addEq(theory::Theory* thReason, TNode eq); - - Node explain(TNode eq); + /** + * Called by theory engine or theories to notify the shared term manager that + * two terms are equal. + * + * @param eq the equality between shared terms + * @param thReason the theory that knows why, NULL means it's a SAT assertion + */ + void addEq(TNode eq, theory::Theory* thReason = NULL); + + /** + * Called by theory engine or theories to notify the shared term manager that + * two terms are disequal. + * + * @param eq the equality between shared terms whose negation now holds + * @param thReason the theory that knows why, NULL means it's a SAT assertion + */ + void addDiseq(TNode eq, theory::Theory* thReason = NULL) { } + + /** + * Get an explanation for an equality known by the SharedTermManager + */ + Node explain(TNode eq) const; + + /** + * Get the representative node in the equivalence class containing n + */ + Node getRep(TNode n) const; };/* class SharedTermManager */ diff --git a/src/theory/theory.h b/src/theory/theory.h index 6da47fbd8..64a3b8f06 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -358,15 +358,15 @@ public: virtual void addSharedTerm(TNode n) { } /** - * This method is called by the shared term manager when a shared term t + * This method is called by the shared term manager when a shared term lhs * which this theory cares about (either because it received a previous - * addSharedTerm call with t or because it received a previous notifyEq call - * with t as the second argument) becomes equal to another shared term u. + * addSharedTerm call with lhs or because it received a previous notifyEq call + * with lhs as the second argument) becomes equal to another shared term rhs. * This call also serves as notice to the theory that the shared term manager - * now considers u the representative for this equivalence class of shared - * terms, so future notifications for this class will be based on u not t. + * now considers rhs the representative for this equivalence class of shared + * terms, so future notifications for this class will be based on rhs not lhs. */ - virtual void notifyEq(TNode t, TNode u) { } + virtual void notifyEq(TNode lhs, TNode rhs) { } /** * Check the current assignment's consistency. diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index d16d80090..4fae94254 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -46,6 +46,14 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) { if (fact.getKind() == kind::NOT) { // No need to register negations - only atoms fact = fact[0]; +// FIXME: In future, might want to track disequalities in shared term manager +// if (fact.getKind() == kind::EQUAL) { +// d_engine->getSharedTermManager()->addDiseq(fact); +// } + } + else if (fact.getKind() == kind::EQUAL) { + // Automatically track all asserted equalities in the shared term manager + d_engine->getSharedTermManager()->addEq(fact); } if(! fact.getAttribute(RegisteredAttr())) { std::list<TNode> toReg; |