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