Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Aina Niemetz, Hans-Joerg Schurr
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 term conversion proof generator utility.
14 : : */
15 : :
16 : : #include "proof/conv_proof_generator.h"
17 : :
18 : : #include <sstream>
19 : :
20 : : #include "expr/term_context.h"
21 : : #include "expr/term_context_stack.h"
22 : : #include "printer/let_binding.h"
23 : : #include "proof/proof_checker.h"
24 : : #include "proof/proof_node.h"
25 : : #include "proof/proof_node_algorithm.h"
26 : :
27 : : using namespace cvc5::internal::kind;
28 : :
29 : : namespace cvc5::internal {
30 : :
31 : 0 : std::ostream& operator<<(std::ostream& out, TConvPolicy tcpol)
32 : : {
33 [ - - ][ - ]: 0 : switch (tcpol)
34 : : {
35 : 0 : case TConvPolicy::FIXPOINT: out << "FIXPOINT"; break;
36 : 0 : case TConvPolicy::ONCE: out << "ONCE"; break;
37 : 0 : default: out << "TConvPolicy:unknown"; break;
38 : : }
39 : 0 : return out;
40 : : }
41 : :
42 : 0 : std::ostream& operator<<(std::ostream& out, TConvCachePolicy tcpol)
43 : : {
44 [ - - ][ - - ]: 0 : switch (tcpol)
45 : : {
46 : 0 : case TConvCachePolicy::STATIC: out << "STATIC"; break;
47 : 0 : case TConvCachePolicy::DYNAMIC: out << "DYNAMIC"; break;
48 : 0 : case TConvCachePolicy::NEVER: out << "NEVER"; break;
49 : 0 : default: out << "TConvCachePolicy:unknown"; break;
50 : : }
51 : 0 : return out;
52 : : }
53 : :
54 : 192909 : TConvProofGenerator::TConvProofGenerator(Env& env,
55 : : context::Context* c,
56 : : TConvPolicy pol,
57 : : TConvCachePolicy cpol,
58 : : std::string name,
59 : : TermContext* tccb,
60 : 192909 : bool rewriteOps)
61 : : : EnvObj(env),
62 : 192909 : d_proof(env, nullptr, c, name + "::LazyCDProof"),
63 : : d_preRewriteMap(c ? c : &d_context),
64 : : d_postRewriteMap(c ? c : &d_context),
65 : : d_policy(pol),
66 : : d_cpolicy(cpol),
67 : : d_name(name),
68 : : d_tcontext(tccb),
69 [ + + ][ + + ]: 385818 : d_rewriteOps(rewriteOps)
70 : : {
71 : 192909 : }
72 : :
73 : 328787 : TConvProofGenerator::~TConvProofGenerator() {}
74 : :
75 : 4326910 : void TConvProofGenerator::addRewriteStep(Node t,
76 : : Node s,
77 : : ProofGenerator* pg,
78 : : bool isPre,
79 : : TrustId trustId,
80 : : bool isClosed,
81 : : uint32_t tctx)
82 : : {
83 : 12980700 : Node eq = registerRewriteStep(t, s, tctx, isPre);
84 [ + + ]: 4326910 : if (!eq.isNull())
85 : : {
86 : 4314540 : d_proof.addLazyStep(eq, pg, trustId, isClosed);
87 : : }
88 : 4326910 : }
89 : :
90 : 0 : void TConvProofGenerator::addRewriteStep(
91 : : Node t, Node s, ProofStep ps, bool isPre, uint32_t tctx)
92 : : {
93 : 0 : Node eq = registerRewriteStep(t, s, tctx, isPre);
94 [ - - ]: 0 : if (!eq.isNull())
95 : : {
96 : 0 : d_proof.addStep(eq, ps);
97 : : }
98 : 0 : }
99 : :
100 : 1489930 : void TConvProofGenerator::addRewriteStep(Node t,
101 : : Node s,
102 : : ProofRule id,
103 : : const std::vector<Node>& children,
104 : : const std::vector<Node>& args,
105 : : bool isPre,
106 : : uint32_t tctx)
107 : : {
108 : 4469780 : Node eq = registerRewriteStep(t, s, tctx, isPre);
109 [ + + ]: 1489930 : if (!eq.isNull())
110 : : {
111 : 1103580 : d_proof.addStep(eq, id, children, args);
112 : : }
113 : 1489930 : }
114 : :
115 : 0 : bool TConvProofGenerator::hasRewriteStep(Node t,
116 : : uint32_t tctx,
117 : : bool isPre) const
118 : : {
119 : 0 : return !getRewriteStep(t, tctx, isPre).isNull();
120 : : }
121 : :
122 : 0 : Node TConvProofGenerator::getRewriteStep(Node t,
123 : : uint32_t tctx,
124 : : bool isPre) const
125 : : {
126 : 0 : Node thash = t;
127 [ - - ]: 0 : if (d_tcontext != nullptr)
128 : : {
129 : 0 : thash = TCtxNode::computeNodeHash(t, tctx);
130 : : }
131 : 0 : return getRewriteStepInternal(thash, isPre);
132 : : }
133 : :
134 : 5816840 : Node TConvProofGenerator::registerRewriteStep(Node t,
135 : : Node s,
136 : : uint32_t tctx,
137 : : bool isPre)
138 : : {
139 [ - + ][ - + ]: 5816840 : Assert(!t.isNull());
[ - - ]
140 [ - + ][ - + ]: 5816840 : Assert(!s.isNull());
[ - - ]
141 : :
142 [ + + ]: 5816840 : if (t == s)
143 : : {
144 : 2961 : return Node::null();
145 : : }
146 : 11627700 : Node thash = t;
147 [ + + ]: 5813870 : if (d_tcontext != nullptr)
148 : : {
149 : 116739 : thash = TCtxNode::computeNodeHash(t, tctx);
150 : : }
151 : : else
152 : : {
153 : : // don't use term context ids if not using term context
154 [ - + ][ - + ]: 5697140 : Assert(tctx == 0);
[ - - ]
155 : : }
156 : : // should not rewrite term to two different things
157 [ + + ]: 5813870 : if (!getRewriteStepInternal(thash, isPre).isNull())
158 : : {
159 : 791494 : Assert(getRewriteStepInternal(thash, isPre) == s)
160 : 395747 : << identify() << " rewriting " << t << " to both " << s << " and "
161 : 395747 : << getRewriteStepInternal(thash, isPre);
162 : 395747 : return Node::null();
163 : : }
164 [ + + ]: 5418130 : NodeNodeMap& rm = isPre ? d_preRewriteMap : d_postRewriteMap;
165 : 5418130 : rm[thash] = s;
166 [ - + ]: 5418130 : if (d_cpolicy == TConvCachePolicy::DYNAMIC)
167 : : {
168 : : // clear the cache
169 : 0 : d_cache.clear();
170 : : }
171 : 5418130 : return t.eqNode(s);
172 : : }
173 : :
174 : 439411 : std::shared_ptr<ProofNode> TConvProofGenerator::getProofFor(Node f)
175 : : {
176 [ + - ][ - + ]: 878822 : Trace("tconv-pf-gen") << "TConvProofGenerator::getProofFor: " << identify()
[ - - ]
177 : 439411 : << ": " << f << std::endl;
178 [ - + ]: 439411 : if (f.getKind() != Kind::EQUAL)
179 : : {
180 : 0 : std::stringstream serr;
181 : 0 : serr << "TConvProofGenerator::getProofFor: " << identify()
182 : 0 : << ": fail, non-equality " << f;
183 : 0 : Unhandled() << serr.str();
184 : : Trace("tconv-pf-gen") << serr.str() << std::endl;
185 : : return nullptr;
186 : : }
187 : : // we use the existing proofs
188 : 878822 : LazyCDProof lpf(d_env, &d_proof, nullptr, d_name + "::LazyCDProof");
189 [ - + ]: 439411 : if (f[0] == f[1])
190 : : {
191 : : // assertion failure in debug
192 : 0 : Assert(false) << "TConvProofGenerator::getProofFor: " << identify()
193 : 0 : << ": don't ask for trivial proofs";
194 : : lpf.addStep(f, ProofRule::REFL, {}, {f[0]});
195 : : }
196 : : else
197 : : {
198 : 439411 : Node conc = getProofForRewriting(f[0], lpf, d_tcontext);
199 [ - + ]: 439411 : if (conc != f)
200 : : {
201 : 0 : bool debugTraceEnabled = TraceIsOn("tconv-pf-gen-debug");
202 : 0 : Assert(conc.getKind() == Kind::EQUAL && conc[0] == f[0]);
203 : 0 : std::stringstream serr;
204 : 0 : serr << "TConvProofGenerator::getProofFor: " << toStringDebug()
205 : 0 : << ": failed, mismatch";
206 [ - - ]: 0 : if (!debugTraceEnabled)
207 : : {
208 : 0 : serr << " (see -t tconv-pf-gen-debug for details)";
209 : : }
210 : 0 : serr << std::endl;
211 : 0 : serr << " source: " << f[0] << std::endl;
212 : 0 : serr << " requested conclusion: " << f[1] << std::endl;
213 : 0 : serr << "conclusion from generator: " << conc[1] << std::endl;
214 : :
215 [ - - ]: 0 : if (debugTraceEnabled)
216 : : {
217 [ - - ]: 0 : Trace("tconv-pf-gen-debug") << "Rewrite steps:" << std::endl;
218 [ - - ]: 0 : for (size_t r = 0; r < 2; r++)
219 : : {
220 [ - - ]: 0 : const NodeNodeMap& rm = r == 0 ? d_preRewriteMap : d_postRewriteMap;
221 : : serr << "Rewrite steps (" << (r == 0 ? "pre" : "post")
222 [ - - ]: 0 : << "):" << std::endl;
223 [ - - ]: 0 : for (NodeNodeMap::const_iterator it = rm.begin(); it != rm.end();
224 : 0 : ++it)
225 : : {
226 : 0 : serr << (*it).first << " -> " << (*it).second << std::endl;
227 : : }
228 : : }
229 : : }
230 : 0 : Unhandled() << serr.str();
231 : : return nullptr;
232 : : }
233 : : }
234 : 878822 : std::shared_ptr<ProofNode> pfn = lpf.getProofFor(f);
235 [ + - ]: 439411 : Trace("tconv-pf-gen") << "... success" << std::endl;
236 [ - + ][ - + ]: 439411 : Assert(pfn != nullptr);
[ - - ]
237 [ + - ]: 439411 : Trace("tconv-pf-gen-debug-pf") << "... proof is " << *pfn << std::endl;
238 : 439411 : return pfn;
239 : : }
240 : :
241 : 30299 : std::shared_ptr<ProofNode> TConvProofGenerator::getProofForRewriting(Node n)
242 : : {
243 : 60598 : LazyCDProof lpf(d_env, &d_proof, nullptr, d_name + "::LazyCDProofRew");
244 : 60598 : Node conc = getProofForRewriting(n, lpf, d_tcontext);
245 [ - + ]: 30299 : if (conc[1] == n)
246 : : {
247 : : // assertion failure in debug
248 : 0 : Assert(false) << "TConvProofGenerator::getProofForRewriting: " << identify()
249 : 0 : << ": don't ask for trivial proofs";
250 : : lpf.addStep(conc, ProofRule::REFL, {}, {n});
251 : : }
252 : 30299 : std::shared_ptr<ProofNode> pfn = lpf.getProofFor(conc);
253 [ - + ][ - + ]: 30299 : Assert(pfn != nullptr);
[ - - ]
254 [ + - ]: 30299 : Trace("tconv-pf-gen-debug-pf") << "... proof is " << *pfn << std::endl;
255 : 60598 : return pfn;
256 : : }
257 : :
258 : 469710 : Node TConvProofGenerator::getProofForRewriting(Node t,
259 : : LazyCDProof& pf,
260 : : TermContext* tctx)
261 : : {
262 : 469710 : NodeManager* nm = nodeManager();
263 : : // Invariant: if visited[hash(t)] = s or rewritten[hash(t)] = s and t,s are
264 : : // distinct, then pf is able to generate a proof of t=s. We must
265 : : // Node in the domains of the maps below due to hashing creating new (SEXPR)
266 : : // nodes.
267 : :
268 : : // the final rewritten form of terms
269 : 939420 : std::unordered_map<Node, Node> visited;
270 : : // the rewritten form of terms we have processed so far
271 : 939420 : std::unordered_map<Node, Node> rewritten;
272 : 469710 : std::unordered_map<Node, Node>::iterator it;
273 : 469710 : std::unordered_map<Node, Node>::iterator itr;
274 : 469710 : std::map<Node, std::shared_ptr<ProofNode> >::iterator itc;
275 [ + - ]: 939420 : Trace("tconv-pf-gen-rewrite")
276 [ - + ][ - - ]: 469710 : << "TConvProofGenerator::getProofForRewriting: " << toStringDebug()
277 : 469710 : << std::endl;
278 [ + - ]: 469710 : Trace("tconv-pf-gen-rewrite") << "Input: " << t << std::endl;
279 : : // if provided, we use term context for cache
280 : 469710 : std::shared_ptr<TCtxStack> visitctx;
281 : : // otherwise, visit is used if we don't have a term context
282 : 939420 : std::vector<TNode> visit;
283 : 939420 : Node tinitialHash;
284 [ + + ]: 469710 : if (tctx != nullptr)
285 : : {
286 : 18004 : visitctx = std::make_shared<TCtxStack>(tctx);
287 : 18004 : visitctx->pushInitial(t);
288 : 18004 : tinitialHash = TCtxNode::computeNodeHash(t, tctx->initialValue());
289 : : }
290 : : else
291 : : {
292 : 451706 : visit.push_back(t);
293 : 451706 : tinitialHash = t;
294 : : }
295 : 939420 : Node cur;
296 : 469710 : uint32_t curCVal = 0;
297 : 939420 : Node curHash;
298 : 16876800 : do
299 : : {
300 : : // pop the top element
301 [ + + ]: 17346500 : if (tctx != nullptr)
302 : : {
303 : 1727860 : std::pair<Node, uint32_t> curPair = visitctx->getCurrent();
304 : 863928 : cur = curPair.first;
305 : 863928 : curCVal = curPair.second;
306 : 863928 : curHash = TCtxNode::computeNodeHash(cur, curCVal);
307 : 863928 : visitctx->pop();
308 : : }
309 : : else
310 : : {
311 : 16482600 : cur = visit.back();
312 : 16482600 : curHash = cur;
313 : 16482600 : visit.pop_back();
314 : : }
315 [ + - ]: 17346500 : Trace("tconv-pf-gen-rewrite") << "* visit : " << curHash << std::endl;
316 : : // has the proof for cur been cached?
317 : 17346500 : itc = d_cache.find(curHash);
318 [ + + ]: 17346500 : if (itc != d_cache.end())
319 : : {
320 : 9270120 : Node res = itc->second->getResult();
321 [ - + ][ - + ]: 4635060 : Assert(res.getKind() == Kind::EQUAL);
[ - - ]
322 [ - + ][ - + ]: 4635060 : Assert(!res[1].isNull());
[ - - ]
323 : 4635060 : visited[curHash] = res[1];
324 : 4635060 : pf.addProof(itc->second);
325 : 4635060 : continue;
326 : : }
327 : 12711500 : it = visited.find(curHash);
328 [ + + ]: 12711500 : if (it == visited.end())
329 : : {
330 [ + - ]: 5224990 : Trace("tconv-pf-gen-rewrite") << "- previsit" << std::endl;
331 : 5224990 : visited[curHash] = Node::null();
332 : : // did we rewrite the current node (at pre-rewrite)?
333 : 10450000 : Node rcur = getRewriteStepInternal(curHash, true);
334 [ + + ]: 5224990 : if (!rcur.isNull())
335 : : {
336 [ + - ]: 1143420 : Trace("tconv-pf-gen-rewrite")
337 : 571708 : << "*** " << curHash << " prerewrites to " << rcur << std::endl;
338 : : // d_proof has a proof of cur = rcur. Hence there is nothing
339 : : // to do here, as pf will reference d_proof to get its proof.
340 [ + + ]: 571708 : if (d_policy == TConvPolicy::FIXPOINT)
341 : : {
342 : : // It may be the case that rcur also rewrites, thus we cannot assign
343 : : // the final rewritten form for cur yet. Instead we revisit cur after
344 : : // finishing visiting rcur.
345 : 525724 : rewritten[curHash] = rcur;
346 [ + + ]: 525724 : if (tctx != nullptr)
347 : : {
348 : 18570 : visitctx->push(cur, curCVal);
349 : 18570 : visitctx->push(rcur, curCVal);
350 : : }
351 : : else
352 : : {
353 : 507154 : visit.push_back(cur);
354 : 507154 : visit.push_back(rcur);
355 : : }
356 : : }
357 : : else
358 : : {
359 [ - + ][ - + ]: 45984 : Assert(d_policy == TConvPolicy::ONCE);
[ - - ]
360 [ + - ]: 91968 : Trace("tconv-pf-gen-rewrite") << "-> (once, prewrite) " << curHash
361 : 45984 : << " = " << rcur << std::endl;
362 : : // not rewriting again, rcur is final
363 [ - + ][ - + ]: 45984 : Assert(!rcur.isNull());
[ - - ]
364 : 45984 : visited[curHash] = rcur;
365 : 45984 : doCache(curHash, cur, rcur, pf);
366 : : }
367 : : }
368 [ + + ]: 4653280 : else if (tctx != nullptr)
369 : : {
370 : 327891 : visitctx->push(cur, curCVal);
371 : : // visit operator if apply uf
372 [ - + ][ - - ]: 327891 : if (d_rewriteOps && cur.getKind() == Kind::APPLY_UF)
[ - + ]
373 : : {
374 : 0 : visitctx->pushOp(cur, curCVal);
375 : : }
376 : 327891 : visitctx->pushChildren(cur, curCVal);
377 : : }
378 : : else
379 : : {
380 : 4325390 : visit.push_back(cur);
381 : : // visit operator if apply uf
382 [ + + ][ + + ]: 4325390 : if (d_rewriteOps && cur.getKind() == Kind::APPLY_UF)
[ + + ]
383 : : {
384 : 141803 : visit.push_back(cur.getOperator());
385 : : }
386 : 4325390 : visit.insert(visit.end(), cur.begin(), cur.end());
387 : : }
388 : : }
389 [ + + ]: 7486480 : else if (it->second.isNull())
390 : : {
391 : 5767890 : itr = rewritten.find(curHash);
392 [ + + ]: 5767890 : if (itr != rewritten.end())
393 : : {
394 : : // only can generate partially rewritten nodes when rewrite again is
395 : : // true.
396 [ - + ][ - + ]: 1371620 : Assert(d_policy != TConvPolicy::ONCE);
[ - - ]
397 : : // if it was rewritten, check the status of the rewritten node,
398 : : // which should be finished now
399 : 2743240 : Node rcur = itr->second;
400 [ + - ]: 2743240 : Trace("tconv-pf-gen-rewrite")
401 : 1371620 : << "- postvisit, previously rewritten to " << rcur << std::endl;
402 : 2743240 : Node rcurHash = rcur;
403 [ + + ]: 1371620 : if (tctx != nullptr)
404 : : {
405 : 34182 : rcurHash = TCtxNode::computeNodeHash(rcur, curCVal);
406 : : }
407 [ - + ][ - + ]: 1371620 : Assert(cur != rcur);
[ - - ]
408 : : // the final rewritten form of cur is the final form of rcur
409 : 1371620 : Node rcurFinal = visited[rcurHash];
410 [ - + ][ - + ]: 1371620 : Assert(!rcurFinal.isNull());
[ - - ]
411 [ + + ]: 1371620 : if (rcurFinal != rcur)
412 : : {
413 : : // must connect via TRANS
414 : 1246650 : std::vector<Node> pfChildren;
415 : 623326 : pfChildren.push_back(cur.eqNode(rcur));
416 : 623326 : pfChildren.push_back(rcur.eqNode(rcurFinal));
417 : 623326 : Node result = cur.eqNode(rcurFinal);
418 : 623326 : pf.addStep(result, ProofRule::TRANS, pfChildren, {});
419 : : }
420 [ + - ]: 2743240 : Trace("tconv-pf-gen-rewrite")
421 : 0 : << "-> (rewritten postrewrite) " << curHash << " = " << rcurFinal
422 : 1371620 : << std::endl;
423 : 1371620 : visited[curHash] = rcurFinal;
424 : 1371620 : doCache(curHash, cur, rcurFinal, pf);
425 : : }
426 : : else
427 : : {
428 [ + - ]: 4396270 : Trace("tconv-pf-gen-rewrite") << "- postvisit" << std::endl;
429 : 8792540 : Node ret = cur;
430 : 8792540 : Node retHash = curHash;
431 : 4396270 : bool childChanged = false;
432 : 8792540 : std::vector<Node> children;
433 : 4396270 : Kind ck = cur.getKind();
434 [ + + ][ + + ]: 4396270 : if (d_rewriteOps && ck == Kind::APPLY_UF)
435 : : {
436 : : // the operator of APPLY_UF is visited
437 : 282350 : Node cop = cur.getOperator();
438 [ - + ]: 141175 : if (tctx != nullptr)
439 : : {
440 : 0 : uint32_t coval = tctx->computeValueOp(cur, curCVal);
441 : 0 : Node coHash = TCtxNode::computeNodeHash(cop, coval);
442 : 0 : it = visited.find(coHash);
443 : : }
444 : : else
445 : : {
446 : 141175 : it = visited.find(cop);
447 : : }
448 [ - + ][ - + ]: 141175 : Assert(it != visited.end());
[ - - ]
449 [ - + ][ - + ]: 141175 : Assert(!it->second.isNull());
[ - - ]
450 [ + - ][ + + ]: 141175 : childChanged = childChanged || cop != it->second;
451 : 282350 : children.push_back(it->second);
452 : : }
453 [ + + ]: 4255100 : else if (cur.getMetaKind() == metakind::PARAMETERIZED)
454 : : {
455 : : // all other parametrized operators are unchanged
456 : 242289 : children.push_back(cur.getOperator());
457 : : }
458 : : // get the results of the children
459 [ + + ]: 4396270 : if (tctx != nullptr)
460 : : {
461 [ + + ]: 764340 : for (size_t i = 0, nchild = cur.getNumChildren(); i < nchild; i++)
462 : : {
463 : 886286 : Node cn = cur[i];
464 : 443143 : uint32_t cnval = tctx->computeValue(cur, curCVal, i);
465 : 886286 : Node cnHash = TCtxNode::computeNodeHash(cn, cnval);
466 : 443143 : it = visited.find(cnHash);
467 [ - + ][ - + ]: 443143 : Assert(it != visited.end());
[ - - ]
468 [ - + ][ - + ]: 443143 : Assert(!it->second.isNull());
[ - - ]
469 [ + + ][ + + ]: 443143 : childChanged = childChanged || cn != it->second;
470 : 443143 : children.push_back(it->second);
471 : : }
472 : : }
473 : : else
474 : : {
475 : : // can use simple loop if not term-context-sensitive
476 [ + + ]: 12286700 : for (const Node& cn : cur)
477 : : {
478 : 8211650 : it = visited.find(cn);
479 [ - + ][ - + ]: 8211650 : Assert(it != visited.end());
[ - - ]
480 [ - + ][ - + ]: 8211650 : Assert(!it->second.isNull());
[ - - ]
481 [ + + ][ + + ]: 8211650 : childChanged = childChanged || cn != it->second;
482 : 8211650 : children.push_back(it->second);
483 : : }
484 : : }
485 [ + + ]: 4396270 : if (childChanged)
486 : : {
487 : 1262470 : ret = nm->mkNode(ck, children);
488 : 1262470 : rewritten[curHash] = ret;
489 : : // congruence to show (cur = ret)
490 : 2524940 : std::vector<Node> pfChildren;
491 : 2524940 : std::vector<Node> pfArgs;
492 : 1262470 : ProofRule congRule = expr::getCongRule(cur, pfArgs);
493 : 1262470 : size_t startIndex = 0;
494 [ + + ]: 1262470 : if (cur.isClosure())
495 : : {
496 : : // Closures always provide the bound variable list as an argument.
497 : : // We skip the bound variable list and add it as an argument.
498 : 13282 : startIndex = 1;
499 : : // The variable list should never change.
500 [ - + ][ - + ]: 13282 : Assert(cur[0] == ret[0]);
[ - - ]
501 : : }
502 [ + + ][ + + ]: 1249190 : else if (ck == Kind::APPLY_UF && children[0] != cur.getOperator())
[ + + ][ + + ]
[ - - ]
503 : : {
504 : 1473 : congRule = ProofRule::HO_CONG;
505 : 1473 : pfArgs.pop_back();
506 : 1473 : pfChildren.push_back(cur.getOperator().eqNode(children[0]));
507 : : }
508 [ + + ]: 4631210 : for (size_t i = startIndex, size = cur.getNumChildren(); i < size;
509 : : i++)
510 : : {
511 [ + + ]: 3368740 : if (cur[i] == ret[i])
512 : : {
513 : : // ensure REFL proof for unchanged children
514 : 2442160 : pf.addStep(cur[i].eqNode(cur[i]), ProofRule::REFL, {}, {cur[i]});
515 : : }
516 : 3368740 : pfChildren.push_back(cur[i].eqNode(ret[i]));
517 : : }
518 : 2524940 : Node result = cur.eqNode(ret);
519 : 1262470 : pf.addStep(result, congRule, pfChildren, pfArgs);
520 : : // must update the hash
521 : 1262470 : retHash = ret;
522 [ + + ]: 1262470 : if (tctx != nullptr)
523 : : {
524 : 108142 : retHash = TCtxNode::computeNodeHash(ret, curCVal);
525 : : }
526 : : }
527 [ + + ]: 3133800 : else if (tctx != nullptr)
528 : : {
529 : : // now we need the hash
530 : 213055 : retHash = TCtxNode::computeNodeHash(cur, curCVal);
531 : : }
532 : : // did we rewrite ret (at post-rewrite)?
533 : 8792540 : Node rret = getRewriteStepInternal(retHash, false);
534 [ + + ][ + + ]: 4396270 : if (!rret.isNull() && d_policy == TConvPolicy::FIXPOINT)
[ + + ]
535 : : {
536 [ + - ]: 1177780 : Trace("tconv-pf-gen-rewrite")
537 : 588888 : << "*** " << retHash << " postrewrites to " << rret << std::endl;
538 : : // d_proof should have a proof of ret = rret, hence nothing to do
539 : : // here, for the same reasons as above. It also may be the case that
540 : : // rret rewrites, hence we must revisit ret.
541 : 588888 : rewritten[retHash] = rret;
542 [ + + ]: 588888 : if (tctx != nullptr)
543 : : {
544 [ + + ]: 8918 : if (cur != ret)
545 : : {
546 : 6694 : visitctx->push(cur, curCVal);
547 : : }
548 : 8918 : visitctx->push(ret, curCVal);
549 : 8918 : visitctx->push(rret, curCVal);
550 : : }
551 : : else
552 : : {
553 [ + + ]: 579970 : if (cur != ret)
554 : : {
555 : 350864 : visit.push_back(cur);
556 : : }
557 : 579970 : visit.push_back(ret);
558 : 579970 : visit.push_back(rret);
559 : : }
560 : : }
561 : : else
562 : : {
563 : : // If we changed due to congruence, and then rewrote, then we
564 : : // require a trans step to connect here
565 [ + + ][ + + ]: 3807380 : if (!rret.isNull() && childChanged)
[ + + ]
566 : : {
567 : 74780 : std::vector<Node> pfChildren;
568 : 37390 : pfChildren.push_back(cur.eqNode(ret));
569 : 37390 : pfChildren.push_back(ret.eqNode(rret));
570 : 37390 : Node result = cur.eqNode(rret);
571 : 37390 : pf.addStep(result, ProofRule::TRANS, pfChildren, {});
572 : : }
573 : : // take its rewrite if it rewrote and we have ONCE rewriting policy
574 [ + + ]: 3807380 : ret = rret.isNull() ? ret : rret;
575 [ + - ]: 7614760 : Trace("tconv-pf-gen-rewrite")
576 : 3807380 : << "-> (postrewrite) " << curHash << " = " << ret << std::endl;
577 : : // it is final
578 [ - + ][ - + ]: 3807380 : Assert(!ret.isNull());
[ - - ]
579 : 3807380 : visited[curHash] = ret;
580 : 3807380 : doCache(curHash, cur, ret, pf);
581 : : }
582 : : }
583 : : }
584 : : else
585 : : {
586 [ + - ]: 1718590 : Trace("tconv-pf-gen-rewrite") << "- already visited" << std::endl;
587 : : }
588 [ + + ][ + + ]: 17346500 : } while (!(tctx != nullptr ? visitctx->empty() : visit.empty()));
589 [ - + ][ - + ]: 469710 : Assert(visited.find(tinitialHash) != visited.end());
[ - - ]
590 [ - + ][ - + ]: 469710 : Assert(!visited.find(tinitialHash)->second.isNull());
[ - - ]
591 [ + - ]: 939420 : Trace("tconv-pf-gen-rewrite")
592 : 469710 : << "...finished, return " << visited[tinitialHash] << std::endl;
593 : : // return the conclusion of the overall proof
594 : 939420 : return t.eqNode(visited[tinitialHash]);
595 : : }
596 : :
597 : 5224990 : void TConvProofGenerator::doCache(Node curHash,
598 : : Node cur,
599 : : Node r,
600 : : LazyCDProof& pf)
601 : : {
602 [ + + ]: 5224990 : if (d_cpolicy != TConvCachePolicy::NEVER)
603 : : {
604 : 2758730 : Node eq = cur.eqNode(r);
605 : 2758730 : d_cache[curHash] = pf.getProofFor(eq);
606 : : }
607 : 5224990 : }
608 : :
609 : 15830900 : Node TConvProofGenerator::getRewriteStepInternal(Node t, bool isPre) const
610 : : {
611 [ + + ]: 15830900 : const NodeNodeMap& rm = isPre ? d_preRewriteMap : d_postRewriteMap;
612 : 15830900 : NodeNodeMap::const_iterator it = rm.find(t);
613 [ + + ]: 15830900 : if (it == rm.end())
614 : : {
615 : 13811700 : return Node::null();
616 : : }
617 : 2019170 : return (*it).second;
618 : : }
619 : 1234 : std::string TConvProofGenerator::identify() const { return d_name; }
620 : :
621 : 0 : std::string TConvProofGenerator::toStringDebug() const
622 : : {
623 : 0 : std::stringstream ss;
624 : 0 : ss << identify() << " (policy=" << d_policy << ", cache policy=" << d_cpolicy
625 [ - - ]: 0 : << (d_tcontext != nullptr ? ", term-context-sensitive" : "") << ")";
626 : 0 : return ss.str();
627 : : }
628 : :
629 : : } // namespace cvc5::internal
|
