[proof] [dot] Print let map (of terms in proof) as part of dot proof (#6853)

The let map is printed as JSON-like dictionary via a comment of the dot output.

2 files changed, 99 insertions, 5 deletions

diff --git a/src/proof/dot/dot_printer.cpp b/src/proof/dot/dot_printer.cpp
index 496085372..9c26c0c24 100644
--- a/src/proof/dot/dot_printer.cpp
+++ b/src/proof/dot/dot_printer.cpp
@@ -17,6 +17,7 @@
 
 #include <sstream>
 
+#include "options/expr_options.h"
 #include "printer/smt2/smt2_printer.h"
 #include "proof/proof_checker.h"
 #include "proof/proof_node_manager.h"
@@ -25,9 +26,34 @@
 namespace cvc5 {
 namespace proof {
 
-DotPrinter::DotPrinter() {}
+DotPrinter::DotPrinter()
+    : d_lbind(options::defaultDagThresh() ? options::defaultDagThresh() + 1 : 0)
+{
+}
+
 DotPrinter::~DotPrinter() {}
 
+std::string DotPrinter::sanitizeStringDoubleQuotes(const std::string& s)
+{
+  std::string newS;
+  newS.reserve(s.size());
+  for (const char c : s)
+  {
+    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;
+}
+
 std::string DotPrinter::sanitizeString(const std::string& s)
 {
   std::string newS;
@@ -87,15 +113,71 @@ void DotPrinter::countSubproofs(const ProofNode* pn)
   } while (!visit.empty());
 }
 
+void DotPrinter::letifyResults(const ProofNode* pn)
+{
+  std::vector<const ProofNode*> visit;
+  std::unordered_set<const ProofNode*> visited;
+  std::unordered_set<const ProofNode*>::iterator it;
+  const ProofNode* cur;
+  visit.push_back(pn);
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    it = visited.find(cur);
+    if (it == visited.end())
+    {
+      d_lbind.process(cur->getResult());
+      visited.insert(cur);
+      const std::vector<std::shared_ptr<ProofNode>>& children =
+          cur->getChildren();
+      for (const std::shared_ptr<ProofNode>& c : children)
+      {
+        visit.push_back(c.get());
+      }
+    }
+  } while (!visit.empty());
+}
+
 void DotPrinter::print(std::ostream& out, const ProofNode* pn)
 {
   uint64_t ruleID = 0;
   countSubproofs(pn);
+  letifyResults(pn);
 
   // 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";
+  // print let map
+  std::vector<Node> letList;
+  d_lbind.letify(letList);
+  if (!letList.empty())
+  {
+    out << "\tcomment=\"{\"letMap\" : {";
+    bool first = true;
+    for (TNode n : letList)
+    {
+      size_t id = d_lbind.getId(n);
+      Assert(id != 0);
+      if (!first)
+      {
+        out << ", ";
+      }
+      else
+      {
+        first = false;
+      }
+      out << "\"let" << id << "\" : \"";
+      std::ostringstream nStr;
+      nStr << d_lbind.convert(n, "let", false);
+      std::string astring = nStr.str();
+      // we double the scaping of quotes because "simple scape" is ambiguous
+      // with the scape of the delimiter of the value in the key-value map
+      out << sanitizeStringDoubleQuotes(astring) << "\"";
+    }
+    out << "}}\"\n";
+  }
   DotPrinter::printInternal(out, pn, ruleID, 0, false);
   out << "}\n";
 }
@@ -112,7 +194,7 @@ void DotPrinter::printInternal(std::ostream& out,
 
   out << "\t" << currentRuleID << " [ label = \"{";
 
-  resultStr << pn->getResult();
+  resultStr << d_lbind.convert(pn->getResult(), "let");
   std::string astring = resultStr.str();
   out << sanitizeString(astring);
 
@@ -196,7 +278,7 @@ void DotPrinter::ruleArguments(std::ostringstream& currentArguments,
     // if two arguments, ignore first and print second
     if (args.size() == 2)
     {
-      currentArguments << args[1];
+      currentArguments << d_lbind.convert(args[1], "let");
     }
     else
     {
@@ -220,10 +302,10 @@ void DotPrinter::ruleArguments(std::ostringstream& currentArguments,
   }
   else
   {
-    currentArguments << args[0];
+    currentArguments << d_lbind.convert(args[0], "let");
     for (size_t i = 1, size = args.size(); i < size; i++)
     {
-      currentArguments << ", " << args[i];
+      currentArguments << ", " << d_lbind.convert(args[i], "let");
     }
   }
   currentArguments << " ]";
diff --git a/src/proof/dot/dot_printer.h b/src/proof/dot/dot_printer.h
index 2d25fe0e7..9cc03a258 100644
--- a/src/proof/dot/dot_printer.h
+++ b/src/proof/dot/dot_printer.h
@@ -20,6 +20,7 @@
 
 #include <iostream>
 
+#include "printer/let_binding.h"
 #include "proof/proof_node.h"
 
 namespace cvc5 {
@@ -73,6 +74,9 @@ class DotPrinter
    */
   static std::string sanitizeString(const std::string& s);
 
+  /** As above, but quotes are doubly escaped. */
+  static std::string sanitizeStringDoubleQuotes(const std::string& s);
+
   /** Traverse proof node and populate d_subpfCounter, mapping each proof node
    * to the number of subproofs it contains, including itself
    *
@@ -80,9 +84,17 @@ class DotPrinter
    */
   void countSubproofs(const ProofNode* pn);
 
+  /** Traverse proof node and populate d_lbind
+   *
+   * @param pn the proof node to be traversed
+   */
+  void letifyResults(const ProofNode* pn);
+
   /** All unique subproofs of a given proof node (counting itself). */
   std::map<const ProofNode*, size_t> d_subpfCounter;
 
+  /** Let binder for terms in proof nodes */
+  LetBinding d_lbind;
 };
 
 }  // namespace proof