summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/theory/arrays/theory_arrays.cpp4
-rw-r--r--src/theory/arrays/theory_arrays.h2
-rw-r--r--src/theory/shared_data.cpp18
-rw-r--r--src/theory/shared_data.h28
-rw-r--r--src/theory/shared_term_manager.cpp131
-rw-r--r--src/theory/shared_term_manager.h60
-rw-r--r--src/theory/theory.h12
-rw-r--r--src/theory/theory_engine.cpp8
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback