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