From: Diego Della Rocca de Camargos <diegodellarocc@gmail.com>
Date: Wed, 4 Aug 2021 21:45:29 +0000 (-0300)
Subject: [proof] [dot] Fix comments on dot printer (#6983)
X-Git-Tag: cvc5-1.0.0~1403
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=25b0456328224186ec699b6dc10d49c077dfb8a2;p=cvc5.git

[proof] [dot] Fix comments on dot printer (#6983)

This PR fixes the escaped characters in the dot printer. The output is now a valid DOT.

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 9c26c0c24..0e8d1a057 100644
--- a/src/proof/dot/dot_printer.cpp
+++ b/src/proof/dot/dot_printer.cpp
@@ -154,7 +154,7 @@ void DotPrinter::print(std::ostream& out, const ProofNode* pn)
   d_lbind.letify(letList);
   if (!letList.empty())
   {
-    out << "\tcomment=\"{\"letMap\" : {";
+    out << "\tcomment=\"{\\\"letMap\\\" : {";
     bool first = true;
     for (TNode n : letList)
     {
@@ -168,15 +168,15 @@ void DotPrinter::print(std::ostream& out, const ProofNode* pn)
       {
         first = false;
       }
-      out << "\"let" << id << "\" : \"";
+      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 << sanitizeStringDoubleQuotes(astring) << "\\\"";
     }
-    out << "}}\"\n";
+    out << "}}\";\n";
   }
   DotPrinter::printInternal(out, pn, ruleID, 0, false);
   out << "}\n";
@@ -247,7 +247,7 @@ void DotPrinter::printInternal(std::ostream& out,
   // add number of subchildren
   std::map<const ProofNode*, size_t>::const_iterator it =
       d_subpfCounter.find(pn);
-  out << ", comment = \"\{\"subProofQty\":" << it->second << "}\"";
+  out << ", comment = \"{\\\"subProofQty\\\":" << it->second << "}\"";
   out << " ];\n";
 
   for (const std::shared_ptr<ProofNode>& c : children)