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