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_ensure_closed.h"
20 : : #include "proof/proof_node_algorithm.h"
21 : : #include "proof/proof_node_manager.h"
22 : : #include "smt/env.h"
23 : :
24 : : namespace cvc5::internal {
25 : :
26 : 69031 : ProofNodeUpdaterCallback::ProofNodeUpdaterCallback() {}
27 : 68988 : ProofNodeUpdaterCallback::~ProofNodeUpdaterCallback() {}
28 : :
29 : 932 : bool ProofNodeUpdaterCallback::update(Node res,
30 : : ProofRule id,
31 : : const std::vector<Node>& children,
32 : : const std::vector<Node>& args,
33 : : CDProof* cdp,
34 : : bool& continueUpdate)
35 : : {
36 : 932 : return false;
37 : : }
38 : :
39 : 10145100 : bool ProofNodeUpdaterCallback::shouldUpdatePost(std::shared_ptr<ProofNode> pn,
40 : : const std::vector<Node>& fa)
41 : : {
42 : 10145100 : return false;
43 : : }
44 : :
45 : 0 : bool ProofNodeUpdaterCallback::updatePost(Node res,
46 : : ProofRule id,
47 : : const std::vector<Node>& children,
48 : : const std::vector<Node>& args,
49 : : CDProof* cdp)
50 : : {
51 : 0 : return false;
52 : : }
53 : :
54 : 0 : bool ProofNodeUpdaterCallback::canMerge(std::shared_ptr<ProofNode> pn)
55 : : {
56 : : // by default, no restriction on what proofs can merge
57 : 0 : return true;
58 : : }
59 : :
60 : 58249 : ProofNodeUpdater::ProofNodeUpdater(Env& env,
61 : : ProofNodeUpdaterCallback& cb,
62 : : bool mergeSubproofs,
63 : 58249 : bool autoSym)
64 : : : EnvObj(env),
65 : : d_cb(cb),
66 : : d_debugFreeAssumps(false),
67 : : d_mergeSubproofs(mergeSubproofs),
68 : 58249 : d_autoSym(autoSym)
69 : : {
70 : 58249 : }
71 : :
72 : 528037 : void ProofNodeUpdater::process(std::shared_ptr<ProofNode> pf)
73 : : {
74 [ - + ]: 528037 : if (d_debugFreeAssumps)
75 : : {
76 [ - - ]: 0 : if (TraceIsOn("pfnu-debug"))
77 : : {
78 [ - - ]: 0 : Trace("pfnu-debug2") << "Initial proof: " << *pf.get() << std::endl;
79 [ - - ]: 0 : Trace("pfnu-debug") << "ProofNodeUpdater::process" << std::endl;
80 [ - - ]: 0 : Trace("pfnu-debug") << "Expected free assumptions: " << std::endl;
81 [ - - ]: 0 : for (const Node& fa : d_freeAssumps)
82 : : {
83 [ - - ]: 0 : Trace("pfnu-debug") << "- " << fa << std::endl;
84 : : }
85 : 0 : std::vector<Node> assump;
86 : 0 : expr::getFreeAssumptions(pf.get(), assump);
87 [ - - ]: 0 : Trace("pfnu-debug") << "Current free assumptions: " << std::endl;
88 [ - - ]: 0 : for (const Node& fa : assump)
89 : : {
90 [ - - ]: 0 : Trace("pfnu-debug") << "- " << fa << std::endl;
91 : : }
92 : : }
93 : : }
94 : 528037 : processInternal(pf, d_freeAssumps);
95 : 528037 : }
96 : :
97 : 528037 : void ProofNodeUpdater::processInternal(std::shared_ptr<ProofNode> pf,
98 : : std::vector<Node>& fa)
99 : : {
100 : : // Note that processInternal uses a single scope; fa is updated based on
101 : : // the current free assumptions of the proof nodes on the stack.
102 : :
103 : : // The list of proof nodes we are currently traversing beneath. This is used
104 : : // for checking for cycles in the overall proof.
105 : 1056070 : std::vector<std::shared_ptr<ProofNode>> traversing;
106 : : // Map from formulas to (closed) proof nodes that prove that fact
107 : 1056070 : std::map<Node, std::shared_ptr<ProofNode>> resCache;
108 : : // Map from formulas to non-closed proof nodes that prove that fact. These
109 : : // are replaced by proofs in the above map when applicable.
110 : 1056070 : std::map<Node, std::vector<std::shared_ptr<ProofNode>>> resCacheNcWaiting;
111 : : // Map from proof nodes to whether they contain assumptions
112 : 1056070 : std::unordered_map<const ProofNode*, bool> cfaMap;
113 : 1056070 : std::unordered_set<Node> cfaAllowed;
114 : 528037 : cfaAllowed.insert(fa.begin(), fa.end());
115 : 1056070 : std::shared_ptr<ProofNode> pft = pf;
116 [ + + ]: 532416 : while (pft->getRule() == ProofRule::SCOPE)
117 : : {
118 : 4379 : const std::vector<Node>& args = pft->getArguments();
119 : 4379 : cfaAllowed.insert(args.begin(), args.end());
120 : 4379 : pft = pft->getChildren()[0];
121 : : }
122 [ + - ]: 528037 : Trace("pf-process") << "ProofNodeUpdater::process" << std::endl;
123 : 1056070 : std::unordered_map<std::shared_ptr<ProofNode>, bool> visited;
124 : 528037 : std::unordered_map<std::shared_ptr<ProofNode>, bool>::iterator it;
125 : 1056070 : std::vector<std::shared_ptr<ProofNode>> visit;
126 : 0 : std::shared_ptr<ProofNode> cur;
127 : 528037 : visit.push_back(pf);
128 : 528037 : std::map<Node, std::shared_ptr<ProofNode>>::iterator itc;
129 : 68880100 : do
130 : : {
131 : 69408200 : cur = visit.back();
132 : 69408200 : visit.pop_back();
133 : 69408200 : it = visited.find(cur);
134 [ + + ]: 69408200 : if (it == visited.end())
135 : : {
136 : : // Check if there is a proof in resCache with the same result.
137 : : // Note that if this returns true, we update the contents of the current
138 : : // proof. Moreover, parents will replace the reference to this proof.
139 : : // Thus, replacing the contents of this proof is not (typically)
140 : : // necessary, but is done anyways in case there are any other references
141 : : // to this proof that are not handled by this loop, that is, proof
142 : : // nodes having this as a child that are not subproofs of pf.
143 [ + + ]: 23307200 : if (checkMergeProof(cur, resCache, cfaMap))
144 : : {
145 : 943311 : visited[cur] = true;
146 : 1392770 : continue;
147 : : }
148 : : // run update to a fixed point
149 : 22363900 : bool continueUpdate = true;
150 [ + + ][ + + ]: 24978300 : while (runUpdate(cur, fa, continueUpdate) && continueUpdate)
[ + - ][ + + ]
[ - - ]
151 : : {
152 [ + - ]: 2614370 : Trace("pf-process-debug") << "...updated proof." << std::endl;
153 : : }
154 : 22363900 : visited[cur] = !continueUpdate;
155 [ + + ]: 22363900 : if (!continueUpdate)
156 : : {
157 : : // no further changes should be made to cur according to the callback
158 [ + - ]: 898924 : Trace("pf-process-debug")
159 : 449462 : << "...marked to not continue update." << std::endl;
160 : 449462 : runFinalize(cur, fa, resCache, resCacheNcWaiting, cfaMap, cfaAllowed);
161 : 449462 : continue;
162 : : }
163 : 21914500 : traversing.push_back(cur);
164 : 21914500 : visit.push_back(cur);
165 : : // If we are not the top-level proof, we were a scope, or became a scope
166 : : // after updating, we do a separate recursive call to this method. This
167 : : // allows us to properly track the assumptions in scope, which is
168 : : // important for example to merge or to determine updates based on free
169 : : // assumptions.
170 [ + + ]: 21914500 : if (cur->getRule() == ProofRule::SCOPE)
171 : : {
172 : 335944 : const std::vector<Node>& args = cur->getArguments();
173 : 335944 : fa.insert(fa.end(), args.begin(), args.end());
174 : : }
175 : 21914500 : const std::vector<std::shared_ptr<ProofNode>>& ccp = cur->getChildren();
176 : : // now, process children
177 [ + + ]: 68880100 : for (const std::shared_ptr<ProofNode>& cp : ccp)
178 : : {
179 : 46965700 : if (std::find(traversing.begin(), traversing.end(), cp)
180 [ - + ]: 93931300 : != traversing.end())
181 : : {
182 : 0 : Unhandled()
183 : : << "ProofNodeUpdater::processInternal: cyclic proof! (use "
184 : 0 : "--proof-check=eager)"
185 : 0 : << std::endl;
186 : : }
187 : 46965700 : visit.push_back(cp);
188 : : }
189 : : }
190 [ + + ]: 46100900 : else if (!it->second)
191 : : {
192 [ - + ][ - + ]: 21914500 : Assert(!traversing.empty());
[ - - ]
193 : 21914500 : traversing.pop_back();
194 : 21914500 : visited[cur] = true;
195 : : // finalize the node
196 [ + + ]: 21914500 : if (cur->getRule() == ProofRule::SCOPE)
197 : : {
198 : 335944 : const std::vector<Node>& args = cur->getArguments();
199 [ - + ][ - + ]: 335944 : Assert(fa.size() >= args.size());
[ - - ]
200 : 335944 : fa.resize(fa.size() - args.size());
201 : : }
202 : : // maybe found a proof in the meantime, i.e. a subproof of the current
203 : : // proof with the same result. Same as above, updating the contents here
204 : : // is typically not necessary since references to this proof will be
205 : : // replaced.
206 [ + + ]: 21914500 : if (checkMergeProof(cur, resCache, cfaMap))
207 : : {
208 : 40319 : visited[cur] = true;
209 : 40319 : continue;
210 : : }
211 : 21874200 : runFinalize(cur, fa, resCache, resCacheNcWaiting, cfaMap, cfaAllowed);
212 : : }
213 [ + + ]: 69408200 : } while (!visit.empty());
214 [ + - ]: 528037 : Trace("pf-process") << "ProofNodeUpdater::process: finished" << std::endl;
215 : 528037 : }
216 : :
217 : 5754700 : bool ProofNodeUpdater::updateProofNode(std::shared_ptr<ProofNode> cur,
218 : : const std::vector<Node>& fa,
219 : : bool& continueUpdate,
220 : : bool preVisit)
221 : : {
222 : 5754700 : ProofRule id = cur->getRule();
223 : : // use CDProof to open a scope for which the callback updates
224 : 17264100 : CDProof cpf(d_env, nullptr, "ProofNodeUpdater::CDProof", d_autoSym);
225 : 5754700 : const std::vector<std::shared_ptr<ProofNode>>& cc = cur->getChildren();
226 : 11509400 : std::vector<Node> ccn;
227 [ + + ]: 20363100 : for (const std::shared_ptr<ProofNode>& cp : cc)
228 : : {
229 : 14608400 : Node cpres = cp->getResult();
230 : 14608400 : ccn.push_back(cpres);
231 : : // store in the proof
232 : 14608400 : cpf.addProof(cp);
233 : : }
234 : 11509400 : Node res = cur->getResult();
235 [ + - ]: 11509400 : Trace("pf-process-debug")
236 : 5754700 : << "Updating (" << cur->getRule() << "): " << res << std::endl;
237 : : // only if the callback updated the node
238 : 5754700 : if (preVisit
239 [ + + ][ + + ]: 11509400 : ? d_cb.update(res, id, ccn, cur->getArguments(), &cpf, continueUpdate)
[ - - ]
240 [ + + ][ + + ]: 5754700 : : d_cb.updatePost(res, id, ccn, cur->getArguments(), &cpf))
[ - - ]
241 : : {
242 : 6378030 : std::shared_ptr<ProofNode> npn = cpf.getProofFor(res);
243 : 3189010 : std::vector<Node> fullFa;
244 [ - + ]: 3189010 : if (d_debugFreeAssumps)
245 : : {
246 : 0 : expr::getFreeAssumptions(cur.get(), fullFa);
247 [ - - ]: 0 : Trace("pfnu-debug") << "Original proof : " << *cur << std::endl;
248 : : }
249 : : // then, update the original proof node based on this one
250 [ + - ]: 3189010 : Trace("pf-process-debug") << "Update node..." << std::endl;
251 : 3189010 : d_env.getProofNodeManager()->updateNode(cur.get(), npn.get());
252 [ + - ]: 3189010 : Trace("pf-process-debug") << "...update node finished." << std::endl;
253 [ - + ]: 3189010 : if (d_debugFreeAssumps)
254 : : {
255 : 0 : fullFa.insert(fullFa.end(), fa.begin(), fa.end());
256 : : // We have that npn is a node we occurring the final updated version of
257 : : // the proof. We can now debug based on the expected set of free
258 : : // assumptions.
259 [ - - ]: 0 : Trace("pfnu-debug") << "Ensure updated closed..." << std::endl;
260 : 0 : pfnEnsureClosedWrt(options(),
261 : : npn.get(),
262 : : fullFa,
263 : : "pfnu-debug",
264 : : "ProofNodeUpdater:postupdate");
265 : : }
266 [ + - ]: 3189010 : Trace("pf-process-debug") << "..finished" << std::endl;
267 : 3189010 : return true;
268 : : }
269 [ + - ]: 2565680 : Trace("pf-process-debug") << "..finished" << std::endl;
270 : 2565680 : return false;
271 : : }
272 : :
273 : 47430800 : bool ProofNodeUpdater::runUpdate(std::shared_ptr<ProofNode> cur,
274 : : const std::vector<Node>& fa,
275 : : bool& continueUpdate,
276 : : bool preVisit)
277 : : {
278 : : // should it be updated?
279 [ + + ][ + + ]: 94861600 : if (preVisit ? !d_cb.shouldUpdate(cur, fa, continueUpdate)
[ - - ]
280 [ + + ][ + + ]: 47430800 : : !d_cb.shouldUpdatePost(cur, fa))
[ - - ]
281 : : {
282 : 41676100 : return false;
283 : : }
284 : 5754700 : return updateProofNode(cur, fa, continueUpdate, preVisit);
285 : : }
286 : :
287 : 22452500 : void ProofNodeUpdater::runFinalize(
288 : : std::shared_ptr<ProofNode> cur,
289 : : const std::vector<Node>& fa,
290 : : std::map<Node, std::shared_ptr<ProofNode>>& resCache,
291 : : std::map<Node, std::vector<std::shared_ptr<ProofNode>>>& resCacheNcWaiting,
292 : : std::unordered_map<const ProofNode*, bool>& cfaMap,
293 : : const std::unordered_set<Node>& cfaAllowed)
294 : : {
295 : : // run update (marked as post-visit) to a fixed point
296 : : bool dummyContinueUpdate;
297 [ + + ]: 22452500 : while (runUpdate(cur, fa, dummyContinueUpdate, false))
298 : : {
299 [ + - ]: 128867 : Trace("pf-process-debug") << "...updated proof." << std::endl;
300 : : }
301 [ + + ]: 22323600 : if (d_mergeSubproofs)
302 : : {
303 : : // if we cannot merge this proof, skip it
304 [ + + ]: 9235620 : if (!d_cb.canMerge(cur))
305 : : {
306 : 363757 : return;
307 : : }
308 : 17743700 : Node res = cur->getResult();
309 : : // cache the result if we don't contain an assumption
310 [ + + ]: 8871870 : if (!expr::containsAssumption(cur.get(), cfaMap, cfaAllowed))
311 : : {
312 [ + - ]: 4633330 : Trace("pf-process-debug") << "No assumption pf: " << res << std::endl;
313 : : // cache result if we are merging subproofs
314 : 4633330 : resCache[res] = cur;
315 : : // go back and merge into the non-closed proofs of the same fact
316 : : std::map<Node, std::vector<std::shared_ptr<ProofNode>>>::iterator itnw =
317 : 4633330 : resCacheNcWaiting.find(res);
318 [ + + ]: 4633330 : if (itnw != resCacheNcWaiting.end())
319 : : {
320 : 3421 : ProofNodeManager* pnm = d_env.getProofNodeManager();
321 [ + + ]: 7918 : for (std::shared_ptr<ProofNode>& ncp : itnw->second)
322 : : {
323 : 4497 : pnm->updateNode(ncp.get(), cur.get());
324 : : }
325 : 3421 : resCacheNcWaiting.erase(res);
326 : : }
327 : : }
328 : : else
329 : : {
330 [ + - ]: 8477070 : Trace("pf-process-debug") << "Assumption pf: " << res << ", with "
331 : 4238530 : << cfaAllowed.size() << std::endl;
332 : 4238530 : resCacheNcWaiting[res].push_back(cur);
333 : : }
334 : : // Now, do update of children, that is, we replace children of the current
335 : : // proof with the representative child in the cache, if they are different.
336 : : // This is necessary to do here since we only locally update the contents of
337 : : // a proof when a duplicate is encountered. Updating the reference to a
338 : : // child is done here.
339 : 8871870 : std::map<Node, std::shared_ptr<ProofNode>>::iterator itr;
340 : 8871870 : const std::vector<std::shared_ptr<ProofNode>>& ccp = cur->getChildren();
341 : 17743700 : std::vector<std::shared_ptr<ProofNode>> newChildren;
342 : 8871870 : bool childChanged = false;
343 [ + + ]: 27099700 : for (const std::shared_ptr<ProofNode>& cp : ccp)
344 : : {
345 : 36455700 : Node cpres = cp->getResult();
346 : 18227800 : itr = resCache.find(cpres);
347 [ + + ][ + + ]: 18227800 : if (itr != resCache.end() && itr->second != cp)
[ + + ]
348 : : {
349 : 1380770 : newChildren.emplace_back(itr->second);
350 : 1380770 : childChanged = true;
351 : : }
352 : : else
353 : : {
354 : 16847100 : newChildren.emplace_back(cp);
355 : : }
356 : : }
357 [ + + ]: 8871870 : if (childChanged)
358 : : {
359 : 966251 : ProofNodeManager* pnm = d_env.getProofNodeManager();
360 : 966251 : pnm->updateNode(
361 : : cur.get(), cur->getRule(), newChildren, cur->getArguments());
362 : : }
363 : : }
364 [ - + ]: 21959900 : if (d_debugFreeAssumps)
365 : : {
366 : : // We have that npn is a node we occurring the final updated version of
367 : : // the proof. We can now debug based on the expected set of free
368 : : // assumptions.
369 [ - - ]: 0 : Trace("pfnu-debug") << "Ensure update closed..." << std::endl;
370 : 0 : pfnEnsureClosedWrt(
371 : : options(), cur.get(), fa, "pfnu-debug", "ProofNodeUpdater:finalize");
372 : : }
373 : : }
374 : :
375 : 45221700 : bool ProofNodeUpdater::checkMergeProof(
376 : : std::shared_ptr<ProofNode>& cur,
377 : : const std::map<Node, std::shared_ptr<ProofNode>>& resCache,
378 : : std::unordered_map<const ProofNode*, bool>& cfaMap)
379 : : {
380 [ + + ]: 45221700 : if (d_mergeSubproofs)
381 : : {
382 : 19495200 : const Node& res = cur->getResult();
383 : : std::map<Node, std::shared_ptr<ProofNode>>::const_iterator itc =
384 : 19495200 : resCache.find(res);
385 [ + + ]: 19495200 : if (itc != resCache.end())
386 : : {
387 : 983630 : ProofNodeManager* pnm = d_env.getProofNodeManager();
388 [ - + ][ - + ]: 983630 : Assert(pnm != nullptr);
[ - - ]
389 : : // already have a proof, merge it into this one
390 : 983630 : pnm->updateNode(cur.get(), itc->second.get());
391 : : // does not contain free assumptions since the range of resCache does
392 : : // not contain free assumptions
393 : 983630 : cfaMap[cur.get()] = false;
394 : 983630 : return true;
395 : : }
396 : : }
397 : 44238100 : return false;
398 : : }
399 : :
400 : 11570 : void ProofNodeUpdater::setFreeAssumptions(const std::vector<Node>& freeAssumps,
401 : : bool doDebug)
402 : : {
403 : 11570 : d_freeAssumps.clear();
404 : : d_freeAssumps.insert(
405 : 11570 : d_freeAssumps.end(), freeAssumps.begin(), freeAssumps.end());
406 : 11570 : d_debugFreeAssumps = doDebug;
407 : 11570 : }
408 : :
409 : : } // namespace cvc5::internal
|
