Rename equality engine trace to print E-graph (#8780)

The current trace depends on `-t equality::internal`, which is pointless and
leads to confusion when one inevitably forgets this when checking which trace to
use to print the E-graph and the output does not contain it.

diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index c615bea3f1006c429dda6a57abc2fc9c3e4da412..9cd7b42cc59a4564e17cec7b5f4ba59a5546ab26 100644 (file)
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -2057,22 +2057,27 @@ void EqualityEngine::propagate() {
   }
 }
 
-void EqualityEngine::debugPrintGraph() const {
-  Trace("equality::graph") << std::endl << "Dumping graph" << std::endl;
-  for (EqualityNodeId nodeId = 0; nodeId < d_nodes.size(); ++ nodeId) {
-
-    Trace("equality::graph") << d_nodes[nodeId] << " " << nodeId << "(" << getEqualityNode(nodeId).getFind() << "):";
+void EqualityEngine::debugPrintGraph() const
+{
+  Trace("equality::internal") << std::endl << "Dumping graph" << std::endl;
+  for (EqualityNodeId nodeId = 0; nodeId < d_nodes.size(); ++nodeId)
+  {
+    Trace("equality::internal") << d_nodes[nodeId] << " " << nodeId << "("
+                                << getEqualityNode(nodeId).getFind() << "):";
 
     EqualityEdgeId edgeId = d_equalityGraph[nodeId];
-    while (edgeId != null_edge) {
+    while (edgeId != null_edge)
+    {
       const EqualityEdge& edge = d_equalityEdges[edgeId];
-      Trace("equality::graph") << " [" << edge.getNodeId() << "] " << d_nodes[edge.getNodeId()] << ":" << edge.getReason();
+      Trace("equality::internal")
+          << " [" << edge.getNodeId() << "] " << d_nodes[edge.getNodeId()]
+          << ":" << edge.getReason();
       edgeId = edge.getNext();
     }
 
-    Trace("equality::graph") << std::endl;
+    Trace("equality::internal") << std::endl;
   }
-  Trace("equality::graph") << std::endl;
+  Trace("equality::internal") << std::endl;
 }
 
 std::string EqualityEngine::debugPrintEqc() const