From: vinciusb <65973642+vinciusb@users.noreply.github.com> Date: Tue, 12 Apr 2022 13:13:56 +0000 (-0300) Subject: [proofs] [dot] Print nodes clusters at dot format (#8574) X-Git-Tag: cvc5-1.0.1~274 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=13fe47404522f2ba984fe411c846e0a9795ee134;p=cvc5.git [proofs] [dot] Print nodes clusters at dot format (#8574) Add a printer option that allows the dot printer to identify each node type and group them up in node clusters. These cluster are determined according to "part of the proof" whether a node belongs to: - input - sat proof - cnf proof - theory lemma proof - preprocessing Signed-off-by: Vinícius Braga Freire vinicius.braga.freire@gmail.com --- diff --git a/src/options/printer_options.toml b/src/options/printer_options.toml index 9ac284ddd..3aa4e321a 100644 --- a/src/options/printer_options.toml +++ b/src/options/printer_options.toml @@ -24,6 +24,14 @@ name = "Printing" default = "true" help = "print instantiations for formulas that do not have given identifiers" +[[option]] + name = "printDotClusters" + category = "regular" + long = "print-dot-clusters" + type = "bool" + default = "false" + help = "Whether the proof node clusters (e.g. SAT, CNF, INPUT) will be printed when using the dot format or not." + [[option]] name = "printUnsatCoresFull" category = "regular" diff --git a/src/proof/dot/dot_printer.cpp b/src/proof/dot/dot_printer.cpp index d2643b927..518c1009f 100644 --- a/src/proof/dot/dot_printer.cpp +++ b/src/proof/dot/dot_printer.cpp @@ -15,9 +15,11 @@ #include "proof/dot/dot_printer.h" +#include #include #include "options/expr_options.h" +#include "options/printer_options.h" #include "options/proof_options.h" #include "printer/smt2/smt2_printer.h" #include "proof/proof_checker.h" @@ -32,6 +34,16 @@ DotPrinter::DotPrinter() : 0), d_ruleID(0) { + const std::string acronyms[5] = {"SAT", "CNF", "TL", "PP", "IN"}; + const std::string colors[5] = {"purple", "yellow", "green", "brown", "blue"}; + + for (unsigned i = 0; i < 5; i++) + { + d_subgraphsStr.push_back(std::ostringstream()); + d_subgraphsStr[i] << "\n\tsubgraph cluster_" << acronyms[i] + << " {\n\t\tlabel=\"" << acronyms[i] + << "\"\n\t\tbgcolor=\"" << colors[i] << "\"\n\t\t"; + } } DotPrinter::~DotPrinter() {} @@ -182,15 +194,24 @@ void DotPrinter::print(std::ostream& out, const ProofNode* pn) } std::map proofLet; - DotPrinter::printInternal(out, pn, proofLet, 0, false); - out << "}\n"; + DotPrinter::printInternal( + out, pn, proofLet, ProofNodeClusterType::NOT_DEFINED); + + if (options::printDotClusters()) + { + // Print the sub-graphs + for (unsigned i = 0; i < 5; i++) + { + out << d_subgraphsStr[i].str() << "\n\t};"; + } + } + out << "\n}\n"; } uint64_t DotPrinter::printInternal(std::ostream& out, const ProofNode* pn, std::map& pfLet, - uint64_t scopeCounter, - bool inPropositionalView) + ProofNodeClusterType parentType) { uint64_t currentRuleID = d_ruleID; @@ -209,11 +230,46 @@ uint64_t DotPrinter::printInternal(std::ostream& out, pfLet[currentHash] = currentRuleID; } + + ProofNodeClusterType proofNodeType = ProofNodeClusterType::NOT_DEFINED; + if (options::printDotClusters()) + { + // Define the type of this node + proofNodeType = defineProofNodeType(pn, parentType); + if (proofNodeType != ProofNodeClusterType::FIRST_SCOPE + && proofNodeType != ProofNodeClusterType::NOT_DEFINED) + { + d_subgraphsStr[static_cast(proofNodeType) - 1] << d_ruleID << " "; + } + } + + printProofNodeInfo(out, pn); + d_ruleID++; + PfRule r = pn->getRule(); + + const std::vector>& children = pn->getChildren(); + for (const std::shared_ptr& c : children) + { + uint64_t childId = printInternal(out, c.get(), pfLet, proofNodeType); + out << "\t" << childId << " -> " << currentRuleID << ";\n"; + } + + // If it's a scope, then remove from the stack + if (isSCOPE(r) && options::printDotClusters()) + { + d_scopesArgs.pop_back(); + } + + return currentRuleID; +} + +void DotPrinter::printProofNodeInfo(std::ostream& out, const ProofNode* pn) +{ std::ostringstream currentArguments, resultStr, classes, colors; - out << "\t" << currentRuleID << " [ label = \"{"; + out << "\t" << d_ruleID << " [ label = \"{"; resultStr << d_lbind.convert(pn->getResult(), "let"); std::string astring = resultStr.str(); @@ -223,63 +279,116 @@ uint64_t DotPrinter::printInternal(std::ostream& out, DotPrinter::ruleArguments(currentArguments, pn); astring = currentArguments.str(); out << "|" << r << sanitizeString(astring) << "}\""; - classes << ", class = \""; - colors << ""; - // set classes and colors, based on the view that the rule belongs - switch (r) - { - case PfRule::SCOPE: - if (scopeCounter < 1) - { - classes << " basic"; - colors << ", color = blue "; - inPropositionalView = true; - } - scopeCounter++; - break; - case PfRule::ASSUME: - // a node can belong to more than one view, so these if's must not be - // exclusive - if (scopeCounter < 2) - { - classes << " basic"; - colors << ", color = blue "; - } - if (inPropositionalView) - { - classes << " propositional"; - colors << ", fillcolor = aquamarine4, style = filled "; - } - break; - case PfRule::CHAIN_RESOLUTION: - case PfRule::FACTORING: - case PfRule::REORDERING: - if (inPropositionalView) - { - classes << " propositional"; - colors << ", fillcolor = aquamarine4, style = filled "; - } - break; - default: inPropositionalView = false; - } - classes << " \""; - out << classes.str() << colors.str(); // add number of subchildren std::map::const_iterator it = d_subpfCounter.find(pn); - out << ", comment = \"{\\\"subProofQty\\\":" << it->second << "}\""; - out << " ];\n"; + out << ", comment = \"{\\\"subProofQty\\\":" << it->second << "}\" ];\n"; +} - const std::vector>& children = pn->getChildren(); - for (const std::shared_ptr& c : children) +ProofNodeClusterType DotPrinter::defineProofNodeType(const ProofNode* pn, + ProofNodeClusterType last) +{ + PfRule rule = pn->getRule(); + if (isSCOPE(rule)) { - uint64_t childId = - printInternal(out, c.get(), pfLet, scopeCounter, inPropositionalView); - out << "\t" << childId << " -> " << currentRuleID << ";\n"; + d_scopesArgs.push_back(pn->getArguments()); } - return currentRuleID; + // If is the first node + if (!d_ruleID) + { + return ProofNodeClusterType::FIRST_SCOPE; + } + // If the rule is in the SAT range and the last node was: FF or SAT + if (isSat(rule) && last <= ProofNodeClusterType::SAT) + { + return ProofNodeClusterType::SAT; + } + // If is a ASSUME + if (isASSUME(rule)) + { + if (isInput(pn)) + { + return ProofNodeClusterType::INPUT; + } + return last; + } + // the last node was: FS, SAT or CNF + if (last <= ProofNodeClusterType::CNF) + { + // If the rule is in the CNF range + if (isCNF(rule)) + { + return ProofNodeClusterType::CNF; + } + // If the first rule after a CNF is a scope + if (isSCOPE(rule)) + { + return ProofNodeClusterType::THEORY_LEMMA; + } + // Is not a scope + return ProofNodeClusterType::PRE_PROCESSING; + } + // If the last rule was pre processing + if (last == ProofNodeClusterType::PRE_PROCESSING) + { + return ProofNodeClusterType::PRE_PROCESSING; + } + // If the last rule was theory lemma + if (last == ProofNodeClusterType::THEORY_LEMMA) + { + return ProofNodeClusterType::THEORY_LEMMA; + } + + return ProofNodeClusterType::NOT_DEFINED; +} + +inline bool DotPrinter::isInput(const ProofNode* pn) +{ + const TNode& thisAssumeArg = pn->getArguments()[0]; + auto& firstScope = d_scopesArgs[0].get(); + + // Verifies if the arg of this assume are in the first scope + if (std::find(firstScope.begin(), firstScope.end(), thisAssumeArg) + == firstScope.end()) + { + return false; + } + + // Verifies if the arg of this assume is at any of the other scopes + for (size_t i = d_scopesArgs.size() - 1; i > 0; i--) + { + auto& args = d_scopesArgs[i].get(); + + if (std::find(args.begin(), args.end(), thisAssumeArg) != args.end()) + { + return false; + } + } + + return true; +} + +inline bool DotPrinter::isSat(const PfRule& rule) +{ + return PfRule::CHAIN_RESOLUTION <= rule + && rule <= PfRule::MACRO_RESOLUTION_TRUST; +} + +inline bool DotPrinter::isCNF(const PfRule& rule) +{ + return PfRule::NOT_NOT_ELIM <= rule && rule <= PfRule::CNF_ITE_NEG3; +} + +inline bool DotPrinter::isSCOPE(const PfRule& rule) +{ + return PfRule::SCOPE == rule; +} + +inline bool DotPrinter::isASSUME(const PfRule& rule) +{ + return PfRule::ASSUME == rule; } void DotPrinter::ruleArguments(std::ostringstream& currentArguments, diff --git a/src/proof/dot/dot_printer.h b/src/proof/dot/dot_printer.h index 175d39b01..f5fe8d25e 100644 --- a/src/proof/dot/dot_printer.h +++ b/src/proof/dot/dot_printer.h @@ -19,6 +19,7 @@ #define CVC5__PROOF__DOT__DOT_PRINTER_H #include +#include #include "printer/let_binding.h" #include "proof/proof_node.h" @@ -26,6 +27,47 @@ namespace cvc5::internal { namespace proof { +/** + * An enumeration for proof nodes cluster type. Each type defines in which + * cluster the proof node will be inserted when printed. + */ +enum class ProofNodeClusterType : uint8_t +{ + // ======== FIRST_SCOPE + // Type of proof node cluster that is always in the root of the graph. + // The rule is always SCOPE. + FIRST_SCOPE = 0, + // ======== SAT + // Type of proof node cluster that is between FIRST_SCOPE and CNF. + // The rules are: CHAIN_RESOLUTION, FACTORING, REORDERING, MACRO_RESOLUTION + // and MACRO_RESOLUTION_TRUST. + SAT, + // ======== CNF + // Type of proof node cluster that is below SAT and above THEORY_LEMMA or + // PRE_PROCESSING. + // The rules, that are described by the PfRule enumeration, are in the range + // between NOT_NOT_ELIM and CNF_ITE_NEG3. + CNF, + // ======== THEORY_LEMMA + // Proof nodes contained in a SCOPE which starts just after a SAT or CNF proof + // cluster. + THEORY_LEMMA, + // ======== PRE_PROCESSING + // Type of proof node cluster that is in the middle of the proof. + // The rules can be of any type. The proof nodes that aren't THEORY_LEMMA + // after CNF are PRE_PROCESSING. Therefore, the root of this cluster type + // can't be a SCOPE proof node. + PRE_PROCESSING, + // ======== INPUT + // Type of proof node that is always a leaf with regard to the FIRST_SCOPE. + // The rules are always ASSUME and the argument assumed by it was only scoped + // by the FIRST_SCOPE and no other SCOPE, i.e., it was not shadowed by an + // inner scope. + INPUT, + // ======== NOT_DEFINED + NOT_DEFINED +}; + class DotPrinter { public: @@ -42,24 +84,30 @@ class DotPrinter private: /** * Print the nodes of the proof in the format: - * $NODE_ID [ label = "{$CONCLUSION|$RULE_NAME($RULE_ARGUMENTS)}", - * $COLORS_AND_CLASSES_RELATED_TO_THE_RULE ]; and then for each child of the + * $NODE_ID [ label = "{$CONCLUSION|$RULE_NAME($RULE_ARGUMENTS)}", comment = + * "{\"subProofQty\":$SUB_PROOF_QUANTITY}" ]; and then for each child of the * node $CHILD_ID -> $NODE_ID; and then recursively calls the function with * 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 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 + * @param pfLet the map of the hashs of proof nodes already printed to their + * ids + * @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, - uint64_t scopeCounter, - bool inPropositionalView); + ProofNodeClusterType parentType); + + /** + * Print the nodes of the proof in the format: + * $NODE_ID [ label = "{$CONCLUSION|$RULE_NAME($RULE_ARGUMENTS)}", comment = + * "{\"subProofQty\":$SUB_PROOF_QUANTITY}" ]; + * @param out the output stream + * @param pn the proof node to print + */ + inline void printProofNodeInfo(std::ostream& out, const ProofNode* pn); /** * Return the arguments of a ProofNode @@ -87,10 +135,56 @@ class DotPrinter /** Traverse proof node and populate d_lbind * - * @param pn the proof node to be traversed + * @param pn The proof node to be traversed */ void letifyResults(const ProofNode* pn); + /** Define the proof node type and populate d_nodesClusterType and + * d_scopesArgs. + * @param pn The proof node to categorize. + * @param last The type of the parent of the current proof node + * @return the current node type + */ + ProofNodeClusterType defineProofNodeType(const ProofNode* pn, + ProofNodeClusterType last); + + /** Whether the proof node is an input node or not. An input is a proof node + * that has an ASSUME rule and the argument assumed by it must be scoped only + * by the FIRST SCOPE. In other words, if there is at least one SCOPE (other + * than the FIRST SCOPE) that is an ancestor of this ASSUME proof node and its + * argument is scoped by this ancestor, then the ASSUME is no longer an input. + * @param pn The proof node to be verified. + * @return The bool indicating if the proof node is or not an input. + */ + inline bool isInput(const ProofNode* pn); + + /** Verify if the rule is in the SAT range (i.e. a PfRule that is + * CHAIN_RESOLUTION, FACTORING, REORDERING, MACRO_RESOLUTION or + * MACRO_RESOLUTION_TRUST). + * @param pn The rule to be verified. + * @return The bool indicating if the rule is or not in the SAT range. + */ + inline bool isSat(const PfRule& rule); + + /** Verify if the rule is in the CNF range (between NOT_NOT_ELIM and + * CNF_ITE_NEG3) in the PfRule enumeration. + * @param pn The rule to be verified. + * @return The bool indicating if the rule is or not in the CNF range. + */ + inline bool isCNF(const PfRule& rule); + + /** Verify if the rule is a SCOPE + * @param pn The rule to be verified. + * @return The bool indicating if the rule is or not a SCOPE. + */ + inline bool isSCOPE(const PfRule& rule); + + /** Verify if the rule is an ASSUME + * @param pn The rule to be verified. + * @return The bool indicating if the rule is or not an ASSUME. + */ + inline bool isASSUME(const PfRule& rule); + /** All unique subproofs of a given proof node (counting itself). */ std::map d_subpfCounter; @@ -99,6 +193,13 @@ class DotPrinter /** Counter that indicates the current rule ID */ uint64_t d_ruleID; + + /** The arguments (assumptions), per level, of all scopes under which the + * traversal is currently under. */ + std::vector>> d_scopesArgs; + + /** All the subgraph description strings */ + std::vector d_subgraphsStr; }; } // namespace proof