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 : : * Implementation of a utility for updating proof nodes.
11 : : */
12 : :
13 : : #include "proof/proof_node_updater.h"
14 : :
15 : : #include "proof/lazy_proof.h"
16 : : #include "proof/proof_checker.h"
17 : : #include "proof/proof_ensure_closed.h"
18 : : #include "proof/proof_node_algorithm.h"
19 : : #include "proof/proof_node_manager.h"
20 : : #include "smt/env.h"
21 : :
22 : : namespace cvc5::internal {
23 : :
24 : 71746 : ProofNodeUpdaterCallback::ProofNodeUpdaterCallback() {}
25 : 71696 : ProofNodeUpdaterCallback::~ProofNodeUpdaterCallback() {}
26 : :
27 : 2250075 : bool ProofNodeUpdaterCallback::shouldUpdate(
28 : : CVC5_UNUSED std::shared_ptr<ProofNode> pn,
29 : : CVC5_UNUSED const std::vector<Node>& fa,
30 : : CVC5_UNUSED bool& continueUpdate)
31 : : {
32 : 2250075 : return false;
33 : : }
34 : :
35 : 1055 : bool ProofNodeUpdaterCallback::update(
36 : : CVC5_UNUSED Node res,
37 : : CVC5_UNUSED ProofRule id,
38 : : CVC5_UNUSED const std::vector<Node>& children,
39 : : CVC5_UNUSED const std::vector<Node>& args,
40 : : CVC5_UNUSED CDProof* cdp,
41 : : CVC5_UNUSED bool& continueUpdate)
42 : : {
43 : 1055 : return false;
44 : : }
45 : :
46 : 8911824 : bool ProofNodeUpdaterCallback::shouldUpdatePost(
47 : : CVC5_UNUSED std::shared_ptr<ProofNode> pn,
48 : : CVC5_UNUSED const std::vector<Node>& fa)
49 : : {
50 : 8911824 : return false;
51 : : }
52 : :
53 : 0 : bool ProofNodeUpdaterCallback::updatePost(
54 : : CVC5_UNUSED Node res,
55 : : CVC5_UNUSED ProofRule id,
56 : : CVC5_UNUSED const std::vector<Node>& children,
57 : : CVC5_UNUSED const std::vector<Node>& args,
58 : : CVC5_UNUSED CDProof* cdp)
59 : : {
60 : 0 : return false;
61 : : }
62 : :
63 : 14892081 : void ProofNodeUpdaterCallback::finalize(
64 : : CVC5_UNUSED std::shared_ptr<ProofNode> pn)
65 : : {
66 : : // do nothing
67 : 14892081 : }
68 : :
69 : 58016 : ProofNodeUpdater::ProofNodeUpdater(Env& env,
70 : : ProofNodeUpdaterCallback& cb,
71 : : bool mergeSubproofs,
72 : 58016 : bool autoSym)
73 : : : EnvObj(env),
74 : 58016 : d_cb(cb),
75 : 58016 : d_debugFreeAssumps(false),
76 : 58016 : d_mergeSubproofs(mergeSubproofs),
77 : 58016 : d_autoSym(autoSym)
78 : : {
79 : 58016 : }
80 : :
81 : 35023 : void ProofNodeUpdater::process(std::shared_ptr<ProofNode> pf)
82 : : {
83 [ - + ]: 35023 : if (d_debugFreeAssumps)
84 : : {
85 [ - - ]: 0 : if (TraceIsOn("pfnu-debug"))
86 : : {
87 [ - - ]: 0 : Trace("pfnu-debug2") << "Initial proof: " << *pf.get() << std::endl;
88 [ - - ]: 0 : Trace("pfnu-debug") << "ProofNodeUpdater::process" << std::endl;
89 [ - - ]: 0 : Trace("pfnu-debug") << "Expected free assumptions: " << std::endl;
90 [ - - ]: 0 : for (const Node& fa : d_freeAssumps)
91 : : {
92 [ - - ]: 0 : Trace("pfnu-debug") << "- " << fa << std::endl;
93 : : }
94 : 0 : std::vector<Node> assump;
95 : 0 : expr::getFreeAssumptions(pf.get(), assump);
96 [ - - ]: 0 : Trace("pfnu-debug") << "Current free assumptions: " << std::endl;
97 [ - - ]: 0 : for (const Node& fa : assump)
98 : : {
99 [ - - ]: 0 : Trace("pfnu-debug") << "- " << fa << std::endl;
100 : : }
101 : 0 : }
102 : : }
103 : 35023 : processInternal(pf, d_freeAssumps);
104 : 35023 : }
105 : :
106 : 35023 : void ProofNodeUpdater::processInternal(std::shared_ptr<ProofNode> pf,
107 : : std::vector<Node>& fa)
108 : : {
109 : : // Note that processInternal uses a single scope; fa is updated based on
110 : : // the current free assumptions of the proof nodes on the stack.
111 : :
112 : : // The list of proof nodes we are currently traversing beneath. This is used
113 : : // for checking for cycles in the overall proof.
114 : 35023 : std::vector<std::shared_ptr<ProofNode>> traversing;
115 : : // Map from formulas to (closed) proof nodes that prove that fact
116 : 35023 : std::map<Node, std::shared_ptr<ProofNode>> resCache;
117 : : // Map from formulas to non-closed proof nodes that prove that fact. These
118 : : // are replaced by proofs in the above map when applicable.
119 : 35023 : std::map<Node, std::vector<std::shared_ptr<ProofNode>>> resCacheNcWaiting;
120 : : // Map from proof nodes to whether they contain assumptions
121 : 35023 : std::unordered_map<const ProofNode*, bool> cfaMap;
122 : 35023 : std::unordered_set<Node> cfaAllowed;
123 : 35023 : cfaAllowed.insert(fa.begin(), fa.end());
124 : 35023 : std::shared_ptr<ProofNode> pft = pf;
125 [ + + ]: 39911 : while (pft->getRule() == ProofRule::SCOPE)
126 : : {
127 : 4888 : const std::vector<Node>& args = pft->getArguments();
128 : 4888 : cfaAllowed.insert(args.begin(), args.end());
129 : 4888 : pft = pft->getChildren()[0];
130 : : }
131 [ + - ]: 35023 : Trace("pf-process") << "ProofNodeUpdater::process" << std::endl;
132 : 35023 : std::unordered_map<std::shared_ptr<ProofNode>, bool> visited;
133 : 35023 : std::unordered_map<std::shared_ptr<ProofNode>, bool>::iterator it;
134 : 35023 : std::vector<std::shared_ptr<ProofNode>> visit;
135 : 35023 : std::shared_ptr<ProofNode> cur;
136 : 35023 : visit.push_back(pf);
137 : 35023 : std::map<Node, std::shared_ptr<ProofNode>>::iterator itc;
138 : : do
139 : : {
140 : 55306549 : cur = visit.back();
141 : 55306549 : visit.pop_back();
142 : 55306549 : it = visited.find(cur);
143 [ + + ]: 55306549 : if (it == visited.end())
144 : : {
145 : : // Check if there is a proof in resCache with the same result.
146 : : // Note that if this returns true, we update the contents of the current
147 : : // proof. Moreover, parents will replace the reference to this proof.
148 : : // Thus, replacing the contents of this proof is not (typically)
149 : : // necessary, but is done anyways in case there are any other references
150 : : // to this proof that are not handled by this loop, that is, proof
151 : : // nodes having this as a child that are not subproofs of pf.
152 [ + + ]: 19036198 : if (checkMergeProof(cur, resCache, cfaMap))
153 : : {
154 [ + - ]: 871274 : Trace("pf-process-merge") << "...merged on previsit" << std::endl;
155 : 871274 : visited[cur] = true;
156 : 1226798 : continue;
157 : : }
158 : 18164924 : preSimplify(cur);
159 : : // run update to a fixed point
160 : 18164924 : bool continueUpdate = true;
161 [ + + ][ + + ]: 20481139 : while (runUpdate(cur, fa, continueUpdate) && continueUpdate)
[ + - ][ + + ]
[ - - ]
162 : : {
163 [ + - ]: 2316215 : Trace("pf-process-debug") << "...updated proof." << std::endl;
164 : : }
165 : 18164924 : visited[cur] = !continueUpdate;
166 [ + + ]: 18164924 : if (!continueUpdate)
167 : : {
168 : : // no further changes should be made to cur according to the callback
169 [ + - ]: 711048 : Trace("pf-process-debug")
170 : 355524 : << "...marked to not continue update." << std::endl;
171 : 355524 : runFinalize(cur, fa, resCache, resCacheNcWaiting, cfaMap, cfaAllowed);
172 : 355524 : continue;
173 : : }
174 : 17809400 : traversing.push_back(cur);
175 : 17809400 : visit.push_back(cur);
176 : : // If we are not the top-level proof, we were a scope, or became a scope
177 : : // after updating, we do a separate recursive call to this method. This
178 : : // allows us to properly track the assumptions in scope, which is
179 : : // important for example to merge or to determine updates based on free
180 : : // assumptions.
181 [ + + ]: 17809400 : if (cur->getRule() == ProofRule::SCOPE)
182 : : {
183 : 328152 : const std::vector<Node>& args = cur->getArguments();
184 : 328152 : fa.insert(fa.end(), args.begin(), args.end());
185 : : }
186 : 17809400 : const std::vector<std::shared_ptr<ProofNode>>& ccp = cur->getChildren();
187 : : // now, process children
188 [ + + ]: 55271526 : for (const std::shared_ptr<ProofNode>& cp : ccp)
189 : : {
190 : 37462126 : if (std::find(traversing.begin(), traversing.end(), cp)
191 [ - + ]: 74924252 : != traversing.end())
192 : : {
193 : 0 : Unhandled()
194 : : << "ProofNodeUpdater::processInternal: cyclic proof! (use "
195 : 0 : "--proof-check=eager)"
196 : 0 : << std::endl;
197 : : }
198 : 37462126 : visit.push_back(cp);
199 : : }
200 : : }
201 [ + + ]: 36270351 : else if (!it->second)
202 : : {
203 [ - + ][ - + ]: 17809400 : Assert(!traversing.empty());
[ - - ]
204 : 17809400 : traversing.pop_back();
205 : 17809400 : visited[cur] = true;
206 : : // finalize the node
207 : 17809400 : ProofRule id = cur->getRule();
208 [ + + ]: 17809400 : if (id == ProofRule::SCOPE)
209 : : {
210 : 328152 : const std::vector<Node>& args = cur->getArguments();
211 [ - + ][ - + ]: 328152 : Assert(fa.size() >= args.size());
[ - - ]
212 : 328152 : fa.resize(fa.size() - args.size());
213 : : }
214 : : // maybe found a proof in the meantime, i.e. a subproof of the current
215 : : // proof with the same result. Same as above, updating the contents here
216 : : // is typically not necessary since references to this proof will be
217 : : // replaced.
218 : : // maybe found a proof in the meantime, i.e. a subproof of the current
219 : : // proof with the same result. Same as above, updating the contents here
220 : : // is typically not necessary since references to this proof will be
221 : : // replaced.
222 [ + + ]: 17809400 : if (!checkMergeProof(cur, resCache, cfaMap))
223 : : {
224 : 17770375 : runFinalize(cur, fa, resCache, resCacheNcWaiting, cfaMap, cfaAllowed);
225 : : }
226 : : else
227 : : {
228 [ + - ]: 78050 : Trace("pf-process-merge") << "...merged on postvisit " << id << " / "
229 : 39025 : << cur->getRule() << std::endl;
230 : : }
231 : : // call the finalize callback, independent of whether it was merged
232 : 17809400 : d_cb.finalize(cur);
233 : : }
234 [ + + ]: 55306549 : } while (!visit.empty());
235 [ + - ]: 35023 : Trace("pf-process") << "ProofNodeUpdater::process: finished" << std::endl;
236 : 35023 : }
237 : :
238 : 20956772 : void ProofNodeUpdater::preSimplify(std::shared_ptr<ProofNode> cur)
239 : : {
240 [ + + ]: 20956772 : if (!d_mergeSubproofs)
241 : : {
242 : 12218429 : return;
243 : : }
244 : 8738343 : std::shared_ptr<ProofNode> toMerge;
245 : : do
246 : : {
247 : 9012302 : ProofRule id = cur->getRule();
248 : 9012302 : toMerge = nullptr;
249 [ + + ][ + ]: 9012302 : switch (id)
250 : : {
251 : 77714 : case ProofRule::AND_ELIM:
252 : : {
253 : : // hardcoded for pattern (AND_ELIM (AND_INTRO ...))
254 : : const std::vector<std::shared_ptr<ProofNode>>& children =
255 : 77714 : cur->getChildren();
256 [ - + ][ - + ]: 77714 : Assert(children.size() == 1);
[ - - ]
257 [ + + ]: 77714 : if (children[0]->getRule() == ProofRule::AND_INTRO)
258 : : {
259 : 13747 : const std::vector<Node>& args = cur->getArguments();
260 [ - + ][ - + ]: 13747 : Assert(args.size() == 1);
[ - - ]
261 : : uint32_t i;
262 [ + - ]: 13747 : if (ProofRuleChecker::getUInt32(args[0], i))
263 : : {
264 : : const std::vector<std::shared_ptr<ProofNode>>& cc =
265 : 13747 : children[0]->getChildren();
266 [ + - ]: 13747 : if (i < cc.size())
267 : : {
268 [ + - ]: 27494 : Trace("pfu-pre-simplify")
269 : 13747 : << "Pre-simplify AND_ELIM over AND_INTRO" << std::endl;
270 : 13747 : toMerge = cc[i];
271 : : }
272 : : }
273 : : }
274 : : }
275 : 77714 : break;
276 : 683723 : case ProofRule::SYMM:
277 : : {
278 : : // hardcoded for pattern (SYMM (SYMM ...))
279 : : const std::vector<std::shared_ptr<ProofNode>>& children =
280 : 683723 : cur->getChildren();
281 [ - + ][ - + ]: 683723 : Assert(children.size() == 1);
[ - - ]
282 [ + + ]: 683723 : if (children[0]->getRule() == ProofRule::SYMM)
283 : : {
284 : : const std::vector<std::shared_ptr<ProofNode>>& cc =
285 : 255858 : children[0]->getChildren();
286 [ + - ]: 511716 : Trace("pfu-pre-simplify")
287 : 255858 : << "Pre-simplify SYMM over SYMM" << std::endl;
288 : 255858 : toMerge = cc[0];
289 : : }
290 : : }
291 : 683723 : break;
292 : 8250865 : default: break;
293 : : }
294 : : // Generic search, which checks if there is a descendent of this proof node
295 : : // (up to a default bound, set to 2), which proves the same conclusion as
296 : : // this node. If this is the case, then we immediately take that subproof.
297 : : // This heuristic makes a big difference for proofs e.g. of the form
298 : : // F1 ......... Fn
299 : : // ---------------- AND_INTRO
300 : : // (and F1 .... Fn)
301 : : // ---------------- MACRO_SR_PRED_INTRO
302 : : // false
303 : : // where one of Fi is false. In this case, we *only* want to post-process
304 : : // the proof of Fi.
305 : : // The case above occurs often in practice when a single assertion in the
306 : : // rewrite rewrites to false. This optimization saves the internal work of
307 : : // post-processing F1 ... F{i-1} F{i+1} ... Fn. The depth is configurable by
308 : : // --proof-pre-simp-lookahead=N, default 2.
309 : 9012302 : uint64_t depthLimit = options().proof.proofPreSimpLookahead;
310 [ + + ][ + - ]: 9012302 : if (toMerge == nullptr && depthLimit > 0)
[ + + ]
311 : : {
312 : 8742697 : Node res = cur->getResult();
313 : 8742697 : std::vector<std::pair<size_t, std::shared_ptr<ProofNode>>> toProcess;
314 : 8742697 : toProcess.emplace_back(0, cur);
315 : 8742697 : std::unordered_map<std::shared_ptr<ProofNode>, size_t> processed;
316 : 8742697 : std::unordered_map<std::shared_ptr<ProofNode>, size_t>::iterator itp;
317 : : do
318 : : {
319 : 61381970 : std::pair<size_t, std::shared_ptr<ProofNode>> p = toProcess.back();
320 : 61381970 : toProcess.pop_back();
321 : 61381970 : std::shared_ptr<ProofNode> cc = p.second;
322 : : // do not traverse SCOPE
323 [ + + ]: 61381970 : if (cc->getRule() == ProofRule::SCOPE)
324 : : {
325 : 787651 : continue;
326 : : }
327 : 60594319 : itp = processed.find(cc);
328 [ - + ][ - - ]: 60594319 : if (itp != processed.end() && p.first >= itp->second)
[ - + ]
329 : : {
330 : 0 : continue;
331 : : }
332 [ + + ]: 60594319 : if (p.first > 0)
333 : : {
334 [ + + ]: 52090920 : if (cc->getResult() == res)
335 : : {
336 : 4354 : toMerge = cc;
337 : 4354 : break;
338 : : }
339 : : }
340 [ + + ]: 60589965 : if (p.first < depthLimit)
341 : : {
342 : : const std::vector<std::shared_ptr<ProofNode>>& children =
343 : 24654944 : cc->getChildren();
344 [ + + ]: 77294421 : for (const std::shared_ptr<ProofNode>& cp : children)
345 : : {
346 : 52639477 : toProcess.emplace_back(p.first + 1, cp);
347 : : }
348 : : }
349 [ + + ][ + + ]: 123551591 : } while (!toProcess.empty());
[ + + ][ + + ]
350 : 8742697 : }
351 [ + + ][ + - ]: 9012302 : if (toMerge != nullptr && toMerge != cur)
[ + + ]
352 : : {
353 : 273959 : ProofNodeManager* pnm = d_env.getProofNodeManager();
354 : 273959 : pnm->updateNode(cur.get(), toMerge.get());
355 : : }
356 [ + + ]: 9012302 : } while (toMerge != nullptr);
357 : 8738343 : }
358 : :
359 : 5911443 : bool ProofNodeUpdater::updateProofNode(std::shared_ptr<ProofNode> cur,
360 : : const std::vector<Node>& fa,
361 : : bool& continueUpdate,
362 : : bool preVisit)
363 : : {
364 : 5911443 : ProofRule id = cur->getRule();
365 : : // use CDProof to open a scope for which the callback updates
366 : 11822886 : CDProof cpf(d_env, nullptr, "ProofNodeUpdater::CDProof", d_autoSym);
367 : 5911443 : const std::vector<std::shared_ptr<ProofNode>>& cc = cur->getChildren();
368 : 5911443 : std::vector<Node> ccn;
369 [ + + ]: 14936463 : for (const std::shared_ptr<ProofNode>& cp : cc)
370 : : {
371 : 9025020 : Node cpres = cp->getResult();
372 : 9025020 : ccn.push_back(cpres);
373 : : // store in the proof
374 : 9025020 : cpf.addProof(cp);
375 : 9025020 : }
376 : 5911443 : Node res = cur->getResult();
377 [ + - ]: 11822886 : Trace("pf-process-debug")
378 : 5911443 : << "Updating (" << cur->getRule() << "): " << res << std::endl;
379 : : // only if the callback updated the node
380 : 5911443 : if (preVisit
381 [ + + ][ + + ]: 11822886 : ? d_cb.update(res, id, ccn, cur->getArguments(), &cpf, continueUpdate)
[ - - ]
382 [ + + ][ + + ]: 5911443 : : d_cb.updatePost(res, id, ccn, cur->getArguments(), &cpf))
[ - - ]
383 : : {
384 : 2791848 : std::shared_ptr<ProofNode> npn = cpf.getProofFor(res);
385 : 2791848 : std::vector<Node> fullFa;
386 [ - + ]: 2791848 : if (d_debugFreeAssumps)
387 : : {
388 : 0 : expr::getFreeAssumptions(cur.get(), fullFa);
389 [ - - ]: 0 : Trace("pfnu-debug") << "Original proof : " << *cur << std::endl;
390 : : }
391 : : // then, update the original proof node based on this one
392 [ + - ]: 2791848 : Trace("pf-process-debug") << "Update node..." << std::endl;
393 : 2791848 : d_env.getProofNodeManager()->updateNode(cur.get(), npn.get());
394 [ + - ]: 2791848 : Trace("pf-process-debug") << "...update node finished." << std::endl;
395 [ - + ]: 2791848 : if (d_debugFreeAssumps)
396 : : {
397 : 0 : fullFa.insert(fullFa.end(), fa.begin(), fa.end());
398 : : // We have that npn is a node we occurring the final updated version of
399 : : // the proof. We can now debug based on the expected set of free
400 : : // assumptions.
401 [ - - ]: 0 : Trace("pfnu-debug") << "Ensure updated closed..." << std::endl;
402 : 0 : pfnEnsureClosedWrt(options(),
403 : : npn.get(),
404 : : fullFa,
405 : : "pfnu-debug",
406 : : "ProofNodeUpdater:postupdate");
407 : : }
408 : : // since we updated, we pre-simplify again
409 : 2791848 : preSimplify(cur);
410 [ + - ]: 2791848 : Trace("pf-process-debug") << "..finished" << std::endl;
411 : 2791848 : return true;
412 : 2791848 : }
413 [ + - ]: 3119595 : Trace("pf-process-debug") << "..finished" << std::endl;
414 : 3119595 : return false;
415 : 5911443 : }
416 : :
417 : 38730459 : bool ProofNodeUpdater::runUpdate(std::shared_ptr<ProofNode> cur,
418 : : const std::vector<Node>& fa,
419 : : bool& continueUpdate,
420 : : bool preVisit)
421 : : {
422 : : // should it be updated?
423 [ + + ][ + + ]: 77460918 : if (preVisit ? !d_cb.shouldUpdate(cur, fa, continueUpdate)
[ - - ]
424 [ + + ][ + + ]: 38730459 : : !d_cb.shouldUpdatePost(cur, fa))
[ - - ]
425 : : {
426 : 32819016 : return false;
427 : : }
428 : 5911443 : return updateProofNode(cur, fa, continueUpdate, preVisit);
429 : : }
430 : :
431 : 18125899 : void ProofNodeUpdater::runFinalize(
432 : : std::shared_ptr<ProofNode> cur,
433 : : const std::vector<Node>& fa,
434 : : std::map<Node, std::shared_ptr<ProofNode>>& resCache,
435 : : std::map<Node, std::vector<std::shared_ptr<ProofNode>>>& resCacheNcWaiting,
436 : : std::unordered_map<const ProofNode*, bool>& cfaMap,
437 : : const std::unordered_set<Node>& cfaAllowed)
438 : : {
439 : : // run update (marked as post-visit) to a fixed point
440 : : bool dummyContinueUpdate;
441 [ + + ]: 18249320 : while (runUpdate(cur, fa, dummyContinueUpdate, false))
442 : : {
443 [ + - ]: 123421 : Trace("pf-process-debug") << "...updated proof." << std::endl;
444 : : }
445 [ + + ]: 18125899 : if (d_mergeSubproofs)
446 : : {
447 : 7851051 : Node res = cur->getResult();
448 : : // cache the result if we don't contain an assumption
449 [ + + ]: 7851051 : if (!expr::containsAssumption(cur.get(), cfaMap, cfaAllowed))
450 : : {
451 [ + - ]: 4340783 : Trace("pf-process-debug") << "No assumption pf: " << res << std::endl;
452 : : // cache result if we are merging subproofs
453 : 4340783 : resCache[res] = cur;
454 : : // go back and merge into the non-closed proofs of the same fact
455 : : std::map<Node, std::vector<std::shared_ptr<ProofNode>>>::iterator itnw =
456 : 4340783 : resCacheNcWaiting.find(res);
457 [ + + ]: 4340783 : if (itnw != resCacheNcWaiting.end())
458 : : {
459 : 2904 : ProofNodeManager* pnm = d_env.getProofNodeManager();
460 [ + + ]: 6193 : for (std::shared_ptr<ProofNode>& ncp : itnw->second)
461 : : {
462 : 3289 : pnm->updateNode(ncp.get(), cur.get());
463 : : }
464 : 2904 : resCacheNcWaiting.erase(res);
465 : : }
466 : : }
467 : : else
468 : : {
469 [ + - ]: 7020536 : Trace("pf-process-debug") << "Assumption pf: " << res << ", with "
470 : 3510268 : << cfaAllowed.size() << std::endl;
471 : 3510268 : resCacheNcWaiting[res].push_back(cur);
472 : : }
473 : : // Now, do update of children, that is, we replace children of the current
474 : : // proof with the representative child in the cache, if they are different.
475 : : // This is necessary to do here since we only locally update the contents of
476 : : // a proof when a duplicate is encountered. Updating the reference to a
477 : : // child is done here.
478 : 7851051 : std::map<Node, std::shared_ptr<ProofNode>>::iterator itr;
479 : 7851051 : const std::vector<std::shared_ptr<ProofNode>>& ccp = cur->getChildren();
480 : 7851051 : std::vector<std::shared_ptr<ProofNode>> newChildren;
481 : 7851051 : bool childChanged = false;
482 [ + + ]: 23349756 : for (const std::shared_ptr<ProofNode>& cp : ccp)
483 : : {
484 : 15498705 : Node cpres = cp->getResult();
485 : 15498705 : itr = resCache.find(cpres);
486 [ + + ][ + + ]: 15498705 : if (itr != resCache.end() && itr->second != cp)
[ + + ]
487 : : {
488 : 1256261 : newChildren.emplace_back(itr->second);
489 : 1256261 : childChanged = true;
490 : : }
491 : : else
492 : : {
493 : 14242444 : newChildren.emplace_back(cp);
494 : : }
495 : 15498705 : }
496 [ + + ]: 7851051 : if (childChanged)
497 : : {
498 : 919719 : ProofNodeManager* pnm = d_env.getProofNodeManager();
499 : 919719 : pnm->updateNode(
500 : : cur.get(), cur->getRule(), newChildren, cur->getArguments());
501 : : }
502 : 7851051 : }
503 [ - + ]: 18125899 : if (d_debugFreeAssumps)
504 : : {
505 : : // We have that npn is a node we occurring the final updated version of
506 : : // the proof. We can now debug based on the expected set of free
507 : : // assumptions.
508 [ - - ]: 0 : Trace("pfnu-debug") << "Ensure update closed..." << std::endl;
509 : 0 : pfnEnsureClosedWrt(
510 : : options(), cur.get(), fa, "pfnu-debug", "ProofNodeUpdater:finalize");
511 : : }
512 : 18125899 : }
513 : :
514 : 36845598 : bool ProofNodeUpdater::checkMergeProof(
515 : : std::shared_ptr<ProofNode>& cur,
516 : : const std::map<Node, std::shared_ptr<ProofNode>>& resCache,
517 : : std::unordered_map<const ProofNode*, bool>& cfaMap)
518 : : {
519 [ + + ]: 36845598 : if (d_mergeSubproofs)
520 : : {
521 : 16648359 : const Node& res = cur->getResult();
522 : : std::map<Node, std::shared_ptr<ProofNode>>::const_iterator itc =
523 : 16648359 : resCache.find(res);
524 [ + + ]: 16648359 : if (itc != resCache.end())
525 : : {
526 : 910299 : ProofNodeManager* pnm = d_env.getProofNodeManager();
527 [ - + ][ - + ]: 910299 : Assert(pnm != nullptr);
[ - - ]
528 : : // already have a proof, merge it into this one
529 : 910299 : pnm->updateNode(cur.get(), itc->second.get());
530 : : // does not contain free assumptions since the range of resCache does
531 : : // not contain free assumptions
532 : 910299 : cfaMap[cur.get()] = false;
533 : 910299 : return true;
534 : : }
535 [ + + ]: 16648359 : }
536 : 35935299 : return false;
537 : : }
538 : :
539 : 10284 : void ProofNodeUpdater::setFreeAssumptions(const std::vector<Node>& freeAssumps,
540 : : bool doDebug)
541 : : {
542 : 10284 : d_freeAssumps.clear();
543 : 20568 : d_freeAssumps.insert(
544 : 10284 : d_freeAssumps.end(), freeAssumps.begin(), freeAssumps.end());
545 : 10284 : d_debugFreeAssumps = doDebug;
546 : 10284 : }
547 : :
548 : : } // namespace cvc5::internal
|
