Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Haniel Barbosa, Hanna Lachnitt, Daniel Larraz
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 : : * The module for printing Alethe proof nodes.
14 : : */
15 : :
16 : : #include "proof/alethe/alethe_printer.h"
17 : :
18 : : #include <iostream>
19 : : #include <sstream>
20 : : #include <unordered_map>
21 : :
22 : : #include "options/printer_options.h"
23 : : #include "options/proof_options.h"
24 : : #include "proof/alethe/alethe_proof_rule.h"
25 : : #include "util/smt2_quote_string.h"
26 : :
27 : : namespace cvc5::internal {
28 : :
29 : : namespace proof {
30 : :
31 : 1425 : LetUpdaterPfCallback::LetUpdaterPfCallback(AletheLetBinding& lbind)
32 : 1425 : : d_lbind(lbind)
33 : : {
34 : 1425 : }
35 : :
36 : 2850 : LetUpdaterPfCallback::~LetUpdaterPfCallback() {}
37 : :
38 : 2067760 : bool LetUpdaterPfCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
39 : : CVC5_UNUSED const std::vector<Node>& fa,
40 : : CVC5_UNUSED bool& continueUpdate)
41 : : {
42 : 2067760 : ProofRule r = pn->getRule();
43 [ + + ]: 2067760 : if (r == ProofRule::ASSUME)
44 : : {
45 : 128163 : d_lbind.process(pn->getResult());
46 : 128163 : return false;
47 : : }
48 : 1939600 : const std::vector<Node>& args = pn->getArguments();
49 [ + + ]: 1939600 : if (r == ProofRule::SCOPE)
50 : : {
51 [ + + ]: 12833 : for (size_t i = 0, size = args.size(); i < size; ++i)
52 : : {
53 : 11414 : d_lbind.process(args[i]);
54 : : }
55 : 1419 : return false;
56 : : }
57 : : // Letification done on the converted terms (thus from the converted
58 : : // conclusion) and potentially on arguments, which means to ignore the first
59 : : // two arguments (which are the Alethe rule and the original conclusion).
60 [ - + ][ - - ]: 1938180 : AlwaysAssert(args.size() > 2)
61 : 1938180 : << "res: " << pn->getResult() << "\nid: " << pn->getRule();
62 [ + + ]: 4879950 : for (size_t i = 2, size = args.size(); i < size; ++i)
63 : : {
64 [ + - ]: 2941770 : Trace("alethe-printer") << "Process " << args[i] << std::endl;
65 : : // We do not share s-expressions, but rather their children
66 [ + + ]: 2941770 : if (args[i].getKind() == Kind::SEXPR)
67 : : {
68 [ + + ]: 8512010 : for (const auto& arg : args[i])
69 : : {
70 : 6573830 : d_lbind.process(arg);
71 : : }
72 : 1938180 : continue;
73 : : }
74 : 1003590 : d_lbind.process(args[i]);
75 : : }
76 : 1938180 : return false;
77 : : }
78 : :
79 : 1425 : AletheProofPrinter::AletheProofPrinter(Env& env, AletheNodeConverter& anc)
80 : : : EnvObj(env),
81 : : d_context(),
82 : : d_assumptionsMap(&d_context),
83 : : d_pfMap(&d_context),
84 : 1419 : d_lbind(options().printer.dagThresh ? options().printer.dagThresh + 1
85 : : : 0),
86 : : d_anc(anc),
87 [ + + ]: 2844 : d_cb(new LetUpdaterPfCallback(d_lbind))
88 : : {
89 : 1425 : }
90 : :
91 : 2585880 : void AletheProofPrinter::printStep(
92 : : std::ostream& out,
93 : : const std::string& stepId,
94 : : AletheRule arule,
95 : : const std::vector<Node>& pfArgs,
96 : : const std::vector<std::shared_ptr<ProofNode>>& pfChildren)
97 : : {
98 : 2585880 : out << "(step " << stepId << " ";
99 : : // print the conclusion and the rule
100 : 2585880 : printTerm(out, pfArgs[2]);
101 : 2585880 : out << " :rule " << arule;
102 [ + + ]: 2585880 : if (!pfChildren.empty())
103 : : {
104 : 1646070 : out << " :premises (";
105 : 1646070 : bool first = true;
106 [ + + ]: 6469020 : for (const std::shared_ptr<ProofNode>& pfChild : pfChildren)
107 : : {
108 [ + + ]: 4822960 : out << (first ? "" : " ");
109 : 4822960 : first = false;
110 : 4822960 : printStepId(out, pfChild);
111 : : }
112 : 1646070 : out << ")";
113 : : }
114 [ + + ]: 2585880 : if (pfArgs.size() > 3)
115 : : {
116 : 587306 : out << " :args (";
117 [ + + ]: 2045590 : for (size_t i = 3, size = pfArgs.size(); i < size; i++)
118 : : {
119 : 1458280 : printTerm(out, pfArgs[i]);
120 [ + + ]: 1458280 : out << (i < pfArgs.size() - 1 ? " " : "");
121 : : }
122 : 587306 : out << ")";
123 : : }
124 : 2585880 : out << ")" << std::endl;
125 : 2585880 : }
126 : :
127 : 4822960 : void AletheProofPrinter::printStepId(std::ostream& out,
128 : : std::shared_ptr<ProofNode> pfn)
129 : : {
130 [ + + ]: 4822960 : if (pfn->getRule() == ProofRule::ASSUME)
131 : : {
132 : 359795 : Node res = d_anc.convert(pfn->getResult());
133 [ - + ][ - + ]: 359795 : Assert(!res.isNull());
[ - - ]
134 [ + - ]: 359795 : Trace("alethe-printer") << "... reached assumption " << res << std::endl;
135 : 359795 : auto it = d_assumptionsMap.find(res);
136 [ - + ][ - - ]: 359795 : Assert(it != d_assumptionsMap.end())
137 [ - + ][ - + ]: 359795 : << "Assumption has not been printed yet! " << res << std::endl;
[ - - ]
138 : 359795 : out << it->second;
139 : 359795 : return;
140 : : }
141 [ - + ][ - - ]: 4463160 : Assert(d_pfMap.find(pfn.get()) != d_pfMap.end())
142 : 4463160 : << "Cannot find pf of " << pfn->getResult() << std::endl;
143 : 4463160 : out << d_pfMap.find(pfn.get())->second;
144 : : }
145 : :
146 : 4313650 : void AletheProofPrinter::printTerm(std::ostream& out, TNode n)
147 : : {
148 : 4313650 : std::stringstream ss;
149 : 4313650 : options::ioutils::applyOutputLanguage(ss, Language::LANG_SMTLIB_V2_6);
150 : : // We print lambda applications in non-curried manner
151 : 4313650 : options::ioutils::applyFlattenHOChains(ss, true);
152 : : // Make sure we do not introduce "let" for sharing, since names will not have
153 : : // been introduced under binders.
154 : 4313650 : options::ioutils::applyDagThresh(ss, 0);
155 : : // Guarantee we print reals as expected
156 : 4313650 : options::ioutils::applyPrintArithLitToken(ss, true);
157 : 4313650 : ss << d_lbind.convert(nodeManager(), n, "@p_");
158 : 4313650 : out << ss.str();
159 : 4313650 : }
160 : :
161 : 1425 : void AletheProofPrinter::print(
162 : : std::ostream& out,
163 : : std::shared_ptr<ProofNode> pfn,
164 : : const std::map<Node, std::string>& assertionNames)
165 : : {
166 [ + - ]: 1425 : Trace("alethe-printer") << "- Print proof in Alethe format." << std::endl;
167 : : // ignore outer scope
168 : 1425 : pfn = pfn->getChildren()[0];
169 : 1425 : std::shared_ptr<ProofNode> innerPf = pfn->getChildren()[0];
170 [ - + ][ - + ]: 1425 : Assert(innerPf);
[ - - ]
171 : :
172 : : // print quantifier Skolems, if they are being defined
173 [ - + ]: 1425 : if (options().proof.proofAletheDefineSkolems)
174 : : {
175 : 0 : const std::map<Node, Node>& skolemDefs = d_anc.getSkolemDefinitions();
176 : 0 : const std::vector<Node>& skolemList = d_anc.getSkolemList();
177 [ - - ]: 0 : for (const auto& skolem : skolemList)
178 : : {
179 : 0 : Assert(skolemDefs.find(skolem) != skolemDefs.end());
180 : 0 : out << "(define-fun " << skolem << " () " << skolem.getType() << " ";
181 : 0 : printTerm(out, skolemDefs.at(skolem));
182 : 0 : out << ")" << std::endl;
183 : : }
184 : : }
185 [ + + ]: 1425 : if (options().printer.dagThresh)
186 : : {
187 : : // Traverse the proof node to letify the (converted) conclusions of proof
188 : : // steps. Note that we traverse the original proof node because assumptions
189 : : // may apper just in them (if they are not used in the rest of the proof).
190 : : // Otherwise repeated terms *only* in assumptions would not be letified.
191 : 2838 : ProofNodeUpdater updater(d_env, *(d_cb.get()), false, false);
192 [ + - ]: 1419 : Trace("alethe-printer") << "- letify." << std::endl;
193 : 1419 : updater.process(pfn);
194 : :
195 : 2838 : std::vector<Node> letList;
196 : 1419 : d_lbind.letify(letList);
197 [ - + ]: 1419 : if (TraceIsOn("alethe-printer"))
198 : : {
199 [ - - ]: 0 : for (TNode n : letList)
200 : : {
201 [ - - ]: 0 : Trace("alethe-printer")
202 : 0 : << "Term " << n << " has id " << d_lbind.getId(n) << std::endl;
203 : : }
204 : : }
205 : : }
206 [ + - ]: 1425 : Trace("alethe-printer") << "- Print assumptions." << std::endl;
207 : 1425 : const std::vector<Node>& args = pfn->getArguments();
208 : : // Special handling for the first scope. Print assumptions and add them to the
209 : : // list but do not print anchor.
210 [ - + ][ - + ]: 1425 : Assert(!args.empty());
[ - - ]
211 [ + + ]: 12863 : for (size_t i = 0, size = args.size(); i < size; i++)
212 : : {
213 : : // search name with original assumption rather than its conversion
214 [ - + ][ - + ]: 11438 : Assert(!d_anc.getOriginalAssumption(args[i]).isNull());
[ - - ]
215 : 22876 : Node original = d_anc.getOriginalAssumption(args[i]);
216 : 11438 : auto it = assertionNames.find(original);
217 [ + + ]: 11438 : if (it != assertionNames.end())
218 : : {
219 : : // Since names can be strings that were originally quoted, we must see if
220 : : // the quotes need to be added back.
221 : 872 : std::string quotedName = quoteSymbol(it->second);
222 : 436 : out << "(assume " << quotedName << " ";
223 : 436 : d_assumptionsMap[args[i]] = quotedName;
224 : : }
225 : : else
226 : : {
227 : 11002 : out << "(assume a" << i << " ";
228 : 11002 : d_assumptionsMap[args[i]] = "a" + std::to_string(i);
229 : : }
230 : 11438 : printTerm(out, args[i]);
231 : 11438 : out << ")" << std::endl;
232 : : }
233 : : // Then, print the rest of the proof node
234 : 1425 : size_t id = 0;
235 : 1425 : printInternal(out, "", id, pfn->getChildren()[0]);
236 : 1425 : }
237 : :
238 : 4873290 : void AletheProofPrinter::printInternal(std::ostream& out,
239 : : const std::string& prefix,
240 : : size_t& id,
241 : : std::shared_ptr<ProofNode> pfn)
242 : : {
243 : : // assumptions are not printed when reached here because in Alethe they are
244 : : // always printed beforehand, i.e., from the scope introducing them, or being
245 : : // the initial assumptions.
246 [ + + ]: 4873290 : if (pfn->getRule() == ProofRule::ASSUME)
247 : : {
248 : 2287420 : return;
249 : : }
250 : : context::CDHashMap<ProofNode*, std::string>::const_iterator pfIt =
251 : 4513490 : d_pfMap.find(pfn.get());
252 [ + + ]: 4513490 : if (pfIt != d_pfMap.end())
253 : : {
254 [ + - ]: 3757360 : Trace("alethe-printer") << "... step is already printed t" << pfIt->second
255 [ - - ]: 1878680 : << " " << pfn->getResult() << " "
256 [ - + ][ - + ]: 1878680 : << getAletheRule(pfn->getArguments()[0]) << "\n";
[ - - ]
257 : 1878680 : return;
258 : : }
259 : 2634810 : const std::vector<Node>& args = pfn->getArguments();
260 : : const std::vector<std::shared_ptr<ProofNode>>& pfChildren =
261 : 2634810 : pfn->getChildren();
262 : : // Get the alethe proof rule
263 : 2634810 : AletheRule arule = getAletheRule(args[0]);
264 [ + - ]: 5269620 : Trace("alethe-printer") << "... print step " << arule << " : " << args[2]
265 : 2634810 : << std::endl;
266 : : // We special case printing anchors
267 : 2634810 : if (arule >= AletheRule::ANCHOR_SUBPROOF
268 [ + + ]: 2634810 : && arule <= AletheRule::ANCHOR_SKO_EX)
269 : : {
270 [ + - ]: 48946 : Trace("alethe-printer") << push;
271 [ - + ][ - + ]: 48946 : Assert(pfChildren.size() == 1);
[ - - ]
272 : 48946 : out << "(anchor :step " << prefix << "t" << id;
273 : 146838 : std::string subproofPrefix = prefix + "t" + std::to_string(id) + ".";
274 : : // create a new context for the subproof
275 : 48946 : d_context.push();
276 : 97892 : std::vector<std::string> dischargeIds;
277 : : // if subproof, print assumptions, otherwise print arguments
278 [ + + ]: 48946 : if (arule == AletheRule::ANCHOR_SUBPROOF)
279 : : {
280 : 35465 : out << ")" << std::endl;
281 [ - + ][ - + ]: 35465 : Assert(args.size() >= 3);
[ - - ]
282 [ + + ]: 220598 : for (size_t i = 3, size = args.size(); i < size; ++i)
283 : : {
284 [ + - ]: 370266 : Trace("alethe-printer")
285 : 185133 : << "... print assumption " << args[i] << std::endl;
286 : 555399 : std::string assumptionId = subproofPrefix + "a" + std::to_string(i - 3);
287 : 185133 : out << "(assume " << assumptionId << " ";
288 : 185133 : printTerm(out, args[i]);
289 : 185133 : out << ")" << std::endl;
290 : 185133 : d_assumptionsMap[args[i]] = assumptionId;
291 : 185133 : dischargeIds.push_back(assumptionId);
292 : : }
293 : : }
294 : : else
295 : : {
296 [ + - ][ + - ]: 26962 : Assert(arule >= AletheRule::ANCHOR_BIND
[ - + ][ - - ]
297 : : && arule <= AletheRule::ANCHOR_SKO_EX);
298 : 13481 : out << " :args (";
299 [ + + ]: 61208 : for (size_t i = 3, size = args.size(); i < size; ++i)
300 : : {
301 [ + + ]: 47727 : if (args[i].getKind() == Kind::EQUAL)
302 : : {
303 [ - + ][ - + ]: 23971 : Assert(args[i][0].getKind() == Kind::BOUND_VARIABLE);
[ - - ]
304 : 23971 : out << "(:= (" << args[i][0] << " " << args[i][0].getType() << ") ";
305 : 23971 : printTerm(out, args[i][1]);
306 [ + + ]: 23971 : out << ")" << (i != args.size() - 1 ? " " : "");
307 : 23971 : continue;
308 : : }
309 : 23756 : Assert(args[i].getKind() == Kind::BOUND_VARIABLE) << args[i];
310 : 23756 : out << "(" << args[i] << " " << args[i].getType() << ") ";
311 : : }
312 : 13481 : out << "))" << std::endl;
313 : : }
314 : : // since the subproof shape relies on having at least one step inside it, if
315 : : // the step relative to children[0] is already d_pfMap, we should just print
316 : : // the step and be done
317 : 48946 : auto it = d_pfMap.find(pfChildren[0].get());
318 [ + + ]: 48946 : if (it != d_pfMap.end())
319 : : {
320 : 42 : std::string childStepId = prefix + "t" + std::to_string(id) + ".t0";
321 : 14 : const std::vector<Node>& childArgs = pfChildren[0]->getArguments();
322 : : const std::vector<std::shared_ptr<ProofNode>>& childPfChildren =
323 : 14 : pfChildren[0]->getChildren();
324 : 14 : AletheRule childArule = getAletheRule(childArgs[0]);
325 : 14 : printStep(out, childStepId, childArule, childArgs, childPfChildren);
326 : : }
327 : : else
328 : : {
329 : 48932 : size_t subproofId = 0;
330 : 48932 : printInternal(out, subproofPrefix, subproofId, pfChildren[0]);
331 : : }
332 : 48946 : d_context.pop();
333 [ + - ]: 48946 : Trace("alethe-printer") << pop;
334 : 97892 : std::string stepId = prefix + "t" + std::to_string(id++);
335 : 48946 : out << "(step " << stepId << " ";
336 : 48946 : printTerm(out, args[2]);
337 : 48946 : out << " :rule " << arule;
338 : : // Discharge assumptions in the case of subproof
339 [ + + ]: 48946 : if (arule == AletheRule::ANCHOR_SUBPROOF)
340 : : {
341 : 35465 : out << " :discharge (";
342 [ + + ]: 220598 : for (size_t i = 3, size = args.size(); i < size; ++i)
343 : : {
344 [ + + ]: 185133 : out << dischargeIds[i - 3] << (i < args.size() - 1 ? " " : "");
345 : : }
346 : 35465 : out << ")";
347 : : }
348 : 48946 : out << ")" << std::endl;
349 : 48946 : d_pfMap[pfn.get()] = stepId;
350 : 48946 : return;
351 : : }
352 : : // Print the steps for children to guarantee we will have ids for them in the
353 : : // premises of this step
354 [ + + ]: 7408790 : for (const std::shared_ptr<ProofNode>& pfChild : pfChildren)
355 : : {
356 [ + - ]: 4822930 : Trace("alethe-printer") << push;
357 : 4822930 : printInternal(out, prefix, id, pfChild);
358 [ + - ]: 4822930 : Trace("alethe-printer") << pop;
359 : : }
360 : : // Print this step
361 : 5171730 : std::string stepId = prefix + "t" + std::to_string(id++);
362 : 2585860 : printStep(out, stepId, arule, args, pfChildren);
363 : 2585860 : d_pfMap[pfn.get()] = stepId;
364 : : }
365 : :
366 : : } // namespace proof
367 : : } // namespace cvc5::internal
|
