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