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 proof node manager.
11 : : */
12 : :
13 : : #include "proof/proof_node_manager.h"
14 : :
15 : : #include <sstream>
16 : :
17 : : #include "options/proof_options.h"
18 : : #include "proof/proof.h"
19 : : #include "proof/proof_checker.h"
20 : : #include "proof/proof_node.h"
21 : : #include "proof/proof_node_algorithm.h"
22 : : #include "theory/rewriter.h"
23 : :
24 : : using namespace cvc5::internal::kind;
25 : :
26 : : namespace cvc5::internal {
27 : :
28 : 18896 : ProofNodeManager::ProofNodeManager(NodeManager* nm,
29 : : const Options& opts,
30 : : theory::Rewriter* rr,
31 : 18896 : ProofChecker* pc)
32 : 18896 : : d_opts(opts), d_rewriter(rr), d_checker(pc)
33 : : {
34 : 18896 : d_true = nm->mkConst(true);
35 : : // we always allocate a proof checker, regardless of the proof checking mode
36 [ - + ][ - + ]: 18896 : Assert(d_checker != nullptr);
[ - - ]
37 : 18896 : }
38 : :
39 : 66238054 : std::shared_ptr<ProofNode> ProofNodeManager::mkNode(
40 : : ProofRule id,
41 : : const std::vector<std::shared_ptr<ProofNode>>& children,
42 : : const std::vector<Node>& args,
43 : : Node expected)
44 : : {
45 [ + - ]: 132476108 : Trace("pnm") << "ProofNodeManager::mkNode " << id << " {" << expected.getId()
46 : 66238054 : << "} " << expected << "\n";
47 : 66238054 : bool didCheck = false;
48 : 66238054 : Node res = checkInternal(id, children, args, expected, didCheck);
49 [ - + ]: 66238054 : if (res.isNull())
50 : : {
51 : : // if it was invalid, then we return the null node
52 : 0 : return nullptr;
53 : : }
54 : : // otherwise construct the proof node and set its proven field
55 : : std::shared_ptr<ProofNode> pn =
56 : 66238054 : std::make_shared<ProofNode>(id, children, args);
57 : 66238054 : pn->d_proven = res;
58 : 66238054 : pn->d_provenChecked = didCheck;
59 : 66238054 : return pn;
60 : 66238054 : }
61 : :
62 : 22786 : std::shared_ptr<ProofNode> ProofNodeManager::mkTrustedNode(
63 : : TrustId id,
64 : : const std::vector<std::shared_ptr<ProofNode>>& children,
65 : : const std::vector<Node>& args,
66 : : const Node& conc)
67 : : {
68 : 22786 : std::vector<Node> sargs;
69 : 22786 : sargs.push_back(mkTrustId(conc.getNodeManager(), id));
70 : 22786 : sargs.push_back(conc);
71 : 22786 : sargs.insert(sargs.end(), args.begin(), args.end());
72 : 45572 : return mkNode(ProofRule::TRUST, children, sargs);
73 : 22786 : }
74 : :
75 : 19465068 : std::shared_ptr<ProofNode> ProofNodeManager::mkAssume(Node fact)
76 : : {
77 [ - + ][ - + ]: 19465068 : Assert(!fact.isNull());
[ - - ]
78 [ - + ][ - + ]: 19465068 : Assert(fact.getType().isBoolean());
[ - - ]
79 : 38930136 : return mkNode(ProofRule::ASSUME, {}, {fact}, fact);
80 : : }
81 : :
82 : 2351839 : std::shared_ptr<ProofNode> ProofNodeManager::mkSymm(
83 : : std::shared_ptr<ProofNode> child, Node expected)
84 : : {
85 [ + + ]: 2351839 : if (child->getRule() == ProofRule::SYMM)
86 : : {
87 : 2030 : Assert(expected.isNull()
88 : : || child->getChildren()[0]->getResult() == expected);
89 : 2030 : return child->getChildren()[0];
90 : : }
91 : 4699618 : return mkNode(ProofRule::SYMM, {child}, {}, expected);
92 : : }
93 : :
94 : 2555 : std::shared_ptr<ProofNode> ProofNodeManager::mkTrans(
95 : : const std::vector<std::shared_ptr<ProofNode>>& children, Node expected)
96 : : {
97 [ - + ][ - + ]: 2555 : Assert(!children.empty());
[ - - ]
98 [ - + ]: 2555 : if (children.size() == 1)
99 : : {
100 : 0 : Assert(expected.isNull() || children[0]->getResult() == expected);
101 : 0 : return children[0];
102 : : }
103 : 2555 : return mkNode(ProofRule::TRANS, children, {}, expected);
104 : : }
105 : :
106 : 1313861 : std::shared_ptr<ProofNode> ProofNodeManager::mkScope(
107 : : std::shared_ptr<ProofNode> pf,
108 : : std::vector<Node>& assumps,
109 : : bool ensureClosed,
110 : : bool doMinimize,
111 : : Node expected)
112 : : {
113 [ + + ][ + - ]: 1313861 : if (!ensureClosed && !doMinimize)
114 : : {
115 : 1159562 : return mkNode(ProofRule::SCOPE, {pf}, assumps, expected);
116 : : }
117 [ + - ]: 734080 : Trace("pnm-scope") << "ProofNodeManager::mkScope " << assumps << std::endl;
118 : : // we first ensure the assumptions are flattened
119 : 734080 : std::unordered_set<Node> ac{assumps.begin(), assumps.end()};
120 : : // map from the rewritten form of assumptions to the original. This is only
121 : : // computed in the rare case when we need rewriting to match the
122 : : // assumptions. An example of this is for Boolean constant equalities in
123 : : // scoped proofs from the proof equality engine.
124 : 734080 : std::unordered_map<Node, Node> acr;
125 : : // whether we have compute the map above
126 : 734080 : bool computedAcr = false;
127 : :
128 : : // The free assumptions of the proof
129 : 734080 : std::map<Node, std::vector<std::shared_ptr<ProofNode>>> famap;
130 : 734080 : expr::getFreeAssumptionsMap(pf, famap);
131 : 734080 : std::unordered_set<Node> acu;
132 : 734080 : for (const std::pair<const Node, std::vector<std::shared_ptr<ProofNode>>>&
133 [ + + ]: 5505152 : fa : famap)
134 : : {
135 : 4036992 : Node a = fa.first;
136 [ + + ]: 4036992 : if (ac.find(a) != ac.end())
137 : : {
138 : : // already covered by an assumption
139 : 3107192 : acu.insert(a);
140 : 3107192 : continue;
141 : : }
142 [ + - ]: 929800 : Trace("pnm-scope") << "- try matching free assumption " << a << "\n";
143 : : // otherwise it may be due to symmetry?
144 : 929800 : Node aeqSym = CDProof::getSymmFact(a);
145 [ + - ]: 929800 : Trace("pnm-scope") << " - try sym " << aeqSym << "\n";
146 : 929800 : Node aMatch;
147 [ + + ][ + - ]: 929800 : if (!aeqSym.isNull() && ac.count(aeqSym))
[ + + ]
148 : : {
149 [ + - ]: 1857816 : Trace("pnm-scope") << "- reorient assumption " << aeqSym << " via " << a
150 : 928908 : << " for " << fa.second.size() << " proof nodes"
151 : 928908 : << std::endl;
152 : 928908 : aMatch = aeqSym;
153 : : }
154 : : else
155 : : {
156 : : // trivial assumption (by rewriting)
157 : 892 : Node ar = d_rewriter->rewrite(a);
158 [ + + ]: 892 : if (ar == d_true)
159 : : {
160 [ + - ]: 20 : Trace("pnm-scope") << "- justify trivial True assumption\n";
161 [ + + ]: 40 : for (std::shared_ptr<ProofNode> pfs : fa.second)
162 : : {
163 [ - + ][ - + ]: 20 : Assert(pfs->getResult() == a);
[ - - ]
164 : 40 : updateNode(pfs.get(), ProofRule::MACRO_SR_PRED_INTRO, {}, {a});
165 : 20 : }
166 [ + - ]: 20 : Trace("pnm-scope") << "...finished" << std::endl;
167 : 20 : acu.insert(a);
168 : 20 : continue;
169 : 20 : }
170 : : // Otherwise, may be derivable by rewriting. Note this is used in
171 : : // ensuring that proofs from the proof equality engine that involve
172 : : // equality with Boolean constants are closed.
173 [ + + ]: 872 : if (!computedAcr)
174 : : {
175 : 395 : computedAcr = true;
176 [ + + ]: 2884 : for (const Node& acc : ac)
177 : : {
178 : 2489 : Node accr = d_rewriter->rewrite(acc);
179 : 2489 : acr[accr] = acc;
180 : 2489 : }
181 : : }
182 [ + - ]: 872 : Trace("pnm-scope") << "- rewritten: " << ar << std::endl;
183 : 872 : std::unordered_map<Node, Node>::iterator itr = acr.find(ar);
184 [ + - ]: 872 : if (itr != acr.end())
185 : : {
186 : 872 : aMatch = itr->second;
187 : : }
188 [ + + ]: 892 : }
189 : :
190 : : // if we found a match either by symmetry or rewriting, then we connect
191 : : // the assumption here.
192 [ + - ]: 929780 : if (!aMatch.isNull())
193 : : {
194 : 929780 : std::shared_ptr<ProofNode> pfaa = mkAssume(aMatch);
195 : : // must correct the orientation on this leaf
196 : 929780 : std::vector<std::shared_ptr<ProofNode>> children;
197 : 929780 : children.push_back(pfaa);
198 [ + + ]: 1859648 : for (std::shared_ptr<ProofNode> pfs : fa.second)
199 : : {
200 [ - + ][ - + ]: 929868 : Assert(pfs->getResult() == a);
[ - - ]
201 : : // use SYMM if possible
202 [ + + ]: 929868 : if (aMatch == aeqSym)
203 : : {
204 [ - + ]: 928996 : if (pfaa->getRule() == ProofRule::SYMM)
205 : : {
206 : 0 : updateNode(pfs.get(), pfaa->getChildren()[0].get());
207 : : }
208 : : else
209 : : {
210 : 928996 : updateNode(pfs.get(), ProofRule::SYMM, children, {});
211 : : }
212 : : }
213 : : else
214 : : {
215 : 1744 : updateNode(
216 : : pfs.get(), ProofRule::MACRO_SR_PRED_TRANSFORM, children, {a});
217 : : }
218 : 929868 : }
219 [ + - ]: 929780 : Trace("pnm-scope") << "...finished" << std::endl;
220 : 929780 : acu.insert(aMatch);
221 : 929780 : continue;
222 : 929780 : }
223 [ - - ]: 0 : if (!ensureClosed)
224 : : {
225 : 0 : continue;
226 : : }
227 : : // If we did not find a match, it is an error, since all free assumptions
228 : : // should be arguments to SCOPE.
229 : 0 : std::stringstream ss;
230 : :
231 : 0 : bool dumpProofTraceOn = TraceIsOn("dump-proof-error");
232 [ - - ]: 0 : if (dumpProofTraceOn)
233 : : {
234 : 0 : ss << "The proof : " << *pf << std::endl;
235 : : }
236 : 0 : ss << std::endl << "Free assumption: " << a << std::endl;
237 [ - - ]: 0 : for (const Node& aprint : ac)
238 : : {
239 : 0 : ss << "- assumption: " << aprint << std::endl;
240 : : }
241 [ - - ]: 0 : if (!dumpProofTraceOn)
242 : : {
243 : 0 : ss << "Use -t dump-proof-error for details on proof" << std::endl;
244 : : }
245 : 0 : Unreachable() << "Generated a proof that is not closed by the scope: "
246 : 0 : << ss.str() << std::endl;
247 : 4036992 : }
248 [ + + ]: 734080 : if (acu.size() < ac.size())
249 : : {
250 : : // All assumptions should match a free assumption; if one does not, then
251 : : // the explanation could have been smaller.
252 [ + + ]: 824619 : for (const Node& a : ac)
253 : : {
254 [ + + ]: 777816 : if (acu.find(a) == acu.end())
255 : : {
256 [ + - ]: 206042 : Trace("pnm") << "ProofNodeManager::mkScope: assumption " << a
257 : 0 : << " does not match a free assumption in proof"
258 : 103021 : << std::endl;
259 : : }
260 : : }
261 : : }
262 [ + + ][ + + ]: 734080 : if (doMinimize && acu.size() < ac.size())
[ + + ]
263 : : {
264 : 42314 : assumps.clear();
265 : 42314 : assumps.insert(assumps.end(), acu.begin(), acu.end());
266 : : }
267 [ + + ]: 691766 : else if (ac.size() < assumps.size())
268 : : {
269 : : // remove duplicates to avoid redundant literals in clauses
270 : 1567 : assumps.clear();
271 : 1567 : assumps.insert(assumps.end(), ac.begin(), ac.end());
272 : : }
273 : 734080 : Node minExpected;
274 : 734080 : Node exp;
275 [ + + ]: 734080 : if (assumps.empty())
276 : : {
277 : : // SCOPE with no arguments is a no-op, just return original
278 : 9303 : return pf;
279 : : }
280 : 724777 : Node conc = pf->getResult();
281 : 724777 : NodeManager* nm = conc.getNodeManager();
282 [ + + ]: 724777 : exp = assumps.size() == 1 ? assumps[0] : nm->mkNode(Kind::AND, assumps);
283 [ + + ][ + + ]: 724777 : if (conc.isConst() && !conc.getConst<bool>())
[ + + ]
284 : : {
285 : 206380 : minExpected = exp.notNode();
286 : : }
287 : : else
288 : : {
289 : 518397 : minExpected = nm->mkNode(Kind::IMPLIES, exp, conc);
290 : : }
291 : 1449554 : return mkNode(ProofRule::SCOPE, {pf}, assumps, minExpected);
292 : 734080 : }
293 : :
294 : 2171831 : bool ProofNodeManager::updateNode(
295 : : ProofNode* pn,
296 : : ProofRule id,
297 : : const std::vector<std::shared_ptr<ProofNode>>& children,
298 : : const std::vector<Node>& args)
299 : : {
300 : 2171831 : return updateNodeInternal(pn, id, children, args, true);
301 : : }
302 : :
303 : 9793996 : bool ProofNodeManager::updateNode(ProofNode* pn, ProofNode* pnr)
304 : : {
305 [ - + ][ - + ]: 9793996 : Assert(pn != nullptr);
[ - - ]
306 [ - + ][ - + ]: 9793996 : Assert(pnr != nullptr);
[ - - ]
307 [ + + ]: 9793996 : if (pn == pnr)
308 : : {
309 : : // same node, no update necessary
310 : 20626 : return true;
311 : : }
312 [ - + ]: 9773370 : if (pn->getResult() != pnr->getResult())
313 : : {
314 : 0 : return false;
315 : : }
316 : : // copy whether we did the check
317 : 9773370 : pn->d_provenChecked = pnr->d_provenChecked;
318 : : // can shortcut re-check of rule
319 : 9773370 : return updateNodeInternal(
320 : 9773370 : pn, pnr->getRule(), pnr->getChildren(), pnr->getArguments(), false);
321 : : }
322 : :
323 : 2211702 : void ProofNodeManager::ensureChecked(ProofNode* pn)
324 : : {
325 [ + + ]: 2211702 : if (pn->d_provenChecked)
326 : : {
327 : : // already checked
328 : 32380 : return;
329 : : }
330 : : // directly call the proof checker
331 : 2179322 : Node res = d_checker->check(pn, pn->getResult());
332 : 2179322 : pn->d_provenChecked = true;
333 : : // should have the correct result
334 [ - + ][ - + ]: 2179322 : Assert(res == pn->d_proven);
[ - - ]
335 : 2179322 : }
336 : :
337 : 68409885 : Node ProofNodeManager::checkInternal(
338 : : ProofRule id,
339 : : const std::vector<std::shared_ptr<ProofNode>>& children,
340 : : const std::vector<Node>& args,
341 : : Node expected,
342 : : bool& didCheck)
343 : : {
344 : : // if the user supplied an expected result, then we trust it if we are in
345 : : // a proof checking mode that does not eagerly check rule applications
346 [ + + ]: 68409885 : if (!expected.isNull())
347 : : {
348 [ + + ]: 65662059 : if (d_opts.proof.proofCheck == options::ProofCheckMode::LAZY
349 [ + + ]: 37516324 : || d_opts.proof.proofCheck == options::ProofCheckMode::NONE)
350 : : {
351 : 65554273 : return expected;
352 : : }
353 : : }
354 : : // check with the checker, which takes expected as argument
355 : 2855612 : Node res = d_checker->check(id, children, args, expected);
356 : 2855612 : didCheck = true;
357 [ - + ][ - + ]: 2855612 : Assert(!res.isNull())
[ - - ]
358 : 0 : << "ProofNodeManager::checkInternal: failed to check proof";
359 : 2855612 : return res;
360 : 2855612 : }
361 : :
362 : 44245927 : ProofChecker* ProofNodeManager::getChecker() const { return d_checker; }
363 : :
364 : 1473053 : ProofNode* ProofNodeManager::cancelDoubleSymm(ProofNode* pn)
365 : : {
366 : : // processed is almost always size <= 1
367 : 1473053 : std::vector<ProofNode*> processed;
368 [ + + ]: 1473128 : while (pn->getRule() == ProofRule::SYMM)
369 : : {
370 : 1473053 : std::shared_ptr<ProofNode> pnc = pn->getChildren()[0];
371 [ + + ]: 1473053 : if (pnc->getRule() == ProofRule::SYMM)
372 : : {
373 : 75 : pn = pnc->getChildren()[0].get();
374 [ - + ]: 75 : if (std::find(processed.begin(), processed.end(), pn) != processed.end())
375 : : {
376 : 0 : Unreachable()
377 : 0 : << "Cyclic proof encountered when cancelling double symmetry";
378 : : }
379 : 75 : processed.push_back(pn);
380 : : }
381 : : else
382 : : {
383 : 1472978 : break;
384 : : }
385 [ + + ]: 1473053 : }
386 : 1473053 : return pn;
387 : 1473053 : }
388 : :
389 : 11945201 : bool ProofNodeManager::updateNodeInternal(
390 : : ProofNode* pn,
391 : : ProofRule id,
392 : : const std::vector<std::shared_ptr<ProofNode>>& children,
393 : : const std::vector<Node>& args,
394 : : bool needsCheck)
395 : : {
396 [ - + ][ - + ]: 11945201 : Assert(pn != nullptr);
[ - - ]
397 : : // ---------------- check for cyclic
398 [ + + ]: 11945201 : if (d_opts.proof.proofCheck == options::ProofCheckMode::EAGER)
399 : : {
400 : 17519 : std::unordered_set<const ProofNode*> visited;
401 [ + + ]: 29415 : for (const std::shared_ptr<ProofNode>& cpc : children)
402 : : {
403 [ - + ]: 11896 : if (expr::containsSubproof(cpc.get(), pn, visited))
404 : : {
405 : 0 : std::stringstream ss;
406 : 0 : ss << "ProofNodeManager::updateNode: attempting to make cyclic proof! "
407 : 0 : << id << " " << pn->getResult() << ", children = " << std::endl;
408 [ - - ]: 0 : for (const std::shared_ptr<ProofNode>& cp : children)
409 : : {
410 : 0 : ss << " " << cp->getRule() << " " << cp->getResult() << std::endl;
411 : : }
412 : 0 : ss << "Full children:" << std::endl;
413 [ - - ]: 0 : for (const std::shared_ptr<ProofNode>& cp : children)
414 : : {
415 : 0 : ss << " - ";
416 : 0 : cp->printDebug(ss);
417 : 0 : ss << std::endl;
418 : : }
419 : 0 : Unreachable() << ss.str();
420 : 0 : }
421 : : }
422 : 17519 : }
423 : : // ---------------- end check for cyclic
424 : :
425 : : // should have already computed what is proven
426 [ - + ][ - + ]: 11945201 : Assert(!pn->d_proven.isNull())
[ - - ]
427 : 0 : << "ProofNodeManager::updateProofNode: invalid proof provided";
428 [ + + ]: 11945201 : if (needsCheck)
429 : : {
430 : : // We expect to prove the same thing as before
431 : 2171831 : bool didCheck = false;
432 : 2171831 : Node res = checkInternal(id, children, args, pn->d_proven, didCheck);
433 [ - + ]: 2171831 : if (res.isNull())
434 : : {
435 : : // if it was invalid, then we do not update
436 : 0 : return false;
437 : : }
438 : : // proven field should already be the same as the result
439 [ - + ][ - + ]: 2171831 : Assert(res == pn->d_proven);
[ - - ]
440 : 2171831 : pn->d_provenChecked = didCheck;
441 [ + - ]: 2171831 : }
442 : :
443 : : // we update its value
444 : 11945201 : pn->setValue(id, children, args);
445 : 11945201 : return true;
446 : : }
447 : :
448 : : } // namespace cvc5::internal
|
