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

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<std::shared_ptr<ProofNode>>& 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<std::shared_ptr<ProofNode>>& 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<ProofNode>& 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