New design in DOT representation, nodes colored based on visions(basic and propositio...

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

diff --git a/src/proof/dot/dot_printer.cpp b/src/proof/dot/dot_printer.cpp
index 4f13ef17a57cc86e86d840d6e82bd3b8eca51a40..4ba409d6d2741a7ceda862fc2a14a2b9b16182a1 100644 (file)
--- 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 368f84ccf0fe872666564cc3c072bd5a38337e29..6e6785080f7d5702bd641e6f3e785f3c55e85cfd 100644 (file)
--- 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