From 01002e4b876c53661aaa2f3b3df9680e1d8e98d7 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Thu, 7 Jun 2012 22:19:53 +0000 Subject: [PATCH] fixing the wrong results. arrays equality adaptor had a missing case when propagating disequalities between shared terms. --- src/theory/arrays/theory_arrays.h | 13 ++- src/theory/uf/equality_engine.cpp | 113 ++++++++++++++---------- src/theory/uf/equality_engine.h | 3 + test/regress/regress0/aufbv/Makefile.am | 5 +- 4 files changed, 81 insertions(+), 53 deletions(-) diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 6592e86cf..3ae0146c1 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -243,7 +243,7 @@ class TheoryArrays : public Theory { } bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { - Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyTriggerTermEquality(" << t1 << ", " << t2 << ")" << std::endl; + Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyTriggerTermEquality(" << t1 << ", " << t2 << ", " << (value ? "true" : "false") << ")" << std::endl; if (value) { if (t1.getType().isArray()) { d_arrays.mergeArrays(t1, t2); @@ -253,9 +253,16 @@ class TheoryArrays : public Theory { } // Propagate equality between shared terms Node equality = Rewriter::rewriteEquality(theory::THEORY_UF, t1.eqNode(t2)); - d_arrays.propagate(equality); + return d_arrays.propagate(equality); + } else { + if (t1.getType().isArray()) { + if (!d_arrays.isShared(t1) || !d_arrays.isShared(t2)) { + return true; + } + } + Node equality = Rewriter::rewriteEquality(theory::THEORY_UF, t1.eqNode(t2)); + return d_arrays.propagate(equality.notNode()); } - // TODO: implement negation propagation return true; } diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index c5ccaaeea..1f45b7827 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -109,17 +109,18 @@ EqualityEngine::EqualityEngine(EqualityEngineNotify& notify, context::Context* c , d_triggerDatabaseSize(context, 0) , d_triggerTermSetUpdatesSize(context, 0) , d_deducedDisequalitiesSize(context, 0) +, d_name(name) { init(); } void EqualityEngine::enqueue(const MergeCandidate& candidate) { - Debug("equality") << "EqualityEngine::enqueue(" << d_nodes[candidate.t1Id] << ", " << d_nodes[candidate.t2Id] << ", " << candidate.type << ")" << std::endl; + Debug("equality") << d_name << "::eq::enqueue(" << d_nodes[candidate.t1Id] << ", " << d_nodes[candidate.t2Id] << ", " << candidate.type << ")" << std::endl; d_propagationQueue.push(candidate); } EqualityNodeId EqualityEngine::newApplicationNode(TNode original, EqualityNodeId t1, EqualityNodeId t2, bool isEquality) { - Debug("equality") << "EqualityEngine::newApplicationNode(" << original << ", " << t1 << ", " << t2 << ")" << std::endl; + Debug("equality") << d_name << "::eq::newApplicationNode(" << original << ", " << t1 << ", " << t2 << ")" << std::endl; ++ d_stats.functionTermsCount; @@ -138,13 +139,13 @@ EqualityNodeId EqualityEngine::newApplicationNode(TNode original, EqualityNodeId ApplicationIdsMap::iterator find = d_applicationLookup.find(funNormalized); if (find == d_applicationLookup.end()) { // When we backtrack, if the lookup is not there anymore, we'll add it again - Debug("equality") << "EqualityEngine::newApplicationNode(" << original << ", " << t1 << ", " << t2 << "): no lookup, setting up" << std::endl; + Debug("equality") << d_name << "::eq::newApplicationNode(" << original << ", " << t1 << ", " << t2 << "): no lookup, setting up" << std::endl; // Mark the normalization to the lookup storeApplicationLookup(funNormalized, funId); // If an equality, we do some extra reasoning if (isEquality && d_isConstant[t1ClassId] && d_isConstant[t2ClassId]) { if (t1ClassId != t2ClassId) { - Debug("equality") << "EqualityEngine::newApplicationNode(" << original << ", " << t1 << ", " << t2 << "): got constants" << std::endl; + Debug("equality") << d_name << "::eq::newApplicationNode(" << original << ", " << t1 << ", " << t2 << "): got constants" << std::endl; Assert(d_nodes[funId].getKind() == kind::EQUAL); enqueue(MergeCandidate(funId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null())); // Also enqueue the symmetric one @@ -158,23 +159,25 @@ EqualityNodeId EqualityEngine::newApplicationNode(TNode original, EqualityNodeId } } else { // If it's there, we need to merge these two - Debug("equality") << "EqualityEngine::newApplicationNode(" << original << ", " << t1 << ", " << t2 << "): lookup exists, adding to queue" << std::endl; + Debug("equality") << d_name << "::eq::newApplicationNode(" << original << ", " << t1 << ", " << t2 << "): lookup exists, adding to queue" << std::endl; enqueue(MergeCandidate(funId, find->second, MERGED_THROUGH_CONGRUENCE, TNode::null())); } // Add to the use lists + Debug("equality") << d_name << "::eq::newApplicationNode(" << original << ", " << t1 << ", " << t2 << "): adding " << original << " to the uselist of " << d_nodes[t1] << std::endl; d_equalityNodes[t1].usedIn(funId, d_useListNodes); + Debug("equality") << d_name << "::eq::newApplicationNode(" << original << ", " << t1 << ", " << t2 << "): adding " << original << " to the uselist of " << d_nodes[t2] << std::endl; d_equalityNodes[t2].usedIn(funId, d_useListNodes); // Return the new id - Debug("equality") << "EqualityEngine::newApplicationNode(" << original << ", " << t1 << ", " << t2 << ") => " << funId << std::endl; + Debug("equality") << d_name << "::eq::newApplicationNode(" << original << ", " << t1 << ", " << t2 << ") => " << funId << std::endl; return funId; } EqualityNodeId EqualityEngine::newNode(TNode node) { - Debug("equality") << "EqualityEngine::newNode(" << node << ")" << std::endl; + Debug("equality") << d_name << "::eq::newNode(" << node << ")" << std::endl; ++ d_stats.termsCount; @@ -201,18 +204,18 @@ EqualityNodeId EqualityEngine::newNode(TNode node) { // Increase the counters d_nodesCount = d_nodesCount + 1; - Debug("equality") << "EqualityEngine::newNode(" << node << ") => " << newId << std::endl; + Debug("equality") << d_name << "::eq::newNode(" << node << ") => " << newId << std::endl; return newId; } void EqualityEngine::addTerm(TNode t) { - Debug("equality") << "EqualityEngine::addTerm(" << t << ")" << std::endl; + Debug("equality") << d_name << "::eq::addTerm(" << t << ")" << std::endl; // If there already, we're done if (hasTerm(t)) { - Debug("equality") << "EqualityEngine::addTerm(" << t << "): already there" << std::endl; + Debug("equality") << d_name << "::eq::addTerm(" << t << "): already there" << std::endl; return; } @@ -265,7 +268,7 @@ void EqualityEngine::addTerm(TNode t) { propagate(); - Debug("equality") << "EqualityEngine::addTerm(" << t << ") => " << result << std::endl; + Debug("equality") << d_name << "::eq::addTerm(" << t << ") => " << result << std::endl; } bool EqualityEngine::hasTerm(TNode t) const { @@ -297,7 +300,7 @@ const EqualityNode& EqualityEngine::getEqualityNode(EqualityNodeId nodeId) const void EqualityEngine::assertEqualityInternal(TNode t1, TNode t2, TNode reason) { - Debug("equality") << "EqualityEngine::addEqualityInternal(" << t1 << "," << t2 << ")" << std::endl; + Debug("equality") << d_name << "::eq::addEqualityInternal(" << t1 << "," << t2 << ")" << std::endl; if (d_done) { return; @@ -314,14 +317,14 @@ void EqualityEngine::assertEqualityInternal(TNode t1, TNode t2, TNode reason) { } void EqualityEngine::assertPredicate(TNode t, bool polarity, TNode reason) { - Debug("equality") << "EqualityEngine::addPredicate(" << t << "," << (polarity ? "true" : "false") << ")" << std::endl; + Debug("equality") << d_name << "::eq::addPredicate(" << t << "," << (polarity ? "true" : "false") << ")" << std::endl; Assert(t.getKind() != kind::EQUAL, "Use assertEquality instead"); assertEqualityInternal(t, polarity ? d_true : d_false, reason); propagate(); } void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason) { - Debug("equality") << "EqualityEngine::addEquality(" << eq << "," << (polarity ? "true" : "false") << std::endl; + Debug("equality") << d_name << "::eq::addEquality(" << eq << "," << (polarity ? "true" : "false") << ")" << std::endl; if (polarity) { // If two terms are already equal, don't assert anything if (hasTerm(eq[0]) && hasTerm(eq[1]) && areEqual(eq[0], eq[1])) { @@ -339,6 +342,8 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason) { return; } + Debug("equality::trigger") << d_name << "::eq::addEquality(" << eq << "," << (polarity ? "true" : "false") << ")" << std::endl; + assertEqualityInternal(eq, d_false, reason); propagate(); assertEqualityInternal(eq[1].eqNode(eq[0]), d_false, reason); @@ -362,6 +367,7 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason) { TriggerTermSetRef aTriggerRef = d_nodeIndividualTrigger[aClassId]; TriggerTermSetRef bTriggerRef = d_nodeIndividualTrigger[bClassId]; if (aTriggerRef != +null_set_id && bTriggerRef != +null_set_id) { + Debug("equality::trigger") << d_name << "::eq::addEquality(" << eq << "," << (polarity ? "true" : "false") << ": have triggers" << std::endl; // The sets of trigger terms TriggerTermSet& aTriggerTerms = getTriggerTermSet(aTriggerRef); TriggerTermSet& bTriggerTerms = getTriggerTermSet(bTriggerRef); @@ -389,6 +395,7 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason) { // We notify even if the it's already been sent (they are not // disequal at assertion, and we need to notify for each tag) + Debug("equality::trigger") << d_name << "::eq::addEquality(" << eq << "," << (polarity ? "true" : "false") << ": notifying " << aTag << " for " << d_nodes[aSharedId] << " != " << d_nodes[bSharedId] << std::endl; if (!d_notify.eqNotifyTriggerTermEquality(aTag, d_nodes[aSharedId], d_nodes[bSharedId], false)) { break; } @@ -402,16 +409,16 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason) { } TNode EqualityEngine::getRepresentative(TNode t) const { - Debug("equality::internal") << "EqualityEngine::getRepresentative(" << t << ")" << std::endl; + Debug("equality::internal") << d_name << "::eq::getRepresentative(" << t << ")" << std::endl; Assert(hasTerm(t)); EqualityNodeId representativeId = getEqualityNode(t).getFind(); - Debug("equality::internal") << "EqualityEngine::getRepresentative(" << t << ") => " << d_nodes[representativeId] << std::endl; + Debug("equality::internal") << d_name << "::eq::getRepresentative(" << t << ") => " << d_nodes[representativeId] << std::endl; return d_nodes[representativeId]; } bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vector& triggersFired) { - Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << ")" << std::endl; + Debug("equality") << d_name << "::eq::merge(" << class1.getFind() << "," << class2.getFind() << ")" << std::endl; Assert(triggersFired.empty()); @@ -448,14 +455,14 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect } // Update class2 representative information - Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): updating class " << class2Id << std::endl; + Debug("equality") << d_name << "::eq::merge(" << class1.getFind() << "," << class2.getFind() << "): updating class " << class2Id << std::endl; EqualityNodeId currentId = class2Id; do { // Get the current node EqualityNode& currentNode = getEqualityNode(currentId); // Update it's find to class1 id - Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): " << currentId << "->" << class1Id << std::endl; + Debug("equality") << d_name << "::eq::merge(" << class1.getFind() << "," << class2.getFind() << "): " << currentId << "->" << class1Id << std::endl; currentNode.setFind(class1Id); // Go through the triggers and inform if necessary @@ -486,11 +493,11 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect // Update class2 table lookup and information if not a boolean // since booleans can't be in an application if (!d_isBoolean[class2Id]) { - Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): updating lookups of " << class2Id << std::endl; + Debug("equality") << d_name << "::eq::merge(" << class1.getFind() << "," << class2.getFind() << "): updating lookups of " << class2Id << std::endl; do { // Get the current node EqualityNode& currentNode = getEqualityNode(currentId); - Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): updating lookups of node " << currentId << std::endl; + Debug("equality") << d_name << "::eq::merge(" << class1.getFind() << "," << class2.getFind() << "): updating lookups of node " << currentId << std::endl; // Go through the uselist and check for congruences UseListNodeId currentUseId = currentNode.getUseList(); @@ -499,7 +506,7 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect UseListNode& useNode = d_useListNodes[currentUseId]; // Get the function application EqualityNodeId funId = useNode.getApplicationId(); - Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): " << d_nodes[currentId] << " in " << d_nodes[funId] << std::endl; + Debug("equality") << d_name << "::eq::merge(" << class1.getFind() << "," << class2.getFind() << "): " << d_nodes[currentId] << " in " << d_nodes[funId] << std::endl; const FunctionApplication& fun = d_applications[useNode.getApplicationId()].normalized; // Check if there is an application with find arguments EqualityNodeId aNormalized = getEqualityNode(fun.a).getFind(); @@ -649,14 +656,14 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect void EqualityEngine::undoMerge(EqualityNode& class1, EqualityNode& class2, EqualityNodeId class2Id) { - Debug("equality") << "EqualityEngine::undoMerge(" << class1.getFind() << "," << class2Id << ")" << std::endl; + Debug("equality") << d_name << "::eq::undoMerge(" << class1.getFind() << "," << class2Id << ")" << std::endl; // Now unmerge the lists (same as merge) class1.merge(class2); // Update class2 representative information EqualityNodeId currentId = class2Id; - Debug("equality") << "EqualityEngine::undoMerge(" << class1.getFind() << "," << class2Id << "): undoing representative info" << std::endl; + Debug("equality") << d_name << "::eq::undoMerge(" << class1.getFind() << "," << class2Id << "): undoing representative info" << std::endl; do { // Get the current node EqualityNode& currentNode = getEqualityNode(currentId); @@ -691,7 +698,7 @@ void EqualityEngine::backtrack() { d_propagationQueue.pop(); } - Debug("equality") << "EqualityEngine::backtrack(): nodes" << std::endl; + Debug("equality") << d_name << "::eq::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 @@ -702,7 +709,7 @@ void EqualityEngine::backtrack() { d_assertedEqualities.resize(d_assertedEqualitiesCount); - Debug("equality") << "EqualityEngine::backtrack(): edges" << std::endl; + Debug("equality") << d_name << "::eq::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]; @@ -745,7 +752,7 @@ void EqualityEngine::backtrack() { // Go down the nodes, check the application nodes and remove them from use-lists for(int i = d_nodes.size() - 1, i_end = (int)d_nodesCount; i >= i_end; -- i) { // Remove from the node -> id map - Debug("equality") << "EqualityEngine::backtrack(): removing node " << d_nodes[i] << std::endl; + Debug("equality") << d_name << "::eq::backtrack(): removing node " << d_nodes[i] << std::endl; d_nodeIds.erase(d_nodes[i]); const FunctionApplication& app = d_applications[i].original; @@ -784,7 +791,7 @@ void EqualityEngine::backtrack() { } void EqualityEngine::addGraphEdge(EqualityNodeId t1, EqualityNodeId t2, MergeReasonType type, TNode reason) { - Debug("equality") << "EqualityEngine::addGraphEdge(" << d_nodes[t1] << "," << d_nodes[t2] << "," << reason << ")" << std::endl; + Debug("equality") << d_name << "::eq::addGraphEdge(" << d_nodes[t1] << "," << d_nodes[t2] << "," << reason << ")" << std::endl; EqualityEdgeId edge = d_equalityEdges.size(); d_equalityEdges.push_back(EqualityEdge(t2, d_equalityGraph[t1], type, reason)); d_equalityEdges.push_back(EqualityEdge(t1, d_equalityGraph[t2], type, reason)); @@ -814,7 +821,7 @@ std::string EqualityEngine::edgesToString(EqualityEdgeId edgeId) const { } void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vector& equalities) const { - Debug("equality") << "EqualityEngine::explainEquality(" << t1 << ", " << t2 << ", " << (polarity ? "true" : "false") << ")" << std::endl; + Debug("equality") << d_name << "::eq::explainEquality(" << t1 << ", " << t2 << ", " << (polarity ? "true" : "false") << ")" << std::endl; // The terms must be there already Assert(hasTerm(t1) && hasTerm(t2));; @@ -839,7 +846,7 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vec } void EqualityEngine::explainPredicate(TNode p, bool polarity, std::vector& assertions) const { - Debug("equality") << "EqualityEngine::explainPredicate(" << p << ")" << std::endl; + Debug("equality") << d_name << "::eq::explainPredicate(" << p << ")" << std::endl; // Must have the term Assert(hasTerm(p)); // Get the explanation @@ -848,7 +855,7 @@ void EqualityEngine::explainPredicate(TNode p, bool polarity, std::vector void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, std::vector& equalities) const { - Debug("equality") << "EqualityEngine::getExplanation(" << d_nodes[t1Id] << "," << d_nodes[t2Id] << ")" << std::endl; + Debug("equality") << d_name << "::eq::getExplanation(" << d_nodes[t1Id] << "," << d_nodes[t2Id] << ")" << std::endl; // We can only explain the nodes that got merged #ifdef CVC4_ASSERTIONS @@ -882,13 +889,13 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st BfsData current = bfsQueue[currentIndex]; EqualityNodeId currentNode = current.nodeId; - Debug("equality") << "EqualityEngine::getExplanation(): currentNode = " << d_nodes[currentNode] << std::endl; + Debug("equality") << d_name << "::eq::getExplanation(): currentNode = " << d_nodes[currentNode] << std::endl; // Go through the equality edges of this node EqualityEdgeId currentEdge = d_equalityGraph[currentNode]; if (Debug.isOn("equality")) { - Debug("equality") << "EqualityEngine::getExplanation(): edgesId = " << currentEdge << std::endl; - Debug("equality") << "EqualityEngine::getExplanation(): edges = " << edgesToString(currentEdge) << std::endl; + Debug("equality") << d_name << "::eq::getExplanation(): edgesId = " << currentEdge << std::endl; + Debug("equality") << d_name << "::eq::getExplanation(): edges = " << edgesToString(currentEdge) << std::endl; } while (currentEdge != null_edge) { @@ -898,12 +905,12 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st // 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") << d_name << "::eq::getExplanation(): currentEdge = (" << d_nodes[currentNode] << "," << d_nodes[edge.getNodeId()] << ")" << std::endl; // Did we find the path if (edge.getNodeId() == t2Id) { - Debug("equality") << "EqualityEngine::getExplanation(): path found: " << std::endl; + Debug("equality") << d_name << "::eq::getExplanation(): path found: " << std::endl; // Reconstruct the path do { @@ -912,13 +919,13 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st EqualityNodeId edgeNode = d_equalityEdges[currentEdge].getNodeId(); MergeReasonType reasonType = d_equalityEdges[currentEdge].getReasonType(); - Debug("equality") << "EqualityEngine::getExplanation(): currentEdge = " << currentEdge << ", currentNode = " << currentNode << std::endl; + Debug("equality") << d_name << "::eq::getExplanation(): currentEdge = " << currentEdge << ", currentNode = " << currentNode << std::endl; // Add the actual equality to the vector switch (reasonType) { case MERGED_THROUGH_CONGRUENCE: { // f(x1, x2) == f(y1, y2) because x1 = y1 and x2 = y2 - Debug("equality") << "EqualityEngine::getExplanation(): due to congruence, going deeper" << std::endl; + Debug("equality") << d_name << "::eq::getExplanation(): due to congruence, going deeper" << std::endl; const FunctionApplication& f1 = d_applications[currentNode].original; const FunctionApplication& f2 = d_applications[edgeNode].original; Debug("equality") << push; @@ -929,12 +936,12 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st } case MERGED_THROUGH_EQUALITY: // Construct the equality - Debug("equality") << "EqualityEngine::getExplanation(): adding: " << d_equalityEdges[currentEdge].getReason() << std::endl; + Debug("equality") << d_name << "::eq::getExplanation(): adding: " << d_equalityEdges[currentEdge].getReason() << std::endl; equalities.push_back(d_equalityEdges[currentEdge].getReason()); break; case MERGED_THROUGH_CONSTANTS: { // (a = b) == false because a and b are different constants - Debug("equality") << "EqualityEngine::getExplanation(): due to constants, going deeper" << std::endl; + Debug("equality") << d_name << "::eq::getExplanation(): due to constants, going deeper" << std::endl; EqualityNodeId eqId = currentNode == d_falseId ? edgeNode : currentNode; const FunctionApplication& eq = d_applications[eqId].original; Assert(eq.isEquality, "Must be an equality"); @@ -1048,7 +1055,7 @@ void EqualityEngine::addTriggerPredicate(TNode predicate) { void EqualityEngine::addTriggerEqualityInternal(TNode t1, TNode t2, TNode trigger, bool polarity) { - Debug("equality") << "EqualityEngine::addTrigger(" << t1 << ", " << t2 << ", " << trigger << ")" << std::endl; + Debug("equality") << d_name << "::eq::addTrigger(" << t1 << ", " << t2 << ", " << trigger << ")" << std::endl; Assert(hasTerm(t1)); Assert(hasTerm(t2)); @@ -1069,7 +1076,7 @@ void EqualityEngine::addTriggerEqualityInternal(TNode t1, TNode t2, TNode trigge // We will attach it to the class representative, since then we know how to backtrack it TriggerId t2TriggerId = d_nodeTriggers[t2classId]; - Debug("equality") << "EqualityEngine::addTrigger(" << trigger << "): " << t1Id << " (" << t1classId << ") = " << t2Id << " (" << t2classId << ")" << std::endl; + Debug("equality") << d_name << "::eq::addTrigger(" << trigger << "): " << t1Id << " (" << t1classId << ") = " << t2Id << " (" << t2classId << ")" << std::endl; // Create the triggers TriggerId t1NewTriggerId = d_equalityTriggers.size(); @@ -1092,12 +1099,12 @@ void EqualityEngine::addTriggerEqualityInternal(TNode t1, TNode t2, TNode trigge debugPrintGraph(); } - Debug("equality") << "EqualityEngine::addTrigger(" << t1 << "," << t2 << ") => (" << t1NewTriggerId << ", " << t2NewTriggerId << ")" << std::endl; + Debug("equality") << d_name << "::eq::addTrigger(" << t1 << "," << t2 << ") => (" << t1NewTriggerId << ", " << t2NewTriggerId << ")" << std::endl; } void EqualityEngine::propagate() { - Debug("equality") << "EqualityEngine::propagate()" << std::endl; + Debug("equality") << d_name << "::eq::propagate()" << std::endl; while (!d_propagationQueue.empty()) { @@ -1135,13 +1142,13 @@ void EqualityEngine::propagate() { // Depending on the merge preference (such as size, or being a constant), merge them std::vector triggers; if ((node2.getSize() > node1.getSize() && !d_isConstant[t1classId]) || d_isConstant[t2classId]) { - Debug("equality") << "EqualityEngine::propagate(): merging " << d_nodes[current.t1Id]<< " into " << d_nodes[current.t2Id] << std::endl; + Debug("equality") << d_name << "::eq::propagate(): merging " << d_nodes[current.t1Id]<< " into " << d_nodes[current.t2Id] << std::endl; d_assertedEqualities.push_back(Equality(t2classId, t1classId)); if (!merge(node2, node1, triggers)) { d_done = true; } } else { - Debug("equality") << "EqualityEngine::propagate(): merging " << d_nodes[current.t2Id] << " into " << d_nodes[current.t1Id] << std::endl; + Debug("equality") << d_name << "::eq::propagate(): merging " << d_nodes[current.t2Id] << " into " << d_nodes[current.t1Id] << std::endl; d_assertedEqualities.push_back(Equality(t1classId, t2classId)); if (!merge(node1, node2, triggers)) { d_done = true; @@ -1184,7 +1191,7 @@ void EqualityEngine::debugPrintGraph() const { } bool EqualityEngine::areEqual(TNode t1, TNode t2) const { - Debug("equality") << "EqualityEngine::areEqual(" << t1 << "," << t2 << ")" << std::endl; + Debug("equality") << d_name << "::eq::areEqual(" << t1 << "," << t2 << ")" << std::endl; Assert(hasTerm(t1)); Assert(hasTerm(t2)); @@ -1194,7 +1201,7 @@ bool EqualityEngine::areEqual(TNode t1, TNode t2) const { bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const { - Debug("equality") << "EqualityEngine::areDisequal(" << t1 << "," << t2 << ")" << std::endl; + Debug("equality") << d_name << "::eq::areDisequal(" << t1 << "," << t2 << ")" << std::endl; // Add the terms Assert(hasTerm(t1)); @@ -1294,7 +1301,7 @@ size_t EqualityEngine::getSize(TNode t) void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag) { - Debug("equality::trigger") << "EqualityEngine::addTriggerTerm(" << t << ", " << tag << ")" << std::endl; + Debug("equality::trigger") << d_name << "::eq::addTriggerTerm(" << t << ", " << tag << ")" << std::endl; Assert(tag != THEORY_LAST); if (d_done) { @@ -1315,6 +1322,7 @@ void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag) // If the term already is in the equivalence class that a tagged representative, just notify if (d_performNotify) { EqualityNodeId triggerId = getTriggerTermSet(triggerSetRef).getTrigger(tag); + Debug("equality::trigger") << d_name << "::eq::addTriggerTerm(" << t << ", " << tag << "): already have this trigger in class with " << d_nodes[triggerId] << std::endl; if (eqNodeId != triggerId && !d_notify.eqNotifyTriggerTermEquality(tag, t, d_nodes[triggerId], true)) { d_done = true; } @@ -1360,6 +1368,7 @@ void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag) d_nodeIndividualTrigger[classId] = triggerSetRef = newTriggerTermSet(); // Propagate trigger term disequalities we remembered + Debug("equality::trigger") << d_name << "::eq::addTriggerTerm(" << t << ", " << tag << "): propagating " << disequalitiesToNotify.size() << " disequalities " << std::endl; propagateTriggerTermDisequalities(tags, triggerSetRef, disequalitiesToNotify); } } @@ -1495,6 +1504,9 @@ void EqualityEngine::getDisequalities(bool allowConstants, EqualityNodeId classI // Go through the equivalence class EqualityNodeId currentId = classId; do { + + Debug("equality::trigger") << d_name << "::getDisequalities() : going through uselist of " << d_nodes[currentId] << std::endl; + // Current node in the equivalence class EqualityNode& currentNode = getEqualityNode(currentId); @@ -1503,6 +1515,9 @@ void EqualityEngine::getDisequalities(bool allowConstants, EqualityNodeId classI while (currentUseId != null_uselist_id) { UseListNode& useListNode = d_useListNodes[currentUseId]; EqualityNodeId funId = useListNode.getApplicationId(); + + Debug("equality::trigger") << d_name << "::getDisequalities() : checking " << d_nodes[funId] << std::endl; + const FunctionApplication& fun = d_applications[useListNode.getApplicationId()].original; // If it's an equality asserted to false, we do the work if (fun.isEquality && getEqualityNode(funId).getFind() == getEqualityNode(d_false).getFind()) { diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 5935ddc1f..ac6f458e9 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -563,6 +563,9 @@ private: bool propagateTriggerTermDisequalities(Theory::Set tags, TriggerTermSetRef triggerSetRef, const TaggedEqualitiesSet& disequalitiesToNotify); + /** Name of the equality engine */ + std::string d_name; + public: /** diff --git a/test/regress/regress0/aufbv/Makefile.am b/test/regress/regress0/aufbv/Makefile.am index cd5f1d981..bdcaaa2d0 100644 --- a/test/regress/regress0/aufbv/Makefile.am +++ b/test/regress/regress0/aufbv/Makefile.am @@ -14,7 +14,10 @@ TESTS = \ bug00.smt \ bug338.smt2 \ try5_small_difret_functions_wp_su.set_char_quoting.il.wp.delta01.smt \ - wchains010ue.delta01.smt + diseqprop.01.smt \ + wchains010ue.delta01.smt \ + wchains010ue.delta02.smt \ + dubreva005ue.delta01.smt EXTRA_DIST = $(TESTS) -- 2.30.2