1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, 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 a utility for updating proof nodes. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "proof/proof_node_updater.h" |
17 |
|
|
18 |
|
#include "proof/lazy_proof.h" |
19 |
|
#include "proof/proof_ensure_closed.h" |
20 |
|
#include "proof/proof_node_algorithm.h" |
21 |
|
#include "proof/proof_node_manager.h" |
22 |
|
|
23 |
|
namespace cvc5 { |
24 |
|
|
25 |
8760 |
ProofNodeUpdaterCallback::ProofNodeUpdaterCallback() {} |
26 |
8760 |
ProofNodeUpdaterCallback::~ProofNodeUpdaterCallback() {} |
27 |
|
|
28 |
|
bool ProofNodeUpdaterCallback::update(Node res, |
29 |
|
PfRule id, |
30 |
|
const std::vector<Node>& children, |
31 |
|
const std::vector<Node>& args, |
32 |
|
CDProof* cdp, |
33 |
|
bool& continueUpdate) |
34 |
|
{ |
35 |
|
return false; |
36 |
|
} |
37 |
|
|
38 |
10309 |
ProofNodeUpdater::ProofNodeUpdater(ProofNodeManager* pnm, |
39 |
|
ProofNodeUpdaterCallback& cb, |
40 |
|
bool mergeSubproofs, |
41 |
10309 |
bool autoSym) |
42 |
|
: d_pnm(pnm), |
43 |
|
d_cb(cb), |
44 |
|
d_debugFreeAssumps(false), |
45 |
|
d_mergeSubproofs(mergeSubproofs), |
46 |
10309 |
d_autoSym(autoSym) |
47 |
|
{ |
48 |
10309 |
} |
49 |
|
|
50 |
8381 |
void ProofNodeUpdater::process(std::shared_ptr<ProofNode> pf) |
51 |
|
{ |
52 |
8381 |
if (d_debugFreeAssumps) |
53 |
|
{ |
54 |
|
if (Trace.isOn("pfnu-debug")) |
55 |
|
{ |
56 |
|
Trace("pfnu-debug2") << "Initial proof: " << *pf.get() << std::endl; |
57 |
|
Trace("pfnu-debug") << "ProofNodeUpdater::process" << std::endl; |
58 |
|
Trace("pfnu-debug") << "Expected free assumptions: " << std::endl; |
59 |
|
for (const Node& fa : d_freeAssumps) |
60 |
|
{ |
61 |
|
Trace("pfnu-debug") << "- " << fa << std::endl; |
62 |
|
} |
63 |
|
std::vector<Node> assump; |
64 |
|
expr::getFreeAssumptions(pf.get(), assump); |
65 |
|
Trace("pfnu-debug") << "Current free assumptions: " << std::endl; |
66 |
|
for (const Node& fa : assump) |
67 |
|
{ |
68 |
|
Trace("pfnu-debug") << "- " << fa << std::endl; |
69 |
|
} |
70 |
|
} |
71 |
|
} |
72 |
16762 |
std::vector<std::shared_ptr<ProofNode>> traversing; |
73 |
8381 |
processInternal(pf, d_freeAssumps, traversing); |
74 |
8381 |
} |
75 |
|
|
76 |
85287 |
void ProofNodeUpdater::processInternal( |
77 |
|
std::shared_ptr<ProofNode> pf, |
78 |
|
const std::vector<Node>& fa, |
79 |
|
std::vector<std::shared_ptr<ProofNode>>& traversing) |
80 |
|
{ |
81 |
85287 |
Trace("pf-process") << "ProofNodeUpdater::process" << std::endl; |
82 |
170574 |
std::unordered_map<std::shared_ptr<ProofNode>, bool> visited; |
83 |
85287 |
std::unordered_map<std::shared_ptr<ProofNode>, bool>::iterator it; |
84 |
170574 |
std::vector<std::shared_ptr<ProofNode>> visit; |
85 |
170574 |
std::shared_ptr<ProofNode> cur; |
86 |
85287 |
visit.push_back(pf); |
87 |
85287 |
std::map<Node, std::shared_ptr<ProofNode>>::iterator itc; |
88 |
|
// A cache from formulas to proof nodes that are in the current scope. |
89 |
|
// Notice that we make a fresh recursive call to process if the current |
90 |
|
// rule is SCOPE below. |
91 |
170574 |
std::map<Node, std::shared_ptr<ProofNode>> resCache; |
92 |
170574 |
Node res; |
93 |
16252120 |
do |
94 |
|
{ |
95 |
16337407 |
cur = visit.back(); |
96 |
16337407 |
visit.pop_back(); |
97 |
16337407 |
it = visited.find(cur); |
98 |
16337407 |
res = cur->getResult(); |
99 |
16337407 |
if (it == visited.end()) |
100 |
|
{ |
101 |
6664658 |
if (d_mergeSubproofs) |
102 |
|
{ |
103 |
2605811 |
itc = resCache.find(res); |
104 |
3076462 |
if (itc != resCache.end()) |
105 |
|
{ |
106 |
|
// already have a proof, merge it into this one |
107 |
470651 |
visited[cur] = true; |
108 |
470651 |
d_pnm->updateNode(cur.get(), itc->second.get()); |
109 |
1807710 |
continue; |
110 |
|
} |
111 |
|
} |
112 |
|
// run update to a fixed point |
113 |
6194007 |
bool continueUpdate = true; |
114 |
6440393 |
while (runUpdate(cur, fa, continueUpdate) && continueUpdate) |
115 |
|
{ |
116 |
123193 |
Trace("pf-process-debug") << "...updated proof." << std::endl; |
117 |
|
} |
118 |
6194007 |
visited[cur] = !continueUpdate; |
119 |
6983509 |
if (!continueUpdate) |
120 |
|
{ |
121 |
|
// no further changes should be made to cur according to the callback |
122 |
1579004 |
Trace("pf-process-debug") |
123 |
789502 |
<< "...marked to not continue update." << std::endl; |
124 |
789502 |
runFinalize(cur, fa, resCache); |
125 |
789502 |
continue; |
126 |
|
} |
127 |
5404505 |
traversing.push_back(cur); |
128 |
5404505 |
visit.push_back(cur); |
129 |
|
// If we are not the top-level proof, we were a scope, or became a scope |
130 |
|
// after updating, we do a separate recursive call to this method. This |
131 |
|
// allows us to properly track the assumptions in scope, which is |
132 |
|
// important for example to merge or to determine updates based on free |
133 |
|
// assumptions. |
134 |
5404505 |
if (cur->getRule() == PfRule::SCOPE && cur != pf) |
135 |
|
{ |
136 |
153812 |
std::vector<Node> nfa; |
137 |
76906 |
nfa.insert(nfa.end(), fa.begin(), fa.end()); |
138 |
76906 |
const std::vector<Node>& args = cur->getArguments(); |
139 |
76906 |
nfa.insert(nfa.end(), args.begin(), args.end()); |
140 |
76906 |
Trace("pfnu-debug2") << "Process new scope with " << args << std::endl; |
141 |
|
// Process in new call separately |
142 |
76906 |
processInternal(cur, nfa, traversing); |
143 |
76906 |
continue; |
144 |
|
} |
145 |
5327599 |
const std::vector<std::shared_ptr<ProofNode>>& ccp = cur->getChildren(); |
146 |
|
// now, process children |
147 |
16175214 |
for (const std::shared_ptr<ProofNode>& cp : ccp) |
148 |
|
{ |
149 |
32542845 |
if (std::find(traversing.begin(), traversing.end(), cp) |
150 |
32542845 |
!= traversing.end()) |
151 |
|
{ |
152 |
|
Unhandled() |
153 |
|
<< "ProofNodeUpdater::processInternal: cyclic proof! (use " |
154 |
|
"--proof-eager-checking)" |
155 |
|
<< std::endl; |
156 |
|
} |
157 |
10847615 |
visit.push_back(cp); |
158 |
|
} |
159 |
|
} |
160 |
9672749 |
else if (!it->second) |
161 |
|
{ |
162 |
5404505 |
Assert(!traversing.empty()); |
163 |
5404505 |
traversing.pop_back(); |
164 |
5404505 |
visited[cur] = true; |
165 |
|
// finalize the node |
166 |
5404505 |
runFinalize(cur, fa, resCache); |
167 |
|
} |
168 |
16337407 |
} while (!visit.empty()); |
169 |
85287 |
Trace("pf-process") << "ProofNodeUpdater::process: finished" << std::endl; |
170 |
85287 |
} |
171 |
|
|
172 |
6317200 |
bool ProofNodeUpdater::runUpdate(std::shared_ptr<ProofNode> cur, |
173 |
|
const std::vector<Node>& fa, |
174 |
|
bool& continueUpdate) |
175 |
|
{ |
176 |
|
// should it be updated? |
177 |
6317200 |
if (!d_cb.shouldUpdate(cur, fa, continueUpdate)) |
178 |
|
{ |
179 |
5175941 |
return false; |
180 |
|
} |
181 |
1141259 |
PfRule id = cur->getRule(); |
182 |
|
// use CDProof to open a scope for which the callback updates |
183 |
2282518 |
CDProof cpf(d_pnm, nullptr, "ProofNodeUpdater::CDProof", d_autoSym); |
184 |
1141259 |
const std::vector<std::shared_ptr<ProofNode>>& cc = cur->getChildren(); |
185 |
2282518 |
std::vector<Node> ccn; |
186 |
2252034 |
for (const std::shared_ptr<ProofNode>& cp : cc) |
187 |
|
{ |
188 |
2221550 |
Node cpres = cp->getResult(); |
189 |
1110775 |
ccn.push_back(cpres); |
190 |
|
// store in the proof |
191 |
1110775 |
cpf.addProof(cp); |
192 |
|
} |
193 |
2282518 |
Node res = cur->getResult(); |
194 |
2282518 |
Trace("pf-process-debug") |
195 |
1141259 |
<< "Updating (" << cur->getRule() << "): " << res << std::endl; |
196 |
|
// only if the callback updated the node |
197 |
1141259 |
if (d_cb.update(res, id, ccn, cur->getArguments(), &cpf, continueUpdate)) |
198 |
|
{ |
199 |
1825390 |
std::shared_ptr<ProofNode> npn = cpf.getProofFor(res); |
200 |
1825390 |
std::vector<Node> fullFa; |
201 |
912695 |
if (d_debugFreeAssumps) |
202 |
|
{ |
203 |
|
expr::getFreeAssumptions(cur.get(), fullFa); |
204 |
|
Trace("pfnu-debug") << "Original proof : " << *cur << std::endl; |
205 |
|
} |
206 |
|
// then, update the original proof node based on this one |
207 |
912695 |
Trace("pf-process-debug") << "Update node..." << std::endl; |
208 |
912695 |
d_pnm->updateNode(cur.get(), npn.get()); |
209 |
912695 |
Trace("pf-process-debug") << "...update node finished." << std::endl; |
210 |
912695 |
if (d_debugFreeAssumps) |
211 |
|
{ |
212 |
|
fullFa.insert(fullFa.end(), fa.begin(), fa.end()); |
213 |
|
// We have that npn is a node we occurring the final updated version of |
214 |
|
// the proof. We can now debug based on the expected set of free |
215 |
|
// assumptions. |
216 |
|
Trace("pfnu-debug") << "Ensure update closed..." << std::endl; |
217 |
|
pfnEnsureClosedWrt( |
218 |
|
npn.get(), fullFa, "pfnu-debug", "ProofNodeUpdater:postupdate"); |
219 |
|
} |
220 |
912695 |
Trace("pf-process-debug") << "..finished" << std::endl; |
221 |
912695 |
return true; |
222 |
|
} |
223 |
228564 |
Trace("pf-process-debug") << "..finished" << std::endl; |
224 |
228564 |
return false; |
225 |
|
} |
226 |
|
|
227 |
6194007 |
void ProofNodeUpdater::runFinalize( |
228 |
|
std::shared_ptr<ProofNode> cur, |
229 |
|
const std::vector<Node>& fa, |
230 |
|
std::map<Node, std::shared_ptr<ProofNode>>& resCache) |
231 |
|
{ |
232 |
6194007 |
if (d_mergeSubproofs) |
233 |
|
{ |
234 |
4270320 |
Node res = cur->getResult(); |
235 |
|
// cache result if we are merging subproofs |
236 |
2135160 |
resCache[res] = cur; |
237 |
|
} |
238 |
6194007 |
if (d_debugFreeAssumps) |
239 |
|
{ |
240 |
|
// We have that npn is a node we occurring the final updated version of |
241 |
|
// the proof. We can now debug based on the expected set of free |
242 |
|
// assumptions. |
243 |
|
Trace("pfnu-debug") << "Ensure update closed..." << std::endl; |
244 |
|
pfnEnsureClosedWrt( |
245 |
|
cur.get(), fa, "pfnu-debug", "ProofNodeUpdater:finalize"); |
246 |
|
} |
247 |
6194007 |
} |
248 |
|
|
249 |
|
void ProofNodeUpdater::setDebugFreeAssumptions( |
250 |
|
const std::vector<Node>& freeAssumps) |
251 |
|
{ |
252 |
|
d_freeAssumps.clear(); |
253 |
|
d_freeAssumps.insert( |
254 |
|
d_freeAssumps.end(), freeAssumps.begin(), freeAssumps.end()); |
255 |
|
d_debugFreeAssumps = true; |
256 |
|
} |
257 |
|
|
258 |
29280 |
} // namespace cvc5 |