From 3546ec8388934b1a30ad025551884a724eeb25b9 Mon Sep 17 00:00:00 2001 From: vinciusb <65973642+vinciusb@users.noreply.github.com> Date: Fri, 20 May 2022 10:55:02 -0300 Subject: [PATCH] Trying to break cycles when printing a .dot DAG (#8698) MIME-Version: 1.0 Content-Type: text/plain; charset=utf8 Content-Transfer-Encoding: 8bit Change the way cvc5 traverse and print the proof when --proof-dot-dag option is used. The main change is related to the way the printer deals with cycles between proof nodes that are in a ancestor/descendant relationship. The new conditions are: - If any proof node under a first proof node has the hash equal to the first one, this would introduces a cycle. To avoid it, then no sharing between nodes happens in this case. Signed-off-by: Vinícius Braga Freire vinicius.braga.freire@gmail.com --- src/proof/dot/dot_printer.cpp | 72 ++++++++++++++++++++++++++--------- src/proof/dot/dot_printer.h | 3 ++ 2 files changed, 56 insertions(+), 19 deletions(-) diff --git a/src/proof/dot/dot_printer.cpp b/src/proof/dot/dot_printer.cpp index b99dab2c1..a19122380 100644 --- a/src/proof/dot/dot_printer.cpp +++ b/src/proof/dot/dot_printer.cpp @@ -197,12 +197,14 @@ void DotPrinter::print(std::ostream& out, const ProofNode* pn) std::map proofLet; std::map firstScopeLet; std::unordered_map cfaMap; + std::vector ancestorHashs; DotPrinter::printInternal(out, pn, proofLet, firstScopeLet, cfaMap, + ancestorHashs, ProofNodeClusterType::NOT_DEFINED); if (options::printDotClusters()) @@ -222,6 +224,7 @@ uint64_t DotPrinter::printInternal( std::map& pfLetClosed, std::map& pfLetOpen, std::unordered_map& cfaMap, + std::vector& ancestorHashs, ProofNodeClusterType parentType) { uint64_t currentRuleID = d_ruleID; @@ -231,27 +234,44 @@ uint64_t DotPrinter::printInternal( { ProofNodeHashFunction hasher; size_t currentHash = hasher(pn); - auto openProofIt = pfLetOpen.find(currentHash); - if (openProofIt != pfLetOpen.end()) - { - return openProofIt->second; - } + std::vector::iterator oldEnd = ancestorHashs.end(); + // Search if the current hash is in the vector + std::vector::iterator it = + std::find(ancestorHashs.begin(), ancestorHashs.end(), currentHash); - auto proofIt = pfLetClosed.find(currentHash); - // If this node has been already saved to the global cache of closed proof - // nodes - if (proofIt != pfLetClosed.end()) - { - Assert(!expr::containsAssumption(pn, cfaMap)); - return proofIt->second; - } - // If this proof node is closed, we add it to the global cache - if (!expr::containsAssumption(pn, cfaMap)) + // Register the current proof node hash in the ancestor vector + ancestorHashs.push_back(currentHash); + + // we only consider sharing when this would not introduce a cycle, which + // would be the case if this hash is occurring under a proof node with the + // same hash (this can happen since our hash computation only takes into + // account the immediate descendants of a proof node, the limit of hash + // representation notwithstanding) + if (it == oldEnd) { - pfLetClosed[currentHash] = currentRuleID; + auto openProofIt = pfLetOpen.find(currentHash); + + if (openProofIt != pfLetOpen.end()) + { + return openProofIt->second; + } + + auto proofIt = pfLetClosed.find(currentHash); + // If this node has been already saved to the global cache of closed proof + // nodes + if (proofIt != pfLetClosed.end()) + { + Assert(!expr::containsAssumption(pn, cfaMap)); + return proofIt->second; + } + // If this proof node is closed, we add it to the global cache + if (!expr::containsAssumption(pn, cfaMap)) + { + pfLetClosed[currentHash] = currentRuleID; + } + pfLetOpen[currentHash] = currentRuleID; } - pfLetOpen[currentHash] = currentRuleID; } ProofNodeClusterType proofNodeType = ProofNodeClusterType::NOT_DEFINED; @@ -282,17 +302,31 @@ uint64_t DotPrinter::printInternal( pfLetClosed, thisScopeLet, cfaMap, + ancestorHashs, proofNodeType); out << "\t" << childId << " -> " << currentRuleID << ";\n"; + if (options::proofDotDAG()) + { + ancestorHashs.pop_back(); + } } else { const std::vector>& children = pn->getChildren(); for (const std::shared_ptr& c : children) { - uint64_t childId = printInternal( - out, c.get(), pfLetClosed, pfLetOpen, cfaMap, proofNodeType); + uint64_t childId = printInternal(out, + c.get(), + pfLetClosed, + pfLetOpen, + cfaMap, + ancestorHashs, + proofNodeType); out << "\t" << childId << " -> " << currentRuleID << ";\n"; + if (options::proofDotDAG()) + { + ancestorHashs.pop_back(); + } } } diff --git a/src/proof/dot/dot_printer.h b/src/proof/dot/dot_printer.h index 7b4b26485..ac9606c90 100644 --- a/src/proof/dot/dot_printer.h +++ b/src/proof/dot/dot_printer.h @@ -95,6 +95,8 @@ class DotPrinter * @param pfLetOpen the map, local to the current scope, of proof node hashs * to their printed ids * @param cfaMap the map from proof nodes to whether they contain assumptions + * @param ancestorHashs a vector containing the hashs of all the proof nodes + * ancestors traversed to get to pn * @param parentType the type of the parent node * @return the id of the proof node printed */ @@ -103,6 +105,7 @@ class DotPrinter std::map& pfLetClosed, std::map& pfLetOpen, std::unordered_map& cfaMap, + std::vector& ancestorHashs, ProofNodeClusterType parentType); /** -- 2.30.2