From 78031276c7452fd687c4a6253ff0f82c501dbac2 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Mon, 28 Jun 2021 10:39:49 -0300 Subject: [PATCH] [proof] [dot] Make dot printer stateful (#6799) In preparation for further changes in the printer. --- src/proof/dot/dot_printer.cpp | 33 ++++++++++++++++----------------- src/proof/dot/dot_printer.h | 31 +++++++++++++++---------------- src/smt/proof_manager.cpp | 3 ++- 3 files changed, 33 insertions(+), 34 deletions(-) diff --git a/src/proof/dot/dot_printer.cpp b/src/proof/dot/dot_printer.cpp index 08be1728b..496085372 100644 --- a/src/proof/dot/dot_printer.cpp +++ b/src/proof/dot/dot_printer.cpp @@ -25,6 +25,9 @@ namespace cvc5 { namespace proof { +DotPrinter::DotPrinter() {} +DotPrinter::~DotPrinter() {} + std::string DotPrinter::sanitizeString(const std::string& s) { std::string newS; @@ -46,8 +49,7 @@ std::string DotPrinter::sanitizeString(const std::string& s) return newS; } -void DotPrinter::countSubproofs( - const ProofNode* pn, std::map& subpfCounter) +void DotPrinter::countSubproofs(const ProofNode* pn) { std::vector visit; std::unordered_map visited; @@ -78,9 +80,9 @@ void DotPrinter::countSubproofs( cur->getChildren(); for (const std::shared_ptr& c : children) { - counter += subpfCounter[c.get()]; + counter += d_subpfCounter[c.get()]; } - subpfCounter[cur] = counter; + d_subpfCounter[cur] = counter; } } while (!visit.empty()); } @@ -88,24 +90,21 @@ void DotPrinter::countSubproofs( void DotPrinter::print(std::ostream& out, const ProofNode* pn) { uint64_t ruleID = 0; - std::map subpfCounter; - countSubproofs(pn, subpfCounter); + countSubproofs(pn); // The dot attribute rankdir="BT" sets the direction of the graph layout, // placing the root node at the top. The "node [shape..." attribute sets the // shape of all nodes to record. out << "digraph proof {\n\trankdir=\"BT\";\n\tnode [shape=record];\n"; - DotPrinter::printInternal(out, pn, ruleID, 0, false, subpfCounter); + DotPrinter::printInternal(out, pn, ruleID, 0, false); out << "}\n"; } -void DotPrinter::printInternal( - std::ostream& out, - const ProofNode* pn, - uint64_t& ruleID, - uint64_t scopeCounter, - bool inPropositionalView, - const std::map& subpfCounter) +void DotPrinter::printInternal(std::ostream& out, + const ProofNode* pn, + uint64_t& ruleID, + uint64_t scopeCounter, + bool inPropositionalView) { uint64_t currentRuleID = ruleID; const std::vector>& children = pn->getChildren(); @@ -164,7 +163,8 @@ void DotPrinter::printInternal( classes << " \""; out << classes.str() << colors.str(); // add number of subchildren - std::map::const_iterator it = subpfCounter.find(pn); + std::map::const_iterator it = + d_subpfCounter.find(pn); out << ", comment = \"\{\"subProofQty\":" << it->second << "}\""; out << " ];\n"; @@ -172,8 +172,7 @@ void DotPrinter::printInternal( { ++ruleID; out << "\t" << ruleID << " -> " << currentRuleID << ";\n"; - printInternal( - out, c.get(), ruleID, scopeCounter, inPropositionalView, subpfCounter); + printInternal(out, c.get(), ruleID, scopeCounter, inPropositionalView); } } diff --git a/src/proof/dot/dot_printer.h b/src/proof/dot/dot_printer.h index a877efe9b..2d25fe0e7 100644 --- a/src/proof/dot/dot_printer.h +++ b/src/proof/dot/dot_printer.h @@ -29,14 +29,14 @@ class DotPrinter { public: DotPrinter(); - ~DotPrinter() {} + ~DotPrinter(); /** * Print the full proof of assertions => false by pn using the dot format. * @param out the output stream * @param pn the root node of the proof to print */ - static void print(std::ostream& out, const ProofNode* pn); + void print(std::ostream& out, const ProofNode* pn); private: /** @@ -53,13 +53,11 @@ class DotPrinter * @param inPropositionalView flag used to mark the proof node being traversed * was generated by the SAT solver and thus belong to the propositional view */ - static void printInternal( - std::ostream& out, - const ProofNode* pn, - uint64_t& ruleID, - uint64_t scopeCounter, - bool inPropositionalView, - const std::map& subpfCounter); + void printInternal(std::ostream& out, + const ProofNode* pn, + uint64_t& ruleID, + uint64_t scopeCounter, + bool inPropositionalView); /** * Return the arguments of a ProofNode @@ -67,8 +65,7 @@ class DotPrinter * pn formatted as "$ARG[0], $ARG[1], ..., $ARG[N-1]" * @param pn a ProofNode */ - static void ruleArguments(std::ostringstream& currentArguments, - const ProofNode* pn); + void ruleArguments(std::ostringstream& currentArguments, const ProofNode* pn); /** Add an escape character before special characters of the given string. * @param s The string to have the characters processed. @@ -76,14 +73,16 @@ class DotPrinter */ static std::string sanitizeString(const std::string& s); - /** Traverse proof node and map each proof node to the number of subproofs it - * contains, including itself + /** Traverse proof node and populate d_subpfCounter, mapping each proof node + * to the number of subproofs it contains, including itself * * @param pn the proof node to be traversed - * @param subpfCounter the map to be populated */ - static void countSubproofs(const ProofNode* pn, - std::map& subpfCounter); + void countSubproofs(const ProofNode* pn); + + /** All unique subproofs of a given proof node (counting itself). */ + std::map d_subpfCounter; + }; } // namespace proof diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index 55cfc1f15..eb5d8e7af 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -153,7 +153,8 @@ void PfManager::printProof(std::ostream& out, if (options::proofFormatMode() == options::ProofFormatMode::DOT) { - proof::DotPrinter::print(out, fp.get()); + proof::DotPrinter dotPrinter; + dotPrinter.print(out, fp.get()); } else { -- 2.30.2