summaryrefslogtreecommitdiff
path: root/src/proof
diff options
context:
space:
mode:
authorDiego Della Rocca de Camargos <diegodellarocc@gmail.com>2021-08-04 18:45:29 -0300
committerGitHub <noreply@github.com>2021-08-04 21:45:29 +0000
commit25b0456328224186ec699b6dc10d49c077dfb8a2 (patch)
treee5cc17a87de5ddda8d9352bfadbad57cf5d67331 /src/proof
parent9c459e04f32f243a58d5afb6687bd8c5f423ac93 (diff)
[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
Diffstat (limited to 'src/proof')
-rw-r--r--src/proof/dot/dot_printer.cpp10
1 files changed, 5 insertions, 5 deletions
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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback