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