From 4b57f0aaa295d0203157ac81ad38360f5210f915 Mon Sep 17 00:00:00 2001 From: vinciusb <65973642+vinciusb@users.noreply.github.com> Date: Thu, 14 Apr 2022 11:00:38 -0300 Subject: [PATCH] [proofs] [dot] New way to traverse the proof when printing a .dot DAG (#8610) 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 tracks visited proof nodes. The new conditions are: - If the proof node has already been visited inside the current scope. - If the proof node is closed (i.e. does not contains a subproof whose rule is ASSUME) and has already been visited (here the condition is global and the scope doesn't matter). Signed-off-by: Vinícius Braga Freire vinicius.braga.freire@gmail.com --- src/proof/dot/dot_printer.cpp | 68 +++++++++++++++++++++++++++-------- src/proof/dot/dot_printer.h | 11 ++++-- 2 files changed, 62 insertions(+), 17 deletions(-) diff --git a/src/proof/dot/dot_printer.cpp b/src/proof/dot/dot_printer.cpp index 518c1009f..8d648140e 100644 --- a/src/proof/dot/dot_printer.cpp +++ b/src/proof/dot/dot_printer.cpp @@ -23,6 +23,7 @@ #include "options/proof_options.h" #include "printer/smt2/smt2_printer.h" #include "proof/proof_checker.h" +#include "proof/proof_node_algorithm.h" #include "proof/proof_node_manager.h" #include "theory/builtin/proof_checker.h" @@ -194,8 +195,15 @@ void DotPrinter::print(std::ostream& out, const ProofNode* pn) } std::map proofLet; - DotPrinter::printInternal( - out, pn, proofLet, ProofNodeClusterType::NOT_DEFINED); + std::map firstScopeLet; + std::unordered_map cfaMap; + + DotPrinter::printInternal(out, + pn, + proofLet, + firstScopeLet, + cfaMap, + ProofNodeClusterType::NOT_DEFINED); if (options::printDotClusters()) { @@ -208,10 +216,13 @@ void DotPrinter::print(std::ostream& out, const ProofNode* pn) out << "\n}\n"; } -uint64_t DotPrinter::printInternal(std::ostream& out, - const ProofNode* pn, - std::map& pfLet, - ProofNodeClusterType parentType) +uint64_t DotPrinter::printInternal( + std::ostream& out, + const ProofNode* pn, + std::map& pfLetClosed, + std::map& pfLetOpen, + std::unordered_map& cfaMap, + ProofNodeClusterType parentType) { uint64_t currentRuleID = d_ruleID; @@ -220,15 +231,27 @@ uint64_t DotPrinter::printInternal(std::ostream& out, { ProofNodeHashFunction hasher; size_t currentHash = hasher(pn); - auto proofIt = pfLet.find(currentHash); + auto openProofIt = pfLetOpen.find(currentHash); - // If this node has been already counted - if (proofIt != pfLet.end()) + if (openProofIt != pfLetOpen.end()) { - return proofIt->second; + return openProofIt->second; } - pfLet[currentHash] = currentRuleID; + 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; } ProofNodeClusterType proofNodeType = ProofNodeClusterType::NOT_DEFINED; @@ -249,12 +272,29 @@ uint64_t DotPrinter::printInternal(std::ostream& out, PfRule r = pn->getRule(); - const std::vector>& children = pn->getChildren(); - for (const std::shared_ptr& c : children) + // Scopes trigger a traversal with a new local cache for proof nodes + if (isSCOPE(r) && currentRuleID) { - uint64_t childId = printInternal(out, c.get(), pfLet, proofNodeType); + // create a new pfLet + std::map thisScopeLet; + uint64_t childId = printInternal(out, + pn->getChildren()[0].get(), + pfLetClosed, + thisScopeLet, + cfaMap, + proofNodeType); out << "\t" << childId << " -> " << currentRuleID << ";\n"; } + 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); + out << "\t" << childId << " -> " << currentRuleID << ";\n"; + } + } // If it's a scope, then remove from the stack if (isSCOPE(r) && options::printDotClusters()) diff --git a/src/proof/dot/dot_printer.h b/src/proof/dot/dot_printer.h index f5fe8d25e..70d89e17e 100644 --- a/src/proof/dot/dot_printer.h +++ b/src/proof/dot/dot_printer.h @@ -90,14 +90,19 @@ class DotPrinter * the child as argument. * @param out the output stream * @param pn the proof node to print - * @param pfLet the map of the hashs of proof nodes already printed to their - * ids + * @param pfLetClosed the map from proof node hashs, of closed proof nodes, to + * their printed ids + * @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 parentType the type of the parent node * @return the id of the proof node printed */ uint64_t printInternal(std::ostream& out, const ProofNode* pn, - std::map& pfLet, + std::map& pfLetClosed, + std::map& pfLetOpen, + std::unordered_map& cfaMap, ProofNodeClusterType parentType); /** -- 2.30.2