From 7e85adc022bc10e2a2b95bd42e216ddddd51e03e Mon Sep 17 00:00:00 2001 From: Diego Della Rocca de Camargos Date: Mon, 26 Apr 2021 14:36:55 -0300 Subject: [PATCH] New design in DOT representation, nodes colored based on visions(basic and propositional) (#6423) Conclusion and rule are placed on the same node (records nodes in the dot format). Nodes are colored based on the view they will belong to. Signed-off-by: Diego Della Rocca de Camargos diegodellarocc@gmail.com --- src/proof/dot/dot_printer.cpp | 105 +++++++++++++++++++++++++--------- src/proof/dot/dot_printer.h | 28 +++++---- 2 files changed, 96 insertions(+), 37 deletions(-) diff --git a/src/proof/dot/dot_printer.cpp b/src/proof/dot/dot_printer.cpp index 4f13ef17a..4ba409d6d 100644 --- a/src/proof/dot/dot_printer.cpp +++ b/src/proof/dot/dot_printer.cpp @@ -25,55 +25,108 @@ namespace cvc5 { namespace proof { -void DotPrinter::cleanQuotes(std::string& s) +std::string DotPrinter::sanitizeString(const std::string& s) { - std::string rep("\\\""); - for (size_t pos = 0; (pos = s.find("\"", pos)) != std::string::npos; - pos += rep.length()) + std::string newS; + newS.reserve(s.size()); + for (const char c : s) { - s.replace(pos, rep.length() - 1, rep); + switch (c) + { + case '\"': newS += "\\\""; break; + case '>': newS += "\\>"; break; + case '<': newS += "\\<"; break; + case '{': newS += "\\{"; break; + case '}': newS += "\\}"; break; + case '|': newS += "\\|"; break; + default: newS += c; break; + } } + + return newS; } void DotPrinter::print(std::ostream& out, const ProofNode* pn) { uint64_t ruleID = 0; - out << "digraph proof {\n"; - DotPrinter::printInternal(out, pn, ruleID); + // 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); out << "}\n"; } void DotPrinter::printInternal(std::ostream& out, const ProofNode* pn, - uint64_t& ruleID) + uint64_t& ruleID, + uint64_t scopeCounter, + bool inPropositionalView) { uint64_t currentRuleID = ruleID; - PfRule r = pn->getRule(); + const std::vector>& children = pn->getChildren(); + std::ostringstream currentArguments, resultStr, classes, colors; - out << "\t\"" << currentRuleID << "\" [ shape = \"box\", label = \"" << r; + out << "\t" << currentRuleID << " [ label = \"{"; - std::ostringstream currentArguments, resultStr; - const std::vector>& children = pn->getChildren(); - DotPrinter::ruleArguments(currentArguments, pn); - // guarantee that arguments do not have unescaped quotes - std::string astring = currentArguments.str(); - cleanQuotes(astring); - out << astring << "\"];\n\t\"" << currentRuleID - << "c\" [ shape = \"ellipse\", label = \""; - // guarantee that conclusion does not have unescaped quotes resultStr << pn->getResult(); - astring = resultStr.str(); - cleanQuotes(astring); + std::string astring = resultStr.str(); + out << sanitizeString(astring); + + PfRule r = pn->getRule(); + DotPrinter::ruleArguments(currentArguments, pn); + astring = currentArguments.str(); + out << "|" << r << sanitizeString(astring) << "}\""; + classes << ", class = \""; + colors << ""; - out << astring << "\" ];\n\t\"" << currentRuleID << "\" -> \"" - << currentRuleID << "c\";\n"; + // 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(); + out << " ];\n"; for (const std::shared_ptr& c : children) { ++ruleID; - out << "\t\"" << ruleID << "c\" -> \"" << currentRuleID << "\";\n"; - printInternal(out, c.get(), ruleID); + out << "\t" << ruleID << " -> " << currentRuleID << ";\n"; + printInternal(out, c.get(), ruleID, scopeCounter, inPropositionalView); } } @@ -131,4 +184,4 @@ void DotPrinter::ruleArguments(std::ostringstream& currentArguments, } } // namespace proof -} // namespace cvc5 +} // namespace cvc5 \ No newline at end of file diff --git a/src/proof/dot/dot_printer.h b/src/proof/dot/dot_printer.h index 368f84ccf..6e6785080 100644 --- a/src/proof/dot/dot_printer.h +++ b/src/proof/dot/dot_printer.h @@ -40,19 +40,24 @@ class DotPrinter private: /** - * Print the rule in the format: - * "$RULE_ID $RULE_NAME($RULE_ARGUMENTS)" [ shape = "box"]; - * "$RULE_ID $RULE_NAME($RULE_ARGUMENTS)" -> "$RULE_ID $RULE_CONCLUSION"; - * and then for each child of the rule print - * "$CHILD_ID $CHILD_CONCLUSION" -> "$RULE_ID $RULE_NAME($RULE_ARGUMENTS)"; - * and then recursively call the function with the child as argument. + * 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 $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 ruleID the id of the rule to print + * @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 */ static void printInternal(std::ostream& out, const ProofNode* pn, - uint64_t& ruleID); + uint64_t& ruleID, + uint64_t scopeCounter, + bool inPropositionalView); /** * Return the arguments of a ProofNode @@ -63,13 +68,14 @@ class DotPrinter static void ruleArguments(std::ostringstream& currentArguments, const ProofNode* pn); - /** Replace all quotes but escaped quotes in given string - * @param s The string to have the quotes processed. + /** Add an escape character before special characters of the given string. + * @param s The string to have the characters processed. + * @return The string with the special characters escaped. */ - static void cleanQuotes(std::string& s); + static std::string sanitizeString(const std::string& s); }; } // namespace proof } // namespace cvc5 -#endif +#endif \ No newline at end of file -- 2.30.2