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 |
350 |
ProofNodeUpdaterCallback::ProofNodeUpdaterCallback() {} |
26 |
350 |
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 |
329 |
ProofNodeUpdater::ProofNodeUpdater(ProofNodeManager* pnm, |
39 |
|
ProofNodeUpdaterCallback& cb, |
40 |
|
bool mergeSubproofs, |
41 |
329 |
bool autoSym) |
42 |
|
: d_pnm(pnm), |
43 |
|
d_cb(cb), |
44 |
|
d_debugFreeAssumps(false), |
45 |
|
d_mergeSubproofs(mergeSubproofs), |
46 |
329 |
d_autoSym(autoSym) |
47 |
|
{ |
48 |
329 |
} |
49 |
|
|
50 |
181 |
void ProofNodeUpdater::process(std::shared_ptr<ProofNode> pf) |
51 |
|
{ |
52 |
181 |
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 |
181 |
processInternal(pf, d_freeAssumps); |
73 |
181 |
} |
74 |
|
|
75 |
181 |
void ProofNodeUpdater::processInternal(std::shared_ptr<ProofNode> pf, |
76 |
|
std::vector<Node>& fa) |
77 |
|
{ |
78 |
|
// Note that processInternal uses a single scope; fa is updated based on |
79 |
|
// the current free assumptions of the proof nodes on the stack. |
80 |
|
|
81 |
|
// The list of proof nodes we are currently traversing beneath. This is used |
82 |
|
// for checking for cycles in the overall proof. |
83 |
362 |
std::vector<std::shared_ptr<ProofNode>> traversing; |
84 |
|
// Map from formulas to (closed) proof nodes that prove that fact |
85 |
362 |
std::map<Node, std::shared_ptr<ProofNode>> resCache; |
86 |
|
// Map from formulas to non-closed proof nodes that prove that fact. These |
87 |
|
// are replaced by proofs in the above map when applicable. |
88 |
362 |
std::map<Node, std::vector<std::shared_ptr<ProofNode>>> resCacheNcWaiting; |
89 |
|
// Map from proof nodes to whether they contain assumptions |
90 |
362 |
std::unordered_map<const ProofNode*, bool> cfaMap; |
91 |
181 |
Trace("pf-process") << "ProofNodeUpdater::process" << std::endl; |
92 |
362 |
std::unordered_map<std::shared_ptr<ProofNode>, bool> visited; |
93 |
181 |
std::unordered_map<std::shared_ptr<ProofNode>, bool>::iterator it; |
94 |
362 |
std::vector<std::shared_ptr<ProofNode>> visit; |
95 |
362 |
std::shared_ptr<ProofNode> cur; |
96 |
181 |
visit.push_back(pf); |
97 |
181 |
std::map<Node, std::shared_ptr<ProofNode>>::iterator itc; |
98 |
362 |
Node res; |
99 |
14705 |
do |
100 |
|
{ |
101 |
14886 |
cur = visit.back(); |
102 |
14886 |
visit.pop_back(); |
103 |
14886 |
it = visited.find(cur); |
104 |
14886 |
res = cur->getResult(); |
105 |
14886 |
if (it == visited.end()) |
106 |
|
{ |
107 |
7379 |
if (d_mergeSubproofs) |
108 |
|
{ |
109 |
3618 |
itc = resCache.find(res); |
110 |
3926 |
if (itc != resCache.end()) |
111 |
|
{ |
112 |
|
// already have a proof, merge it into this one |
113 |
308 |
visited[cur] = true; |
114 |
308 |
d_pnm->updateNode(cur.get(), itc->second.get()); |
115 |
|
// does not contain free assumptions since the range of resCache does |
116 |
|
// not contain free assumptions |
117 |
308 |
cfaMap[cur.get()] = false; |
118 |
656 |
continue; |
119 |
|
} |
120 |
|
} |
121 |
|
// run update to a fixed point |
122 |
7071 |
bool continueUpdate = true; |
123 |
7831 |
while (runUpdate(cur, fa, continueUpdate) && continueUpdate) |
124 |
|
{ |
125 |
380 |
Trace("pf-process-debug") << "...updated proof." << std::endl; |
126 |
|
} |
127 |
7071 |
visited[cur] = !continueUpdate; |
128 |
7111 |
if (!continueUpdate) |
129 |
|
{ |
130 |
|
// no further changes should be made to cur according to the callback |
131 |
80 |
Trace("pf-process-debug") |
132 |
40 |
<< "...marked to not continue update." << std::endl; |
133 |
40 |
runFinalize(cur, fa, resCache, resCacheNcWaiting, cfaMap); |
134 |
40 |
continue; |
135 |
|
} |
136 |
7031 |
traversing.push_back(cur); |
137 |
7031 |
visit.push_back(cur); |
138 |
|
// If we are not the top-level proof, we were a scope, or became a scope |
139 |
|
// after updating, we do a separate recursive call to this method. This |
140 |
|
// allows us to properly track the assumptions in scope, which is |
141 |
|
// important for example to merge or to determine updates based on free |
142 |
|
// assumptions. |
143 |
7031 |
if (cur->getRule() == PfRule::SCOPE) |
144 |
|
{ |
145 |
36 |
const std::vector<Node>& args = cur->getArguments(); |
146 |
36 |
fa.insert(fa.end(), args.begin(), args.end()); |
147 |
|
} |
148 |
7031 |
const std::vector<std::shared_ptr<ProofNode>>& ccp = cur->getChildren(); |
149 |
|
// now, process children |
150 |
14705 |
for (const std::shared_ptr<ProofNode>& cp : ccp) |
151 |
|
{ |
152 |
23022 |
if (std::find(traversing.begin(), traversing.end(), cp) |
153 |
23022 |
!= traversing.end()) |
154 |
|
{ |
155 |
|
Unhandled() |
156 |
|
<< "ProofNodeUpdater::processInternal: cyclic proof! (use " |
157 |
|
"--proof-eager-checking)" |
158 |
|
<< std::endl; |
159 |
|
} |
160 |
7674 |
visit.push_back(cp); |
161 |
|
} |
162 |
|
} |
163 |
7507 |
else if (!it->second) |
164 |
|
{ |
165 |
7031 |
Assert(!traversing.empty()); |
166 |
7031 |
traversing.pop_back(); |
167 |
7031 |
visited[cur] = true; |
168 |
|
// finalize the node |
169 |
7031 |
if (cur->getRule() == PfRule::SCOPE) |
170 |
|
{ |
171 |
36 |
const std::vector<Node>& args = cur->getArguments(); |
172 |
36 |
Assert(fa.size() >= args.size()); |
173 |
36 |
fa.resize(fa.size() - args.size()); |
174 |
|
} |
175 |
7031 |
runFinalize(cur, fa, resCache, resCacheNcWaiting, cfaMap); |
176 |
|
} |
177 |
14886 |
} while (!visit.empty()); |
178 |
181 |
Trace("pf-process") << "ProofNodeUpdater::process: finished" << std::endl; |
179 |
181 |
} |
180 |
|
|
181 |
7451 |
bool ProofNodeUpdater::runUpdate(std::shared_ptr<ProofNode> cur, |
182 |
|
const std::vector<Node>& fa, |
183 |
|
bool& continueUpdate) |
184 |
|
{ |
185 |
|
// should it be updated? |
186 |
7451 |
if (!d_cb.shouldUpdate(cur, fa, continueUpdate)) |
187 |
|
{ |
188 |
6608 |
return false; |
189 |
|
} |
190 |
843 |
PfRule id = cur->getRule(); |
191 |
|
// use CDProof to open a scope for which the callback updates |
192 |
1686 |
CDProof cpf(d_pnm, nullptr, "ProofNodeUpdater::CDProof", d_autoSym); |
193 |
843 |
const std::vector<std::shared_ptr<ProofNode>>& cc = cur->getChildren(); |
194 |
1686 |
std::vector<Node> ccn; |
195 |
918 |
for (const std::shared_ptr<ProofNode>& cp : cc) |
196 |
|
{ |
197 |
150 |
Node cpres = cp->getResult(); |
198 |
75 |
ccn.push_back(cpres); |
199 |
|
// store in the proof |
200 |
75 |
cpf.addProof(cp); |
201 |
|
} |
202 |
1686 |
Node res = cur->getResult(); |
203 |
1686 |
Trace("pf-process-debug") |
204 |
843 |
<< "Updating (" << cur->getRule() << "): " << res << std::endl; |
205 |
|
// only if the callback updated the node |
206 |
843 |
if (d_cb.update(res, id, ccn, cur->getArguments(), &cpf, continueUpdate)) |
207 |
|
{ |
208 |
840 |
std::shared_ptr<ProofNode> npn = cpf.getProofFor(res); |
209 |
840 |
std::vector<Node> fullFa; |
210 |
420 |
if (d_debugFreeAssumps) |
211 |
|
{ |
212 |
|
expr::getFreeAssumptions(cur.get(), fullFa); |
213 |
|
Trace("pfnu-debug") << "Original proof : " << *cur << std::endl; |
214 |
|
} |
215 |
|
// then, update the original proof node based on this one |
216 |
420 |
Trace("pf-process-debug") << "Update node..." << std::endl; |
217 |
420 |
d_pnm->updateNode(cur.get(), npn.get()); |
218 |
420 |
Trace("pf-process-debug") << "...update node finished." << std::endl; |
219 |
420 |
if (d_debugFreeAssumps) |
220 |
|
{ |
221 |
|
fullFa.insert(fullFa.end(), fa.begin(), fa.end()); |
222 |
|
// We have that npn is a node we occurring the final updated version of |
223 |
|
// the proof. We can now debug based on the expected set of free |
224 |
|
// assumptions. |
225 |
|
Trace("pfnu-debug") << "Ensure update closed..." << std::endl; |
226 |
|
pfnEnsureClosedWrt( |
227 |
|
npn.get(), fullFa, "pfnu-debug", "ProofNodeUpdater:postupdate"); |
228 |
|
} |
229 |
420 |
Trace("pf-process-debug") << "..finished" << std::endl; |
230 |
420 |
return true; |
231 |
|
} |
232 |
423 |
Trace("pf-process-debug") << "..finished" << std::endl; |
233 |
423 |
return false; |
234 |
|
} |
235 |
|
|
236 |
7071 |
void ProofNodeUpdater::runFinalize( |
237 |
|
std::shared_ptr<ProofNode> cur, |
238 |
|
const std::vector<Node>& fa, |
239 |
|
std::map<Node, std::shared_ptr<ProofNode>>& resCache, |
240 |
|
std::map<Node, std::vector<std::shared_ptr<ProofNode>>>& resCacheNcWaiting, |
241 |
|
std::unordered_map<const ProofNode*, bool>& cfaMap) |
242 |
|
{ |
243 |
7071 |
if (d_mergeSubproofs) |
244 |
|
{ |
245 |
6620 |
Node res = cur->getResult(); |
246 |
|
// cache the result if we don't contain an assumption |
247 |
3310 |
if (!expr::containsAssumption(cur.get(), cfaMap)) |
248 |
|
{ |
249 |
|
// cache result if we are merging subproofs |
250 |
2160 |
resCache[res] = cur; |
251 |
|
// go back and merge into the non-closed proofs of the same fact |
252 |
|
std::map<Node, std::vector<std::shared_ptr<ProofNode>>>::iterator itnw = |
253 |
2160 |
resCacheNcWaiting.find(res); |
254 |
2160 |
if (itnw != resCacheNcWaiting.end()) |
255 |
|
{ |
256 |
|
for (std::shared_ptr<ProofNode>& ncp : itnw->second) |
257 |
|
{ |
258 |
|
d_pnm->updateNode(ncp.get(), cur.get()); |
259 |
|
} |
260 |
|
resCacheNcWaiting.erase(res); |
261 |
|
} |
262 |
|
} |
263 |
|
else |
264 |
|
{ |
265 |
1150 |
resCacheNcWaiting[res].push_back(cur); |
266 |
|
} |
267 |
|
} |
268 |
7071 |
if (d_debugFreeAssumps) |
269 |
|
{ |
270 |
|
// We have that npn is a node we occurring the final updated version of |
271 |
|
// the proof. We can now debug based on the expected set of free |
272 |
|
// assumptions. |
273 |
|
Trace("pfnu-debug") << "Ensure update closed..." << std::endl; |
274 |
|
pfnEnsureClosedWrt( |
275 |
|
cur.get(), fa, "pfnu-debug", "ProofNodeUpdater:finalize"); |
276 |
|
} |
277 |
7071 |
} |
278 |
|
|
279 |
|
void ProofNodeUpdater::setDebugFreeAssumptions( |
280 |
|
const std::vector<Node>& freeAssumps) |
281 |
|
{ |
282 |
|
d_freeAssumps.clear(); |
283 |
|
d_freeAssumps.insert( |
284 |
|
d_freeAssumps.end(), freeAssumps.begin(), freeAssumps.end()); |
285 |
|
d_debugFreeAssumps = true; |
286 |
|
} |
287 |
|
|
288 |
22746 |
} // namespace cvc5 |