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