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 lazy proof utility.
11 : : */
12 : :
13 : : #include "proof/lazy_proof_chain.h"
14 : :
15 : : #include "options/proof_options.h"
16 : : #include "proof/proof.h"
17 : : #include "proof/proof_ensure_closed.h"
18 : : #include "proof/proof_node.h"
19 : : #include "proof/proof_node_algorithm.h"
20 : : #include "proof/proof_node_manager.h"
21 : :
22 : : namespace cvc5::internal {
23 : :
24 : 82059 : LazyCDProofChain::LazyCDProofChain(Env& env,
25 : : bool cyclic,
26 : : context::Context* c,
27 : : ProofGenerator* defGen,
28 : : bool defRec,
29 : 82059 : const std::string& name)
30 : : : CDProof(env, c, name, false),
31 : 82059 : d_cyclic(cyclic),
32 : 82059 : d_defRec(defRec),
33 : 82059 : d_context(),
34 [ + + ]: 82059 : d_gens(c ? c : &d_context),
35 : 82059 : d_defGen(defGen),
36 : 164118 : d_name(name)
37 : : {
38 : 82059 : }
39 : :
40 : 121359 : LazyCDProofChain::~LazyCDProofChain() {}
41 : :
42 : 0 : const std::map<Node, std::shared_ptr<ProofNode>> LazyCDProofChain::getLinks()
43 : : const
44 : : {
45 : 0 : std::map<Node, std::shared_ptr<ProofNode>> links;
46 [ - - ]: 0 : for (const std::pair<const Node, ProofGenerator* const>& link : d_gens)
47 : : {
48 : 0 : Assert(link.second);
49 : 0 : std::shared_ptr<ProofNode> pfn = link.second->getProofFor(link.first);
50 : 0 : Assert(pfn);
51 : 0 : links[link.first] = pfn;
52 : 0 : }
53 : 0 : return links;
54 : 0 : }
55 : :
56 : 102100 : std::shared_ptr<ProofNode> LazyCDProofChain::getProofFor(Node fact)
57 : : {
58 [ + - ]: 204200 : Trace("lazy-cdproofchain")
59 : 102100 : << "LazyCDProofChain::getProofFor of gen " << d_name << "\n";
60 [ + - ]: 204200 : Trace("lazy-cdproofchain")
61 : 102100 : << "LazyCDProofChain::getProofFor: " << fact << "\n";
62 : : // which facts have had proofs retrieved for. This is maintained to avoid
63 : : // cycles. It also saves the proof node of the fact
64 : 102100 : std::unordered_map<Node, std::shared_ptr<ProofNode>> toConnect;
65 : : // leaves of proof node links in the chain, i.e. assumptions, yet to be
66 : : // expanded
67 : : std::unordered_map<Node, std::vector<std::shared_ptr<ProofNode>>>
68 : 102100 : assumptionsToExpand;
69 : : // invariant of the loop below, the first iteration notwithstanding:
70 : : // visit = domain(assumptionsToExpand) \ domain(toConnect)
71 : 306300 : std::vector<Node> visit{fact};
72 : 102100 : std::unordered_map<Node, bool> visited;
73 : 102100 : Node cur;
74 : : do
75 : : {
76 : 10375817 : cur = visit.back();
77 : 10375817 : visit.pop_back();
78 : 10375817 : auto itVisited = visited.find(cur);
79 : : // pre-traversal
80 [ + + ]: 10375817 : if (itVisited == visited.end())
81 : : {
82 [ + - ]: 2825520 : Trace("lazy-cdproofchain")
83 : 1412760 : << "LazyCDProofChain::getProofFor: check " << cur << "\n";
84 [ - + ][ - + ]: 1412760 : Assert(toConnect.find(cur) == toConnect.end());
[ - - ]
85 : : // The current fact may be justified by concrete steps added to this
86 : : // proof, in which case we do not use the generators.
87 : 1412760 : bool rec = true;
88 : 1412760 : std::shared_ptr<ProofNode> curPfn = getProofForInternal(cur, rec);
89 [ + + ]: 1412760 : if (curPfn == nullptr)
90 : : {
91 [ + - ]: 2015194 : Trace("lazy-cdproofchain")
92 : 1007597 : << "LazyCDProofChain::getProofFor: No proof found, skip\n";
93 : 1007597 : visited[cur] = true;
94 : 1007597 : continue;
95 : : }
96 : : // map node whose proof node must be expanded to the respective poof
97 : : // node
98 : 405163 : toConnect[cur] = curPfn;
99 : : // We may not want to recursively connect this proof so we skip.
100 [ + + ]: 405163 : if (!rec)
101 : : {
102 : 58794 : visited[cur] = true;
103 : 58794 : continue;
104 : : }
105 [ + - ]: 692738 : Trace("lazy-cdproofchain-debug")
106 : 0 : << "LazyCDProofChain::getProofFor: stored proof: " << *curPfn.get()
107 : 346369 : << "\n";
108 : : // retrieve free assumptions and their respective proof nodes
109 : 346369 : std::map<Node, std::vector<std::shared_ptr<ProofNode>>> famap;
110 : 346369 : expr::getFreeAssumptionsMap(curPfn, famap);
111 [ + - ]: 346369 : if (d_cyclic)
112 : : {
113 : : // First check for a trivial cycle, which is when cur is a free
114 : : // assumption of curPfn. Note that in the special case in which curPfn
115 : : // has cur as an assumption and cur is actually the initial fact that
116 : : // getProofFor is called on, the general cycle detection below would
117 : : // prevent this method from generating a proof for cur, which would be
118 : : // wrong since there is a justification for it in curPfn.
119 : 346369 : bool isCyclic = false;
120 [ + + ]: 10323436 : for (const auto& fap : famap)
121 : : {
122 [ + + ]: 10026738 : if (cur == fap.first)
123 : : {
124 : : // connect it to one of the assumption proof nodes
125 : 49671 : toConnect[cur] = fap.second[0];
126 : 49671 : isCyclic = true;
127 : 49671 : break;
128 : : }
129 : : }
130 [ + + ]: 346369 : if (isCyclic)
131 : : {
132 [ + - ]: 99342 : Trace("lazy-cdproofchain")
133 : 0 : << "LazyCDProofChain::getProofFor: trivial cycle detected for "
134 : 49671 : << cur << ", abort\n";
135 : 49671 : visited[cur] = true;
136 : 49671 : continue;
137 : : }
138 [ - + ]: 296698 : if (TraceIsOn("lazy-cdproofchain"))
139 : : {
140 : 0 : unsigned alreadyToVisit = 0;
141 [ - - ]: 0 : Trace("lazy-cdproofchain")
142 : 0 : << "LazyCDProofChain::getProofFor: " << famap.size()
143 : 0 : << " free assumptions:\n";
144 [ - - ]: 0 : for (auto fap : famap)
145 : : {
146 [ - - ]: 0 : Trace("lazy-cdproofchain")
147 : 0 : << "LazyCDProofChain::getProofFor: - " << fap.first << "\n";
148 : 0 : alreadyToVisit +=
149 : 0 : std::find(visit.begin(), visit.end(), fap.first) != visit.end()
150 [ - - ]: 0 : ? 1
151 : : : 0;
152 : 0 : }
153 [ - - ]: 0 : Trace("lazy-cdproofchain")
154 : 0 : << "LazyCDProofChain::getProofFor: " << alreadyToVisit
155 : 0 : << " already to visit\n";
156 : : }
157 : : // If we are controlling cycle, check whether any of the assumptions of
158 : : // cur would provoke a cycle. In such we remove cur from toConnect and
159 : : // do not proceed to expand any of its assumptions.
160 [ + - ]: 593396 : Trace("lazy-cdproofchain") << "LazyCDProofChain::getProofFor: marking "
161 : 296698 : << cur << " for cycle check\n";
162 : : // enqueue free assumptions to process
163 [ + + ]: 10273729 : for (const auto& fap : famap)
164 : : {
165 : : // A cycle is characterized by cur having an assumption being
166 : : // *currently* expanded that is seen again, i.e. in toConnect and not
167 : : // yet post-visited
168 : 9977043 : auto itToConnect = toConnect.find(fap.first);
169 [ + + ][ + + ]: 9977043 : if (itToConnect != toConnect.end() && !visited[fap.first])
[ + + ]
170 : : {
171 : : // Since we have a cycle with an assumption, we must:
172 : : // - remove that assumption from toConnect, since this class cannot
173 : : // generate a well-formed proof to it.
174 : : // - remove curr from toConnect, since its proof will no longer be
175 : : // needed. Note that nothing prevents cur from appearing as a
176 : : // dependency in another chain and being then expanded,
177 : : // podentially without a cycle.
178 : 12 : isCyclic = true;
179 [ + - ]: 24 : Trace("lazy-cdproofchain")
180 : 0 : << "LazyCDProofChain::getProofFor: cyclic assumption "
181 : 12 : << fap.first << "; removing it from toConnect\n";
182 : 12 : toConnect.erase(itToConnect);
183 : 12 : break;
184 : : }
185 : : }
186 [ + + ]: 296698 : if (isCyclic)
187 : : {
188 [ + - ]: 24 : Trace("lazy-cdproofchain")
189 : 0 : << "LazyCDProofChain::getProofFor: Removing " << cur
190 : 12 : << " from toConnect\n";
191 : 12 : toConnect.erase(toConnect.find(cur));
192 : 12 : continue;
193 : : }
194 : 296686 : visit.push_back(cur);
195 : 296686 : visited[cur] = false;
196 : : }
197 : : else
198 : : {
199 : 0 : visited[cur] = true;
200 : : }
201 : : // enqueue free assumptions to process
202 [ + + ]: 10273717 : for (const auto& fap : famap)
203 : : {
204 [ + - ]: 19954062 : Trace("lazy-cdproofchain")
205 : 0 : << "LazyCDProofChain::getProofFor: marking " << fap.first
206 : 0 : << " for revisit and for expansion (curr: "
207 : 0 : << assumptionsToExpand[fap.first].size()
208 : 9977031 : << ", adding: " << fap.second.size() << ")\n";
209 : : // We always add assumptions to visit so that their last seen occurrence
210 : : // is expanded (rather than the first seen occurrence, if we were not
211 : : // adding assumptions, say, in assumptionsToExpand). This is so because
212 : : // in the case where we are checking cycles this is necessary (and
213 : : // harmless when we are not). For example the cycle
214 : : //
215 : : // a2
216 : : // ...
217 : : // ----
218 : : // a1
219 : : // ...
220 : : // --------
221 : : // a0 a1 a2
222 : : // ...
223 : : // ---------------
224 : : // n
225 : : //
226 : : // in which a2 has a1 as an assumption, which has a2 an assumption,
227 : : // would not be captured if we did not revisit a1, which is an
228 : : // assumption of n and this already occur in assumptionsToExpand when
229 : : // it shows up again as an assumption of a2.
230 : 9977031 : visit.push_back(fap.first);
231 : : // add assumption proof nodes to be updated
232 : 19954062 : assumptionsToExpand[fap.first].insert(
233 : 19954062 : assumptionsToExpand[fap.first].end(),
234 : : fap.second.begin(),
235 : : fap.second.end());
236 : : }
237 [ + - ]: 296686 : if (d_cyclic)
238 : : {
239 [ + - ]: 296686 : Trace("lazy-cdproofchain") << push;
240 [ + - ]: 296686 : Trace("lazy-cdproofchain-debug") << push;
241 : : }
242 [ + + ][ + + ]: 1462443 : }
243 [ + + ]: 8963057 : else if (!itVisited->second)
244 : : {
245 : 296686 : visited[cur] = true;
246 [ + - ]: 296686 : Trace("lazy-cdproofchain") << pop;
247 [ + - ]: 296686 : Trace("lazy-cdproofchain-debug") << pop;
248 [ + - ]: 593372 : Trace("lazy-cdproofchain")
249 : 296686 : << "LazyCDProofChain::getProofFor: post-visited " << cur << "\n";
250 : : }
251 : : else
252 : : {
253 [ + - ]: 17332742 : Trace("lazy-cdproofchain")
254 : 0 : << "LazyCDProofChain::getProofFor: already fully processed " << cur
255 : 8666371 : << "\n";
256 : : }
257 [ + + ]: 10375817 : } while (!visit.empty());
258 : 102100 : ProofNodeManager* pnm = getManager();
259 : : // expand all assumptions marked to be connected
260 : 102100 : for (const std::pair<const Node, std::shared_ptr<ProofNode>>& npfn :
261 [ + + ]: 609339 : toConnect)
262 : : {
263 : 405139 : auto it = assumptionsToExpand.find(npfn.first);
264 [ + + ]: 405139 : if (it == assumptionsToExpand.end())
265 : : {
266 [ - + ][ - + ]: 99028 : Assert(npfn.first == fact);
[ - - ]
267 : 99028 : continue;
268 : : }
269 [ - + ][ - + ]: 306111 : Assert(npfn.second);
[ - - ]
270 [ + - ]: 612222 : Trace("lazy-cdproofchain")
271 : 0 : << "LazyCDProofChain::getProofFor: expand assumption " << npfn.first
272 : 306111 : << "\n";
273 [ + - ]: 612222 : Trace("lazy-cdproofchain-debug")
274 : 0 : << "LazyCDProofChain::getProofFor: ...expand to " << *npfn.second.get()
275 : 306111 : << "\n";
276 : : // update each assumption proof node
277 [ + + ]: 1672924 : for (std::shared_ptr<ProofNode> pfn : it->second)
278 : : {
279 : 1366813 : pnm->updateNode(pfn.get(), npfn.second.get());
280 : 1366813 : }
281 : : }
282 [ + - ]: 102100 : Trace("lazy-cdproofchain") << "===========\n";
283 : : // final proof of fact
284 : 102100 : auto it = toConnect.find(fact);
285 [ + + ]: 102100 : if (it == toConnect.end())
286 : : {
287 : 3072 : return nullptr;
288 : : }
289 : 99028 : return it->second;
290 : 102100 : }
291 : :
292 : 448655 : void LazyCDProofChain::addLazyStep(Node expected, ProofGenerator* pg)
293 : : {
294 [ - + ][ - + ]: 448655 : Assert(pg != nullptr);
[ - - ]
295 [ + - ]: 897310 : Trace("lazy-cdproofchain") << "LazyCDProofChain::addLazyStep: " << expected
296 [ - + ][ - - ]: 448655 : << " set to generator " << pg->identify() << "\n";
297 : : // note this will replace the generator for expected, if any
298 : 448655 : d_gens.insert(expected, pg);
299 : 448655 : }
300 : :
301 : 0 : void LazyCDProofChain::addLazyStep(Node expected,
302 : : ProofGenerator* pg,
303 : : const std::vector<Node>& assumptions,
304 : : const char* ctx)
305 : : {
306 : 0 : Assert(pg != nullptr);
307 [ - - ]: 0 : Trace("lazy-cdproofchain") << "LazyCDProofChain::addLazyStep: " << expected
308 : 0 : << " set to generator " << pg->identify() << "\n";
309 : : // note this will rewrite the generator for expected, if any
310 : 0 : d_gens.insert(expected, pg);
311 : : // check if chain is closed if eager checking is on
312 [ - - ]: 0 : if (options().proof.proofCheck == options::ProofCheckMode::EAGER)
313 : : {
314 [ - - ]: 0 : Trace("lazy-cdproofchain")
315 : 0 : << "LazyCDProofChain::addLazyStep: Checking closed proof...\n";
316 : 0 : std::shared_ptr<ProofNode> pfn = pg->getProofFor(expected);
317 : 0 : std::vector<Node> allowedLeaves{assumptions.begin(), assumptions.end()};
318 : : // add all current links in the chain
319 [ - - ]: 0 : for (const std::pair<const Node, ProofGenerator* const>& link : d_gens)
320 : : {
321 : 0 : allowedLeaves.push_back(link.first);
322 : : }
323 [ - - ]: 0 : if (TraceIsOn("lazy-cdproofchain"))
324 : : {
325 [ - - ]: 0 : Trace("lazy-cdproofchain") << "Checking relative to leaves...\n";
326 [ - - ]: 0 : for (const Node& n : allowedLeaves)
327 : : {
328 [ - - ]: 0 : Trace("lazy-cdproofchain") << " - " << n << "\n";
329 : : }
330 [ - - ]: 0 : Trace("lazy-cdproofchain") << "\n";
331 : : }
332 : 0 : pfnEnsureClosedWrt(
333 : : options(), pfn.get(), allowedLeaves, "lazy-cdproofchain", ctx);
334 : 0 : }
335 : 0 : }
336 : :
337 : 209907 : bool LazyCDProofChain::hasGenerator(Node fact) const
338 : : {
339 : 209907 : return d_gens.find(fact) != d_gens.end();
340 : : }
341 : :
342 : 0 : ProofGenerator* LazyCDProofChain::getGeneratorFor(Node fact)
343 : : {
344 : 0 : bool rec = true;
345 : 0 : return getGeneratorForInternal(fact, rec);
346 : : }
347 : :
348 : 1412737 : ProofGenerator* LazyCDProofChain::getGeneratorForInternal(Node fact, bool& rec)
349 : : {
350 : 1412737 : auto it = d_gens.find(fact);
351 [ + + ]: 1412737 : if (it != d_gens.end())
352 : : {
353 : 298482 : return (*it).second;
354 : : }
355 : : // otherwise, if no explicit generators, we use the default one
356 [ + + ]: 1114255 : if (d_defGen != nullptr)
357 : : {
358 : 116037 : rec = d_defRec;
359 : 116037 : return d_defGen;
360 : : }
361 : 998218 : return nullptr;
362 : : }
363 : :
364 : 1412760 : std::shared_ptr<ProofNode> LazyCDProofChain::getProofForInternal(Node fact,
365 : : bool& rec)
366 : : {
367 : 1412760 : std::shared_ptr<ProofNode> pfn = CDProof::getProofFor(fact);
368 [ - + ][ - + ]: 1412760 : Assert(pfn != nullptr);
[ - - ]
369 : : // If concrete proof, save it, otherwise try generators.
370 [ + + ]: 1412760 : if (pfn->getRule() != ProofRule::ASSUME)
371 : : {
372 : 23 : return pfn;
373 : : }
374 : 1412737 : ProofGenerator* pg = getGeneratorForInternal(fact, rec);
375 [ + + ]: 1412737 : if (!pg)
376 : : {
377 : 998218 : return nullptr;
378 : : }
379 [ + - ]: 829038 : Trace("lazy-cdproofchain")
380 [ - + ][ - - ]: 414519 : << "LazyCDProofChain::getProofFor: Call generator " << pg->identify()
381 : 414519 : << " for chain link " << fact << "\n";
382 : 414519 : return pg->getProofFor(fact);
383 : 1412760 : }
384 : :
385 : 0 : std::string LazyCDProofChain::identify() const { return d_name; }
386 : :
387 : : } // namespace cvc5::internal
|
