Improving equality engine tracing (#4770)

To keep track of the reasoning in the equality engine for n-ary kinds, for which partial applications amount to valid fully-applied terms, it's imperative to be able to see the IDs of the internal representation of the equality engine nodes. This commit updates tracing messages to print these IDs. It also improves the tracing for explanation generation.

1 files changed, 76 insertions, 27 deletions

diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index b532bcfa5..171140d89 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -166,10 +166,11 @@ void EqualityEngine::setMasterEqualityEngine(EqualityEngine* master) {
 }
 
 void EqualityEngine::enqueue(const MergeCandidate& candidate, bool back) {
-  Debug("equality") << d_name << "::eq::enqueue(" << d_nodes[candidate.d_t1Id]
-                    << ", " << d_nodes[candidate.d_t2Id] << ", "
-                    << candidate.d_type << "). reason: " << candidate.d_reason
-                    << std::endl;
+  Debug("equality") << d_name << "::eq::enqueue({" << candidate.d_t1Id << "} "
+                    << d_nodes[candidate.d_t1Id] << ", {" << candidate.d_t2Id
+                    << "} " << d_nodes[candidate.d_t2Id] << ", "
+                    << static_cast<MergeReasonType>(candidate.d_type)
+                    << "). reason: " << candidate.d_reason << std::endl;
   if (back) {
     d_propagationQueue.push_back(candidate);
   } else {
@@ -178,7 +179,9 @@ void EqualityEngine::enqueue(const MergeCandidate& candidate, bool back) {
 }
 
 EqualityNodeId EqualityEngine::newApplicationNode(TNode original, EqualityNodeId t1, EqualityNodeId t2, FunctionApplicationType type) {
-  Debug("equality") << d_name << "::eq::newApplicationNode(" << original << ", " << t1 << ", " << t2 << ")" << std::endl;
+  Debug("equality") << d_name << "::eq::newApplicationNode(" << original
+                    << ", {" << t1 << "} " << d_nodes[t1] << ", {" << t2 << "} "
+                    << d_nodes[t2] << ")" << std::endl;
 
   ++d_stats.d_functionTermsCount;
 
@@ -190,13 +193,22 @@ EqualityNodeId EqualityEngine::newApplicationNode(TNode original, EqualityNodeId
   EqualityNodeId t2ClassId = getEqualityNode(t2).getFind();
   FunctionApplication funNormalized(type, t1ClassId, t2ClassId);
 
+  Debug("equality") << d_name << "::eq::newApplicationNode: funOriginal: ("
+                    << type << " " << d_nodes[t1] << " " << d_nodes[t2]
+                    << "), funNorm: (" << type << " " << d_nodes[t1ClassId]
+                    << " " << d_nodes[t2ClassId] << ")\n";
+
   // We add the original version
   d_applications[funId] = FunctionApplicationPair(funOriginal, funNormalized);
 
   // Add the lookup data, if it's not already there
   ApplicationIdsMap::iterator find = d_applicationLookup.find(funNormalized);
   if (find == d_applicationLookup.end()) {
-    Debug("equality") << d_name << "::eq::newApplicationNode(" << original << ", " << t1 << ", " << t2 << "): no lookup, setting up" << std::endl;
+    Debug("equality") << d_name << "::eq::newApplicationNode(" << original
+                      << ", " << t1 << ", " << t2
+                      << "): no lookup, setting up funNorm: (" << type << " "
+                      << d_nodes[t1ClassId] << " " << d_nodes[t2ClassId]
+                      << ") => " << funId << std::endl;
     // Mark the normalization to the lookup
     storeApplicationLookup(funNormalized, funId);
   } else {
@@ -425,8 +437,10 @@ const EqualityNode& EqualityEngine::getEqualityNode(EqualityNodeId nodeId) const
 }
 
 void EqualityEngine::assertEqualityInternal(TNode t1, TNode t2, TNode reason, unsigned pid) {
-
-  Debug("equality") << d_name << "::eq::addEqualityInternal(" << t1 << "," << t2 << "), reason = " << reason << ", pid = " << pid << std::endl;
+  Debug("equality") << d_name << "::eq::addEqualityInternal(" << t1 << "," << t2
+                    << "), reason = " << reason
+                    << ", pid = " << static_cast<MergeReasonType>(pid)
+                    << std::endl;
 
   if (d_done) {
     return;
@@ -935,7 +949,9 @@ void EqualityEngine::backtrack() {
 }
 
 void EqualityEngine::addGraphEdge(EqualityNodeId t1, EqualityNodeId t2, unsigned type, TNode reason) {
-  Debug("equality") << d_name << "::eq::addGraphEdge(" << d_nodes[t1] << "," << d_nodes[t2] << "," << reason << ")" << std::endl;
+  Debug("equality") << d_name << "::eq::addGraphEdge({" << t1 << "} "
+                    << d_nodes[t1] << ", {" << t2 << "} " << 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));
@@ -956,7 +972,7 @@ std::string EqualityEngine::edgesToString(EqualityEdgeId edgeId) const {
     while (edgeId != null_edge) {
       const EqualityEdge& edge = d_equalityEdges[edgeId];
       if (!first) out << ",";
-      out << d_nodes[edge.getNodeId()];
+      out << "{" << edge.getNodeId() << "} " << d_nodes[edge.getNodeId()];
       edgeId = edge.getNext();
       first = false;
     }
@@ -974,7 +990,10 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity,
   // The terms must be there already
   Assert(hasTerm(t1) && hasTerm(t2));
   ;
-
+  if (Debug.isOn("equality::internal"))
+  {
+    debugPrintGraph();
+  }
   // Get the ids
   EqualityNodeId t1Id = getNodeId(t1);
   EqualityNodeId t2Id = getNodeId(t2);
@@ -994,7 +1013,12 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity,
     Assert(d_disequalityReasonsMap.find(pair) != d_disequalityReasonsMap.end())
         << "Don't ask for stuff I didn't notify you about";
     DisequalityReasonRef reasonRef = d_disequalityReasonsMap.find(pair)->second;
-
+    if (eqp)
+    {
+      Debug("pf::ee") << "Deq reason for " << eqp->d_node << " "
+                      << reasonRef.d_mergesStart << "..."
+                      << reasonRef.d_mergesEnd << std::endl;
+    }
     for (unsigned i = reasonRef.d_mergesStart; i < reasonRef.d_mergesEnd; ++i)
     {
       EqualityPair toExplain = d_deducedDisequalityReasons[i];
@@ -1003,6 +1027,9 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity,
       // If we're constructing a (transitivity) proof, we don't need to include an explanation for x=x.
       if (eqp && toExplain.first != toExplain.second) {
         eqpc = std::make_shared<EqProof>();
+        Debug("pf::ee") << "Deq getExplanation #" << i << " for " << eqp->d_node
+                        << " : " << toExplain.first << " " << toExplain.second
+                        << std::endl;
       }
 
       getExplanation(
@@ -1084,6 +1111,10 @@ void EqualityEngine::explainPredicate(TNode p, bool polarity,
   // Must have the term
   Assert(hasTerm(p));
   std::map<std::pair<EqualityNodeId, EqualityNodeId>, EqProof*> cache;
+  if (Debug.isOn("equality::internal"))
+  {
+    debugPrintGraph();
+  }
   // Get the explanation
   getExplanation(
       getNodeId(p), polarity ? d_trueId : d_falseId, assertions, cache, eqp);
@@ -1096,8 +1127,9 @@ void EqualityEngine::getExplanation(
     std::map<std::pair<EqualityNodeId, EqualityNodeId>, EqProof*>& cache,
     EqProof* eqp) const
 {
-  Trace("eq-exp") << d_name << "::eq::getExplanation(" << d_nodes[t1Id] << ","
-                  << d_nodes[t2Id] << ") size = " << cache.size() << std::endl;
+  Trace("eq-exp") << d_name << "::eq::getExplanation({" << t1Id << "} "
+                  << d_nodes[t1Id] << ", {" << t2Id << "} " << d_nodes[t2Id]
+                  << ") size = " << cache.size() << std::endl;
 
   // determine if we have already computed the explanation.
   std::pair<EqualityNodeId, EqualityNodeId> cacheKey;
@@ -1169,11 +1201,6 @@ void EqualityEngine::getExplanation(
     return;
   }
 
-
-  if (Debug.isOn("equality::internal")) {
-    debugPrintGraph();
-  }
-
   // Queue for the BFS containing nodes
   std::vector<BfsData> bfsQueue;
 
@@ -1188,7 +1215,9 @@ void EqualityEngine::getExplanation(
     BfsData current = bfsQueue[currentIndex];
     EqualityNodeId currentNode = current.d_nodeId;
 
-    Debug("equality") << d_name << "::eq::getExplanation(): currentNode =  " << d_nodes[currentNode] << std::endl;
+    Debug("equality") << d_name << "::eq::getExplanation(): currentNode = {"
+                      << currentNode << "} " << d_nodes[currentNode]
+                      << std::endl;
 
     // Go through the equality edges of this node
     EqualityEdgeId currentEdge = d_equalityGraph[currentNode];
@@ -1204,7 +1233,11 @@ void EqualityEngine::getExplanation(
       // If not just the backwards edge
       if ((currentEdge | 1u) != (current.d_edgeId | 1u))
       {
-        Debug("equality") << d_name << "::eq::getExplanation(): currentEdge = (" << d_nodes[currentNode] << "," << d_nodes[edge.getNodeId()] << ")" << std::endl;
+        Debug("equality") << d_name
+                          << "::eq::getExplanation(): currentEdge = ({"
+                          << currentNode << "} " << d_nodes[currentNode]
+                          << ", {" << edge.getNodeId() << "} "
+                          << d_nodes[edge.getNodeId()] << ")" << std::endl;
 
         // Did we find the path
         if (edge.getNodeId() == t2Id) {
@@ -1221,10 +1254,21 @@ void EqualityEngine::getExplanation(
             unsigned reasonType = d_equalityEdges[currentEdge].getReasonType();
             Node reason = d_equalityEdges[currentEdge].getReason();
 
-            Debug("equality") << d_name << "::eq::getExplanation(): currentEdge = " << currentEdge << ", currentNode = " << currentNode << std::endl;
-            Debug("equality") << d_name << "                     targetNode = " << d_nodes[edgeNode] << std::endl;
-            Debug("equality") << d_name << "                     in currentEdge = (" << d_nodes[currentNode] << "," << d_nodes[edge.getNodeId()] << ")" << std::endl;
-            Debug("equality") << d_name << "                     reason type = " << reasonType << std::endl;
+            Debug("equality")
+                << d_name
+                << "::eq::getExplanation(): currentEdge = " << currentEdge
+                << ", currentNode = " << currentNode << std::endl;
+            Debug("equality")
+                << d_name << "                       targetNode = {" << edgeNode
+                << "} " << d_nodes[edgeNode] << std::endl;
+            Debug("equality")
+                << d_name << "                       in currentEdge = ({"
+                << currentNode << "} " << d_nodes[currentNode] << ", {"
+                << edge.getNodeId() << "} " << d_nodes[edge.getNodeId()] << ")"
+                << std::endl;
+            Debug("equality")
+                << d_name << "                       reason type = "
+                << static_cast<MergeReasonType>(reasonType) << std::endl;
 
             std::shared_ptr<EqProof> eqpc;;
             // Make child proof if a proof is being constructed
@@ -1237,7 +1281,10 @@ void EqualityEngine::getExplanation(
             switch (reasonType) {
             case MERGED_THROUGH_CONGRUENCE: {
               // f(x1, x2) == f(y1, y2) because x1 = y1 and x2 = y2
-              Debug("equality") << d_name << "::eq::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].d_original;
               const FunctionApplication& f2 =
@@ -1358,7 +1405,9 @@ void EqualityEngine::getExplanation(
               // Construct the equality
               Debug("equality") << d_name << "::eq::getExplanation(): adding: "
                                 << reason << std::endl;
-              Debug("equality") << d_name << "::eq::getExplanation(): reason type = " << reasonType << std::endl;
+              Debug("equality")
+                  << d_name << "::eq::getExplanation(): reason type = "
+                  << static_cast<MergeReasonType>(reasonType) << std::endl;
               Node a = d_nodes[currentNode];
               Node b = d_nodes[d_equalityEdges[currentEdge].getNodeId()];