It is currently tracking all asserted equalities for simplicity.
Might want to check if this is a performance hit
}
-void TheoryArrays::notifyEq(TNode eq) {
+void TheoryArrays::notifyEq(TNode lhs, TNode rhs) {
Debug("arrays") << "TheoryArrays::notifyEq(): "
- << eq << endl;
+ << lhs << " = " << rhs << endl;
}
}
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) { }
d_size(1),
d_find(this),
d_proofNext(this),
+ d_edgeReversed(false),
d_explainingTheory(NULL),
d_rep(n) {
}
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;
}
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);
parent = current;
current = tmpData;
}
- current->setEquality(equality);
+ current->setEdgeReversed(!reversed);
current->setExplainingTheory(explainingTheory);
current->setProofNext(parent);
}
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;
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
}
-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;
// 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);
}
-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;
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) {
}
+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");
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
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;
}
+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 */
*/
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 */
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.
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;
--- /dev/null
+(benchmark simple_arr
+ :logic QF_AX
+ :status unsat
+ :extrafuns ((a Array))
+ :extrafuns ((i1 Index) (i2 Index) (i3 Index))
+ :formula (not (implies (and (= i1 i2) (= i2 i3)) (= (select a i1) (select a i3))))
+)
# All unit tests
UNIT_TESTS = \
+ theory/shared_term_manager_black \
+ theory/theory_engine_white \
+ theory/theory_black \
+ theory/theory_uf_white \
+ theory/theory_arith_white \
expr/expr_public \
expr/expr_manager_public \
expr/node_white \
context/cdlist_black \
context/cdmap_black \
context/cdmap_white \
- theory/theory_engine_white \
- theory/theory_black \
- theory/theory_uf_white \
- theory/theory_arith_white \
util/assert_white \
util/bitvector_black \
util/configuration_black \
--- /dev/null
+/********************* */
+/*! \file shared_term_manager_black.h
+ ** \verbatim
+ ** Original author: barrett
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Black box testing of CVC4::SharedTermManager.
+ **
+ ** Black box testing of CVC4::SharedTermManager.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include <iostream>
+#include <string>
+#include <deque>
+
+#include "theory/theory.h"
+#include "theory/theory_engine.h"
+#include "theory/theoryof_table.h"
+#include "expr/node.h"
+#include "expr/node_manager.h"
+#include "expr/kind.h"
+#include "context/context.h"
+#include "util/rational.h"
+#include "util/integer.h"
+#include "util/Assert.h"
+
+using namespace CVC4;
+using namespace CVC4::theory;
+using namespace CVC4::expr;
+using namespace CVC4::context;
+using namespace CVC4::kind;
+
+using namespace std;
+
+/**
+ * Test the SharedTermManager.
+ */
+class SharedTermManagerBlack : public CxxTest::TestSuite {
+ Context* d_ctxt;
+
+ NodeManager* d_nm;
+ NodeManagerScope* d_scope;
+ TheoryEngine* d_theoryEngine;
+
+public:
+
+ void setUp() {
+ d_ctxt = new Context;
+
+ d_nm = new NodeManager(d_ctxt);
+ d_scope = new NodeManagerScope(d_nm);
+
+ d_theoryEngine = new TheoryEngine(d_ctxt);
+
+ }
+
+ void tearDown() {
+ delete d_theoryEngine;
+
+ delete d_scope;
+ delete d_nm;
+
+ delete d_ctxt;
+ }
+
+ void testExplanation() {
+ // Example from Barcelogic paper
+ SharedTermManager* stm = d_theoryEngine->getSharedTermManager();
+
+ Node x1 = d_nm->mkVar("x1", d_nm->integerType());
+ Node x2 = d_nm->mkVar("x2", d_nm->integerType());
+ Node x3 = d_nm->mkVar("x3", d_nm->integerType());
+ Node x4 = d_nm->mkVar("x4", d_nm->integerType());
+ Node x5 = d_nm->mkVar("x5", d_nm->integerType());
+ Node x6 = d_nm->mkVar("x6", d_nm->integerType());
+ Node x7 = d_nm->mkVar("x7", d_nm->integerType());
+ Node x8 = d_nm->mkVar("x8", d_nm->integerType());
+ Node x9 = d_nm->mkVar("x9", d_nm->integerType());
+ Node x10 = d_nm->mkVar("x10", d_nm->integerType());
+ Node x11 = d_nm->mkVar("x11", d_nm->integerType());
+ Node x12 = d_nm->mkVar("x12", d_nm->integerType());
+ Node x13 = d_nm->mkVar("x13", d_nm->integerType());
+ Node x14 = d_nm->mkVar("x14", d_nm->integerType());
+
+ Node a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12;
+
+ d_ctxt->push();
+
+ stm->addEq(a1 = d_nm->mkNode(EQUAL, x1, x8));
+ stm->addEq(a2 = d_nm->mkNode(EQUAL, x7, x2));
+ stm->addEq(a3 = d_nm->mkNode(EQUAL, x3, x13));
+ stm->addEq(a4 = d_nm->mkNode(EQUAL, x7, x1));
+ stm->addEq(a5 = d_nm->mkNode(EQUAL, x6, x7));
+ stm->addEq(a6 = d_nm->mkNode(EQUAL, x9, x5));
+ stm->addEq(a7 = d_nm->mkNode(EQUAL, x9, x3));
+ stm->addEq(a8 = d_nm->mkNode(EQUAL, x14, x11));
+ stm->addEq(a9 = d_nm->mkNode(EQUAL, x10, x4));
+ stm->addEq(a10 = d_nm->mkNode(EQUAL, x12, x9));
+ stm->addEq(a11 = d_nm->mkNode(EQUAL, x4, x11));
+ stm->addEq(a12 = d_nm->mkNode(EQUAL, x10, x7));
+
+ Node explanation = stm->explain(d_nm->mkNode(EQUAL, x1, x4));
+
+ TS_ASSERT(explanation.getNumChildren() == 3);
+
+ Node e0 = explanation[0];
+ Node e1 = explanation[1];
+ Node e2 = explanation[2];
+
+ TS_ASSERT(e0 == a4 && e1 == a9 && e2 == a12);
+
+ TS_ASSERT(stm->getRep(x8) == stm->getRep(x14));
+ TS_ASSERT(stm->getRep(x2) != stm->getRep(x12));
+
+ d_ctxt->pop();
+
+ TS_ASSERT(stm->getRep(x8) != stm->getRep(x14));
+
+ d_ctxt->push();
+
+ stm->addEq(a1 = d_nm->mkNode(EQUAL, x1, x8));
+ stm->addEq(a2 = d_nm->mkNode(EQUAL, x8, x2));
+ stm->addEq(a3 = d_nm->mkNode(EQUAL, x2, x3));
+
+ explanation = stm->explain(d_nm->mkNode(EQUAL, x1, x3));
+ TS_ASSERT(explanation.getNumChildren() == 3);
+
+ e0 = explanation[0];
+ e1 = explanation[1];
+ e2 = explanation[2];
+
+ TS_ASSERT(e0 == a1 && e1 == a2 && e2 == a3);
+
+ TS_ASSERT(stm->getRep(x8) == stm->getRep(x2));
+
+ d_ctxt->pop();
+ }
+
+};
projects / cvc5.git / commitdiff