diff options
author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2020-07-18 02:20:19 -0300 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-07-17 22:20:19 -0700 |
commit | 96c168b25d940ccbb20c80087bc17bf7687cc9ab (patch) | |
tree | e52b99e9bdc9595e35f0202434431cfe936ce3bd /src/theory/uf/equality_engine.cpp | |
parent | 750b53312a1930d6c0e4a43b7ae85736a30aa6d4 (diff) |
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.
Diffstat (limited to 'src/theory/uf/equality_engine.cpp')
-rw-r--r-- | src/theory/uf/equality_engine.cpp | 103 |
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()]; |