From e39bf3a391cdd92412bb109419ce5ca66fd3a0f0 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Mon, 16 May 2022 18:07:59 -0300 Subject: [PATCH] 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. --- src/theory/uf/equality_engine.cpp | 23 ++++++++++++++--------- 1 file changed, 14 insertions(+), 9 deletions(-) diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index c615bea3f..9cd7b42cc 100644 --- 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 -- 2.30.2