From: vinciusb <65973642+vinciusb@users.noreply.github.com> Date: Tue, 22 Feb 2022 13:51:21 +0000 (-0300) Subject: [proofs] [dot] Enable DAG and tree printing with dot files (#8107) X-Git-Tag: cvc5-1.0.0~409 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=48471e5f6202cbe681d7d71c9974da603704160f;p=cvc5.git [proofs] [dot] Enable DAG and tree printing with dot files (#8107) Add a proof option that allows DAG and tree print format when using dot files. Signed-off-by: Vinícius Braga Freire vinicius.braga.freire@gmail.com --- diff --git a/src/options/proof_options.toml b/src/options/proof_options.toml index c63f99534..346a0dc4e 100644 --- a/src/options/proof_options.toml +++ b/src/options/proof_options.toml @@ -114,3 +114,11 @@ name = "Proof" type = "bool" default = "false" help = "Add pivots to Alethe resolution steps" + +[[option]] + name = "proofDotDAG" + category = "regular" + long = "proof-dot-dag" + type = "bool" + default = "false" + help = "Indicates if the dot proof will be printed as a DAG or as a tree" diff --git a/src/proof/dot/dot_printer.cpp b/src/proof/dot/dot_printer.cpp index 0e8d1a057..c5f97711d 100644 --- a/src/proof/dot/dot_printer.cpp +++ b/src/proof/dot/dot_printer.cpp @@ -18,6 +18,7 @@ #include #include "options/expr_options.h" +#include "options/proof_options.h" #include "printer/smt2/smt2_printer.h" #include "proof/proof_checker.h" #include "proof/proof_node_manager.h" @@ -27,7 +28,9 @@ namespace cvc5 { namespace proof { DotPrinter::DotPrinter() - : d_lbind(options::defaultDagThresh() ? options::defaultDagThresh() + 1 : 0) + : d_lbind(options::defaultDagThresh() ? options::defaultDagThresh() + 1 + : 0), + d_ruleID(0) { } @@ -141,7 +144,6 @@ void DotPrinter::letifyResults(const ProofNode* pn) void DotPrinter::print(std::ostream& out, const ProofNode* pn) { - uint64_t ruleID = 0; countSubproofs(pn); letifyResults(pn); @@ -178,18 +180,37 @@ void DotPrinter::print(std::ostream& out, const ProofNode* pn) } out << "}}\";\n"; } - DotPrinter::printInternal(out, pn, ruleID, 0, false); + + std::map proofLet; + DotPrinter::printInternal(out, pn, proofLet, 0, false); out << "}\n"; } -void DotPrinter::printInternal(std::ostream& out, - const ProofNode* pn, - uint64_t& ruleID, - uint64_t scopeCounter, - bool inPropositionalView) +uint64_t DotPrinter::printInternal(std::ostream& out, + const ProofNode* pn, + std::map& pfLet, + uint64_t scopeCounter, + bool inPropositionalView) { - uint64_t currentRuleID = ruleID; - const std::vector>& children = pn->getChildren(); + uint64_t currentRuleID = d_ruleID; + + // Print DAG option enabled + if (options::proofDotDAG()) + { + ProofNodeHashFunction hasher; + size_t currentHash = hasher(pn); + auto proofIt = pfLet.find(currentHash); + + // If this node has been already counted + if (proofIt != pfLet.end()) + { + return proofIt->second; + } + + pfLet[currentHash] = currentRuleID; + } + d_ruleID++; + std::ostringstream currentArguments, resultStr, classes, colors; out << "\t" << currentRuleID << " [ label = \"{"; @@ -250,12 +271,15 @@ void DotPrinter::printInternal(std::ostream& out, out << ", comment = \"{\\\"subProofQty\\\":" << it->second << "}\""; out << " ];\n"; + const std::vector>& children = pn->getChildren(); for (const std::shared_ptr& c : children) { - ++ruleID; - out << "\t" << ruleID << " -> " << currentRuleID << ";\n"; - printInternal(out, c.get(), ruleID, scopeCounter, inPropositionalView); + uint64_t childId = + printInternal(out, c.get(), pfLet, scopeCounter, inPropositionalView); + out << "\t" << childId << " -> " << currentRuleID << ";\n"; } + + return currentRuleID; } void DotPrinter::ruleArguments(std::ostringstream& currentArguments, diff --git a/src/proof/dot/dot_printer.h b/src/proof/dot/dot_printer.h index 9cc03a258..c3ec82e2d 100644 --- a/src/proof/dot/dot_printer.h +++ b/src/proof/dot/dot_printer.h @@ -48,17 +48,18 @@ class DotPrinter * the child as argument. * @param out the output stream * @param pn the proof node to print - * @param ruleID the id of the rule to print + * @param pfLet the map of the hashs of proof nodes already printed to their ids * @param scopeCounter counter of how many SCOPE were already depth-first * traversed in the proof up to this point * @param inPropositionalView flag used to mark the proof node being traversed * was generated by the SAT solver and thus belong to the propositional view + * @return the id of the proof node printed */ - void printInternal(std::ostream& out, - const ProofNode* pn, - uint64_t& ruleID, - uint64_t scopeCounter, - bool inPropositionalView); + uint64_t printInternal(std::ostream& out, + const ProofNode* pn, + std::map& pfLet, + uint64_t scopeCounter, + bool inPropositionalView); /** * Return the arguments of a ProofNode @@ -95,6 +96,9 @@ class DotPrinter /** Let binder for terms in proof nodes */ LetBinding d_lbind; + + /** Counter that indicates the current rule ID */ + uint64_t d_ruleID; }; } // namespace proof diff --git a/src/proof/proof_node.cpp b/src/proof/proof_node.cpp index 2a141919d..a857b252a 100644 --- a/src/proof/proof_node.cpp +++ b/src/proof/proof_node.cpp @@ -70,4 +70,26 @@ std::ostream& operator<<(std::ostream& out, const ProofNode& pn) return out; } +size_t ProofNodeHashFunction::operator()(const ProofNode* pfn) const +{ + uint64_t ret = fnv1a::offsetBasis; + + ret = fnv1a::fnv1a_64(ret, std::hash()(pfn->getResult())); + ret = fnv1a::fnv1a_64(ret, static_cast(pfn->getRule())); + + const std::vector>& children = pfn->getChildren(); + for (const Pf& child : children) + { + ret = fnv1a::fnv1a_64(ret, std::hash()(child->getResult())); + } + + const std::vector& args = pfn->getArguments(); + for (const Node& arg : args) + { + ret = fnv1a::fnv1a_64(ret, std::hash()(arg)); + } + + return static_cast(ret); +} + } // namespace cvc5 diff --git a/src/proof/proof_node.h b/src/proof/proof_node.h index f4552ae43..5f7aaec3d 100644 --- a/src/proof/proof_node.h +++ b/src/proof/proof_node.h @@ -34,6 +34,7 @@ using Pf = std::shared_ptr; struct ProofNodeHashFunction { inline size_t operator()(std::shared_ptr pfn) const; + size_t operator()(const ProofNode* pfn) const; }; /* struct ProofNodeHashFunction */ /** A node in a proof