1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Haniel Barbosa, Aina Niemetz |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 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::kind; |
28 |
|
|
29 |
|
namespace cvc5 { |
30 |
|
|
31 |
3794 |
ProofNodeManager::ProofNodeManager(ProofChecker* pc) : d_checker(pc) |
32 |
|
{ |
33 |
3794 |
d_true = NodeManager::currentNM()->mkConst(true); |
34 |
|
// we always allocate a proof checker, regardless of the proof checking mode |
35 |
3794 |
Assert(d_checker != nullptr); |
36 |
3794 |
} |
37 |
|
|
38 |
18995454 |
std::shared_ptr<ProofNode> ProofNodeManager::mkNode( |
39 |
|
PfRule id, |
40 |
|
const std::vector<std::shared_ptr<ProofNode>>& children, |
41 |
|
const std::vector<Node>& args, |
42 |
|
Node expected) |
43 |
|
{ |
44 |
37990908 |
Trace("pnm") << "ProofNodeManager::mkNode " << id << " {" << expected.getId() |
45 |
18995454 |
<< "} " << expected << "\n"; |
46 |
18995454 |
bool didCheck = false; |
47 |
37990908 |
Node res = checkInternal(id, children, args, expected, didCheck); |
48 |
18995454 |
if (res.isNull()) |
49 |
|
{ |
50 |
|
// if it was invalid, then we return the null node |
51 |
|
return nullptr; |
52 |
|
} |
53 |
|
// otherwise construct the proof node and set its proven field |
54 |
|
std::shared_ptr<ProofNode> pn = |
55 |
37990908 |
std::make_shared<ProofNode>(id, children, args); |
56 |
18995454 |
pn->d_proven = res; |
57 |
18995454 |
pn->d_provenChecked = didCheck; |
58 |
18995454 |
return pn; |
59 |
|
} |
60 |
|
|
61 |
9902233 |
std::shared_ptr<ProofNode> ProofNodeManager::mkAssume(Node fact) |
62 |
|
{ |
63 |
9902233 |
Assert(!fact.isNull()); |
64 |
9902233 |
Assert(fact.getType().isBoolean()); |
65 |
9902233 |
return mkNode(PfRule::ASSUME, {}, {fact}, fact); |
66 |
|
} |
67 |
|
|
68 |
372538 |
std::shared_ptr<ProofNode> ProofNodeManager::mkSymm( |
69 |
|
std::shared_ptr<ProofNode> child, Node expected) |
70 |
|
{ |
71 |
372538 |
if (child->getRule() == PfRule::SYMM) |
72 |
|
{ |
73 |
193 |
Assert(expected.isNull() |
74 |
|
|| child->getChildren()[0]->getResult() == expected); |
75 |
193 |
return child->getChildren()[0]; |
76 |
|
} |
77 |
372345 |
return mkNode(PfRule::SYMM, {child}, {}, expected); |
78 |
|
} |
79 |
|
|
80 |
366 |
std::shared_ptr<ProofNode> ProofNodeManager::mkTrans( |
81 |
|
const std::vector<std::shared_ptr<ProofNode>>& children, Node expected) |
82 |
|
{ |
83 |
366 |
Assert(!children.empty()); |
84 |
366 |
if (children.size() == 1) |
85 |
|
{ |
86 |
|
Assert(expected.isNull() || children[0]->getResult() == expected); |
87 |
|
return children[0]; |
88 |
|
} |
89 |
366 |
return mkNode(PfRule::TRANS, children, {}, expected); |
90 |
|
} |
91 |
|
|
92 |
188312 |
std::shared_ptr<ProofNode> ProofNodeManager::mkScope( |
93 |
|
std::shared_ptr<ProofNode> pf, |
94 |
|
std::vector<Node>& assumps, |
95 |
|
bool ensureClosed, |
96 |
|
bool doMinimize, |
97 |
|
Node expected) |
98 |
|
{ |
99 |
188312 |
if (!ensureClosed) |
100 |
|
{ |
101 |
57528 |
return mkNode(PfRule::SCOPE, {pf}, assumps, expected); |
102 |
|
} |
103 |
130784 |
Trace("pnm-scope") << "ProofNodeManager::mkScope " << assumps << std::endl; |
104 |
|
// we first ensure the assumptions are flattened |
105 |
261568 |
std::unordered_set<Node> ac{assumps.begin(), assumps.end()}; |
106 |
|
// map from the rewritten form of assumptions to the original. This is only |
107 |
|
// computed in the rare case when we need rewriting to match the |
108 |
|
// assumptions. An example of this is for Boolean constant equalities in |
109 |
|
// scoped proofs from the proof equality engine. |
110 |
261568 |
std::unordered_map<Node, Node> acr; |
111 |
|
// whether we have compute the map above |
112 |
130784 |
bool computedAcr = false; |
113 |
|
|
114 |
|
// The free assumptions of the proof |
115 |
261568 |
std::map<Node, std::vector<std::shared_ptr<ProofNode>>> famap; |
116 |
130784 |
expr::getFreeAssumptionsMap(pf, famap); |
117 |
261568 |
std::unordered_set<Node> acu; |
118 |
577726 |
for (const std::pair<const Node, std::vector<std::shared_ptr<ProofNode>>>& |
119 |
130784 |
fa : famap) |
120 |
|
{ |
121 |
1155452 |
Node a = fa.first; |
122 |
1018836 |
if (ac.find(a) != ac.end()) |
123 |
|
{ |
124 |
|
// already covered by an assumption |
125 |
441110 |
acu.insert(a); |
126 |
441110 |
continue; |
127 |
|
} |
128 |
|
// trivial assumption |
129 |
136616 |
if (a == d_true) |
130 |
|
{ |
131 |
|
Trace("pnm-scope") << "- justify trivial True assumption\n"; |
132 |
|
for (std::shared_ptr<ProofNode> pfs : fa.second) |
133 |
|
{ |
134 |
|
Assert(pfs->getResult() == a); |
135 |
|
updateNode(pfs.get(), PfRule::MACRO_SR_PRED_INTRO, {}, {a}); |
136 |
|
} |
137 |
|
Trace("pnm-scope") << "...finished" << std::endl; |
138 |
|
acu.insert(a); |
139 |
|
continue; |
140 |
|
} |
141 |
136616 |
Trace("pnm-scope") << "- try matching free assumption " << a << "\n"; |
142 |
|
// otherwise it may be due to symmetry? |
143 |
273232 |
Node aeqSym = CDProof::getSymmFact(a); |
144 |
136616 |
Trace("pnm-scope") << " - try sym " << aeqSym << "\n"; |
145 |
273232 |
Node aMatch; |
146 |
136616 |
if (!aeqSym.isNull() && ac.count(aeqSym)) |
147 |
|
{ |
148 |
271998 |
Trace("pnm-scope") << "- reorient assumption " << aeqSym << " via " << a |
149 |
271998 |
<< " for " << fa.second.size() << " proof nodes" |
150 |
135999 |
<< std::endl; |
151 |
135999 |
aMatch = aeqSym; |
152 |
|
} |
153 |
|
else |
154 |
|
{ |
155 |
|
// Otherwise, may be derivable by rewriting. Note this is used in |
156 |
|
// ensuring that proofs from the proof equality engine that involve |
157 |
|
// equality with Boolean constants are closed. |
158 |
617 |
if (!computedAcr) |
159 |
|
{ |
160 |
243 |
computedAcr = true; |
161 |
3508 |
for (const Node& acc : ac) |
162 |
|
{ |
163 |
6530 |
Node accr = theory::Rewriter::rewrite(acc); |
164 |
3265 |
if (accr != acc) |
165 |
|
{ |
166 |
1262 |
acr[accr] = acc; |
167 |
|
} |
168 |
|
} |
169 |
|
} |
170 |
1234 |
Node ar = theory::Rewriter::rewrite(a); |
171 |
617 |
std::unordered_map<Node, Node>::iterator itr = acr.find(ar); |
172 |
617 |
if (itr != acr.end()) |
173 |
|
{ |
174 |
617 |
aMatch = itr->second; |
175 |
|
} |
176 |
|
} |
177 |
|
|
178 |
|
// if we found a match either by symmetry or rewriting, then we connect |
179 |
|
// the assumption here. |
180 |
136616 |
if (!aMatch.isNull()) |
181 |
|
{ |
182 |
273232 |
std::shared_ptr<ProofNode> pfaa = mkAssume(aMatch); |
183 |
|
// must correct the orientation on this leaf |
184 |
273232 |
std::vector<std::shared_ptr<ProofNode>> children; |
185 |
136616 |
children.push_back(pfaa); |
186 |
273232 |
for (std::shared_ptr<ProofNode> pfs : fa.second) |
187 |
|
{ |
188 |
136616 |
Assert(pfs->getResult() == a); |
189 |
|
// use SYMM if possible |
190 |
136616 |
if (aMatch == aeqSym) |
191 |
|
{ |
192 |
135999 |
if (pfaa->getRule() == PfRule::SYMM) |
193 |
|
{ |
194 |
|
updateNode(pfs.get(), pfaa->getChildren()[0].get()); |
195 |
|
} |
196 |
|
else |
197 |
|
{ |
198 |
135999 |
updateNode(pfs.get(), PfRule::SYMM, children, {}); |
199 |
|
} |
200 |
|
} |
201 |
|
else |
202 |
|
{ |
203 |
617 |
updateNode(pfs.get(), PfRule::MACRO_SR_PRED_TRANSFORM, children, {a}); |
204 |
|
} |
205 |
|
} |
206 |
136616 |
Trace("pnm-scope") << "...finished" << std::endl; |
207 |
136616 |
acu.insert(aMatch); |
208 |
136616 |
continue; |
209 |
|
} |
210 |
|
// If we did not find a match, it is an error, since all free assumptions |
211 |
|
// should be arguments to SCOPE. |
212 |
|
std::stringstream ss; |
213 |
|
|
214 |
|
bool dumpProofTraceOn = Trace.isOn("dump-proof-error"); |
215 |
|
if (dumpProofTraceOn) |
216 |
|
{ |
217 |
|
ss << "The proof : " << *pf << std::endl; |
218 |
|
} |
219 |
|
ss << std::endl << "Free assumption: " << a << std::endl; |
220 |
|
for (const Node& aprint : ac) |
221 |
|
{ |
222 |
|
ss << "- assumption: " << aprint << std::endl; |
223 |
|
} |
224 |
|
if (!dumpProofTraceOn) |
225 |
|
{ |
226 |
|
ss << "Use -t dump-proof-error for details on proof" << std::endl; |
227 |
|
} |
228 |
|
Unreachable() << "Generated a proof that is not closed by the scope: " |
229 |
|
<< ss.str() << std::endl; |
230 |
|
} |
231 |
130784 |
if (acu.size() < ac.size()) |
232 |
|
{ |
233 |
|
// All assumptions should match a free assumption; if one does not, then |
234 |
|
// the explanation could have been smaller. |
235 |
47182 |
for (const Node& a : ac) |
236 |
|
{ |
237 |
42924 |
if (acu.find(a) == acu.end()) |
238 |
|
{ |
239 |
26421 |
Notice() << "ProofNodeManager::mkScope: assumption " << a |
240 |
|
<< " does not match a free assumption in proof" << std::endl; |
241 |
|
} |
242 |
|
} |
243 |
|
} |
244 |
130784 |
if (doMinimize && acu.size() < ac.size()) |
245 |
|
{ |
246 |
3221 |
assumps.clear(); |
247 |
3221 |
assumps.insert(assumps.end(), acu.begin(), acu.end()); |
248 |
|
} |
249 |
127563 |
else if (ac.size() < assumps.size()) |
250 |
|
{ |
251 |
|
// remove duplicates to avoid redundant literals in clauses |
252 |
677 |
assumps.clear(); |
253 |
677 |
assumps.insert(assumps.end(), ac.begin(), ac.end()); |
254 |
|
} |
255 |
261568 |
Node minExpected; |
256 |
130784 |
NodeManager* nm = NodeManager::currentNM(); |
257 |
261568 |
Node exp; |
258 |
130784 |
if (assumps.empty()) |
259 |
|
{ |
260 |
|
// SCOPE with no arguments is a no-op, just return original |
261 |
2496 |
return pf; |
262 |
|
} |
263 |
256576 |
Node conc = pf->getResult(); |
264 |
128288 |
exp = assumps.size() == 1 ? assumps[0] : nm->mkNode(AND, assumps); |
265 |
128288 |
if (conc.isConst() && !conc.getConst<bool>()) |
266 |
|
{ |
267 |
43405 |
minExpected = exp.notNode(); |
268 |
|
} |
269 |
|
else |
270 |
|
{ |
271 |
84883 |
minExpected = nm->mkNode(IMPLIES, exp, conc); |
272 |
|
} |
273 |
128288 |
return mkNode(PfRule::SCOPE, {pf}, assumps, minExpected); |
274 |
|
} |
275 |
|
|
276 |
194098 |
bool ProofNodeManager::updateNode( |
277 |
|
ProofNode* pn, |
278 |
|
PfRule id, |
279 |
|
const std::vector<std::shared_ptr<ProofNode>>& children, |
280 |
|
const std::vector<Node>& args) |
281 |
|
{ |
282 |
194098 |
return updateNodeInternal(pn, id, children, args, true); |
283 |
|
} |
284 |
|
|
285 |
2221703 |
bool ProofNodeManager::updateNode(ProofNode* pn, ProofNode* pnr) |
286 |
|
{ |
287 |
2221703 |
Assert(pn != nullptr); |
288 |
2221703 |
Assert(pnr != nullptr); |
289 |
2221703 |
if (pn == pnr) |
290 |
|
{ |
291 |
|
// same node, no update necessary |
292 |
2168 |
return true; |
293 |
|
} |
294 |
2219535 |
if (pn->getResult() != pnr->getResult()) |
295 |
|
{ |
296 |
|
return false; |
297 |
|
} |
298 |
|
// copy whether we did the check |
299 |
2219535 |
pn->d_provenChecked = pnr->d_provenChecked; |
300 |
|
// can shortcut re-check of rule |
301 |
2219535 |
return updateNodeInternal( |
302 |
2219535 |
pn, pnr->getRule(), pnr->getChildren(), pnr->getArguments(), false); |
303 |
|
} |
304 |
|
|
305 |
2551982 |
void ProofNodeManager::ensureChecked(ProofNode* pn) |
306 |
|
{ |
307 |
2551982 |
if (pn->d_provenChecked) |
308 |
|
{ |
309 |
|
// already checked |
310 |
47795 |
return; |
311 |
|
} |
312 |
|
// directly call the proof checker |
313 |
5008374 |
Node res = d_checker->check(pn, pn->getResult()); |
314 |
2504187 |
pn->d_provenChecked = true; |
315 |
|
// should have the correct result |
316 |
2504187 |
Assert(res == pn->d_proven); |
317 |
|
} |
318 |
|
|
319 |
19189552 |
Node ProofNodeManager::checkInternal( |
320 |
|
PfRule id, |
321 |
|
const std::vector<std::shared_ptr<ProofNode>>& children, |
322 |
|
const std::vector<Node>& args, |
323 |
|
Node expected, |
324 |
|
bool& didCheck) |
325 |
|
{ |
326 |
|
// if the user supplied an expected result, then we trust it if we are in |
327 |
|
// a proof checking mode that does not eagerly check rule applications |
328 |
19189552 |
if (!expected.isNull()) |
329 |
|
{ |
330 |
36226958 |
if (options::proofCheck() == options::ProofCheckMode::LAZY |
331 |
18113479 |
|| options::proofCheck() == options::ProofCheckMode::NONE) |
332 |
|
{ |
333 |
18113479 |
return expected; |
334 |
|
} |
335 |
|
} |
336 |
|
// check with the checker, which takes expected as argument |
337 |
2152146 |
Node res = d_checker->check(id, children, args, expected); |
338 |
1076073 |
didCheck = true; |
339 |
1076073 |
Assert(!res.isNull()) |
340 |
|
<< "ProofNodeManager::checkInternal: failed to check proof"; |
341 |
1076073 |
return res; |
342 |
|
} |
343 |
|
|
344 |
11118246 |
ProofChecker* ProofNodeManager::getChecker() const { return d_checker; } |
345 |
|
|
346 |
63580 |
std::shared_ptr<ProofNode> ProofNodeManager::clone( |
347 |
|
std::shared_ptr<ProofNode> pn) const |
348 |
|
{ |
349 |
63580 |
const ProofNode* orig = pn.get(); |
350 |
127160 |
std::unordered_map<const ProofNode*, std::shared_ptr<ProofNode>> visited; |
351 |
63580 |
std::unordered_map<const ProofNode*, std::shared_ptr<ProofNode>>::iterator it; |
352 |
127160 |
std::vector<const ProofNode*> visit; |
353 |
127160 |
std::shared_ptr<ProofNode> cloned; |
354 |
63580 |
visit.push_back(orig); |
355 |
|
const ProofNode* cur; |
356 |
4618502 |
while (!visit.empty()) |
357 |
|
{ |
358 |
2277461 |
cur = visit.back(); |
359 |
2277461 |
it = visited.find(cur); |
360 |
2277461 |
if (it == visited.end()) |
361 |
|
{ |
362 |
1042613 |
visited[cur] = nullptr; |
363 |
|
const std::vector<std::shared_ptr<ProofNode>>& children = |
364 |
1042613 |
cur->getChildren(); |
365 |
2213881 |
for (const std::shared_ptr<ProofNode>& cp : children) |
366 |
|
{ |
367 |
1171268 |
visit.push_back(cp.get()); |
368 |
|
} |
369 |
1042613 |
continue; |
370 |
|
} |
371 |
1234848 |
visit.pop_back(); |
372 |
1234848 |
if (it->second.get() == nullptr) |
373 |
|
{ |
374 |
2085226 |
std::vector<std::shared_ptr<ProofNode>> cchildren; |
375 |
|
const std::vector<std::shared_ptr<ProofNode>>& children = |
376 |
1042613 |
cur->getChildren(); |
377 |
2213881 |
for (const std::shared_ptr<ProofNode>& cp : children) |
378 |
|
{ |
379 |
1171268 |
it = visited.find(cp.get()); |
380 |
1171268 |
Assert(it != visited.end()); |
381 |
|
// if we encounter nullptr here, then this child is currently being |
382 |
|
// traversed at a higher level, hence this corresponds to a cyclic |
383 |
|
// proof. |
384 |
1171268 |
if (it->second == nullptr) |
385 |
|
{ |
386 |
|
Unreachable() << "Cyclic proof encountered when cloning a proof node"; |
387 |
|
} |
388 |
1171268 |
cchildren.push_back(it->second); |
389 |
|
} |
390 |
2085226 |
cloned = std::make_shared<ProofNode>( |
391 |
2085226 |
cur->getRule(), cchildren, cur->getArguments()); |
392 |
1042613 |
visited[cur] = cloned; |
393 |
|
// we trust the above cloning does not change what is proven |
394 |
1042613 |
cloned->d_proven = cur->d_proven; |
395 |
1042613 |
cloned->d_provenChecked = cur->d_provenChecked; |
396 |
|
} |
397 |
|
} |
398 |
63580 |
Assert(visited.find(orig) != visited.end()); |
399 |
127160 |
return visited[orig]; |
400 |
|
} |
401 |
|
|
402 |
343195 |
ProofNode* ProofNodeManager::cancelDoubleSymm(ProofNode* pn) |
403 |
|
{ |
404 |
344277 |
while (pn->getRule() == PfRule::SYMM) |
405 |
|
{ |
406 |
343195 |
std::shared_ptr<ProofNode> pnc = pn->getChildren()[0]; |
407 |
342113 |
if (pnc->getRule() == PfRule::SYMM) |
408 |
|
{ |
409 |
1082 |
pn = pnc->getChildren()[0].get(); |
410 |
|
} |
411 |
|
else |
412 |
|
{ |
413 |
341031 |
break; |
414 |
|
} |
415 |
|
} |
416 |
342113 |
return pn; |
417 |
|
} |
418 |
|
|
419 |
2413633 |
bool ProofNodeManager::updateNodeInternal( |
420 |
|
ProofNode* pn, |
421 |
|
PfRule id, |
422 |
|
const std::vector<std::shared_ptr<ProofNode>>& children, |
423 |
|
const std::vector<Node>& args, |
424 |
|
bool needsCheck) |
425 |
|
{ |
426 |
2413633 |
Assert(pn != nullptr); |
427 |
|
// ---------------- check for cyclic |
428 |
2413633 |
if (options::proofCheck() == options::ProofCheckMode::EAGER) |
429 |
|
{ |
430 |
|
std::unordered_set<const ProofNode*> visited; |
431 |
|
for (const std::shared_ptr<ProofNode>& cpc : children) |
432 |
|
{ |
433 |
|
if (expr::containsSubproof(cpc.get(), pn, visited)) |
434 |
|
{ |
435 |
|
std::stringstream ss; |
436 |
|
ss << "ProofNodeManager::updateNode: attempting to make cyclic proof! " |
437 |
|
<< id << " " << pn->getResult() << ", children = " << std::endl; |
438 |
|
for (const std::shared_ptr<ProofNode>& cp : children) |
439 |
|
{ |
440 |
|
ss << " " << cp->getRule() << " " << cp->getResult() << std::endl; |
441 |
|
} |
442 |
|
ss << "Full children:" << std::endl; |
443 |
|
for (const std::shared_ptr<ProofNode>& cp : children) |
444 |
|
{ |
445 |
|
ss << " - "; |
446 |
|
cp->printDebug(ss); |
447 |
|
ss << std::endl; |
448 |
|
} |
449 |
|
Unreachable() << ss.str(); |
450 |
|
} |
451 |
|
} |
452 |
|
} |
453 |
|
// ---------------- end check for cyclic |
454 |
|
|
455 |
|
// should have already computed what is proven |
456 |
2413633 |
Assert(!pn->d_proven.isNull()) |
457 |
|
<< "ProofNodeManager::updateProofNode: invalid proof provided"; |
458 |
2413633 |
if (needsCheck) |
459 |
|
{ |
460 |
|
// We expect to prove the same thing as before |
461 |
194098 |
bool didCheck = false; |
462 |
388196 |
Node res = checkInternal(id, children, args, pn->d_proven, didCheck); |
463 |
194098 |
if (res.isNull()) |
464 |
|
{ |
465 |
|
// if it was invalid, then we do not update |
466 |
|
return false; |
467 |
|
} |
468 |
|
// proven field should already be the same as the result |
469 |
194098 |
Assert(res == pn->d_proven); |
470 |
194098 |
pn->d_provenChecked = didCheck; |
471 |
|
} |
472 |
|
|
473 |
|
// we update its value |
474 |
2413633 |
pn->setValue(id, children, args); |
475 |
2413633 |
return true; |
476 |
|
} |
477 |
|
|
478 |
29574 |
} // namespace cvc5 |