fixing the wrong results. arrays equality adaptor had a missing case when propagating...

diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 6592e86cf54508752f079e70b26a0fd8c1b63901..3ae0146c194d28aafced4fadbeb625b95cecfc19 100644 (file)
--- 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 c5ccaaeea17e66d6adeb8bd5b93a4007f480cd4d..1f45b7827f08bcfc7bc3ea254c608e874cd25d0b 100644 (file)
--- 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<TriggerId>& 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<false>(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<TNode>& 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<TNode>& 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<TNode>
 
 void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, std::vector<TNode>& 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<TriggerId> 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 5935ddc1f8784ee86922f14ecfbaddfb8198bd85..ac6f458e9995c3e6e714f694fc09ab5fe03193c2 100644 (file)
--- 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 cd5f1d981dace41142e6cfa088635830acedc9e0..bdcaaa2d0bdf232c05cb9c5ab43060be88987f42 100644 (file)
--- 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)