1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
|
/******************************************************************************
* Top contributors (to current version):
* Diego Della Rocca de Camargos
*
* This file is part of the cvc5 project.
*
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
* in the top-level source directory and their institutional affiliations.
* All rights reserved. See the file COPYING in the top-level source
* directory for licensing information.
* ****************************************************************************
*
* Implemantation of the module for printing dot proofs.
*/
#include "proof/dot/dot_printer.h"
#include <sstream>
#include "expr/proof_checker.h"
#include "expr/proof_node_manager.h"
#include "printer/smt2/smt2_printer.h"
#include "theory/builtin/proof_checker.h"
namespace cvc5 {
namespace proof {
void DotPrinter::cleanQuotes(std::string& s)
{
std::string rep("\\\"");
for (size_t pos = 0; (pos = s.find("\"", pos)) != std::string::npos;
pos += rep.length())
{
s.replace(pos, rep.length() - 1, rep);
}
}
void DotPrinter::print(std::ostream& out, const ProofNode* pn)
{
uint64_t ruleID = 0;
out << "digraph proof {\n";
DotPrinter::printInternal(out, pn, ruleID);
out << "}\n";
}
void DotPrinter::printInternal(std::ostream& out,
const ProofNode* pn,
uint64_t& ruleID)
{
uint64_t currentRuleID = ruleID;
PfRule r = pn->getRule();
out << "\t\"" << currentRuleID << "\" [ shape = \"box\", label = \"" << r;
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);
out << astring << "\" ];\n\t\"" << currentRuleID << "\" -> \""
<< currentRuleID << "c\";\n";
for (const std::shared_ptr<ProofNode>& c : children)
{
++ruleID;
out << "\t\"" << ruleID << "c\" -> \"" << currentRuleID << "\";\n";
printInternal(out, c.get(), ruleID);
}
}
void DotPrinter::ruleArguments(std::ostringstream& currentArguments,
const ProofNode* pn)
{
const std::vector<Node>& args = pn->getArguments();
PfRule r = pn->getRule();
// don't process arguments of rules whose conclusion is in the arguments
if (!args.size() || r == PfRule::ASSUME || r == PfRule::REORDERING
|| r == PfRule::REFL)
{
return;
}
currentArguments << " :args [ ";
// if cong, special process
if (r == PfRule::CONG)
{
AlwaysAssert(args.size() == 1 || args.size() == 2);
// if two arguments, ignore first and print second
if (args.size() == 2)
{
currentArguments << args[1];
}
else
{
Kind k;
ProofRuleChecker::getKind(args[0], k);
currentArguments << printer::smt2::Smt2Printer::smtKindString(k);
}
}
// if th_rw, likewise
else if (r == PfRule::THEORY_REWRITE)
{
// print the second argument
theory::TheoryId id;
theory::builtin::BuiltinProofRuleChecker::getTheoryId(args[1], id);
std::ostringstream ss;
ss << id;
std::string s = ss.str();
// delete "THEORY_" prefix
s.erase(0, 7);
currentArguments << s;
}
else
{
currentArguments << args[0];
for (size_t i = 1, size = args.size(); i < size; i++)
{
currentArguments << ", " << args[i];
}
}
currentArguments << " ]";
}
} // namespace proof
} // namespace cvc5
|
