From: Dejan Jovanović Date: Fri, 24 Sep 2010 22:38:21 +0000 (+0000) Subject: equality triggers for the equality engine X-Git-Tag: cvc5-1.0.0~8849 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6e59b60947283d864877c2c2dc883e878913a2d8;p=cvc5.git equality triggers for the equality engine fixed order of destruction in smt_engine --- diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index cdb659760..cb97d7f4c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -95,8 +95,8 @@ SmtEngine::~SmtEngine() { shutdown(); - delete d_propEngine; delete d_theoryEngine; + delete d_propEngine; delete d_decisionEngine; } diff --git a/src/theory/bv/equality_engine.cpp b/src/theory/bv/equality_engine.cpp index 8f75f5e86..b88a3cc86 100644 --- a/src/theory/bv/equality_engine.cpp +++ b/src/theory/bv/equality_engine.cpp @@ -2,4 +2,7 @@ using namespace CVC4::theory::bv; -const size_t NodeIdTraits::null = ((size_t)(-1) << (sizeof(size_t)*8 - NodeIdTraits::s_id_bits)) >> (sizeof(size_t)*8 - NodeIdTraits::s_id_bits); +const size_t BitSizeTraits::id_null = (1u << BitSizeTraits::id_bits) - 1; +const size_t BitSizeTraits::trigger_id_null = (1u << BitSizeTraits::trigger_id_bits) - 1; + + diff --git a/src/theory/bv/equality_engine.h b/src/theory/bv/equality_engine.h index 03895a598..9f3064483 100644 --- a/src/theory/bv/equality_engine.h +++ b/src/theory/bv/equality_engine.h @@ -13,13 +13,20 @@ namespace CVC4 { namespace theory { namespace bv { -struct NodeIdTraits { +struct BitSizeTraits { + /** The null id */ - static const size_t null; // Defined in the cpp file (GCC bug) + static const size_t id_null; // Defined in the cpp file (GCC bug) + /** The null trigger id */ + static const size_t trigger_id_null; + /** Number of bits we use for the id */ - static const size_t s_id_bits = 24; + static const size_t id_bits = 24; /** Number of bits we use for the size the equivalence class */ - static const size_t s_size_bits = 16; + static const size_t size_bits = 16; + /** Number of bits we use for the trigger id */ + static const size_t trigger_id_bits = 24; + }; class EqualityNode { @@ -27,22 +34,23 @@ class EqualityNode { public: /** The size of this equivalence class (if it's a representative) */ - size_t d_size : NodeIdTraits::s_size_bits; + size_t d_size : BitSizeTraits::size_bits; /** The id (in the eq-manager) of the representative equality node */ - size_t d_findId : NodeIdTraits::s_id_bits; + size_t d_findId : BitSizeTraits::id_bits; /** The next equality node in this class */ - size_t d_nextId : NodeIdTraits::s_id_bits; + size_t d_nextId : BitSizeTraits::id_bits; public: /** * Creates a new node, which is in a list of it's own. */ - EqualityNode(size_t nodeId = NodeIdTraits::null) + EqualityNode(size_t nodeId = BitSizeTraits::id_null) : d_size(1), d_findId(nodeId), d_nextId(nodeId) {} + /** Initialize the equality node */ inline void init(size_t nodeId) { d_size = 1; d_findId = d_nextId = nodeId; @@ -70,10 +78,8 @@ public: inline void merge(EqualityNode& other) { size_t tmp = d_nextId; d_nextId = other.d_nextId; other.d_nextId = tmp; if (addSize) { - Assert(d_size + other.d_size > d_size); d_size += other.d_size; } else { - Assert(d_size > other.d_size); d_size -= other.d_size; } } @@ -115,11 +121,11 @@ class EqualityEngine { */ struct Equality { /** Left hand side of the equality */ - size_t lhs : NodeIdTraits::s_id_bits; + size_t lhs : BitSizeTraits::id_bits; /** Right hand side of the equality */ - size_t rhs : NodeIdTraits::s_id_bits; + size_t rhs : BitSizeTraits::id_bits; /** Equality constructor */ - Equality(size_t lhs = NodeIdTraits::null, size_t rhs = NodeIdTraits::null) + Equality(size_t lhs = BitSizeTraits::id_null, size_t rhs = BitSizeTraits::id_null) : lhs(lhs), rhs(rhs) {} }; @@ -133,13 +139,13 @@ class EqualityEngine { class EqualityEdge { // The id of the RHS of this equality - size_t d_nodeId : NodeIdTraits::s_id_bits; + size_t d_nodeId : BitSizeTraits::id_bits; // The next edge - size_t d_nextId : NodeIdTraits::s_id_bits; + size_t d_nextId : BitSizeTraits::id_bits; public: - EqualityEdge(size_t nodeId = NodeIdTraits::null, size_t nextId = NodeIdTraits::null) + EqualityEdge(size_t nodeId = BitSizeTraits::id_null, size_t nextId = BitSizeTraits::id_null) : d_nodeId(nodeId), d_nextId(nextId) {} /** Returns the id of the next edge */ @@ -175,7 +181,7 @@ class EqualityEngine { inline size_t getNodeId(TNode node) const; /** Merge the class2 into class1 */ - void merge(EqualityNode& class1, EqualityNode& class2); + void merge(EqualityNode& class1, EqualityNode& class2, std::vector& triggers); /** Undo the mereg of class2 into class1 */ void undoMerge(EqualityNode& class1, EqualityNode& class2, size_t class2Id); @@ -188,25 +194,47 @@ class EqualityEngine { */ struct BfsData { // The current node - size_t nodeId : NodeIdTraits::s_id_bits; + size_t nodeId : BitSizeTraits::id_bits; // The index of the edge we traversed - size_t edgeId : NodeIdTraits::s_id_bits; + size_t edgeId : BitSizeTraits::id_bits; // Index in the queue of the previous node. Shouldn't be too much of them, at most the size // of the biggest equivalence class - size_t previousIndex : NodeIdTraits::s_size_bits; + size_t previousIndex : BitSizeTraits::size_bits; - BfsData(size_t nodeId = NodeIdTraits::null, size_t edgeId = NodeIdTraits::null, size_t prev = 0) + BfsData(size_t nodeId = BitSizeTraits::id_null, size_t edgeId = BitSizeTraits::id_null, size_t prev = 0) : nodeId(nodeId), edgeId(edgeId), previousIndex(prev) {} }; /** - * Trigger that will + * Trigger that will be updated */ struct Trigger { - size_t class1Id : NodeIdTraits::s_id_bits; - size_t class2Id : NodeIdTraits::s_id_bits; + /** The current class id of the LHS of the trigger */ + size_t classId : BitSizeTraits::id_bits; + /** Next trigger for class 1 */ + size_t nextTrigger : BitSizeTraits::id_bits; + + Trigger(size_t classId, size_t nextTrigger) + : classId(classId), nextTrigger(nextTrigger) {} }; + /** + * Vector of triggers (persistent and not-backtrackable). Triggers come in pairs for an + * equality trigger (t1, t2): one at position 2k for t1, and one at position 2k + 1 for t2. When + * updating triggers we always know where the other one is (^1). + */ + std::vector d_equalityTriggers; + + /** + * Trigger lists per node. The begin id changes as we merge, but the end always points to + * the acutal end of the triggers for this node. + */ + std::vector d_nodeTriggers; + + /** + * Adds the trigger with triggerId to the begining of the trigger list of the node with id nodeId. + */ + inline void addTriggerToList(size_t nodeId, size_t triggerId); public: @@ -215,7 +243,10 @@ public: * the owner information. */ EqualityEngine(OwnerClass& owner, context::Context* context) - : d_notify(owner), d_assertedEqualitiesCount(context, 0) {} + : d_notify(owner), d_assertedEqualitiesCount(context, 0) { + Debug("equality") << "EqualityEdge::EqualityEdge(): id_null = " << BitSizeTraits::id_null << + ", trigger_id_null = " << BitSizeTraits::trigger_id_null << std::endl; + } /** * Adds a term to the term database. Returns the internal id of the term. @@ -228,9 +259,9 @@ public: inline bool hasTerm(TNode t) const; /** - * Adds an equality t1 = t2 to the database. + * Adds an equality t1 = t2 to the database. Returns false if any of the triggers failed. */ - void addEquality(TNode t1, TNode t2); + bool addEquality(TNode t1, TNode t2); /** * Returns the representative of the term t. @@ -253,14 +284,14 @@ public: * Adds a notify trigger for equality t1 = t2, i.e. when t1 = t2 the notify will be called with * (t1, t2). */ - void addTrigger(TNode t1, TNode t2); + size_t addTrigger(TNode t1, TNode t2); }; template size_t EqualityEngine::addTerm(TNode t) { - Debug("equality") << "addTerm(" << t << ")" << std::endl; + Debug("equality") << "EqualityEngine::addTerm(" << t << ")" << std::endl; // If term already added, retrurn it's id if (hasTerm(t)) return getNodeId(t); @@ -270,8 +301,10 @@ size_t EqualityEngine::addTerm(TNode t) { d_nodeIds[t] = newId; // Add the node to it's position d_nodes.push_back(t); + // Add the trigger list for this node + d_nodeTriggers.push_back(BitSizeTraits::trigger_id_null); // Add it to the equality graph - d_equalityGraph.push_back(NodeIdTraits::null); + d_equalityGraph.push_back(BitSizeTraits::id_null); // Add the equality node to the nodes if (d_equalityNodes.size() <= newId) { d_equalityNodes.resize(newId + 100); @@ -304,9 +337,9 @@ EqualityNode& EqualityEngine::getEqualityNode(size_t no } template -void EqualityEngine::addEquality(TNode t1, TNode t2) { +bool EqualityEngine::addEquality(TNode t1, TNode t2) { - Debug("equality") << "addEquality(" << t1 << "," << t2 << ")" << std::endl; + Debug("equality") << "EqualityEngine::addEquality(" << t1 << "," << t2 << ")" << std::endl; // Backtrack if necessary backtrack(); @@ -320,7 +353,7 @@ void EqualityEngine::addEquality(TNode t1, TNode t2) { size_t t2classId = getEqualityNode(t2Id).getFind(); // If already the same, we're done - if (t1classId == t2classId) return; + if (t1classId == t2classId) return true; // Get the nodes of the representatives EqualityNode& node1 = getEqualityNode(t1classId); @@ -330,27 +363,37 @@ void EqualityEngine::addEquality(TNode t1, TNode t2) { Assert(node2.getFind() == t2classId); // Depending on the size, merge them + std::vector triggers; if (node1.getSize() < node2.getSize()) { - merge(node2, node1); + merge(node2, node1, triggers); d_assertedEqualities.push_back(Equality(t2classId, t1classId)); } else { - merge(node1, node2); + merge(node1, node2, triggers); d_assertedEqualities.push_back(Equality(t1classId, t2classId)); } // Add the actuall equality to the equality graph addGraphEdge(t1Id, t2Id); - Assert(2*d_assertedEqualities.size() == d_equalityEdges.size()); - // One more equality added d_assertedEqualitiesCount = d_assertedEqualitiesCount + 1; + + Assert(2*d_assertedEqualities.size() == d_equalityEdges.size()); + Assert(d_assertedEqualities.size() == d_assertedEqualitiesCount); + + // Notify the triggers + for (size_t i = 0, i_end = triggers.size(); i < i_end; ++ i) { + // Notify the trigger and exit if it fails + if (!d_notify(triggers[i])) return false; + } + + return true; } template TNode EqualityEngine::getRepresentative(TNode t) const { - Debug("equality") << "getRepresentative(" << t << ")" << std::endl; + Debug("equality") << "EqualityEngine::getRepresentative(" << t << ")" << std::endl; Assert(hasTerm(t)); @@ -358,14 +401,14 @@ TNode EqualityEngine::getRepresentative(TNode t) const const_cast(this)->backtrack(); size_t representativeId = const_cast(this)->getEqualityNode(t).getFind(); - Debug("equality") << "getRepresentative(" << t << ") => " << d_nodes[representativeId] << std::endl; + Debug("equality") << "EqualityEngine::getRepresentative(" << t << ") => " << d_nodes[representativeId] << std::endl; return d_nodes[representativeId]; } template bool EqualityEngine::areEqual(TNode t1, TNode t2) const { - Debug("equality") << "areEqual(" << t1 << "," << t2 << ")" << std::endl; + Debug("equality") << "EqualityEngine::areEqual(" << t1 << "," << t2 << ")" << std::endl; Assert(hasTerm(t1)); Assert(hasTerm(t2)); @@ -375,15 +418,17 @@ bool EqualityEngine::areEqual(TNode t1, TNode t2) const size_t rep1 = const_cast(this)->getEqualityNode(t1).getFind(); size_t rep2 = const_cast(this)->getEqualityNode(t2).getFind(); - Debug("equality") << "areEqual(" << t1 << "," << t2 << ") => " << (rep1 == rep2 ? "true" : "false") << std::endl; + Debug("equality") << "EqualityEngine::areEqual(" << t1 << "," << t2 << ") => " << (rep1 == rep2 ? "true" : "false") << std::endl; return rep1 == rep2; } template -void EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2) { +void EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vector& triggers) { + + Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << ")" << std::endl; - Debug("equality") << "merge(" << class1.getFind() << "," << class2.getFind() << ")" << std::endl; + Assert(triggers.empty()); size_t class1Id = class1.getFind(); size_t class2Id = class2.getFind(); @@ -397,6 +442,26 @@ void EqualityEngine::merge(EqualityNode& class1, Equali // Update it's find to class1 id currentNode.setFind(class1Id); + // Go through the triggers and inform if necessary + size_t currentTrigger = d_nodeTriggers[currentId]; + while (currentTrigger != BitSizeTraits::trigger_id_null) { + Trigger& trigger = d_equalityTriggers[currentTrigger]; + Trigger& otherTrigger = d_equalityTriggers[currentTrigger ^ 1]; + + // If the two are not already in the same class + if (otherTrigger.classId != trigger.classId) { + trigger.classId = class1Id; + // If they became the same, call the trigger + if (otherTrigger.classId == class1Id) { + // Id of the real trigger is half the internal one + triggers.push_back(currentTrigger >> 1); + } + } + + // Go to the next trigger + currentTrigger = trigger.nextTrigger; + } + // Move to the next node currentId = currentNode.getNext(); @@ -409,7 +474,7 @@ void EqualityEngine::merge(EqualityNode& class1, Equali template void EqualityEngine::undoMerge(EqualityNode& class1, EqualityNode& class2, size_t class2Id) { - Debug("equality") << "undoMerge(" << class1.getFind() << "," << class2Id << ")" << std::endl; + Debug("equality") << "EqualityEngine::undoMerge(" << class1.getFind() << "," << class2Id << ")" << std::endl; // Now unmerge the lists (same as merge) class1.merge(class2); @@ -423,6 +488,14 @@ void EqualityEngine::undoMerge(EqualityNode& class1, Eq // Update it's find to class1 id currentNode.setFind(class2Id); + // Go through the trigger list (if any) and undo the class + size_t currentTrigger = d_nodeTriggers[currentId]; + while (currentTrigger != BitSizeTraits::trigger_id_null) { + Trigger& trigger = d_equalityTriggers[currentTrigger]; + trigger.classId = class2Id; + currentTrigger = trigger.nextTrigger; + } + // Move to the next node currentId = currentNode.getNext(); @@ -436,7 +509,7 @@ void EqualityEngine::backtrack() { // If we need to backtrack then do it if (d_assertedEqualitiesCount < d_assertedEqualities.size()) { - Debug("equality") << "backtrack(): nodes" << std::endl; + Debug("equality") << "EqualityEngine::backtrack(): nodes" << std::endl; for (int i = (int)d_assertedEqualities.size() - 1, i_end = (int)d_assertedEqualitiesCount; i >= i_end; --i) { // Get the ids of the merged classes @@ -447,7 +520,7 @@ void EqualityEngine::backtrack() { d_assertedEqualities.resize(d_assertedEqualitiesCount); - Debug("equality") << "backtrack(): edges" << std::endl; + Debug("equality") << "EqualityEngine::backtrack(): edges" << std::endl; for (int i = (int)d_equalityEdges.size() - 2, i_end = (int)(2*d_assertedEqualitiesCount); i >= i_end; i -= 2) { EqualityEdge& edge1 = d_equalityEdges[i]; @@ -463,6 +536,7 @@ void EqualityEngine::backtrack() { template void EqualityEngine::addGraphEdge(size_t t1, size_t t2) { + Debug("equality") << "EqualityEngine::addGraphEdge(" << d_nodes[t1] << "," << d_nodes[t2] << ")" << std::endl; size_t edge = d_equalityEdges.size(); d_equalityEdges.push_back(EqualityEdge(t2, d_equalityGraph[t1])); d_equalityEdges.push_back(EqualityEdge(t1, d_equalityGraph[t2])); @@ -476,7 +550,7 @@ void EqualityEngine::getExplanation(TNode t1, TNode t2, Assert(t1 != t2); Assert(getRepresentative(t1) == getRepresentative(t2)); - Debug("equality") << "getExplanation(" << t1 << "," << t2 << ")" << std::endl; + Debug("equality") << "EqualityEngine::getExplanation(" << t1 << "," << t2 << ")" << std::endl; const_cast(this)->backtrack(); @@ -488,7 +562,7 @@ void EqualityEngine::getExplanation(TNode t1, TNode t2, size_t t2Id = getNodeId(t2); // Find a path from t1 to t2 in the graph (BFS) - bfsQueue.push_back(BfsData(t1Id, NodeIdTraits::null, 0)); + bfsQueue.push_back(BfsData(t1Id, BitSizeTraits::id_null, 0)); size_t currentIndex = 0; while (true) { // There should always be a path, and every node can be visited only once (tree) @@ -498,45 +572,47 @@ void EqualityEngine::getExplanation(TNode t1, TNode t2, BfsData& current = bfsQueue[currentIndex]; size_t currentNode = current.nodeId; - Debug("equality") << "getExplanation(): currentNode: " << currentNode << std::endl; + Debug("equality") << "EqualityEngine::getExplanation(): currentNode = " << d_nodes[currentNode] << std::endl; // Go through the equality edges of this node size_t currentEdge = d_equalityGraph[currentNode]; - while (currentEdge != NodeIdTraits::null) { - Debug("equality") << "getExplanation(): currentEdge: " << currentEdge << std::endl; - + while (currentEdge != BitSizeTraits::id_null) { // Get the edge const EqualityEdge& edge = d_equalityEdges[currentEdge]; - // Did we find the path - if (edge.getNodeId() == t2Id) { + // If not just the backwards edge + if ((currentEdge | 1u) != (current.edgeId | 1u)) { + + Debug("equality") << "EqualityEngine::getExplanation(): currentEdge = (" << d_nodes[currentNode] << "," << d_nodes[edge.getNodeId()] << ")" << std::endl; - Debug("equality") << "getExplanation(): path found: " << std::endl; + // Did we find the path + if (edge.getNodeId() == t2Id) { - // Reconstruct the path - do { - // Get the left and right hand side from the edge - size_t firstEdge = (currentEdge >> 1) << 1; - size_t secondEdge = (currentEdge | 1); - TNode lhs = d_nodes[d_equalityEdges[secondEdge].getNodeId()]; - TNode rhs = d_nodes[d_equalityEdges[firstEdge].getNodeId()]; - // Add the actual equality to the vector - equalities.push_back(lhs.eqNode(rhs)); + Debug("equality") << "EqualityEngine::getExplanation(): path found: " << std::endl; - Debug("equality") << "getExplanation(): adding: " << lhs.eqNode(rhs) << std::endl; + // Reconstruct the path + do { + // Get the left and right hand side from the edge + size_t firstEdge = (currentEdge >> 1) << 1; + size_t secondEdge = (currentEdge | 1); + TNode lhs = d_nodes[d_equalityEdges[secondEdge].getNodeId()]; + TNode rhs = d_nodes[d_equalityEdges[firstEdge].getNodeId()]; + // Add the actual equality to the vector + equalities.push_back(lhs.eqNode(rhs)); - // Go to the previous - currentEdge = bfsQueue[currentIndex].edgeId; - currentIndex = bfsQueue[currentIndex].previousIndex; - } while (currentEdge != NodeIdTraits::null); + Debug("equality") << "EqualityEngine::getExplanation(): adding: " << lhs.eqNode(rhs) << std::endl; + + // Go to the previous + currentEdge = bfsQueue[currentIndex].edgeId; + currentIndex = bfsQueue[currentIndex].previousIndex; + } while (currentEdge != BitSizeTraits::id_null); // Done return; } // Push to the visitation queue if it's not the backward edge - if ((currentEdge | 1) != (current.edgeId | 1)) { bfsQueue.push_back(BfsData(edge.getNodeId(), currentEdge, currentIndex)); } @@ -550,13 +626,38 @@ void EqualityEngine::getExplanation(TNode t1, TNode t2, } template -void EqualityEngine::addTrigger(TNode t1, TNode t2) { +size_t EqualityEngine::addTrigger(TNode t1, TNode t2) { + + Debug("equality") << "EqualityEngine::addTrigger(" << t1 << "," << t2 << ")" << std::endl; + Assert(hasTerm(t1)); + Assert(hasTerm(t2)); + // Get the information about t1 + size_t t1Id = getNodeId(t1); + size_t t1TriggerId = d_nodeTriggers[t1Id]; + size_t t1classId = getEqualityNode(t1Id).getFind(); -} + // Get the information about t2 + size_t t2Id = getNodeId(t2); + size_t t2TriggerId = d_nodeTriggers[t2Id]; + size_t t2classId = getEqualityNode(t2Id).getFind(); + + // Create the triggers + size_t t1NewTriggerId = d_equalityTriggers.size(); + size_t t2NewTriggerId = t1NewTriggerId | 1; + d_equalityTriggers.push_back(Trigger(t1classId, t1TriggerId)); + d_equalityTriggers.push_back(Trigger(t2classId, t2TriggerId)); + // Add the trigger to the trigger graph + d_nodeTriggers[t1Id] = t1NewTriggerId; + d_nodeTriggers[t2Id] = t2NewTriggerId; + Debug("equality") << "EqualityEngine::addTrigger(" << t1 << "," << t2 << ") => " << t1NewTriggerId / 2 << std::endl; + + // Return the global id of the trigger + return t1NewTriggerId / 2; +} } // Namespace bv } // Namespace theory diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index e08c19dbd..f957c4f49 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -14,6 +14,9 @@ void TheoryBV::preRegisterTerm(TNode node) { if (node.getKind() == kind::EQUAL) { d_eqEngine.addTerm(node[0]); d_eqEngine.addTerm(node[1]); + size_t triggerId = d_eqEngine.addTrigger(node[0], node[1]); + Assert(triggerId == d_triggers.size()); + d_triggers.push_back(node); } } @@ -82,24 +85,26 @@ void TheoryBV::check(Effort e) { // Get the assertion TNode assertion = get(); + d_assertions.insert(assertion); Debug("bitvector") << "TheoryBV::check(" << e << "): asserting: " << assertion << std::endl; // Do the right stuff switch (assertion.getKind()) { - case kind::EQUAL: - d_eqEngine.addEquality(assertion[0], assertion[1]); + case kind::EQUAL: { + bool ok = d_eqEngine.addEquality(assertion[0], assertion[1]); + if (!ok) return; break; + } case kind::NOT: { + // We need to check this as the equality trigger might have been true when we made it TNode equality = assertion[0]; if (d_eqEngine.areEqual(equality[0], equality[1])) { vector assertions; d_eqEngine.getExplanation(equality[0], equality[1], assertions); - // We can assume that the explanation is bigger than one node assertions.push_back(assertion); - d_out->conflict(mkAnd(assertions)); - } else { - d_disequalities.push_back(assertion); + d_out->conflict(mkAnd(assertions)); + return; } break; } @@ -107,21 +112,32 @@ void TheoryBV::check(Effort e) { Unhandled(); } } +} - // In full effort go back and check the disequalities - if (true) { - Debug("bitvector") << "TheoryBV::check(" << e << "): checking disequalities" << std::endl; +bool TheoryBV::triggerEquality(size_t triggerId) { + Debug("bitvector") << "TheoryBV::triggerEquality(" << triggerId << ")" << std::endl; + Assert(triggerId < d_triggers.size()); + Debug("bitvector") << "TheoryBV::triggerEquality(" << triggerId << "): " << d_triggers[triggerId] << std::endl; - for (unsigned i = 0; i < d_disequalities.size(); ++ i) { - TNode assertion = d_disequalities[i]; - TNode equality = assertion[0]; - if (d_eqEngine.areEqual(equality[0], equality[1])) { - vector assertions; - d_eqEngine.getExplanation(equality[0], equality[1], assertions); - assertions.push_back(assertion); - // We can assume that the explanation is bigger than one node - d_out->conflict(mkAnd(assertions)); - } - } + TNode equality = d_triggers[triggerId]; + + // If we have just asserted this equality ignore it + if (d_assertions.contains(equality)) return true; + + // If we have a negation asserted, we have a confict + if (d_assertions.contains(equality.notNode())) { + + vector assertions; + d_eqEngine.getExplanation(equality[0], equality[1], assertions); + assertions.push_back(equality.notNode()); + d_out->conflict(mkAnd(assertions)); + + return false; } + + // Otherwise we propagate this equality + d_out->propagate(equality); + + return true; } + diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 912c453b4..b71233797 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -23,7 +23,7 @@ #include "theory/theory.h" #include "context/context.h" -#include "context/cdlist.h" +#include "context/cdset.h" #include "equality_engine.h" namespace CVC4 { @@ -39,6 +39,10 @@ public: public: EqualityNotify(TheoryBV& theoryBV) : d_theoryBV(theoryBV) {} + + bool operator () (size_t triggerId) { + return d_theoryBV.triggerEquality(triggerId); + } }; private: @@ -46,21 +50,33 @@ private: /** Equality reasoning engine */ EqualityEngine d_eqEngine; - /** The disequalities */ - context::CDList d_disequalities; + /** Equality triggers indexed by ids from the equality manager */ + std::vector d_triggers; + + /** The asserted stuff */ + context::CDSet d_assertions; + + /** Called by the equality managere on triggers */ + bool triggerEquality(size_t triggerId); public: TheoryBV(int id, context::Context* c, OutputChannel& out) : - Theory(id, c, out), d_eqEngine(*this, c), d_disequalities(c) { + Theory(id, c, out), d_eqEngine(*this, c), d_assertions(c) { } void preRegisterTerm(TNode n); + void registerTerm(TNode n) { } + void check(Effort e); + void propagate(Effort e) {} + void explain(TNode n, Effort e) { } + RewriteResponse postRewrite(TNode n, bool topLevel); + std::string identify() const { return std::string("TheoryBV"); } };/* class TheoryBV */