Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Abdalrhman Mohamed, Daniel Larraz
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 : : * Rewrite database proof reconstructor
14 : : */
15 : :
16 : : #include "rewriter/rewrite_db_proof_cons.h"
17 : :
18 : : #include "expr/aci_norm.h"
19 : : #include "expr/node_algorithm.h"
20 : : #include "options/proof_options.h"
21 : : #include "proof/proof_node_algorithm.h"
22 : : #include "rewriter/rewrite_db_term_process.h"
23 : : #include "smt/env.h"
24 : : #include "theory/arith/arith_poly_norm.h"
25 : : #include "theory/builtin/proof_checker.h"
26 : : #include "theory/rewriter.h"
27 : : #include "util/bitvector.h"
28 : :
29 : : using namespace cvc5::internal::kind;
30 : :
31 : : namespace cvc5::internal {
32 : : namespace rewriter {
33 : :
34 : : // fixed point limit set to 1000
35 : : size_t RewriteDbProofCons::s_fixedPointLimit = 1000;
36 : :
37 : 3568 : RewriteDbProofCons::RewriteDbProofCons(Env& env, RewriteDb* db)
38 : : : EnvObj(env),
39 : : d_notify(*this),
40 : : d_trrc(env),
41 : : d_rdnc(nodeManager()),
42 : : d_db(db),
43 : : d_eval(nullptr),
44 : : d_currRecLimit(0),
45 : : d_currStepLimit(0),
46 : : d_currFixedPointId(ProofRewriteRule::NONE),
47 : : d_statTotalInputs(
48 : 3568 : statisticsRegistry().registerInt("RewriteDbProofCons::totalInputs")),
49 : 3568 : d_statTotalAttempts(statisticsRegistry().registerInt(
50 : 3568 : "RewriteDbProofCons::totalAttempts")),
51 : 3568 : d_statTotalInputSuccess(statisticsRegistry().registerInt(
52 : 7136 : "RewriteDbProofCons::totalInputSuccess"))
53 : : {
54 : 3568 : NodeManager* nm = nodeManager();
55 : 3568 : d_true = nm->mkConst(true);
56 : 3568 : d_false = nm->mkConst(false);
57 : 3568 : }
58 : :
59 : 372712 : bool RewriteDbProofCons::prove(
60 : : CDProof* cdp,
61 : : const Node& a,
62 : : const Node& b,
63 : : int64_t recLimit,
64 : : int64_t stepLimit,
65 : : TheoryRewriteMode tmode)
66 : : {
67 : 372712 : d_tmode = tmode;
68 : : // clear the proof caches
69 : 372712 : d_pcache.clear();
70 : : // clear the evaluate cache
71 : 372712 : d_evalCache.clear();
72 : 745424 : Node eq = a.eqNode(b);
73 [ + - ]: 745424 : Trace("rpc") << "RewriteDbProofCons::prove: " << a << " == " << b
74 : 372712 : << std::endl;
75 : : // As a heuristic, always apply CONG if we are an equality between two
76 : : // binder terms with the same quantifier prefix or ALPHA_EQUIV if they have
77 : : // a different prefix whose types are the same.
78 [ + + ]: 372712 : if (a.isClosure())
79 : : {
80 : : // Note we apply this to fixed point, which should only occur at most 2
81 : : // times (first ALPHA_EQUIV, then CONG).
82 : 15966 : Node eqp;
83 : 332 : do
84 : : {
85 : 8315 : eqp = preprocessClosureEq(cdp, eq[0], eq[1]);
86 [ + + ]: 8315 : if (!eqp.isNull())
87 : : {
88 : 3307 : eq = eqp;
89 : 6614 : Trace("rpc") << "- closure-preprocess to " << eq[0] << " == " << eq[1]
90 : 3307 : << std::endl;
91 : : }
92 : : else
93 : : {
94 [ + - ]: 5008 : Trace("rpc") << "...does not closure-preprocess" << std::endl;
95 : : }
96 [ + + ][ + + ]: 8315 : } while (!eqp.isNull() && eqp[0].isClosure());
[ + + ][ + + ]
[ - - ]
97 : : }
98 : 372712 : ++d_statTotalInputs;
99 : 372712 : bool success = false;
100 : : // first try unconverted
101 : 372712 : Node eqi;
102 [ + + ]: 372712 : if (proveEqStratified(cdp, eq, eq, recLimit, stepLimit, tmode))
103 : : {
104 : 364695 : success = true;
105 : : }
106 : : else
107 : : {
108 : 8017 : eqi = d_rdnc.convert(eq);
109 : : // if converter didn't make a difference, don't try to prove again
110 [ + + ]: 8017 : if (eqi != eq)
111 : : {
112 [ + - ]: 5821 : Trace("rpc-debug") << "...now try converted" << std::endl;
113 [ + + ]: 5821 : if (proveEqStratified(cdp, eq, eqi, recLimit, stepLimit, tmode))
114 : : {
115 : 3704 : success = true;
116 : : }
117 : : }
118 : : else
119 : : {
120 [ + - ]: 4392 : Trace("rpc-debug") << "...do not try converted, did not change"
121 : 2196 : << std::endl;
122 : : }
123 : : }
124 [ + + ]: 372712 : if (!success)
125 : : {
126 : : // Now try the "post-prove" method as a last resort. We try the unconverted
127 : : // then the converted form of eq, if applicable.
128 [ + + ]: 4313 : if (d_trrc.postProve(cdp, eq[0], eq[1], tmode))
129 : : {
130 [ + - ]: 1045 : Trace("rpc") << "...success (post-prove basic)" << std::endl;
131 : 1045 : success = true;
132 : : }
133 : 3268 : else if (eqi != eq && d_trrc.postProve(cdp, eqi[0], eqi[1], tmode))
134 : : {
135 [ + - ]: 2 : Trace("rpc") << "...success (post-prove basic)" << std::endl;
136 : 2 : d_trrc.ensureProofForEncodeTransform(cdp, eq, eqi);
137 : 2 : success = true;
138 : : }
139 : : else
140 : : {
141 [ + - ]: 3266 : Trace("rpc") << "...fail" << std::endl;
142 : : }
143 : : }
144 : : else
145 : : {
146 [ + - ]: 368399 : Trace("rpc") << "...success" << std::endl;
147 : : }
148 : 745424 : return success;
149 : : }
150 : :
151 : 378533 : bool RewriteDbProofCons::proveEqStratified(
152 : : CDProof* cdp,
153 : : const Node& eq,
154 : : const Node& eqi,
155 : : int64_t recLimit,
156 : : int64_t stepLimit,
157 : : TheoryRewriteMode tmode)
158 : : {
159 : 378533 : bool success = false;
160 : : // first, try the basic utility
161 [ + + ]: 378533 : if (d_trrc.prove(cdp, eqi[0], eqi[1], tmode))
162 : : {
163 [ + - ]: 41899 : Trace("rpc") << "...success (basic)" << std::endl;
164 : 41899 : success = true;
165 : : }
166 : : else
167 : : {
168 : : // prove the equality
169 [ + + ]: 401882 : for (int64_t i = 0; i <= recLimit; i++)
170 : : {
171 [ + - ]: 391748 : Trace("rpc-debug") << "* Try recursion depth " << i << std::endl;
172 [ + + ]: 391748 : if (proveEq(cdp, eqi, i, stepLimit))
173 : : {
174 [ + - ]: 326500 : Trace("rpc") << "...success" << std::endl;
175 : 326500 : success = true;
176 : 326500 : break;
177 : : }
178 : : }
179 : : }
180 [ + + ]: 378533 : if (success)
181 : : {
182 : : // if eqi was converted, update the proof to account for this
183 [ + + ]: 368399 : if (eq != eqi)
184 : : {
185 : 3704 : d_trrc.ensureProofForEncodeTransform(cdp, eq, eqi);
186 : : }
187 : 368399 : return true;
188 : : }
189 : 10134 : return false;
190 : : }
191 : :
192 : 8315 : Node RewriteDbProofCons::preprocessClosureEq(CDProof* cdp,
193 : : const Node& a,
194 : : const Node& b)
195 : : {
196 : : // Ensure patterns are removed by calling d_rdnc postConvert (single step),
197 : : // which also ensures differences e.g. LAMBDA vs FUNCTION_ARRAY_CONST are
198 : : // resolved. We do not apply convert recursively here.
199 : 16630 : Node ai = d_rdnc.postConvert(a);
200 : 16630 : Node bi = d_rdnc.postConvert(b);
201 : : // The kinds must match.
202 [ + + ]: 8315 : if (ai.getKind() != bi.getKind())
203 : : {
204 : 3222 : return Node::null();
205 : : }
206 : : // only apply this to standard binders (those with 2 children)
207 [ + - ][ - + ]: 5093 : if (ai.getNumChildren() != 2 || bi.getNumChildren() != 2)
[ - + ]
208 : : {
209 : 0 : return Node::null();
210 : : }
211 : 5093 : theory::Rewriter* rr = d_env.getRewriter();
212 : : ProofRewriteRule prid =
213 : 5093 : rr->findRule(ai, bi, theory::TheoryRewriteCtx::PRE_DSL);
214 [ + + ]: 5093 : if (prid != ProofRewriteRule::NONE)
215 : : {
216 : : // a simple theory rewrite happens to solve it, do not continue
217 : 1728 : return Node::null();
218 : : }
219 : 6730 : Node eq;
220 : 6730 : Node eqConv = ai.eqNode(bi);
221 [ + + ]: 3365 : if (ai[0] == bi[0])
222 : : {
223 : 2975 : std::vector<Node> cargs;
224 : 2975 : ProofRule cr = expr::getCongRule(ai, cargs);
225 : : // remains to prove their bodies are equal
226 : 2975 : eq = ai[1].eqNode(bi[1]);
227 : 5950 : cdp->addStep(eqConv, cr, {eq}, cargs);
228 : : }
229 [ + + ]: 390 : else if (ai[0].getNumChildren() == bi[0].getNumChildren())
230 : : {
231 : 344 : size_t nchild = ai[0].getNumChildren();
232 : 344 : std::vector<Node> vars;
233 : 344 : std::vector<Node> subs;
234 : 344 : std::unordered_set<Node> uvars;
235 [ + + ]: 846 : for (size_t i = 0; i < nchild; i++)
236 : : {
237 : : // rare corner case: don't use if duplicate variables
238 [ - + ]: 540 : if (!uvars.insert(ai[0][i]).second)
239 : : {
240 : 0 : return Node::null();
241 : : }
242 [ + + ]: 540 : if (ai[0][i] != bi[0][i])
243 : : {
244 [ + + ]: 534 : if (ai[0][i].getType() != bi[0][i].getType())
245 : : {
246 : 38 : return Node::null();
247 : : }
248 : 496 : vars.emplace_back(ai[0][i]);
249 : 496 : subs.emplace_back(bi[0][i]);
250 : : }
251 : : }
252 [ - + ]: 306 : if (vars.empty())
253 : : {
254 : 0 : return Node::null();
255 : : }
256 : 306 : NodeManager* nm = nodeManager();
257 : 306 : std::vector<Node> aeArgs;
258 : 306 : aeArgs.push_back(ai);
259 : 306 : aeArgs.push_back(nm->mkNode(Kind::SEXPR, vars));
260 : 306 : aeArgs.push_back(nm->mkNode(Kind::SEXPR, subs));
261 : 306 : ProofChecker* pc = d_env.getProofNodeManager()->getChecker();
262 : 612 : Node res = pc->checkDebug(ProofRule::ALPHA_EQUIV, {}, aeArgs);
263 [ + - ]: 306 : if (!res.isNull())
264 : : {
265 [ - + ][ - + ]: 306 : Assert(res.getKind() == Kind::EQUAL);
[ - - ]
266 : 306 : cdp->addStep(res, ProofRule::ALPHA_EQUIV, {}, aeArgs);
267 : : // Remains to prove that the result of applying alpha equivalence to the
268 : : // left hand side is equal to the right hand side. This may be a
269 : : // reflexive equality when ALPHA_EQUIV alone suffices. Note that when this
270 : : // occurs eq is not a free assumption in cdp. Proof generation will
271 : : // easily succeed in proving eq by REFL, but this will not be used
272 : : // in the final proof.
273 : 306 : eq = res[1].eqNode(bi);
274 [ + + ]: 306 : if (res != eqConv)
275 : : {
276 [ + + ][ - - ]: 24 : cdp->addStep(eqConv, ProofRule::TRANS, {res, eq}, {});
277 : : }
278 : : }
279 : : else
280 : : {
281 : 0 : return Node::null();
282 : : }
283 : : }
284 [ + + ]: 46 : else if (ai[0].getNumChildren() > bi[0].getNumChildren())
285 : : {
286 : : // maybe unused variables on the left hand side
287 : 30 : Node aiu = rr->rewriteViaRule(ProofRewriteRule::QUANT_UNUSED_VARS, ai);
288 [ + + ]: 30 : if (!aiu.isNull())
289 : : {
290 [ - + ][ - + ]: 26 : Assert(aiu != ai);
[ - - ]
291 : 26 : Node eqq = ai.eqNode(aiu);
292 : 26 : cdp->addTheoryRewriteStep(eqq, ProofRewriteRule::QUANT_UNUSED_VARS);
293 : : // remains to prove the result of removing variables is equal to
294 : : // the right hand side.
295 : 26 : eq = aiu.eqNode(bi);
296 [ + + ][ - - ]: 78 : cdp->addStep(eqConv, ProofRule::TRANS, {eqq, eq}, {});
297 : : }
298 : : else
299 : : {
300 : 4 : return Node::null();
301 : : }
302 : : }
303 : : else
304 : : {
305 : 16 : return Node::null();
306 : : }
307 : 6614 : std::vector<Node> transEq;
308 [ + + ]: 3307 : if (ai != a)
309 : : {
310 : 832 : Node aeq = a.eqNode(ai);
311 : 832 : cdp->addStep(aeq, ProofRule::ENCODE_EQ_INTRO, {}, {a});
312 : 416 : transEq.push_back(aeq);
313 : : }
314 : 3307 : transEq.push_back(eqConv);
315 [ + + ]: 3307 : if (bi != b)
316 : : {
317 : 888 : Node beq = b.eqNode(bi);
318 : 888 : cdp->addStep(beq, ProofRule::ENCODE_EQ_INTRO, {}, {b});
319 : 888 : Node beqs = bi.eqNode(b);
320 : 888 : cdp->addStep(beqs, ProofRule::SYMM, {beq}, {});
321 : 444 : transEq.push_back(beqs);
322 : : }
323 [ + + ]: 3307 : if (transEq.size() > 1)
324 : : {
325 : 446 : Node eqo = a.eqNode(b);
326 : 446 : cdp->addStep(eqo, ProofRule::TRANS, transEq, {});
327 : : }
328 : 3307 : return eq;
329 : : }
330 : :
331 : 391748 : bool RewriteDbProofCons::proveEq(CDProof* cdp,
332 : : const Node& eqi,
333 : : int64_t recLimit,
334 : : int64_t stepLimit)
335 : : {
336 : : // add one to recursion limit, since it is decremented whenever we
337 : : // initiate the getMatches routine.
338 : 391748 : d_currRecLimit = recLimit + 1;
339 : 391748 : d_currStepLimit = stepLimit;
340 : : RewriteProofStatus id;
341 [ + + ]: 391748 : if (!proveInternalBase(eqi, id))
342 : : {
343 [ + - ]: 389994 : Trace("rpc-debug") << "- prove internal" << std::endl;
344 : : // Otherwise, we call the main prove internal method, which recurisvely
345 : : // tries to find a matched conclusion whose conditions can be proven
346 : 389994 : id = proveInternal(eqi);
347 [ + - ]: 389994 : Trace("rpc-debug") << "- finished prove internal" << std::endl;
348 : : }
349 : : // if a proof was provided, fill it in
350 [ + + ][ + - ]: 391748 : if (id != RewriteProofStatus::FAIL && cdp != nullptr)
351 : : {
352 : 326500 : ++d_statTotalInputSuccess;
353 [ + - ]: 326500 : Trace("rpc-debug") << "- ensure proof" << std::endl;
354 : 326500 : ensureProofInternal(cdp, eqi);
355 : 326500 : AlwaysAssert(cdp->hasStep(eqi)) << eqi;
356 [ + - ]: 326500 : Trace("rpc-debug") << "- finish ensure proof" << std::endl;
357 : 326500 : return true;
358 : : }
359 : 65248 : return false;
360 : : }
361 : :
362 : 1964630 : RewriteProofStatus RewriteDbProofCons::proveInternal(const Node& eqi)
363 : : {
364 : 1964630 : d_currProving.insert(eqi);
365 : 1964630 : ++d_statTotalAttempts;
366 : : // eqi should not hold trivially and should not be cached
367 [ + - ]: 1964630 : Trace("rpc-debug2") << "proveInternal " << eqi << std::endl;
368 : : // Otherwise, call the get matches routine. This will call notifyMatch below
369 : : // for each matching rewrite rule conclusion in the database
370 : : // decrease the recursion depth
371 [ - + ][ - + ]: 1964630 : Assert(eqi.getKind() == Kind::EQUAL);
[ - - ]
372 : : // first, try congruence if possible, which does not count towards recursion
373 : : // limit.
374 : 1964630 : RewriteProofStatus retId = proveInternalViaStrategy(eqi);
375 : 1964630 : d_currProving.erase(eqi);
376 : 1964630 : return retId;
377 : : }
378 : :
379 : 1964630 : RewriteProofStatus RewriteDbProofCons::proveInternalViaStrategy(const Node& eqi)
380 : : {
381 [ - + ][ - + ]: 1964630 : Assert(eqi.getKind() == Kind::EQUAL);
[ - - ]
382 [ + + ]: 1964630 : if (proveWithRule(RewriteProofStatus::CONG, eqi, {}, {}, false, false, true))
383 : : {
384 [ + - ]: 15792 : Trace("rpc-debug2") << "...proved via congruence" << std::endl;
385 : 15792 : return RewriteProofStatus::CONG;
386 : : }
387 [ + + ]: 1948840 : if (proveWithRule(
388 : : RewriteProofStatus::CONG_EVAL, eqi, {}, {}, false, false, true))
389 : : {
390 [ + - ]: 1115 : Trace("rpc-debug2") << "...proved via congruence + evaluation" << std::endl;
391 : 1115 : return RewriteProofStatus::CONG_EVAL;
392 : : }
393 : : // maybe by absorb?
394 [ + + ]: 1947720 : if (proveWithRule(
395 : : RewriteProofStatus::ABSORB, eqi, {}, {}, false, false, true))
396 : : {
397 : 6818 : return RewriteProofStatus::ABSORB;
398 : : }
399 : : // standard normalization
400 [ + + ]: 1940900 : if (proveWithRule(
401 : : RewriteProofStatus::ACI_NORM, eqi, {}, {}, false, false, true))
402 : : {
403 : 42103 : return RewriteProofStatus::ACI_NORM;
404 : : }
405 : : // if arithmetic, maybe holds by arithmetic normalization?
406 [ + + ]: 1898800 : if (proveWithRule(
407 : : RewriteProofStatus::ARITH_POLY_NORM, eqi, {}, {}, false, false, true))
408 : : {
409 : 125966 : return RewriteProofStatus::ARITH_POLY_NORM;
410 : : }
411 : : // Maybe holds via a THEORY_REWRITE that has been marked with
412 : : // TheoryRewriteCtx::DSL_SUBCALL.
413 [ + + ]: 1772830 : if (d_tmode==TheoryRewriteMode::STANDARD)
414 : : {
415 [ + + ]: 1685310 : if (proveWithRule(
416 : : RewriteProofStatus::THEORY_REWRITE, eqi, {}, {}, false, false, true))
417 : : {
418 : 3321 : return RewriteProofStatus::THEORY_REWRITE;
419 : : }
420 : : }
421 [ + - ]: 1769510 : Trace("rpc-debug2") << "...not proved via builtin tactic" << std::endl;
422 : 3539020 : Node prevTarget = d_target;
423 : 1769510 : d_target = eqi;
424 : 1769510 : d_db->getMatches(eqi[0], &d_notify);
425 : 1769510 : d_target = prevTarget;
426 : : // check if we determined the proof in the above call, which is the case
427 : : // if we succeeded, or we are already marked as a failure at a lower depth.
428 : 1769510 : std::unordered_map<Node, ProvenInfo>::iterator it = d_pcache.find(eqi);
429 [ + + ]: 1769510 : if (it != d_pcache.end())
430 : : {
431 : 1174420 : if (it->second.d_id != RewriteProofStatus::FAIL
432 [ + + ][ + + ]: 1174420 : || d_currRecLimit <= it->second.d_failMaxDepth)
[ + + ]
433 : : {
434 : 450567 : return it->second.d_id;
435 : : }
436 : : }
437 : : // if target is (= (= t1 t2) true), maybe try showing (= t1 t2); otherwise
438 : : // try showing (= target true)
439 : 1318940 : RewriteProofStatus eqTrueId = eqi[1] == d_true
440 [ + + ]: 1318940 : ? RewriteProofStatus::TRUE_INTRO
441 : 1318940 : : RewriteProofStatus::TRUE_ELIM;
442 [ + + ]: 1318940 : if (proveWithRule(eqTrueId, eqi, {}, {}, false, false, true))
443 : : {
444 [ + - ]: 1640 : Trace("rpc-debug2") << "...proved via " << eqTrueId << std::endl;
445 : 1640 : return eqTrueId;
446 : : }
447 : 2634610 : Trace("rpc-fail") << "FAIL: cannot prove " << eqi[0] << " == " << eqi[1]
448 : 1317300 : << std::endl;
449 : : // store failure, and its maximum depth
450 : 1317300 : ProvenInfo& pi = d_pcache[eqi];
451 : 1317300 : pi.d_id = RewriteProofStatus::FAIL;
452 : 1317300 : pi.d_failMaxDepth = d_currRecLimit;
453 : 1317300 : return RewriteProofStatus::FAIL;
454 : : }
455 : :
456 : 2777290 : bool RewriteDbProofCons::notifyMatch(const Node& s,
457 : : const Node& n,
458 : : std::vector<Node>& vars,
459 : : std::vector<Node>& subs)
460 : : {
461 : : // if we reach our step limit, do not continue trying
462 [ + - ]: 5554570 : Trace("rpc-debug2") << "[steps remaining: " << d_currStepLimit << "]"
463 : 2777290 : << std::endl;
464 [ + - ]: 5554570 : Trace("rpc-debug2") << "notifyMatch: " << s << " from " << n << " via "
465 : 2777290 : << vars << " -> " << subs << std::endl;
466 [ - + ][ - + ]: 2777290 : Assert(d_target.getKind() == Kind::EQUAL);
[ - - ]
467 [ - + ][ - + ]: 2777290 : Assert(s.getType().isComparableTo(n.getType()));
[ - - ]
468 [ - + ][ - + ]: 2777290 : Assert(vars.size() == subs.size());
[ - - ]
469 [ + + ]: 2777290 : if (d_currFixedPointId != ProofRewriteRule::NONE)
470 : : {
471 [ + - ]: 374052 : Trace("rpc-debug2") << "Part of fixed point for rule " << d_currFixedPointId
472 : 187026 : << std::endl;
473 : 187026 : const RewriteProofRule& rpr = d_db->getRule(d_currFixedPointId);
474 : : // get the conclusion
475 : 374052 : Node target = rpr.getConclusion(true);
476 : : // apply substitution, which may notice vars may be out of order wrt rule
477 : : // var list
478 : 187026 : target = expr::narySubstitute(target, vars, subs);
479 : : // it may be impossible to construct the conclusion due to null terminators
480 : : // for approximate types, return false in this case
481 [ + + ]: 187026 : if (target.isNull())
482 : : {
483 : : // note that we return false here, indicating that we don't want any
484 : : // more matches, since we have failed for the current fixed point rule.
485 : 18 : return false;
486 : : }
487 : : // We now prove with the given rule. this should only fail if there are
488 : : // conditions on the rule which fail. Notice we never allow recursion here.
489 : : // We also don't permit inflection matching (which regardless should not
490 : : // apply).
491 [ + - ]: 187008 : if (proveWithRule(RewriteProofStatus::DSL,
492 : : target,
493 : : vars,
494 : : subs,
495 : : false,
496 : : false,
497 : : false,
498 : : d_currFixedPointId))
499 : : {
500 : : // successfully proved, store in temporary variable
501 : 187008 : d_currFixedPointConc = target;
502 : 187008 : d_currFixedPointSubs = subs;
503 : : }
504 : : // regardless, no further matches, due to semantics of fixed point which
505 : : // limits to first match
506 : 187008 : return false;
507 : : }
508 [ - + ][ - + ]: 2590260 : Assert(d_target[0] == s);
[ - - ]
509 : 2590260 : bool recurse = d_currRecLimit > 0;
510 : : // get the rule identifiers for the conclusion
511 : 2590260 : const std::vector<ProofRewriteRule>& ids = d_db->getRuleIdsForHead(n);
512 [ - + ][ - + ]: 2590260 : Assert(!ids.empty());
[ - - ]
513 : : // check each rule instance, succeed if one proves
514 [ + + ]: 5384530 : for (ProofRewriteRule id : ids)
515 : : {
516 : : // try to prove target with the current rule, using inflection matching
517 : : // and fixed point semantics
518 [ + + ]: 2994750 : if (proveWithRule(RewriteProofStatus::DSL,
519 : 2994750 : d_target,
520 : : vars,
521 : : subs,
522 : : true,
523 : : true,
524 : : recurse,
525 : : id))
526 : : {
527 : : // if successful, we do not want to be notified of further matches
528 : : // and return false here.
529 : 200485 : return false;
530 : : }
531 : : // notice that we do not cache a failure here since we only know that the
532 : : // current rule was not able to prove the current target
533 : : }
534 : : // want to keep getting notify calls
535 : 2389780 : return true;
536 : : }
537 : :
538 : 15886900 : bool RewriteDbProofCons::proveWithRule(RewriteProofStatus id,
539 : : const Node& target,
540 : : const std::vector<Node>& vars,
541 : : const std::vector<Node>& subs,
542 : : bool doInflectMatch,
543 : : bool doFixedPoint,
544 : : bool doRecurse,
545 : : ProofRewriteRule r)
546 : : {
547 [ + - ][ + - ]: 15886900 : Assert(!target.isNull() && target.getKind() == Kind::EQUAL)
[ - - ]
548 [ - + ][ - + ]: 15886900 : << "Unknown " << target << " with rule " << id << " " << r << std::endl;
[ - - ]
549 [ + - ]: 31773800 : Trace("rpc-debug2") << "Check rule "
550 [ - - ]: 15886900 : << (id == RewriteProofStatus::DSL ? toString(r)
551 : 0 : : toString(id))
552 : 15886900 : << std::endl;
553 : 31773800 : std::vector<Node> vcs;
554 : : // the implied substitution if we have a rule with free variables on RHS
555 : 31773800 : std::vector<Node> impliedVs;
556 : 31773800 : std::vector<Node> impliedSs;
557 : 31773800 : Node transEq;
558 : 31773800 : ProvenInfo pic;
559 : : // whether we require decrementing the recursion limit to apply this rule
560 : 15886900 : bool decRecLimit = true;
561 [ + + ]: 15886900 : if (id == RewriteProofStatus::CONG)
562 : : {
563 : 1964630 : size_t nchild = target[0].getNumChildren();
564 [ + + ][ + + ]: 3864440 : if (nchild == 0 || nchild != target[1].getNumChildren()
[ - - ]
565 : 3864440 : || target[0].getOperator() != target[1].getOperator())
566 : : {
567 : : // cannot show congruence between different operators
568 : 1740540 : return false;
569 : : }
570 : 224085 : pic.d_id = id;
571 [ + + ]: 592962 : for (size_t i = 0; i < nchild; i++)
572 : : {
573 : : // for closures, their first argument (the bound variable list) must be
574 : : // equivalent, and should not be given as a child proof.
575 [ + + ][ + + ]: 410598 : if (i == 0 && target[0].isClosure())
[ + + ][ + + ]
[ - - ]
576 : : {
577 [ + + ]: 1092 : if (target[0][0] != target[1][0])
578 : : {
579 : 41721 : return false;
580 : : }
581 : 298 : continue;
582 : : }
583 [ + + ]: 409506 : if (!target[0][i].getType().isComparableTo(target[1][i].getType()))
584 : : {
585 : : // type error on children (required for certain polymorphic operators)
586 : 40927 : return false;
587 : : }
588 : 1105740 : Node eq = target[0][i].eqNode(target[1][i]);
589 : 368579 : vcs.push_back(eq);
590 : 368579 : pic.d_vars.push_back(eq);
591 : : }
592 : : // congruence (f(a) = f(b)) <= (a = b) is treated as a "propagation", i.e.
593 : : // it does not require decrementing the recursion limit, as a heuristic.
594 : 182364 : decRecLimit = false;
595 : : }
596 [ + + ]: 13922300 : else if (id == RewriteProofStatus::CONG_EVAL)
597 : : {
598 : 1948840 : size_t nchild = target[0].getNumChildren();
599 : : // evaluate the right hand side
600 : 1948840 : Node r2 = doEvaluate(target[1]);
601 [ + + ][ + + ]: 1948840 : if (nchild == 0 || r2.isNull())
[ + + ]
602 : : {
603 : 725662 : return false;
604 : : }
605 : 1223170 : Node rr1 = rewriteConcrete(target[0]);
606 [ + + ]: 1223170 : if (rr1 != r2)
607 : : {
608 : 1018140 : return false;
609 : : }
610 : 205036 : pic.d_id = id;
611 : : // if all children rewrite to a constant, try proving equalities
612 : : // on those children
613 : 205036 : std::vector<Node> rchildren;
614 [ + + ]: 346650 : for (size_t i = 0; i < nchild; i++)
615 : : {
616 : 549970 : Node rr = rewriteConcrete(target[0][i]);
617 [ + + ]: 274985 : if (!rr.isConst())
618 : : {
619 : 133371 : return false;
620 : : }
621 : 424842 : Node eq = target[0][i].eqNode(rr);
622 : 141614 : vcs.push_back(eq);
623 : 141614 : pic.d_vars.push_back(eq);
624 : 141614 : rchildren.push_back(rr);
625 : : }
626 : : // must check if it truly evaluates. This can fail if the evaluator does
627 : : // not support constant folding for the operator in question, which is the
628 : : // case e.g. for operators that return regular expressions, datatypes,
629 : : // sequences, sets.
630 [ + + ]: 71665 : if (target[0].getMetaKind() == metakind::PARAMETERIZED)
631 : : {
632 : 1696 : rchildren.insert(rchildren.begin(), target[0].getOperator());
633 : : }
634 : 71665 : NodeManager* nm = nodeManager();
635 : 71665 : Node tappc = nm->mkNode(target[0].getKind(), rchildren);
636 [ + + ]: 71665 : if (doEvaluate(tappc) != r2)
637 : : {
638 : 5098 : return false;
639 : : }
640 : : }
641 [ + + ]: 11973400 : else if (id == RewriteProofStatus::TRUE_ELIM)
642 : : {
643 [ - + ]: 528620 : if (target[1] == d_true)
644 : : {
645 : : // don't do for equals true, avoids unbounded recursion
646 : 0 : return false;
647 : : }
648 : 528620 : pic.d_id = id;
649 : 1057240 : Node eq = target.eqNode(d_true);
650 : 528620 : vcs.push_back(eq);
651 : 528620 : pic.d_vars.push_back(eq);
652 : : }
653 [ + + ]: 11444800 : else if (id == RewriteProofStatus::TRUE_INTRO)
654 : : {
655 : 790325 : if (target[1] != d_true || target[0].getKind() != Kind::EQUAL)
656 : : {
657 : : // only works for (= (= t1 t2) true)
658 : 407757 : return false;
659 : : }
660 : 382568 : pic.d_id = id;
661 : 382568 : Node eq = target[0];
662 : 382568 : vcs.push_back(eq);
663 : 382568 : pic.d_vars.push_back(eq);
664 : : // also treated as a "propagation" heuristic
665 : 382568 : decRecLimit = false;
666 : : }
667 [ + + ]: 10654500 : else if (id == RewriteProofStatus::ABSORB)
668 : : {
669 [ + + ]: 1947720 : if (!target[1].isConst())
670 : : {
671 : 1940900 : return false;
672 : : }
673 : : Node zero = expr::getZeroElement(
674 : 2494920 : nodeManager(), target[0].getKind(), target[0].getType());
675 [ + + ]: 1247460 : if (zero != target[1])
676 : : {
677 : 1197580 : return false;
678 : : }
679 [ + + ]: 49885 : if (!expr::isAbsorb(target[0], target[1]))
680 : : {
681 : 43067 : return false;
682 : : }
683 : 6818 : pic.d_id = id;
684 : : }
685 [ + + ]: 8706770 : else if (id == RewriteProofStatus::ACI_NORM)
686 : : {
687 [ + + ]: 1940900 : if (!expr::isACINorm(target[0], target[1]))
688 : : {
689 : 1898800 : return false;
690 : : }
691 : 42103 : pic.d_id = id;
692 : : }
693 [ + + ]: 6765870 : else if (id == RewriteProofStatus::ARITH_POLY_NORM)
694 : : {
695 [ + + ]: 1898800 : if (target[0].getType().isBoolean())
696 : : {
697 : 1603130 : Rational rx, ry;
698 [ + + ]: 1603130 : if (!theory::arith::PolyNorm::isArithPolyNormRel(
699 : : target[0], target[1], rx, ry))
700 : : {
701 : 1535320 : return false;
702 : : }
703 : : Node premise = theory::arith::PolyNorm::getArithPolyNormRelPremise(
704 : 203406 : target[0], target[1], rx, ry);
705 : 135604 : ProvenInfo ppremise;
706 : 67802 : ppremise.d_id = id;
707 : 67802 : d_pcache[premise] = ppremise;
708 : 67802 : pic.d_id = id;
709 : 67802 : pic.d_vars.push_back(premise);
710 : : }
711 : : else
712 : : {
713 [ + + ]: 295673 : if (!theory::arith::PolyNorm::isArithPolyNorm(target[0], target[1]))
714 : : {
715 : 237509 : return false;
716 : : }
717 : 58164 : pic.d_id = id;
718 : : }
719 : : }
720 [ + + ]: 4867070 : else if (id == RewriteProofStatus::THEORY_REWRITE)
721 : : {
722 : 1685310 : ProofRewriteRule prid = d_env.getRewriter()->findRule(
723 : : target[0], target[1], theory::TheoryRewriteCtx::DSL_SUBCALL);
724 [ + + ]: 1685310 : if (prid == ProofRewriteRule::NONE)
725 : : {
726 : 1681990 : return false;
727 : : }
728 : 3321 : pic.d_id = id;
729 : 3321 : pic.d_dslId = prid;
730 : : }
731 : : else
732 : : {
733 [ - + ][ - + ]: 3181760 : Assert(id == RewriteProofStatus::DSL);
[ - - ]
734 : 3181760 : const RewriteProofRule& rpr = d_db->getRule(r);
735 : : // does it conclusion match what we are trying to show?
736 : 3181760 : Node conc = rpr.getConclusion();
737 [ + - ][ + - ]: 6363520 : Assert(conc.getKind() == Kind::EQUAL && target.getKind() == Kind::EQUAL);
[ - + ][ - - ]
738 : : // get rule conclusion, which may incorporate fixed point semantics when
739 : : // doFixedPoint is true. This stores the rule for the conclusion in pic,
740 : : // which is either r or RewriteProofStatus::TRANS.
741 : 3181760 : Node stgt = getRuleConclusion(rpr, vars, subs, pic, doFixedPoint);
742 [ + - ][ - + ]: 3181760 : Trace("rpc-debug2") << " RHS: " << conc[1] << std::endl;
[ - - ]
743 [ + - ]: 3181760 : Trace("rpc-debug2") << "Substituted RHS: " << stgt << std::endl;
744 [ + - ][ - + ]: 3181760 : Trace("rpc-debug2") << " Target RHS: " << target[1] << std::endl;
[ - - ]
745 : : // check if conclusion is null
746 [ + + ]: 3181760 : if (stgt.isNull())
747 : : {
748 : : // this is likely due to not finding a null terminator for a gradual
749 : : // type term
750 [ + - ]: 18 : Trace("rpc-debug2") << "...fail (no construct conclusion)" << std::endl;
751 : 18 : return false;
752 : : }
753 [ + + ]: 3181740 : if (expr::hasBoundVar(stgt))
754 : : {
755 : 192183 : rpr.getConditionalDefinitions(vars, subs, impliedVs, impliedSs);
756 [ + - ]: 384366 : Trace("rpc-debug2") << " Implied definitions: " << impliedVs << " -> "
757 : 192183 : << impliedSs << std::endl;
758 [ + + ]: 192183 : if (!impliedVs.empty())
759 : : {
760 : : // evaluate them
761 [ + + ]: 109047 : for (Node& s : impliedSs)
762 : : {
763 : 64451 : s = evaluate(s, {}, {});
764 : : }
765 : 44596 : stgt = expr::narySubstitute(stgt, impliedVs, impliedSs);
766 [ + - ]: 89192 : Trace("rpc-debug2") << " Implied definitions (post-eval): " << impliedVs
767 : 44596 : << " -> " << impliedSs << std::endl;
768 [ + - ]: 89192 : Trace("rpc-debug2")
769 : 44596 : << "Substituted RHS (post-eval): " << stgt << std::endl;
770 : : }
771 : : }
772 : : // inflection substitution, used if conclusion does not exactly match
773 : 3181740 : std::unordered_map<Node, std::pair<Node, Node>> isubs;
774 [ + + ]: 3181740 : if (stgt != target[1])
775 : : {
776 [ - + ]: 2542170 : if (!doInflectMatch)
777 : : {
778 [ - - ]: 0 : Trace("rpc-debug2") << "...fail (no inflection)" << std::endl;
779 : 0 : return false;
780 : : }
781 : : // The conclusion term may actually change type. Note that we must rewrite
782 : : // the terms, since they may involve operators with abstract type that
783 : : // evaluate to terms with concrete types.
784 [ + + ]: 7626510 : if (!rewriteConcrete(stgt).getType().isComparableTo(
785 : 5084340 : rewriteConcrete(target[1]).getType()))
786 : : {
787 [ + - ]: 754 : Trace("rpc-debug2") << "...fail (types)" << std::endl;
788 : 754 : return false;
789 : : }
790 : : // the missing transitivity link is a subgoal to prove
791 : 2541420 : transEq = stgt.eqNode(target[1]);
792 [ + - ]: 2541420 : Trace("rpc-debug2") << " Try transitive with " << transEq << std::endl;
793 : : }
794 : : // do its conditions hold?
795 : : // Get the conditions, substituted { vars -> subs } and with side conditions
796 : : // evaluated.
797 [ + + ]: 3180990 : if (!impliedVs.empty())
798 : : {
799 : 44596 : std::vector<Node> vsall = vars;
800 : 44596 : std::vector<Node> subsall = subs;
801 : 44596 : vsall.insert(vsall.end(), impliedVs.begin(), impliedVs.end());
802 : 44596 : subsall.insert(subsall.end(), impliedSs.begin(), impliedSs.end());
803 [ - + ]: 44596 : if (!rpr.getObligations(vsall, subsall, vcs))
804 : : {
805 : : // cannot get conditions, likely due to failed side condition
806 [ - - ]: 0 : Trace("rpc-debug2") << "...fail (obligations)" << std::endl;
807 : 0 : return false;
808 : : }
809 : : }
810 [ - + ]: 3136390 : else if (!rpr.getObligations(vars, subs, vcs))
811 : : {
812 : : // cannot get conditions, likely due to failed side condition
813 [ - - ]: 0 : Trace("rpc-debug2") << "...fail (obligations)" << std::endl;
814 : 0 : return false;
815 : : }
816 : : // Prove transitive equality last. We choose this order since the
817 : : // transitive equality is expected to be the hardest to prove. Also, the
818 : : // conditions may guard instances where the RHS is not well typed (e.g.
819 : : // bv-eq-extract-elim1,2,3).
820 [ + + ]: 3180990 : if (!transEq.isNull())
821 : : {
822 : 2541420 : vcs.push_back(transEq);
823 : : }
824 : : }
825 : : // First, check which premises are non-trivial, and if there is a trivial
826 : : // failure. Those that are non-trivial are added to condToProve.
827 : 9038630 : std::vector<Node> condToProve;
828 [ + + ]: 6686810 : for (const Node& cond : vcs)
829 : : {
830 [ - + ][ - + ]: 4599850 : Assert(cond.getKind() == Kind::EQUAL);
[ - - ]
831 : : // substitute to get the condition-to-prove
832 : : RewriteProofStatus cid;
833 : : // check whether condition is already known to hold or not hold
834 [ + + ]: 4599850 : if (proveInternalBase(cond, cid))
835 : : {
836 [ + + ]: 1494200 : if (cid == RewriteProofStatus::FAIL)
837 : : {
838 : : // does not hold, we fail
839 [ + - ]: 2538220 : Trace("rpc-debug2") << "...fail (simple condition failure for " << cond
840 : 1269110 : << ")" << std::endl;
841 : 2432350 : return false;
842 : : }
843 : : // already holds, continue
844 : 225093 : continue;
845 : : }
846 [ + + ][ + + ]: 3105650 : if (!doRecurse || (decRecLimit && d_currRecLimit == 0))
[ + + ]
847 : : {
848 : : // we can't apply recursion, return false
849 [ + - ]: 1163250 : Trace("rpc-debug2") << "...fail (recursion limit)" << std::endl;
850 : 1163250 : return false;
851 : : }
852 : : // save, to check below
853 : 1942400 : condToProve.push_back(cond);
854 : : }
855 : : // if we have any sub-conditions to prove, we require decrementing the
856 : : // recursion limit
857 [ + + ]: 2086960 : if (!condToProve.empty())
858 : : {
859 : : // we could only add condToProve if d_currRecLimit>0 above.
860 [ + + ][ - + ]: 1556760 : Assert(!decRecLimit || d_currRecLimit > 0);
[ - + ][ - - ]
861 [ + + ]: 1556760 : if (decRecLimit)
862 : : {
863 : 1369200 : d_currRecLimit--;
864 [ + + ]: 1369200 : if (d_currStepLimit == 0)
865 : : {
866 : 434 : return false;
867 : : }
868 : 1368770 : d_currStepLimit--;
869 : : }
870 [ + - ]: 3112660 : Trace("rpc-debug") << "Recurse rule "
871 [ - - ]: 1556330 : << (id == RewriteProofStatus::DSL ? toString(r)
872 : 0 : : toString(id))
873 : 1556330 : << std::endl;
874 : 1556330 : bool recSuccess = true;
875 : : // if no trivial failures, go back and try to recursively prove
876 [ + + ]: 1628680 : for (const Node& cond : condToProve)
877 : : {
878 [ + - ]: 1574630 : Trace("rpc-infer-sc") << "Check condition: " << cond << std::endl;
879 : : // recursively check if the condition holds
880 : 1574630 : RewriteProofStatus cid = proveInternal(cond);
881 [ + + ]: 1574630 : if (cid == RewriteProofStatus::FAIL)
882 : : {
883 : : // print reason for failure
884 [ + - ]: 3004550 : Trace("rpc-infer-debug")
885 : 1502280 : << "required: " << cond << " for " << id << std::endl;
886 : 1502280 : recSuccess = false;
887 : 1502280 : break;
888 : : }
889 : : }
890 [ + + ]: 1556330 : if (decRecLimit)
891 : : {
892 : 1368770 : d_currRecLimit++;
893 : : }
894 [ + + ]: 1556330 : if (!recSuccess)
895 : : {
896 : 1502280 : return false;
897 : : }
898 : : }
899 : : // successfully found instance of rule
900 [ - + ]: 584248 : if (TraceIsOn("rpc-infer"))
901 : : {
902 [ - - ]: 0 : Trace("rpc-infer") << "INFER " << target << " by " << id
903 [ - - ]: 0 : << (transEq.isNull() ? "" : " + TRANS") << std::endl;
904 : : }
905 : : // cache the success
906 : 584248 : ProvenInfo* pi = &d_pcache[target];
907 [ + + ]: 584248 : if (!transEq.isNull())
908 : : {
909 [ + - ]: 39135 : Trace("rpc-debug2") << "..." << target << " proved by TRANS" << std::endl;
910 : 78270 : Node transEqStart = target[0].eqNode(transEq[0]);
911 : : // proves both
912 : 39135 : pi->d_id = RewriteProofStatus::TRANS;
913 : 39135 : pi->d_vars.clear();
914 : 39135 : pi->d_vars.push_back(transEqStart);
915 : 39135 : pi->d_vars.push_back(transEq);
916 [ + - ]: 78270 : Trace("rpc-debug2") << "...original equality was " << transEqStart
917 : 39135 : << std::endl;
918 : : // we also prove the original
919 : 39135 : pi = &d_pcache[transEqStart];
920 : : }
921 : 584248 : pi->d_id = pic.d_id;
922 : 584248 : pi->d_dslId = pic.d_dslId;
923 [ + + ]: 584248 : if (pic.isInternalRule())
924 : : {
925 : 194744 : pi->d_vars = pic.d_vars;
926 : : }
927 : : else
928 : : {
929 : 389504 : pi->d_vars = vars;
930 : 389504 : pi->d_subs = subs;
931 [ + + ]: 389504 : if (!impliedVs.empty())
932 : : {
933 : 1128 : pi->d_vars.insert(pi->d_vars.end(), impliedVs.begin(), impliedVs.end());
934 : 1128 : pi->d_subs.insert(pi->d_subs.end(), impliedSs.begin(), impliedSs.end());
935 : : }
936 : : }
937 [ + - ]: 1168500 : Trace("rpc-debug2") << "...target proved by " << d_pcache[target].d_id
938 : 584248 : << std::endl;
939 : : // success
940 : 584248 : return true;
941 : : }
942 : :
943 : 4991600 : bool RewriteDbProofCons::proveInternalBase(const Node& eqi,
944 : : RewriteProofStatus& idb)
945 : : {
946 [ + - ]: 4991600 : Trace("rpc-debug2") << "Prove internal base: " << eqi << "?" << std::endl;
947 [ - + ][ - + ]: 4991600 : Assert(eqi.getKind() == Kind::EQUAL);
[ - - ]
948 : : // if we are currently trying to prove this, fail
949 [ + + ]: 4991600 : if (d_currProving.find(eqi) != d_currProving.end())
950 : : {
951 [ + - ]: 594467 : Trace("rpc-debug2") << "...fail (already proving)" << std::endl;
952 : 594467 : idb = RewriteProofStatus::FAIL;
953 : 594467 : return true;
954 : : }
955 : : // already cached?
956 : 4397130 : std::unordered_map<Node, ProvenInfo>::iterator it = d_pcache.find(eqi);
957 [ + + ]: 4397130 : if (it != d_pcache.end())
958 : : {
959 [ + + ]: 1731400 : if (it->second.d_id != RewriteProofStatus::FAIL)
960 : : {
961 : : // proof exists, return
962 : 178224 : idb = it->second.d_id;
963 [ + - ]: 178224 : Trace("rpc-debug2") << "...success, already exists" << std::endl;
964 : 178224 : return true;
965 : : }
966 [ + + ]: 1553170 : if (d_currRecLimit <= it->second.d_failMaxDepth)
967 : : {
968 : 408646 : idb = it->second.d_id;
969 [ + - ]: 408646 : Trace("rpc-debug2") << "...fail (at higher depth)" << std::endl;
970 : 408646 : return true;
971 : : }
972 [ + - ]: 1144530 : Trace("rpc-debug2") << "...unknown (already fail)" << std::endl;
973 : : // Will not succeed below, since we know we've already tried. Hence, we
974 : : // are in a situation where we have yet to succeed to prove eqi for some
975 : : // depth, but we are currently trying at a higher maximum depth.
976 : 1144530 : return false;
977 : : }
978 : : // reflexivity, applied potentially to non-Booleans
979 [ + + ]: 2665740 : if (eqi[0] == eqi[1])
980 : : {
981 : 15621 : ProvenInfo& pi = d_pcache[eqi];
982 : 15621 : idb = RewriteProofStatus::REFL;
983 : 15621 : pi.d_id = idb;
984 [ + - ]: 15621 : Trace("rpc-debug2") << "...success, refl" << std::endl;
985 : 15621 : return true;
986 : : }
987 : : // non-well-typed equalities cannot be proven
988 : : // also, variables cannot be rewritten
989 : 2650110 : if (eqi.getTypeOrNull().isNull() || eqi[0].isVar())
990 : : {
991 [ + - ]: 105568 : Trace("rpc-debug2") << "...fail ("
992 [ - - ][ - + ]: 52784 : << (eqi[0].isVar() ? "variable" : "ill-typed") << ")"
[ - - ]
993 : 52784 : << std::endl;
994 : 52784 : ProvenInfo& pi = d_pcache[eqi];
995 : 52784 : idb = RewriteProofStatus::FAIL;
996 : 52784 : pi.d_failMaxDepth = 0;
997 : 52784 : pi.d_id = idb;
998 : 52784 : return true;
999 : : }
1000 : : // evaluate the two sides of the equality, without help of the rewriter
1001 [ + + ][ + + ]: 15584000 : Node ev[2];
[ - - ]
1002 : 2597330 : bool evalSuccess = true;
1003 [ + + ]: 2883720 : for (size_t i = 0; i < 2; i++)
1004 : : {
1005 : 2772540 : ev[i] = doEvaluate(eqi[i]);
1006 [ + - ][ - + ]: 5545080 : Trace("rpc-debug2") << "...evaluate " << eqi[i] << " to " << ev[i]
[ - - ]
1007 : 2772540 : << std::endl;
1008 [ + + ]: 2772540 : if (ev[i].isNull())
1009 : : {
1010 : : // does not evaluate
1011 : : // If it rewrites to false, then it is obviously infeasible. Notice that
1012 : : // rewriting is more expensive than evaluation, so we do it as a second
1013 : : // resort.
1014 [ + + ]: 2486150 : Node lhs = i == 1 ? ev[0] : eqi[0];
1015 : 2486150 : Node eq = lhs.eqNode(eqi[1]);
1016 [ - + ]: 2486150 : if (eq.getTypeOrNull().isNull())
1017 : : {
1018 : 0 : ProvenInfo& pi = d_pcache[eqi];
1019 : 0 : idb = RewriteProofStatus::FAIL;
1020 : 0 : pi.d_failMaxDepth = 0;
1021 : 0 : pi.d_id = idb;
1022 [ - - ]: 0 : Trace("rpc-debug2") << "...fail, ill-typed equality" << std::endl;
1023 : 0 : return true;
1024 : : }
1025 : 2486150 : Node eqr = rewriteConcrete(eq);
1026 [ + + ]: 2486150 : if (eqr.isConst())
1027 : : {
1028 : : // definitely not true
1029 [ + + ]: 810327 : if (!eqr.getConst<bool>())
1030 : : {
1031 : 80158 : ProvenInfo& pi = d_pcache[eqi];
1032 [ + - ][ - - ]: 160316 : Trace("rpc-debug2") << "fail, infeasible due to rewriting: " << eqi[0]
1033 [ - + ][ - + ]: 80158 : << " == " << eqi[1] << std::endl;
[ - - ]
1034 : 80158 : idb = RewriteProofStatus::FAIL;
1035 : 80158 : pi.d_failMaxDepth = 0;
1036 : 80158 : pi.d_id = idb;
1037 : 80158 : return true;
1038 : : }
1039 : : // NOTE: if eqr does not rewrite to true, it still could be true, hence
1040 : : // we fail
1041 : : }
1042 : 2405990 : evalSuccess = false;
1043 : 2405990 : break;
1044 : : }
1045 : : }
1046 [ + + ]: 2517170 : if (evalSuccess)
1047 : : {
1048 : 111180 : ProvenInfo& pi = d_pcache[eqi];
1049 : : // we can evaluate both sides, check to see if the values are the same
1050 [ + + ]: 111180 : if (ev[0] == ev[1])
1051 : : {
1052 [ + - ]: 32864 : Trace("rpc-debug2") << "...success, eval" << std::endl;
1053 : 32864 : idb = RewriteProofStatus::EVAL;
1054 : : }
1055 : : else
1056 : : {
1057 [ + - ]: 156632 : Trace("rpc-debug2") << "...fail (eval " << ev[0] << " and " << ev[1]
1058 : 78316 : << ")" << std::endl;
1059 : 78316 : idb = RewriteProofStatus::FAIL;
1060 : : // failure relies on nothing, depth is 0
1061 : 78316 : pi.d_failMaxDepth = 0;
1062 : : }
1063 : : // cache it
1064 : 111180 : pi.d_id = idb;
1065 : 111180 : return true;
1066 : : }
1067 [ + + ]: 2405990 : if (eqi[0].isConst())
1068 : : {
1069 [ + - ]: 54875 : Trace("rpc-debug2") << "...fail (constant head)" << std::endl;
1070 : 54875 : ProvenInfo& pi = d_pcache[eqi];
1071 : 54875 : idb = RewriteProofStatus::FAIL;
1072 : 54875 : pi.d_failMaxDepth = 0;
1073 : 54875 : pi.d_id = idb;
1074 : 54875 : return true;
1075 : : }
1076 [ + - ]: 2351120 : Trace("rpc-debug2") << "...unknown (default)" << std::endl;
1077 : : // otherwise, we fail to either prove or disprove the equality
1078 : 2351120 : return false;
1079 : : }
1080 : :
1081 : 326500 : bool RewriteDbProofCons::ensureProofInternal(CDProof* cdp, const Node& eqi)
1082 : : {
1083 : : // note we could use single internal cdp to improve subproof sharing
1084 : 326500 : NodeManager* nm = nodeManager();
1085 : 653000 : std::unordered_map<TNode, bool> visited;
1086 : 653000 : std::unordered_map<TNode, std::vector<Node>> premises;
1087 : 653000 : std::unordered_map<TNode, std::vector<Node>> pfArgs;
1088 : 326500 : std::unordered_map<TNode, bool>::iterator it;
1089 : : bool inserted;
1090 : 326500 : std::unordered_map<Node, ProvenInfo>::iterator itd;
1091 : 326500 : std::vector<Node>::iterator itv;
1092 : 653000 : std::vector<TNode> visit;
1093 : 653000 : TNode cur;
1094 : 326500 : visit.push_back(eqi);
1095 : 714762 : do
1096 : : {
1097 : 1041260 : cur = visit.back();
1098 : 1041260 : visit.pop_back();
1099 : 1041260 : std::tie(it, inserted) = visited.emplace(cur, false);
1100 : 1041260 : itd = d_pcache.find(cur);
1101 [ - + ][ - + ]: 1041260 : Assert(itd != d_pcache.end());
[ - - ]
1102 : 1041260 : ProvenInfo& pcur = itd->second;
1103 [ - + ][ - + ]: 1041260 : Assert(cur.getKind() == Kind::EQUAL);
[ - - ]
1104 [ + + ]: 1041260 : if (inserted)
1105 : : {
1106 [ + - ]: 517413 : Trace("rpc-debug") << "Ensure proof for " << cur << std::endl;
1107 : 517413 : visit.push_back(cur);
1108 : : // may already have a proof rule from a previous call
1109 [ + + ]: 517413 : if (cdp->hasStep(cur))
1110 : : {
1111 : 116 : it->second = true;
1112 [ + - ]: 116 : Trace("rpc-debug") << "...already proven" << std::endl;
1113 : : }
1114 : : else
1115 : : {
1116 [ - + ][ - + ]: 517297 : Assert(pcur.d_id != RewriteProofStatus::FAIL);
[ - - ]
1117 [ + - ]: 517297 : Trace("rpc-debug") << "...proved via " << pcur.d_id << std::endl;
1118 [ + + ]: 517297 : if (pcur.d_id == RewriteProofStatus::REFL)
1119 : : {
1120 : 9093 : it->second = true;
1121 : : // trivial proof
1122 [ - + ][ - + ]: 9093 : Assert(cur[0] == cur[1]);
[ - - ]
1123 : 18186 : cdp->addStep(cur, ProofRule::REFL, {}, {cur[0]});
1124 : : }
1125 [ + + ]: 508204 : else if (pcur.d_id == RewriteProofStatus::EVAL)
1126 : : {
1127 : 11565 : it->second = true;
1128 : : // NOTE: this could just evaluate the equality itself
1129 [ - + ][ - + ]: 11565 : Assert(cur.getKind() == Kind::EQUAL);
[ - - ]
1130 : 23130 : std::vector<Node> transc;
1131 [ + + ]: 34695 : for (size_t i = 0; i < 2; ++i)
1132 : : {
1133 : 46260 : Node curv = doEvaluate(cur[i]);
1134 [ + + ]: 23130 : if (curv == cur[i])
1135 : : {
1136 : 9749 : continue;
1137 : : }
1138 : 13381 : Node eq = cur[i].eqNode(curv);
1139 : : // flip orientation for second child
1140 [ + + ][ + + ]: 13381 : transc.push_back(i == 1 ? curv.eqNode(cur[i]) : eq);
[ - - ]
1141 : : // trivial evaluation, add evaluation method id
1142 : 26762 : cdp->addStep(eq, ProofRule::EVALUATE, {}, {cur[i]});
1143 : : }
1144 [ + + ]: 11565 : if (transc.size() == 2)
1145 : : {
1146 : : // do transitivity if both sides evaluate
1147 : 1816 : cdp->addStep(cur, ProofRule::TRANS, transc, {});
1148 : : }
1149 : : }
1150 : : else
1151 : : {
1152 : 496639 : std::vector<Node>& ps = premises[cur];
1153 : 496639 : std::vector<Node>& pfac = pfArgs[cur];
1154 [ + + ]: 496639 : if (pcur.isInternalRule())
1155 : : {
1156 : : // premises are the steps, stored in d_vars
1157 : 307422 : ps.insert(ps.end(), pcur.d_vars.begin(), pcur.d_vars.end());
1158 : : }
1159 : : else
1160 : : {
1161 [ - + ][ - + ]: 189217 : Assert(cur.getKind() == Kind::EQUAL);
[ - - ]
1162 [ - + ][ - + ]: 189217 : Assert(pcur.d_dslId != ProofRewriteRule::NONE);
[ - - ]
1163 : : // add the DSL proof rule we used
1164 : 189217 : pfac.push_back(
1165 : 378434 : nm->mkConstInt(Rational(static_cast<uint32_t>(pcur.d_dslId))));
1166 [ + + ]: 189217 : if (pcur.d_id == RewriteProofStatus::DSL)
1167 : : {
1168 : 188443 : const RewriteProofRule& rpr = d_db->getRule(pcur.d_dslId);
1169 : : // compute premises based on the used substitution
1170 : : // build the substitution context
1171 : 188443 : const std::vector<Node>& vs = rpr.getVarList();
1172 [ - + ][ - + ]: 188443 : Assert(pcur.d_vars.size() == vs.size());
[ - - ]
1173 : 188443 : std::vector<Node> rsubs;
1174 : : // must order the variables to match order of rewrite rule
1175 [ + + ]: 530288 : for (const Node& v : vs)
1176 : : {
1177 : 341845 : itv = std::find(pcur.d_vars.begin(), pcur.d_vars.end(), v);
1178 : 341845 : size_t d = std::distance(pcur.d_vars.begin(), itv);
1179 [ - + ][ - + ]: 341845 : Assert(d < pcur.d_subs.size());
[ - - ]
1180 : 341845 : rsubs.push_back(pcur.d_subs[d]);
1181 : : }
1182 : : // get the conditions, store into premises of cur.
1183 [ - + ]: 188443 : if (!rpr.getObligations(vs, rsubs, ps))
1184 : : {
1185 : 0 : Assert(false) << "failed a side condition?";
1186 : : return false;
1187 : : }
1188 : 188443 : pfac.insert(pfac.end(), rsubs.begin(), rsubs.end());
1189 : : }
1190 : : else
1191 : : {
1192 [ - + ][ - + ]: 774 : Assert(pcur.d_id == RewriteProofStatus::THEORY_REWRITE);
[ - - ]
1193 : 774 : pfac.push_back(cur);
1194 : : }
1195 : : }
1196 : : // recurse on premises
1197 : 496639 : visit.insert(visit.end(), ps.begin(), ps.end());
1198 : : }
1199 : : }
1200 : : }
1201 [ + + ]: 523849 : else if (!it->second)
1202 : : {
1203 : : // Now, add the proof rule. We do this after its children proofs already
1204 : : // exist.
1205 : 496639 : it->second = true;
1206 [ - + ][ - + ]: 496639 : Assert(premises.find(cur) != premises.end());
[ - - ]
1207 : 496639 : std::vector<Node>& ps = premises[cur];
1208 : : // get the conclusion
1209 : 993278 : Node conc;
1210 [ + + ]: 496639 : if (pcur.d_id == RewriteProofStatus::TRANS)
1211 : : {
1212 : 40133 : conc = ps[0][0].eqNode(ps.back()[1]);
1213 : 40133 : cdp->addStep(conc, ProofRule::TRANS, ps, {});
1214 : : }
1215 [ + + ]: 456506 : else if (pcur.d_id == RewriteProofStatus::CONG)
1216 : : {
1217 : : // get the appropriate CONG rule
1218 : 22593 : std::vector<Node> cargs;
1219 : 22593 : ProofRule cr = expr::getCongRule(cur[0], cargs);
1220 : 22593 : cdp->addStep(cur, cr, ps, cargs);
1221 : : }
1222 [ + + ]: 433913 : else if (pcur.d_id == RewriteProofStatus::CONG_EVAL)
1223 : : {
1224 : : // congruence + evaluation, given we are trying to prove
1225 : : // (f t1 ... tn) == c
1226 : : // This tactic checks if t1 ... tn rewrite to constants c1 ... cn.
1227 : : // If so, we try to show subgoals
1228 : : // t1 == c1 ... tn == cn
1229 : : // The final proof is a congruence step + evaluation:
1230 : : // (f t1 ... tn) == (f c1 ... cn) == c.
1231 : 1534 : Node lhs = cur[0];
1232 : 1534 : std::vector<Node> lhsTgtc;
1233 [ + + ]: 767 : if (cur[0].getMetaKind() == metakind::PARAMETERIZED)
1234 : : {
1235 : 50 : lhsTgtc.push_back(cur[0].getOperator());
1236 : : }
1237 [ + + ]: 2247 : for (const Node& eq : pcur.d_vars)
1238 : : {
1239 [ - + ][ - + ]: 1480 : Assert(eq.getKind() == Kind::EQUAL);
[ - - ]
1240 : 1480 : lhsTgtc.push_back(eq[1]);
1241 : : }
1242 : 1534 : Node lhsTgt = nm->mkNode(cur[0].getKind(), lhsTgtc);
1243 : 2301 : Node rhs = doEvaluate(cur[1]);
1244 [ - + ][ - + ]: 767 : Assert(!rhs.isNull());
[ - - ]
1245 : 1534 : Node eq1 = lhs.eqNode(lhsTgt);
1246 : 1534 : Node eq2 = lhsTgt.eqNode(rhs);
1247 : 3835 : std::vector<Node> transChildren = {eq1, eq2};
1248 : : // get the appropriate CONG rule
1249 : 767 : std::vector<Node> cargs;
1250 : 767 : ProofRule cr = expr::getCongRule(eq1[0], cargs);
1251 : 767 : cdp->addStep(eq1, cr, ps, cargs);
1252 : 1534 : cdp->addStep(eq2, ProofRule::EVALUATE, {}, {lhsTgt});
1253 [ - + ]: 767 : if (rhs != cur[1])
1254 : : {
1255 : 0 : cdp->addStep(cur[1].eqNode(rhs), ProofRule::EVALUATE, {}, {cur[1]});
1256 : 0 : transChildren.push_back(rhs.eqNode(cur[1]));
1257 : : }
1258 : 767 : cdp->addStep(cur, ProofRule::TRANS, transChildren, {});
1259 : : }
1260 [ + + ]: 433146 : else if (pcur.d_id == RewriteProofStatus::TRUE_ELIM)
1261 : : {
1262 : 1069 : conc = ps[0][0];
1263 : 1069 : cdp->addStep(conc, ProofRule::TRUE_ELIM, ps, {});
1264 : : }
1265 [ + + ]: 432077 : else if (pcur.d_id == RewriteProofStatus::TRUE_INTRO)
1266 : : {
1267 : 513 : conc = ps[0].eqNode(d_true);
1268 : 513 : cdp->addStep(conc, ProofRule::TRUE_INTRO, ps, {});
1269 : : }
1270 [ + + ]: 431564 : else if (pcur.d_id == RewriteProofStatus::ABSORB)
1271 : : {
1272 : 13472 : cdp->addStep(cur, ProofRule::ABSORB, {}, {cur});
1273 : : }
1274 [ + + ]: 424828 : else if (pcur.d_id == RewriteProofStatus::ACI_NORM)
1275 : : {
1276 : 84152 : cdp->addStep(cur, ProofRule::ACI_NORM, {}, {cur});
1277 : : }
1278 [ + + ]: 382752 : else if (pcur.d_id == RewriteProofStatus::ARITH_POLY_NORM)
1279 : : {
1280 : : TypeNode tn =
1281 : 522562 : pcur.d_vars.empty() ? cur[0].getType() : cur[0][0].getType();
1282 : 193535 : bool isBitVec = (tn.isBitVector());
1283 : 193535 : ProofRule pr =
1284 [ + + ]: 193535 : isBitVec ? ProofRule::BV_POLY_NORM : ProofRule::ARITH_POLY_NORM;
1285 [ + + ]: 193535 : if (pcur.d_vars.empty())
1286 : : {
1287 : 251578 : cdp->addStep(cur, pr, {}, {cur});
1288 : : }
1289 : : else
1290 : : {
1291 [ + + ]: 67746 : ProofRule prr = isBitVec ? ProofRule::BV_POLY_NORM_EQ
1292 : : : ProofRule::ARITH_POLY_NORM_REL;
1293 : 135492 : cdp->addStep(pcur.d_vars[0], pr, {}, {pcur.d_vars[0]});
1294 : 203238 : cdp->addStep(cur, prr, {pcur.d_vars[0]}, {cur});
1295 : : }
1296 : : }
1297 [ + + ]: 189217 : else if (pcur.d_id == RewriteProofStatus::DSL
1298 [ + - ]: 774 : || pcur.d_id == RewriteProofStatus::THEORY_REWRITE)
1299 : : {
1300 [ - + ][ - + ]: 189217 : Assert(pfArgs.find(cur) != pfArgs.end());
[ - - ]
1301 [ - + ][ - + ]: 189217 : Assert(pcur.d_dslId != ProofRewriteRule::NONE);
[ - - ]
1302 : 189217 : const std::vector<Node>& args = pfArgs[cur];
1303 : : ProofRule pfr;
1304 [ + + ]: 189217 : if (pcur.d_id == RewriteProofStatus::DSL)
1305 : : {
1306 : 188443 : std::vector<Node> subs(args.begin() + 1, args.end());
1307 : 188443 : const RewriteProofRule& rpr = d_db->getRule(pcur.d_dslId);
1308 : 188443 : conc = rpr.getConclusionFor(subs);
1309 [ + - ]: 188443 : Trace("rpc-debug") << "Finalize proof for " << cur << std::endl;
1310 [ + - ]: 188443 : Trace("rpc-debug") << "Proved: " << cur << std::endl;
1311 [ + - ]: 188443 : Trace("rpc-debug") << "From: " << conc << std::endl;
1312 : 188443 : pfr = ProofRule::DSL_REWRITE;
1313 : 188443 : cdp->addStep(conc, pfr, ps, args);
1314 : : }
1315 : : else
1316 : : {
1317 [ - + ][ - + ]: 774 : Assert(pcur.d_id == RewriteProofStatus::THEORY_REWRITE);
[ - - ]
1318 : : // use the utility, possibly to do macro expansion
1319 : 774 : d_trrc.ensureProofForTheoryRewrite(cdp, pcur.d_dslId, cur);
1320 : : }
1321 : : }
1322 : : }
1323 [ + + ]: 1041260 : } while (!visit.empty());
1324 : 326500 : return true;
1325 : : }
1326 : :
1327 : 4816940 : Node RewriteDbProofCons::doEvaluate(const Node& n)
1328 : : {
1329 : 4816940 : auto [itv, inserted] = d_evalCache.emplace(n, Node());
1330 [ + + ]: 4816940 : if (inserted)
1331 : : {
1332 : 2087170 : itv->second = d_eval.eval(n, {}, {});
1333 : : }
1334 : 9633870 : return itv->second;
1335 : : }
1336 : :
1337 : 3181760 : Node RewriteDbProofCons::getRuleConclusion(const RewriteProofRule& rpr,
1338 : : const std::vector<Node>& vars,
1339 : : const std::vector<Node>& subs,
1340 : : ProvenInfo& pi,
1341 : : bool doFixedPoint)
1342 : : {
1343 : 3181760 : pi.d_id = RewriteProofStatus::DSL;
1344 : 3181760 : pi.d_dslId = rpr.getId();
1345 : 6363520 : Node conc = rpr.getConclusion(true);
1346 : 6363520 : Node concRhs = conc[1];
1347 [ + - ]: 6363520 : Trace("rpc-ctx") << "***GET CONCLUSION " << pi.d_dslId << " for " << vars
1348 : 3181760 : << " -> " << subs << std::endl;
1349 : : // if fixed point, we continue applying
1350 [ + + ][ + + ]: 3181760 : if (doFixedPoint && rpr.isFixedPoint())
[ + + ]
1351 : : {
1352 [ - + ][ - + ]: 51077 : Assert(d_currFixedPointId == ProofRewriteRule::NONE);
[ - - ]
1353 [ - + ][ - + ]: 51077 : Assert(d_currFixedPointConc.isNull());
[ - - ]
1354 : 51077 : d_currFixedPointId = rpr.getId();
1355 : 51077 : Node context = rpr.getContext();
1356 [ - + ][ - + ]: 51077 : Assert(!context.isNull());
[ - - ]
1357 [ + - ]: 51077 : Trace("rpc-ctx") << "Context is " << context << std::endl;
1358 : : // check if stgt also rewrites with the same rule?
1359 : : bool continueFixedPoint;
1360 : 51077 : std::vector<Node> steps;
1361 : 51077 : std::vector<std::vector<Node>> stepsSubs;
1362 : : // start from the source, match again to start the chain. Notice this is
1363 : : // required for uniformity since we want to successfully cache the first
1364 : : // step, independent of the target.
1365 : 51077 : Node ssrc = expr::narySubstitute(conc[0], vars, subs);
1366 : 51077 : Node stgt = ssrc;
1367 : 238085 : do
1368 : : {
1369 [ + - ]: 238085 : Trace("rpc-ctx") << "Get matches " << stgt << std::endl;
1370 [ + - ]: 238085 : Trace("rpc-ctx") << "Conclusion is " << concRhs << std::endl;
1371 : 238085 : continueFixedPoint = false;
1372 : 238085 : rpr.getMatches(stgt, &d_notify);
1373 [ + - ]: 476170 : Trace("rpc-ctx") << "...conclusion is " << d_currFixedPointConc
1374 : 238085 : << std::endl;
1375 [ + + ]: 238085 : if (!d_currFixedPointConc.isNull())
1376 : : {
1377 : : // currently avoid accidental loops: arbitrarily bound to 1000
1378 : 187008 : continueFixedPoint = steps.size() <= s_fixedPointLimit;
1379 [ - + ][ - + ]: 187008 : Assert(d_currFixedPointConc.getKind() == Kind::EQUAL);
[ - - ]
1380 : 187008 : stepsSubs.emplace_back(d_currFixedPointSubs.begin(),
1381 : 374016 : d_currFixedPointSubs.end());
1382 : 187008 : stgt = d_currFixedPointConc[1];
1383 : : // For example, we have now computed
1384 : : // (str.len (str.++ x y z)) --> (+ (str.len x) (str.len (str.++ y z)))
1385 : : // where stgt is the RHS. We now want to continue to rewrite the right
1386 : : // hand side, where to find the next target term to rewrite, we match
1387 : : // the context of the rule to the RHS.
1388 : : // In particular, given a context (+ (str.len S0) ?0), we would match
1389 : : // ?0 to (str.len (str.++ y z)). This indicates that the user suggests
1390 : : // that (str.len (str.++ y z)) is the term to continue to rewrite.
1391 : : // We update stgt to this term to proceed with the loop.
1392 : 374016 : std::unordered_map<Node, Node> msubs;
1393 : 187008 : expr::match(context[1], stgt, msubs);
1394 [ + - ]: 374016 : Trace("rpc-ctx") << "Matching context " << context << " with " << stgt
1395 : 187008 : << " gives " << msubs[context[0][0]] << std::endl;
1396 : 187008 : stgt = msubs[context[0][0]];
1397 [ - + ][ - + ]: 187008 : Assert(!stgt.isNull());
[ - - ]
1398 : 187008 : steps.push_back(stgt);
1399 : : }
1400 [ + + ]: 238085 : d_currFixedPointConc = Node::null();
1401 : : } while (continueFixedPoint);
1402 : :
1403 : 51077 : std::vector<Node> transEq;
1404 : 51077 : Node prev = ssrc;
1405 : 51077 : Node placeholder = context[0][0];
1406 : 51077 : Node body = context[1];
1407 : 51077 : Node currConc = body;
1408 : 51077 : Node currContext = placeholder;
1409 [ + + ]: 238085 : for (size_t i = 0, size = steps.size(); i < size; ++i)
1410 : : {
1411 : 187008 : const std::vector<Node>& stepSubs = stepsSubs[i];
1412 : 374016 : Node step = steps[i];
1413 : 374016 : Node source = expr::narySubstitute(conc[0], vars, stepSubs);
1414 : 374016 : Node target = expr::narySubstitute(body, vars, stepSubs);
1415 : 187008 : target = target.substitute(TNode(placeholder), TNode(step));
1416 : 187008 : cacheProofSubPlaceholder(currContext, placeholder, source, target);
1417 [ + - ]: 374016 : Trace("rpc-ctx") << "Step " << source << " == " << target << " from "
1418 : 0 : << body << " " << vars << " -> " << stepSubs << ", "
1419 : 187008 : << placeholder << " -> " << step << std::endl;
1420 : :
1421 : 187008 : ProvenInfo& dpi = d_pcache[source.eqNode(target)];
1422 : 187008 : dpi.d_id = pi.d_id;
1423 : 187008 : dpi.d_dslId = pi.d_dslId;
1424 : 187008 : dpi.d_vars = vars;
1425 : 187008 : dpi.d_subs = stepSubs;
1426 : :
1427 : 187008 : currConc = expr::narySubstitute(currConc, vars, stepSubs);
1428 : 187008 : currContext = currConc;
1429 : 374016 : Node prevConc = currConc;
1430 [ + + ]: 187008 : if (i < size - 1)
1431 : : {
1432 : 135949 : currConc = currConc.substitute(TNode(placeholder), TNode(body));
1433 : : }
1434 : 561024 : Node stepConc = prevConc.substitute(TNode(placeholder), TNode(step));
1435 : 187008 : transEq.push_back(prev.eqNode(stepConc));
1436 : 187008 : prev = stepConc;
1437 : : }
1438 : :
1439 : 51077 : d_currFixedPointId = ProofRewriteRule::NONE;
1440 : : // add the transistivity rule here if needed
1441 [ + + ]: 51077 : if (transEq.size() >= 2)
1442 : : {
1443 : 30062 : pi.d_id = RewriteProofStatus::TRANS;
1444 : : // store transEq in d_vars
1445 : 30062 : pi.d_vars = transEq;
1446 [ + - ][ - + ]: 30062 : Trace("rpc-ctx") << "***RETURN trans " << transEq.back()[1] << std::endl;
[ - - ]
1447 : : // return the end of the chain, which will be used for constrained
1448 : : // matching
1449 : 30062 : return transEq.back()[1];
1450 : : }
1451 : : }
1452 : :
1453 : 6303390 : Node ret = expr::narySubstitute(concRhs, vars, subs);
1454 [ + - ]: 3151700 : Trace("rpc-ctx") << "***RETURN " << ret << std::endl;
1455 : 3151700 : return ret;
1456 : : }
1457 : :
1458 : 187008 : void RewriteDbProofCons::cacheProofSubPlaceholder(TNode context,
1459 : : TNode placeholder,
1460 : : TNode source,
1461 : : TNode target)
1462 : : {
1463 : 748032 : std::vector<TNode> toVisit = {context};
1464 : 374016 : std::unordered_map<TNode, TNode> parent;
1465 : 374016 : std::vector<Node> congs;
1466 : 187008 : parent[context] = TNode::null();
1467 : 374016 : std::unordered_map<TNode, Node> visitedSrc;
1468 : 374016 : std::unordered_map<TNode, Node> visitedTgt;
1469 [ + - ]: 558359 : while (!toVisit.empty())
1470 : : {
1471 : 558359 : TNode curr = toVisit.back();
1472 : 558359 : toVisit.pop_back();
1473 : :
1474 [ + + ]: 558359 : if (curr == placeholder)
1475 : : {
1476 : 374016 : TNode currp;
1477 [ + + ]: 558359 : while ((currp = parent[curr]) != Node::null())
1478 : : {
1479 : : Node lhs =
1480 : 2228110 : expr::narySubstitute(currp, {placeholder}, {source}, visitedSrc);
1481 : : Node rhs =
1482 : 2228110 : expr::narySubstitute(currp, {placeholder}, {target}, visitedTgt);
1483 : 371351 : congs.emplace_back(lhs.eqNode(rhs));
1484 : 371351 : curr = currp;
1485 : : }
1486 : 187008 : break;
1487 : : }
1488 : :
1489 [ + + ]: 1116920 : for (TNode n : curr)
1490 : : {
1491 : : // if we successfully inserted
1492 [ + + ]: 745564 : if (parent.emplace(n, curr).second)
1493 : : {
1494 : 736683 : toVisit.emplace_back(n);
1495 : : }
1496 : : }
1497 : : }
1498 : :
1499 [ + + ]: 558359 : for (const Node& cong : congs)
1500 : : {
1501 : 371351 : ProvenInfo& cpi = d_pcache[cong];
1502 : 371351 : cpi.d_id = RewriteProofStatus::CONG;
1503 : 371351 : cpi.d_vars.clear();
1504 [ + + ]: 1116920 : for (size_t i = 0, size = cong[0].getNumChildren(); i < size; i++)
1505 : : {
1506 : 2236690 : TNode lhs = cong[0][i];
1507 : 1491130 : TNode rhs = cong[1][i];
1508 [ + + ]: 745564 : if (lhs == rhs)
1509 : : {
1510 : 374213 : ProvenInfo& pi = d_pcache[lhs.eqNode(rhs)];
1511 : 374213 : pi.d_id = RewriteProofStatus::REFL;
1512 : : }
1513 : 745564 : cpi.d_vars.emplace_back(lhs.eqNode(rhs));
1514 : : }
1515 : : }
1516 : 187008 : }
1517 : :
1518 : 9068650 : Node RewriteDbProofCons::rewriteConcrete(const Node& n)
1519 : : {
1520 [ + + ]: 9068650 : if (expr::hasAbstractSubterm(n))
1521 : : {
1522 : 9150 : return n;
1523 : : }
1524 : 9059500 : return rewrite(n);
1525 : : }
1526 : :
1527 : : } // namespace rewriter
1528 : : } // namespace cvc5::internal
|
