1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Haniel Barbosa |
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 the module for processing proof nodes in the prop engine. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "prop/proof_post_processor.h" |
17 |
|
|
18 |
|
#include "theory/builtin/proof_checker.h" |
19 |
|
|
20 |
|
namespace cvc5 { |
21 |
|
namespace prop { |
22 |
|
|
23 |
1254 |
ProofPostprocessCallback::ProofPostprocessCallback( |
24 |
1254 |
ProofNodeManager* pnm, ProofCnfStream* proofCnfStream) |
25 |
1254 |
: d_pnm(pnm), d_proofCnfStream(proofCnfStream) |
26 |
|
{ |
27 |
1254 |
} |
28 |
|
|
29 |
2811 |
void ProofPostprocessCallback::initializeUpdate() { d_assumpToProof.clear(); } |
30 |
|
|
31 |
890182 |
bool ProofPostprocessCallback::shouldUpdate(std::shared_ptr<ProofNode> pn, |
32 |
|
const std::vector<Node>& fa, |
33 |
|
bool& continueUpdate) |
34 |
|
{ |
35 |
890182 |
bool result = pn->getRule() == PfRule::ASSUME |
36 |
1780364 |
&& d_proofCnfStream->hasProofFor(pn->getResult()); |
37 |
|
// check if should continue traversing |
38 |
890182 |
if (d_proofCnfStream->isBlocked(pn)) |
39 |
|
{ |
40 |
|
continueUpdate = false; |
41 |
|
result = false; |
42 |
|
} |
43 |
890182 |
return result; |
44 |
|
} |
45 |
|
|
46 |
555126 |
bool ProofPostprocessCallback::update(Node res, |
47 |
|
PfRule id, |
48 |
|
const std::vector<Node>& children, |
49 |
|
const std::vector<Node>& args, |
50 |
|
CDProof* cdp, |
51 |
|
bool& continueUpdate) |
52 |
|
{ |
53 |
1110252 |
Trace("prop-proof-pp-debug") |
54 |
555126 |
<< "- Post process " << id << " " << children << " / " << args << "\n"; |
55 |
555126 |
Assert(id == PfRule::ASSUME); |
56 |
|
// we cache based on the assumption node, not the proof node, since there |
57 |
|
// may be multiple occurrences of the same node. |
58 |
1110252 |
Node f = args[0]; |
59 |
1110252 |
std::shared_ptr<ProofNode> pfn; |
60 |
|
std::map<Node, std::shared_ptr<ProofNode>>::iterator it = |
61 |
555126 |
d_assumpToProof.find(f); |
62 |
555126 |
if (it != d_assumpToProof.end()) |
63 |
|
{ |
64 |
435198 |
Trace("prop-proof-pp-debug") << "...already computed" << std::endl; |
65 |
435198 |
pfn = it->second; |
66 |
|
} |
67 |
|
else |
68 |
|
{ |
69 |
119928 |
Assert(d_proofCnfStream != nullptr); |
70 |
|
// get proof from proof cnf stream |
71 |
119928 |
pfn = d_proofCnfStream->getProofFor(f); |
72 |
119928 |
Assert(pfn != nullptr && pfn->getResult() == f); |
73 |
119928 |
if (Trace.isOn("prop-proof-pp")) |
74 |
|
{ |
75 |
|
Trace("prop-proof-pp") << "=== Connect CNF proof for: " << f << "\n"; |
76 |
|
Trace("prop-proof-pp") << *pfn.get() << "\n"; |
77 |
|
} |
78 |
119928 |
d_assumpToProof[f] = pfn; |
79 |
|
} |
80 |
|
// connect the proof |
81 |
555126 |
cdp->addProof(pfn); |
82 |
|
// do not recursively process the result |
83 |
555126 |
continueUpdate = false; |
84 |
|
// moreover block the fact f so that its proof node is not traversed if we run |
85 |
|
// this post processor again (which can happen in incremental benchmarks) |
86 |
555126 |
d_proofCnfStream->addBlocked(pfn); |
87 |
1110252 |
return true; |
88 |
|
} |
89 |
|
|
90 |
1254 |
ProofPostproccess::ProofPostproccess(ProofNodeManager* pnm, |
91 |
1254 |
ProofCnfStream* proofCnfStream) |
92 |
1254 |
: d_cb(pnm, proofCnfStream), d_pnm(pnm) |
93 |
|
{ |
94 |
1254 |
} |
95 |
|
|
96 |
1254 |
ProofPostproccess::~ProofPostproccess() {} |
97 |
|
|
98 |
2811 |
void ProofPostproccess::process(std::shared_ptr<ProofNode> pf) |
99 |
|
{ |
100 |
|
// Initialize the callback, which computes necessary static information about |
101 |
|
// how to process, including how to process assumptions in pf. |
102 |
2811 |
d_cb.initializeUpdate(); |
103 |
|
// now, process |
104 |
5622 |
ProofNodeUpdater updater(d_pnm, d_cb); |
105 |
2811 |
updater.process(pf); |
106 |
2811 |
} |
107 |
|
|
108 |
|
} // namespace prop |
109 |
29340 |
} // namespace cvc5 |