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 : 214212 : TConvProofGenerator::TConvProofGenerator(Env& env,
56 : : context::Context* c,
57 : : TConvPolicy pol,
58 : : TConvCachePolicy cpol,
59 : : std::string name,
60 : : TermContext* tccb,
61 : 214212 : bool rewriteOps)
62 : : : EnvObj(env),
63 : 214212 : 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 [ + + ][ + + ]: 428424 : d_rewriteOps(rewriteOps)
71 : : {
72 : 214212 : }
73 : :
74 : 346512 : TConvProofGenerator::~TConvProofGenerator() {}
75 : :
76 : 2309180 : 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 : 6927540 : Node eq = registerRewriteStep(t, s, tctx, isPre);
85 [ + + ]: 2309180 : if (!eq.isNull())
86 : : {
87 : 2294260 : d_proof.addLazyStep(eq, pg, trustId, isClosed);
88 : : }
89 : 2309180 : }
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 : 1405190 : 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 : 4215570 : Node eq = registerRewriteStep(t, s, tctx, isPre);
110 [ + + ]: 1405190 : if (!eq.isNull())
111 : : {
112 : 1005060 : d_proof.addStep(eq, id, children, args);
113 : : }
114 : 1405190 : }
115 : :
116 : 18 : void TConvProofGenerator::addTheoryRewriteStep(
117 : : Node t, Node s, ProofRewriteRule id, bool isPre, uint32_t tctx)
118 : : {
119 : 18 : std::vector<Node> sargs;
120 : 18 : sargs.push_back(rewriter::mkRewriteRuleNode(nodeManager(), id));
121 : 18 : sargs.push_back(t.eqNode(s));
122 : 18 : addRewriteStep(t, s, ProofRule::THEORY_REWRITE, {}, sargs, isPre, tctx);
123 : 18 : }
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 : 3714370 : Node TConvProofGenerator::registerRewriteStep(Node t,
145 : : Node s,
146 : : uint32_t tctx,
147 : : bool isPre)
148 : : {
149 [ - + ][ - + ]: 3714370 : Assert(!t.isNull());
[ - - ]
150 [ - + ][ - + ]: 3714370 : Assert(!s.isNull());
[ - - ]
151 : :
152 [ - + ]: 3714370 : if (t == s)
153 : : {
154 : 0 : return Node::null();
155 : : }
156 : 7428740 : Node thash = t;
157 [ + + ]: 3714370 : if (d_tcontext != nullptr)
158 : : {
159 : 206257 : thash = TCtxNode::computeNodeHash(t, tctx);
160 : : }
161 : : else
162 : : {
163 : : // don't use term context ids if not using term context
164 [ - + ][ - + ]: 3508120 : Assert(tctx == 0);
[ - - ]
165 : : }
166 : : // should not rewrite term to two different things
167 [ + + ]: 3714370 : if (!getRewriteStepInternal(thash, isPre).isNull())
168 : : {
169 : 830106 : Assert(getRewriteStepInternal(thash, isPre) == s)
170 : 415053 : << identify() << " rewriting " << t << " to both " << s << " and "
171 : 415053 : << getRewriteStepInternal(thash, isPre);
172 : 415053 : return Node::null();
173 : : }
174 [ + + ]: 3299320 : NodeNodeMap& rm = isPre ? d_preRewriteMap : d_postRewriteMap;
175 : 3299320 : rm[thash] = s;
176 [ - + ]: 3299320 : if (d_cpolicy == TConvCachePolicy::DYNAMIC)
177 : : {
178 : : // clear the cache
179 : 0 : d_cache.clear();
180 : : }
181 : 3299320 : return t.eqNode(s);
182 : : }
183 : :
184 : 436843 : std::shared_ptr<ProofNode> TConvProofGenerator::getProofFor(Node f)
185 : : {
186 [ + - ][ - + ]: 873686 : Trace("tconv-pf-gen") << "TConvProofGenerator::getProofFor: " << identify()
[ - - ]
187 : 436843 : << ": " << f << std::endl;
188 [ - + ]: 436843 : 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 : 873686 : LazyCDProof lpf(d_env, &d_proof, nullptr, d_name + "::LazyCDProof");
199 [ + + ]: 436843 : if (f[0] == f[1])
200 : : {
201 : 4 : lpf.addStep(f, ProofRule::REFL, {}, {f[0]});
202 : : }
203 : : else
204 : : {
205 : 436841 : Node conc = getProofForRewriting(f[0], lpf, d_tcontext);
206 [ - + ]: 436841 : 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 : 873686 : std::shared_ptr<ProofNode> pfn = lpf.getProofFor(f);
242 [ + - ]: 436843 : Trace("tconv-pf-gen") << "... success" << std::endl;
243 [ - + ][ - + ]: 436843 : Assert(pfn != nullptr);
[ - - ]
244 [ + - ]: 436843 : Trace("tconv-pf-gen-debug-pf") << "... proof is " << *pfn << std::endl;
245 : 436843 : return pfn;
246 : : }
247 : :
248 : 23780 : std::shared_ptr<ProofNode> TConvProofGenerator::getProofForRewriting(Node n)
249 : : {
250 : 47560 : LazyCDProof lpf(d_env, &d_proof, nullptr, d_name + "::LazyCDProofRew");
251 : 47560 : Node conc = getProofForRewriting(n, lpf, d_tcontext);
252 [ + + ]: 23780 : if (conc[1] == n)
253 : : {
254 : 300 : lpf.addStep(conc, ProofRule::REFL, {}, {n});
255 : : }
256 : 23780 : std::shared_ptr<ProofNode> pfn = lpf.getProofFor(conc);
257 [ - + ][ - + ]: 23780 : Assert(pfn != nullptr);
[ - - ]
258 [ + - ]: 23780 : Trace("tconv-pf-gen-debug-pf") << "... proof is " << *pfn << std::endl;
259 : 47560 : return pfn;
260 : : }
261 : :
262 : 460621 : Node TConvProofGenerator::getProofForRewriting(Node t,
263 : : LazyCDProof& pf,
264 : : TermContext* tctx)
265 : : {
266 : 460621 : 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 : 921242 : std::unordered_map<Node, Node> visited;
274 : : // the rewritten form of terms we have processed so far
275 : 921242 : std::unordered_map<Node, Node> rewritten;
276 : 460621 : std::unordered_map<Node, Node>::iterator it;
277 : 460621 : std::unordered_map<Node, Node>::iterator itr;
278 : 460621 : std::map<Node, std::shared_ptr<ProofNode> >::iterator itc;
279 [ + - ]: 921242 : Trace("tconv-pf-gen-rewrite")
280 [ - + ][ - - ]: 460621 : << "TConvProofGenerator::getProofForRewriting: " << toStringDebug()
281 : 460621 : << std::endl;
282 [ + - ]: 460621 : Trace("tconv-pf-gen-rewrite") << "Input: " << t << std::endl;
283 : : // if provided, we use term context for cache
284 : 460621 : std::shared_ptr<TCtxStack> visitctx;
285 : : // otherwise, visit is used if we don't have a term context
286 : 921242 : std::vector<TNode> visit;
287 : 921242 : Node tinitialHash;
288 [ + + ]: 460621 : if (tctx != nullptr)
289 : : {
290 : 58873 : visitctx = std::make_shared<TCtxStack>(tctx);
291 : 58873 : visitctx->pushInitial(t);
292 : 58873 : tinitialHash = TCtxNode::computeNodeHash(t, tctx->initialValue());
293 : : }
294 : : else
295 : : {
296 : 401748 : visit.push_back(t);
297 : 401748 : tinitialHash = t;
298 : : }
299 : 921242 : Node cur;
300 : 460621 : uint32_t curCVal = 0;
301 : 921242 : Node curHash;
302 : 15031800 : do
303 : : {
304 : : // pop the top element
305 [ + + ]: 15492500 : if (tctx != nullptr)
306 : : {
307 : 5395170 : std::pair<Node, uint32_t> curPair = visitctx->getCurrent();
308 : 2697580 : cur = curPair.first;
309 : 2697580 : curCVal = curPair.second;
310 : 2697580 : curHash = TCtxNode::computeNodeHash(cur, curCVal);
311 : 2697580 : visitctx->pop();
312 : : }
313 : : else
314 : : {
315 : 12794900 : cur = visit.back();
316 : 12794900 : curHash = cur;
317 : 12794900 : visit.pop_back();
318 : : }
319 [ + - ]: 15492500 : Trace("tconv-pf-gen-rewrite") << "* visit : " << curHash << std::endl;
320 : : // has the proof for cur been cached?
321 : 15492500 : itc = d_cache.find(curHash);
322 [ + + ]: 15492500 : if (itc != d_cache.end())
323 : : {
324 : 7095660 : Node res = itc->second->getResult();
325 [ - + ][ - + ]: 3547830 : Assert(res.getKind() == Kind::EQUAL);
[ - - ]
326 [ - + ][ - + ]: 3547830 : Assert(!res[1].isNull());
[ - - ]
327 : 3547830 : visited[curHash] = res[1];
328 : 3547830 : pf.addProof(itc->second);
329 : 3547830 : continue;
330 : : }
331 : 11944600 : it = visited.find(curHash);
332 [ + + ]: 11944600 : if (it == visited.end())
333 : : {
334 [ + - ]: 4786690 : Trace("tconv-pf-gen-rewrite") << "- previsit" << std::endl;
335 : 4786690 : visited[curHash] = Node::null();
336 : : // did we rewrite the current node (at pre-rewrite)?
337 : 9573380 : Node rcur = getRewriteStepInternal(curHash, true);
338 [ + + ]: 4786690 : if (!rcur.isNull())
339 : : {
340 [ + - ]: 963894 : Trace("tconv-pf-gen-rewrite")
341 : 481947 : << "*** " << 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 [ + + ]: 481947 : 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 : 443175 : rewritten[curHash] = rcur;
350 [ + + ]: 443175 : if (tctx != nullptr)
351 : : {
352 : 45812 : visitctx->push(cur, curCVal);
353 : 45812 : visitctx->push(rcur, curCVal);
354 : : }
355 : : else
356 : : {
357 : 397363 : visit.push_back(cur);
358 : 397363 : visit.push_back(rcur);
359 : : }
360 : : }
361 : : else
362 : : {
363 [ - + ][ - + ]: 38772 : Assert(d_policy == TConvPolicy::ONCE);
[ - - ]
364 [ + - ]: 77544 : Trace("tconv-pf-gen-rewrite") << "-> (once, prewrite) " << curHash
365 : 38772 : << " = " << rcur << std::endl;
366 : : // not rewriting again, rcur is final
367 [ - + ][ - + ]: 38772 : Assert(!rcur.isNull());
[ - - ]
368 : 38772 : visited[curHash] = rcur;
369 : 38772 : doCache(curHash, cur, rcur, pf);
370 : : }
371 : : }
372 [ + + ]: 4304740 : else if (tctx != nullptr)
373 : : {
374 : 928083 : visitctx->push(cur, curCVal);
375 : : // visit operator if apply uf
376 [ + + ][ + + ]: 928083 : if (d_rewriteOps && cur.getKind() == Kind::APPLY_UF)
[ + + ]
377 : : {
378 : 527 : visitctx->pushOp(cur, curCVal);
379 : : }
380 : 928083 : visitctx->pushChildren(cur, curCVal);
381 : : }
382 : : else
383 : : {
384 : 3376660 : visit.push_back(cur);
385 : : // visit operator if apply uf
386 [ + + ][ + + ]: 3376660 : if (d_rewriteOps && cur.getKind() == Kind::APPLY_UF)
[ + + ]
387 : : {
388 : 95884 : visit.push_back(cur.getOperator());
389 : : }
390 : 3376660 : visit.insert(visit.end(), cur.begin(), cur.end());
391 : : }
392 : : }
393 [ + + ]: 7157940 : else if (it->second.isNull())
394 : : {
395 : 5313280 : itr = rewritten.find(curHash);
396 [ + + ]: 5313280 : if (itr != rewritten.end())
397 : : {
398 : : // only can generate partially rewritten nodes when rewrite again is
399 : : // true.
400 [ - + ][ - + ]: 1246600 : Assert(d_policy != TConvPolicy::ONCE);
[ - - ]
401 : : // if it was rewritten, check the status of the rewritten node,
402 : : // which should be finished now
403 : 2493190 : Node rcur = itr->second;
404 [ + - ]: 2493190 : Trace("tconv-pf-gen-rewrite")
405 : 1246600 : << "- postvisit, previously rewritten to " << rcur << std::endl;
406 : 2493190 : Node rcurHash = rcur;
407 [ + + ]: 1246600 : if (tctx != nullptr)
408 : : {
409 : 123971 : rcurHash = TCtxNode::computeNodeHash(rcur, curCVal);
410 : : }
411 [ - + ][ - + ]: 1246600 : Assert(cur != rcur);
[ - - ]
412 : : // the final rewritten form of cur is the final form of rcur
413 : 1246600 : Node rcurFinal = visited[rcurHash];
414 [ - + ][ - + ]: 1246600 : Assert(!rcurFinal.isNull());
[ - - ]
415 [ + + ]: 1246600 : if (rcurFinal != rcur)
416 : : {
417 : : // must connect via TRANS
418 : 1131140 : std::vector<Node> pfChildren;
419 : 565571 : pfChildren.push_back(cur.eqNode(rcur));
420 : 565571 : pfChildren.push_back(rcur.eqNode(rcurFinal));
421 : 565571 : Node result = cur.eqNode(rcurFinal);
422 : 565571 : pf.addStep(result, ProofRule::TRANS, pfChildren, {});
423 : : }
424 [ + - ]: 2493190 : Trace("tconv-pf-gen-rewrite")
425 : 0 : << "-> (rewritten postrewrite) " << curHash << " = " << rcurFinal
426 : 1246600 : << std::endl;
427 : 1246600 : visited[curHash] = rcurFinal;
428 : 1246600 : doCache(curHash, cur, rcurFinal, pf);
429 : : }
430 : : else
431 : : {
432 [ + - ]: 4066690 : Trace("tconv-pf-gen-rewrite") << "- postvisit" << std::endl;
433 : 8133370 : Node ret = cur;
434 : 8133370 : Node retHash = curHash;
435 : 4066690 : bool childChanged = false;
436 : 8133370 : std::vector<Node> children;
437 : 4066690 : Kind ck = cur.getKind();
438 [ + + ][ + + ]: 4066690 : if (d_rewriteOps && ck == Kind::APPLY_UF)
439 : : {
440 : : // the operator of APPLY_UF is visited
441 : 192584 : Node cop = cur.getOperator();
442 [ + + ]: 96292 : if (tctx != nullptr)
443 : : {
444 : 408 : uint32_t coval = tctx->computeValueOp(cur, curCVal);
445 : 816 : Node coHash = TCtxNode::computeNodeHash(cop, coval);
446 : 408 : it = visited.find(coHash);
447 : : }
448 : : else
449 : : {
450 : 95884 : it = visited.find(cop);
451 : : }
452 [ - + ][ - + ]: 96292 : Assert(it != visited.end());
[ - - ]
453 [ - + ][ - + ]: 96292 : Assert(!it->second.isNull());
[ - - ]
454 [ + - ][ + + ]: 96292 : childChanged = childChanged || cop != it->second;
455 : 192584 : children.push_back(it->second);
456 : : }
457 [ + + ]: 3970390 : else if (cur.getMetaKind() == metakind::PARAMETERIZED)
458 : : {
459 : : // all other parametrized operators are unchanged
460 : 271999 : children.push_back(cur.getOperator());
461 : : }
462 : : // get the results of the children
463 [ + + ]: 4066690 : if (tctx != nullptr)
464 : : {
465 [ + + ]: 2364130 : for (size_t i = 0, nchild = cur.getNumChildren(); i < nchild; i++)
466 : : {
467 : 2909810 : Node cn = cur[i];
468 : 1454910 : uint32_t cnval = tctx->computeValue(cur, curCVal, i);
469 : 2909810 : Node cnHash = TCtxNode::computeNodeHash(cn, cnval);
470 : 1454910 : it = visited.find(cnHash);
471 [ - + ][ - + ]: 1454910 : Assert(it != visited.end());
[ - - ]
472 [ - + ][ - + ]: 1454910 : Assert(!it->second.isNull());
[ - - ]
473 [ + + ][ + + ]: 1454910 : childChanged = childChanged || cn != it->second;
474 : 1454910 : children.push_back(it->second);
475 : : }
476 : : }
477 : : else
478 : : {
479 : : // can use simple loop if not term-context-sensitive
480 [ + + ]: 9289870 : for (const Node& cn : cur)
481 : : {
482 : 6132410 : it = visited.find(cn);
483 [ - + ][ - + ]: 6132410 : Assert(it != visited.end());
[ - - ]
484 [ - + ][ - + ]: 6132410 : Assert(!it->second.isNull());
[ - - ]
485 [ + + ][ + + ]: 6132410 : childChanged = childChanged || cn != it->second;
486 : 6132410 : children.push_back(it->second);
487 : : }
488 : : }
489 [ + + ]: 4066690 : if (childChanged)
490 : : {
491 : 1101610 : ret = nm->mkNode(ck, children);
492 : 1101610 : rewritten[curHash] = ret;
493 : : // congruence to show (cur = ret)
494 : 2203210 : std::vector<Node> pfChildren;
495 : 2203210 : std::vector<Node> pfArgs;
496 : 1101610 : ProofRule congRule = expr::getCongRule(cur, pfArgs);
497 : 1101610 : size_t startIndex = 0;
498 [ + + ]: 1101610 : 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 : 16564 : startIndex = 1;
503 : : // The variable list should never change.
504 [ - + ][ - + ]: 16564 : Assert(cur[0] == ret[0]);
[ - - ]
505 : : }
506 [ + + ][ + + ]: 1085040 : else if (ck == Kind::APPLY_UF && children[0] != cur.getOperator())
[ + + ][ + + ]
[ - - ]
507 : : {
508 : 1231 : congRule = ProofRule::HO_CONG;
509 : 1231 : pfArgs.clear();
510 : 1231 : pfArgs.push_back(ProofRuleChecker::mkKindNode(nm, Kind::APPLY_UF));
511 : 1231 : pfChildren.push_back(cur.getOperator().eqNode(children[0]));
512 : : }
513 [ + + ]: 3902300 : for (size_t i = startIndex, size = cur.getNumChildren(); i < size;
514 : : i++)
515 : : {
516 [ + + ]: 2800700 : if (cur[i] == ret[i])
517 : : {
518 : : // ensure REFL proof for unchanged children
519 : 1870980 : pf.addStep(cur[i].eqNode(cur[i]), ProofRule::REFL, {}, {cur[i]});
520 : : }
521 : 2800700 : pfChildren.push_back(cur[i].eqNode(ret[i]));
522 : : }
523 : 2203210 : Node result = cur.eqNode(ret);
524 : 1101610 : pf.addStep(result, congRule, pfChildren, pfArgs);
525 : : // must update the hash
526 : 1101610 : retHash = ret;
527 [ + + ]: 1101610 : if (tctx != nullptr)
528 : : {
529 : 165203 : retHash = TCtxNode::computeNodeHash(ret, curCVal);
530 : : }
531 : : }
532 [ + + ]: 2965080 : else if (tctx != nullptr)
533 : : {
534 : : // now we need the hash
535 : 744019 : retHash = TCtxNode::computeNodeHash(cur, curCVal);
536 : : }
537 : : // did we rewrite ret (at post-rewrite)?
538 : 8133370 : Node rret = getRewriteStepInternal(retHash, false);
539 [ + + ][ + + ]: 4066690 : if (!rret.isNull() && d_policy == TConvPolicy::FIXPOINT)
[ + + ]
540 : : {
541 [ + - ]: 1130730 : Trace("tconv-pf-gen-rewrite")
542 : 565367 : << "*** " << 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 : 565367 : rewritten[retHash] = rret;
547 [ + + ]: 565367 : if (tctx != nullptr)
548 : : {
549 [ + + ]: 59298 : if (cur != ret)
550 : : {
551 : 18881 : visitctx->push(cur, curCVal);
552 : : }
553 : 59298 : visitctx->push(ret, curCVal);
554 : 59298 : visitctx->push(rret, curCVal);
555 : : }
556 : : else
557 : : {
558 [ + + ]: 506069 : if (cur != ret)
559 : : {
560 : 313359 : visit.push_back(cur);
561 : : }
562 : 506069 : visit.push_back(ret);
563 : 506069 : 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 [ + + ][ + + ]: 3501320 : if (!rret.isNull() && childChanged)
[ + + ]
571 : : {
572 : 70832 : std::vector<Node> pfChildren;
573 : 35416 : pfChildren.push_back(cur.eqNode(ret));
574 : 35416 : pfChildren.push_back(ret.eqNode(rret));
575 : 35416 : Node result = cur.eqNode(rret);
576 : 35416 : pf.addStep(result, ProofRule::TRANS, pfChildren, {});
577 : : }
578 : : // take its rewrite if it rewrote and we have ONCE rewriting policy
579 [ + + ]: 3501320 : ret = rret.isNull() ? ret : rret;
580 [ + - ]: 7002640 : Trace("tconv-pf-gen-rewrite")
581 : 3501320 : << "-> (postrewrite) " << curHash << " = " << ret << std::endl;
582 : : // it is final
583 [ - + ][ - + ]: 3501320 : Assert(!ret.isNull());
[ - - ]
584 : 3501320 : visited[curHash] = ret;
585 : 3501320 : doCache(curHash, cur, ret, pf);
586 : : }
587 : : }
588 : : }
589 : : else
590 : : {
591 [ + - ]: 1844660 : Trace("tconv-pf-gen-rewrite") << "- already visited" << std::endl;
592 : : }
593 [ + + ][ + + ]: 15492500 : } while (!(tctx != nullptr ? visitctx->empty() : visit.empty()));
594 [ - + ][ - + ]: 460621 : Assert(visited.find(tinitialHash) != visited.end());
[ - - ]
595 [ - + ][ - + ]: 460621 : Assert(!visited.find(tinitialHash)->second.isNull());
[ - - ]
596 [ + - ]: 921242 : Trace("tconv-pf-gen-rewrite")
597 : 460621 : << "...finished, return " << visited[tinitialHash] << std::endl;
598 : : // return the conclusion of the overall proof
599 : 921242 : return t.eqNode(visited[tinitialHash]);
600 : : }
601 : :
602 : 4786690 : void TConvProofGenerator::doCache(Node curHash,
603 : : Node cur,
604 : : Node r,
605 : : LazyCDProof& pf)
606 : : {
607 [ + + ]: 4786690 : if (d_cpolicy != TConvCachePolicy::NEVER)
608 : : {
609 : 2348820 : Node eq = cur.eqNode(r);
610 : 2348820 : d_cache[curHash] = pf.getProofFor(eq);
611 : : }
612 : 4786690 : }
613 : :
614 : 12982800 : Node TConvProofGenerator::getRewriteStepInternal(Node t, bool isPre) const
615 : : {
616 [ + + ]: 12982800 : const NodeNodeMap& rm = isPre ? d_preRewriteMap : d_postRewriteMap;
617 : 12982800 : NodeNodeMap::const_iterator it = rm.find(t);
618 [ + + ]: 12982800 : if (it == rm.end())
619 : : {
620 : 11043400 : return Node::null();
621 : : }
622 : 1939400 : return (*it).second;
623 : : }
624 : 2163 : 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
|
