Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * VinÃcius Braga Freire, Haniel Barbosa, Diego Della Rocca de Camargos
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 by the authors listed in the file AUTHORS
8 : : * in the top-level source directory and their institutional affiliations.
9 : : * All rights reserved. See the file COPYING in the top-level source
10 : : * directory for licensing information.
11 : : * ****************************************************************************
12 : : *
13 : : * Implemantation of the module for printing dot proofs.
14 : : */
15 : :
16 : : #include "proof/dot/dot_printer.h"
17 : :
18 : : #include <algorithm>
19 : : #include <sstream>
20 : :
21 : : #include "options/expr_options.h"
22 : : #include "options/printer_options.h"
23 : : #include "options/proof_options.h"
24 : : #include "printer/smt2/smt2_printer.h"
25 : : #include "proof/proof_checker.h"
26 : : #include "proof/proof_node_algorithm.h"
27 : : #include "proof/proof_node_manager.h"
28 : : #include "proof/trust_id.h"
29 : : #include "theory/builtin/proof_checker.h"
30 : :
31 : : namespace cvc5::internal {
32 : : namespace proof {
33 : :
34 : 0 : DotPrinter::DotPrinter(Env& env)
35 : : : EnvObj(env),
36 : : d_lbind(
37 : : "let",
38 : 0 : options().printer.dagThresh ? options().printer.dagThresh + 1 : 0),
39 [ - - ]: 0 : d_ruleID(0)
40 : : {
41 : 0 : const std::string acronyms[5] = {"SAT", "CNF", "TL", "PP", "IN"};
42 : 0 : const std::string colors[5] = {"purple", "yellow", "green", "brown", "blue"};
43 : :
44 [ - - ]: 0 : for (unsigned i = 0; i < 5; i++)
45 : : {
46 : 0 : d_subgraphsStr.push_back(std::ostringstream());
47 : 0 : d_subgraphsStr[i] << "\n\tsubgraph cluster_" << acronyms[i]
48 : 0 : << " {\n\t\tlabel=\"" << acronyms[i]
49 : 0 : << "\"\n\t\tbgcolor=\"" << colors[i] << "\"\n\t\t";
50 : : }
51 : 0 : }
52 : :
53 : 0 : DotPrinter::~DotPrinter() {}
54 : :
55 : 0 : std::string DotPrinter::sanitizeStringDoubleQuotes(const std::string& s)
56 : : {
57 : 0 : std::string newS;
58 : 0 : newS.reserve(s.size());
59 [ - - ]: 0 : for (const char c : s)
60 : : {
61 [ - - ][ - - ]: 0 : switch (c)
[ - - ][ - ]
62 : : {
63 : 0 : case '\"': newS += "\\\\\\\""; break;
64 : 0 : case '>': newS += "\\>"; break;
65 : 0 : case '<': newS += "\\<"; break;
66 : 0 : case '{': newS += "\\{"; break;
67 : 0 : case '}': newS += "\\}"; break;
68 : 0 : case '|': newS += "\\|"; break;
69 : 0 : default: newS += c; break;
70 : : }
71 : : }
72 : :
73 : 0 : return newS;
74 : : }
75 : :
76 : 0 : std::string DotPrinter::sanitizeString(const std::string& s)
77 : : {
78 : 0 : std::string newS;
79 : 0 : newS.reserve(s.size());
80 [ - - ]: 0 : for (const char c : s)
81 : : {
82 [ - - ][ - - ]: 0 : switch (c)
[ - - ][ - ]
83 : : {
84 : 0 : case '\"': newS += "\\\""; break;
85 : 0 : case '>': newS += "\\>"; break;
86 : 0 : case '<': newS += "\\<"; break;
87 : 0 : case '{': newS += "\\{"; break;
88 : 0 : case '}': newS += "\\}"; break;
89 : 0 : case '|': newS += "\\|"; break;
90 : 0 : default: newS += c; break;
91 : : }
92 : : }
93 : :
94 : 0 : return newS;
95 : : }
96 : :
97 : 0 : void DotPrinter::countSubproofs(const ProofNode* pn)
98 : : {
99 : 0 : std::vector<const ProofNode*> visit;
100 : 0 : std::unordered_map<const ProofNode*, bool> visited;
101 : 0 : std::unordered_map<const ProofNode*, bool>::iterator it;
102 : : const ProofNode* cur;
103 : 0 : visit.push_back(pn);
104 : 0 : do
105 : : {
106 : 0 : cur = visit.back();
107 : 0 : visit.pop_back();
108 : 0 : it = visited.find(cur);
109 [ - - ]: 0 : if (it == visited.end())
110 : : {
111 : 0 : visited[cur] = false;
112 : 0 : visit.push_back(cur);
113 : : const std::vector<std::shared_ptr<ProofNode>>& children =
114 : 0 : cur->getChildren();
115 [ - - ]: 0 : for (const std::shared_ptr<ProofNode>& c : children)
116 : : {
117 : 0 : visit.push_back(c.get());
118 : : }
119 : : }
120 [ - - ]: 0 : else if (!it->second)
121 : : {
122 : 0 : visited[cur] = true;
123 : 0 : size_t counter = 1;
124 : : const std::vector<std::shared_ptr<ProofNode>>& children =
125 : 0 : cur->getChildren();
126 [ - - ]: 0 : for (const std::shared_ptr<ProofNode>& c : children)
127 : : {
128 : 0 : counter += d_subpfCounter[c.get()];
129 : : }
130 : 0 : d_subpfCounter[cur] = counter;
131 : : }
132 [ - - ]: 0 : } while (!visit.empty());
133 : 0 : }
134 : :
135 : 0 : void DotPrinter::letifyResults(const ProofNode* pn)
136 : : {
137 : 0 : std::vector<const ProofNode*> visit;
138 : 0 : std::unordered_set<const ProofNode*> visited;
139 : 0 : std::unordered_set<const ProofNode*>::iterator it;
140 : : const ProofNode* cur;
141 : 0 : visit.push_back(pn);
142 : 0 : do
143 : : {
144 : 0 : cur = visit.back();
145 : 0 : visit.pop_back();
146 : 0 : it = visited.find(cur);
147 [ - - ]: 0 : if (it == visited.end())
148 : : {
149 : 0 : d_lbind.process(cur->getResult());
150 : 0 : visited.insert(cur);
151 : : const std::vector<std::shared_ptr<ProofNode>>& children =
152 : 0 : cur->getChildren();
153 [ - - ]: 0 : for (const std::shared_ptr<ProofNode>& c : children)
154 : : {
155 : 0 : visit.push_back(c.get());
156 : : }
157 : : }
158 [ - - ]: 0 : } while (!visit.empty());
159 : 0 : }
160 : :
161 : 0 : void DotPrinter::print(std::ostream& out, const ProofNode* pn)
162 : : {
163 : 0 : countSubproofs(pn);
164 : 0 : letifyResults(pn);
165 : :
166 : : // The dot attribute rankdir="BT" sets the direction of the graph layout,
167 : : // placing the root node at the top. The "node [shape..." attribute sets the
168 : : // shape of all nodes to record.
169 : 0 : out << "digraph proof {\n\trankdir=\"BT\";\n\tnode [shape=record];\n";
170 : : // print let map
171 : 0 : std::vector<Node> letList;
172 : 0 : d_lbind.letify(letList);
173 [ - - ]: 0 : if (!letList.empty())
174 : : {
175 : 0 : out << "\tcomment=\"{\\\"letMap\\\" : {";
176 : 0 : bool first = true;
177 [ - - ]: 0 : for (TNode n : letList)
178 : : {
179 : 0 : size_t id = d_lbind.getId(n);
180 : 0 : Assert(id != 0);
181 [ - - ]: 0 : if (!first)
182 : : {
183 : 0 : out << ", ";
184 : : }
185 : : else
186 : : {
187 : 0 : first = false;
188 : : }
189 : 0 : out << "\\\"let" << id << "\\\" : \\\"";
190 : 0 : std::ostringstream nStr;
191 : 0 : nStr << d_lbind.convert(n, false);
192 : 0 : std::string astring = nStr.str();
193 : : // we double the scaping of quotes because "simple scape" is ambiguous
194 : : // with the scape of the delimiter of the value in the key-value map
195 : 0 : out << sanitizeStringDoubleQuotes(astring) << "\\\"";
196 : : }
197 : 0 : out << "}}\";\n";
198 : : }
199 : :
200 : 0 : std::map<size_t, uint64_t> proofLet;
201 : 0 : std::map<size_t, uint64_t> firstScopeLet;
202 : 0 : std::unordered_map<const ProofNode*, bool> cfaMap;
203 : 0 : std::vector<size_t> ancestorHashs;
204 : :
205 : 0 : DotPrinter::printInternal(out,
206 : : pn,
207 : : proofLet,
208 : : firstScopeLet,
209 : : cfaMap,
210 : : ancestorHashs,
211 : : ProofNodeClusterType::NOT_DEFINED);
212 : :
213 [ - - ]: 0 : if (options().proof.printDotClusters)
214 : : {
215 : : // Print the sub-graphs
216 [ - - ]: 0 : for (unsigned i = 0; i < 5; i++)
217 : : {
218 : 0 : out << d_subgraphsStr[i].str() << "\n\t};";
219 : : }
220 : : }
221 : 0 : out << "\n}\n";
222 : 0 : }
223 : :
224 : 0 : uint64_t DotPrinter::printInternal(
225 : : std::ostream& out,
226 : : const ProofNode* pn,
227 : : std::map<size_t, uint64_t>& pfLetClosed,
228 : : std::map<size_t, uint64_t>& pfLetOpen,
229 : : std::unordered_map<const ProofNode*, bool>& cfaMap,
230 : : std::vector<size_t>& ancestorHashs,
231 : : ProofNodeClusterType parentType)
232 : : {
233 : 0 : uint64_t currentRuleID = d_ruleID;
234 : :
235 : : // Print DAG option enabled
236 [ - - ]: 0 : if (options().proof.printDotAsDAG)
237 : : {
238 : : ProofNodeHashFunction hasher;
239 : 0 : size_t currentHash = hasher(pn);
240 : :
241 : 0 : std::vector<size_t>::iterator oldEnd = ancestorHashs.end();
242 : : // Search if the current hash is in the vector
243 : : std::vector<size_t>::iterator it =
244 : 0 : std::find(ancestorHashs.begin(), ancestorHashs.end(), currentHash);
245 : :
246 : : // Register the current proof node hash in the ancestor vector
247 : 0 : ancestorHashs.push_back(currentHash);
248 : :
249 : : // we only consider sharing when this would not introduce a cycle, which
250 : : // would be the case if this hash is occurring under a proof node with the
251 : : // same hash (this can happen since our hash computation only takes into
252 : : // account the immediate descendants of a proof node, the limit of hash
253 : : // representation notwithstanding)
254 [ - - ]: 0 : if (it == oldEnd)
255 : : {
256 : 0 : auto openProofIt = pfLetOpen.find(currentHash);
257 : :
258 [ - - ]: 0 : if (openProofIt != pfLetOpen.end())
259 : : {
260 : 0 : return openProofIt->second;
261 : : }
262 : :
263 : 0 : auto proofIt = pfLetClosed.find(currentHash);
264 : : // If this node has been already saved to the global cache of closed proof
265 : : // nodes
266 [ - - ]: 0 : if (proofIt != pfLetClosed.end())
267 : : {
268 : 0 : Assert(!expr::containsAssumption(pn, cfaMap));
269 : 0 : return proofIt->second;
270 : : }
271 : : // If this proof node is closed, we add it to the global cache
272 [ - - ]: 0 : if (!expr::containsAssumption(pn, cfaMap))
273 : : {
274 : 0 : pfLetClosed[currentHash] = currentRuleID;
275 : : }
276 : 0 : pfLetOpen[currentHash] = currentRuleID;
277 : : }
278 : : }
279 : :
280 : 0 : ProofNodeClusterType proofNodeType = ProofNodeClusterType::NOT_DEFINED;
281 [ - - ]: 0 : if (options().proof.printDotClusters)
282 : : {
283 : : // Define the type of this node
284 : 0 : proofNodeType = defineProofNodeType(pn, parentType);
285 [ - - ]: 0 : if (proofNodeType != ProofNodeClusterType::FIRST_SCOPE
286 [ - - ]: 0 : && proofNodeType != ProofNodeClusterType::NOT_DEFINED)
287 : : {
288 : 0 : d_subgraphsStr[static_cast<int>(proofNodeType) - 1] << d_ruleID << " ";
289 : : }
290 : : }
291 : :
292 : 0 : printProofNodeInfo(out, pn);
293 : :
294 : 0 : d_ruleID++;
295 : :
296 : 0 : ProofRule r = pn->getRule();
297 : :
298 : : // Scopes trigger a traversal with a new local cache for proof nodes
299 [ - - ][ - - ]: 0 : if (isSCOPE(r) && currentRuleID)
[ - - ]
300 : : {
301 : : // create a new pfLet
302 : 0 : std::map<size_t, uint64_t> thisScopeLet;
303 : 0 : uint64_t childId = printInternal(out,
304 : 0 : pn->getChildren()[0].get(),
305 : : pfLetClosed,
306 : : thisScopeLet,
307 : : cfaMap,
308 : : ancestorHashs,
309 : : proofNodeType);
310 : 0 : out << "\t" << childId << " -> " << currentRuleID << ";\n";
311 [ - - ]: 0 : if (options().proof.printDotAsDAG)
312 : : {
313 : 0 : ancestorHashs.pop_back();
314 : : }
315 : : }
316 : : else
317 : : {
318 : 0 : const std::vector<std::shared_ptr<ProofNode>>& children = pn->getChildren();
319 [ - - ]: 0 : for (const std::shared_ptr<ProofNode>& c : children)
320 : : {
321 : 0 : uint64_t childId = printInternal(out,
322 : 0 : c.get(),
323 : : pfLetClosed,
324 : : pfLetOpen,
325 : : cfaMap,
326 : : ancestorHashs,
327 : : proofNodeType);
328 : 0 : out << "\t" << childId << " -> " << currentRuleID << ";\n";
329 [ - - ]: 0 : if (options().proof.printDotAsDAG)
330 : : {
331 : 0 : ancestorHashs.pop_back();
332 : : }
333 : : }
334 : : }
335 : :
336 : : // If it's a scope, then remove from the stack
337 : 0 : if (isSCOPE(r) && options().proof.printDotClusters)
338 : : {
339 : 0 : d_scopesArgs.pop_back();
340 : : }
341 : :
342 : 0 : return currentRuleID;
343 : : }
344 : :
345 : 0 : void DotPrinter::printProofNodeInfo(std::ostream& out, const ProofNode* pn)
346 : : {
347 : 0 : std::ostringstream currentArguments, resultStr, classes, colors;
348 : :
349 : 0 : out << "\t" << d_ruleID << " [ label = \"{";
350 : :
351 : 0 : resultStr << d_lbind.convert(pn->getResult());
352 : 0 : std::string astring = resultStr.str();
353 : 0 : out << sanitizeString(astring);
354 : :
355 : 0 : ProofRule r = pn->getRule();
356 : 0 : DotPrinter::ruleArguments(currentArguments, pn);
357 : 0 : astring = currentArguments.str();
358 : 0 : out << "|" << r << sanitizeString(astring) << "}\"";
359 : :
360 : : // add number of subchildren
361 : : std::map<const ProofNode*, size_t>::const_iterator it =
362 : 0 : d_subpfCounter.find(pn);
363 : 0 : out << ", comment = \"{\\\"subProofQty\\\":" << it->second << "}\" ];\n";
364 : 0 : }
365 : :
366 : 0 : ProofNodeClusterType DotPrinter::defineProofNodeType(const ProofNode* pn,
367 : : ProofNodeClusterType last)
368 : : {
369 : 0 : ProofRule rule = pn->getRule();
370 [ - - ]: 0 : if (isSCOPE(rule))
371 : : {
372 : 0 : d_scopesArgs.push_back(pn->getArguments());
373 : : }
374 : :
375 : : // If is the first node
376 [ - - ]: 0 : if (!d_ruleID)
377 : : {
378 : 0 : return ProofNodeClusterType::FIRST_SCOPE;
379 : : }
380 : : // If the rule is in the SAT range and the last node was: FF or SAT
381 [ - - ][ - - ]: 0 : if (last <= ProofNodeClusterType::SAT && isSat(rule))
[ - - ]
382 : : {
383 : 0 : return ProofNodeClusterType::SAT;
384 : : }
385 : : // If is a ASSUME
386 [ - - ]: 0 : if (isASSUME(rule))
387 : : {
388 [ - - ]: 0 : if (isInput(pn))
389 : : {
390 : 0 : return ProofNodeClusterType::INPUT;
391 : : }
392 : 0 : return last;
393 : : }
394 : : // the last node was: FS, SAT or CNF
395 [ - - ]: 0 : if (last <= ProofNodeClusterType::CNF)
396 : : {
397 : : // If the rule is in the CNF range
398 [ - - ]: 0 : if (isCNF(rule))
399 : : {
400 : 0 : return ProofNodeClusterType::CNF;
401 : : }
402 : : // If the first rule after a CNF is in the TL range
403 [ - - ]: 0 : if (isTheoryLemma(pn))
404 : : {
405 : 0 : return ProofNodeClusterType::THEORY_LEMMA;
406 : : }
407 : : // Is not a scope
408 : 0 : return ProofNodeClusterType::PRE_PROCESSING;
409 : : }
410 : : // If the last rule was pre processing
411 [ - - ]: 0 : if (last == ProofNodeClusterType::PRE_PROCESSING)
412 : : {
413 : 0 : return ProofNodeClusterType::PRE_PROCESSING;
414 : : }
415 : : // If the last rule was theory lemma
416 [ - - ]: 0 : if (last == ProofNodeClusterType::THEORY_LEMMA)
417 : : {
418 : 0 : return ProofNodeClusterType::THEORY_LEMMA;
419 : : }
420 : :
421 : 0 : return ProofNodeClusterType::NOT_DEFINED;
422 : : }
423 : :
424 : 0 : inline bool DotPrinter::isInput(const ProofNode* pn)
425 : : {
426 : 0 : const TNode& thisAssumeArg = pn->getArguments()[0];
427 : 0 : auto& firstScope = d_scopesArgs[0].get();
428 : :
429 : : // Verifies if the arg of this assume are in the first scope
430 : 0 : if (std::find(firstScope.begin(), firstScope.end(), thisAssumeArg)
431 [ - - ]: 0 : == firstScope.end())
432 : : {
433 : 0 : return false;
434 : : }
435 : :
436 : : // Verifies if the arg of this assume is at any of the other scopes
437 [ - - ]: 0 : for (size_t i = d_scopesArgs.size() - 1; i > 0; i--)
438 : : {
439 : 0 : auto& args = d_scopesArgs[i].get();
440 : :
441 [ - - ]: 0 : if (std::find(args.begin(), args.end(), thisAssumeArg) != args.end())
442 : : {
443 : 0 : return false;
444 : : }
445 : : }
446 : :
447 : 0 : return true;
448 : : }
449 : :
450 : 0 : inline bool DotPrinter::isSat(const ProofRule& rule)
451 : : {
452 : 0 : return ProofRule::CHAIN_RESOLUTION <= rule
453 [ - - ][ - - ]: 0 : && rule <= ProofRule::MACRO_RESOLUTION_TRUST;
454 : : }
455 : :
456 : 0 : inline bool DotPrinter::isCNF(const ProofRule& rule)
457 : : {
458 [ - - ][ - - ]: 0 : return ProofRule::NOT_NOT_ELIM <= rule && rule <= ProofRule::CNF_ITE_NEG3;
459 : : }
460 : :
461 : 0 : inline bool DotPrinter::isSCOPE(const ProofRule& rule)
462 : : {
463 : 0 : return ProofRule::SCOPE == rule;
464 : : }
465 : :
466 : 0 : inline bool DotPrinter::isTheoryLemma(const ProofNode* pn)
467 : : {
468 : 0 : ProofRule rule = pn->getRule();
469 [ - - ]: 0 : if (rule == ProofRule::TRUST)
470 : : {
471 : : TrustId tid;
472 [ - - ]: 0 : if (getTrustId(pn->getArguments()[0], tid))
473 : : {
474 : 0 : return tid == TrustId::THEORY_LEMMA;
475 : : }
476 : : }
477 : : return rule == ProofRule::SCOPE
478 [ - - ][ - - ]: 0 : || (ProofRule::CNF_ITE_NEG3 < rule && rule < ProofRule::LFSC_RULE);
[ - - ]
479 : : }
480 : :
481 : 0 : inline bool DotPrinter::isASSUME(const ProofRule& rule)
482 : : {
483 : 0 : return ProofRule::ASSUME == rule;
484 : : }
485 : :
486 : 0 : void DotPrinter::ruleArguments(std::ostringstream& currentArguments,
487 : : const ProofNode* pn)
488 : : {
489 : 0 : const std::vector<Node>& args = pn->getArguments();
490 : 0 : ProofRule r = pn->getRule();
491 : : // don't process arguments of rules whose conclusion is in the arguments
492 [ - - ][ - - ]: 0 : if (!args.size() || r == ProofRule::ASSUME || r == ProofRule::REORDERING
493 [ - - ][ - - ]: 0 : || r == ProofRule::REFL)
[ - - ]
494 : : {
495 : 0 : return;
496 : : }
497 : 0 : currentArguments << " :args [ ";
498 : :
499 : : // if cong, special process
500 [ - - ][ - - ]: 0 : if (r == ProofRule::CONG || r == ProofRule::NARY_CONG)
501 : : {
502 : 0 : AlwaysAssert(args.size() == 1 || args.size() == 2);
503 : : // if two arguments, ignore first and print second
504 [ - - ]: 0 : if (args.size() == 2)
505 : : {
506 : 0 : currentArguments << d_lbind.convert(args[1]);
507 : : }
508 : : else
509 : : {
510 : 0 : Kind k = Kind::UNDEFINED_KIND;
511 : 0 : ProofRuleChecker::getKind(args[0], k);
512 : 0 : currentArguments << printer::smt2::Smt2Printer::smtKindString(k);
513 : 0 : }
514 : : }
515 : : // if th_rw, likewise
516 [ - - ]: 0 : else if (r == ProofRule::TRUST_THEORY_REWRITE)
517 : : {
518 : : // print the second argument
519 : : theory::TheoryId id;
520 : 0 : theory::builtin::BuiltinProofRuleChecker::getTheoryId(args[1], id);
521 : 0 : std::ostringstream ss;
522 : 0 : ss << id;
523 : 0 : std::string s = ss.str();
524 : : // delete "THEORY_" prefix
525 : 0 : s.erase(0, 7);
526 : 0 : currentArguments << s;
527 : : }
528 : : else
529 : : {
530 : 0 : currentArguments << d_lbind.convert(args[0]);
531 [ - - ]: 0 : for (size_t i = 1, size = args.size(); i < size; i++)
532 : : {
533 : 0 : currentArguments << ", " << d_lbind.convert(args[i]);
534 : : }
535 : : }
536 : 0 : currentArguments << " ]";
537 : : }
538 : :
539 : : } // namespace proof
540 : : } // namespace cvc5::internal
|
