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 : : * Rewrite database proof reconstructor
11 : : */
12 : :
13 : : #include "rewriter/rewrite_db_proof_cons.h"
14 : :
15 : : #include "expr/aci_norm.h"
16 : : #include "expr/algorithm/flatten.h"
17 : : #include "expr/node_algorithm.h"
18 : : #include "options/proof_options.h"
19 : : #include "proof/proof_node_algorithm.h"
20 : : #include "rewriter/rewrite_db_term_process.h"
21 : : #include "smt/env.h"
22 : : #include "theory/arith/arith_poly_norm.h"
23 : : #include "theory/builtin/proof_checker.h"
24 : : #include "theory/rewriter.h"
25 : : #include "util/bitvector.h"
26 : :
27 : : using namespace cvc5::internal::kind;
28 : :
29 : : namespace cvc5::internal {
30 : : namespace rewriter {
31 : :
32 : : // fixed point limit set to 1000
33 : : size_t RewriteDbProofCons::s_fixedPointLimit = 1000;
34 : :
35 : 6773 : RewriteDbProofCons::RewriteDbProofCons(Env& env, RewriteDb* db)
36 : : : EnvObj(env),
37 : 6773 : d_notify(*this),
38 : 6773 : d_trrc(env),
39 : 6773 : d_rdnc(nodeManager()),
40 : 6773 : d_db(db),
41 : 6773 : d_eval(nullptr),
42 : 6773 : d_currRecLimit(0),
43 : 6773 : d_currStepLimit(0),
44 : 6773 : d_currFailResource(false),
45 : 6773 : d_currFixedPointId(ProofRewriteRule::NONE),
46 : : d_statTotalInputs(
47 : 6773 : statisticsRegistry().registerInt("RewriteDbProofCons::totalInputs")),
48 : 6773 : d_statTotalAttempts(statisticsRegistry().registerInt(
49 : : "RewriteDbProofCons::totalAttempts")),
50 : 6773 : d_statTotalInputSuccess(statisticsRegistry().registerInt(
51 : 13546 : "RewriteDbProofCons::totalInputSuccess"))
52 : : {
53 : 6773 : NodeManager* nm = nodeManager();
54 : 6773 : d_true = nm->mkConst(true);
55 : 6773 : d_false = nm->mkConst(false);
56 : 6773 : }
57 : :
58 : 569106 : bool RewriteDbProofCons::prove(CDProof* cdp,
59 : : const Node& a,
60 : : const Node& b,
61 : : int64_t recLimit,
62 : : int64_t stepLimit,
63 : : TheoryRewriteMode tmode)
64 : : {
65 : 569106 : d_tmode = tmode;
66 : : // clear the proof caches
67 : 569106 : d_pcache.clear();
68 : : // clear the evaluate cache
69 : 569106 : d_evalCache.clear();
70 : 569106 : Node eq = a.eqNode(b);
71 [ + - ]: 1138212 : Trace("rpc") << "RewriteDbProofCons::prove: " << a << " == " << b << ", mode "
72 : 569106 : << tmode << std::endl;
73 : : // As a heuristic, always apply CONG if we are an equality between two
74 : : // binder terms with the same quantifier prefix or ALPHA_EQUIV if they have
75 : : // a different prefix whose types are the same.
76 [ + + ]: 569106 : if (a.isClosure())
77 : : {
78 : : // Note we apply this to fixed point, which should only occur at most 2
79 : : // times (first ALPHA_EQUIV, then CONG).
80 : 11854 : Node eqp;
81 : : do
82 : : {
83 : 12351 : eqp = preprocessClosureEq(cdp, eq[0], eq[1]);
84 [ + + ]: 12351 : if (!eqp.isNull())
85 : : {
86 : 4862 : eq = eqp;
87 : 9724 : Trace("rpc") << "- closure-preprocess to " << eq[0] << " == " << eq[1]
88 : 4862 : << std::endl;
89 : : }
90 : : else
91 : : {
92 [ + - ]: 7489 : Trace("rpc") << "...does not closure-preprocess" << std::endl;
93 : : }
94 [ + + ][ + + ]: 12351 : } while (!eqp.isNull() && eqp[0].isClosure());
[ + + ][ + + ]
[ - - ]
95 : 11854 : }
96 : 569106 : ++d_statTotalInputs;
97 : 569106 : bool success = false;
98 : : // first try unconverted
99 : 569106 : Node eqi;
100 [ + + ]: 569106 : if (proveEqStratified(cdp, eq, eq, recLimit, stepLimit, tmode))
101 : : {
102 : 557546 : success = true;
103 : : }
104 : : else
105 : : {
106 : 11560 : eqi = d_rdnc.convert(eq);
107 : : // if converter didn't make a difference, don't try to prove again
108 [ + + ]: 11560 : if (eqi != eq)
109 : : {
110 [ + - ]: 8734 : Trace("rpc-debug") << "...now try converted" << std::endl;
111 [ + + ]: 8734 : if (proveEqStratified(cdp, eq, eqi, recLimit, stepLimit, tmode))
112 : : {
113 : 6249 : success = true;
114 : : }
115 : : }
116 : : else
117 : : {
118 [ + - ]: 5652 : Trace("rpc-debug") << "...do not try converted, did not change"
119 : 2826 : << std::endl;
120 : : }
121 : : }
122 [ + + ]: 569106 : if (!success)
123 : : {
124 : : // Now try the "post-prove" method as a last resort. We try the unconverted
125 : : // then the converted form of eq, if applicable.
126 [ + + ]: 5311 : if (d_trrc.postProve(cdp, eq[0], eq[1], tmode))
127 : : {
128 [ + - ]: 702 : Trace("rpc") << "...success (post-prove basic)" << std::endl;
129 : 702 : success = true;
130 : : }
131 : 4609 : else if (eqi != eq && d_trrc.postProve(cdp, eqi[0], eqi[1], tmode))
132 : : {
133 [ - - ]: 0 : Trace("rpc") << "...success (post-prove basic)" << std::endl;
134 : 0 : d_trrc.ensureProofForEncodeTransform(cdp, eq, eqi);
135 : 0 : success = true;
136 : : }
137 : : else
138 : : {
139 [ + - ]: 4609 : Trace("rpc") << "...fail" << std::endl;
140 : : }
141 : : }
142 : : else
143 : : {
144 [ + - ]: 563795 : Trace("rpc") << "...success" << std::endl;
145 : : }
146 : 569106 : return success;
147 : 569106 : }
148 : :
149 : 577840 : bool RewriteDbProofCons::proveEqStratified(CDProof* cdp,
150 : : const Node& eq,
151 : : const Node& eqi,
152 : : int64_t recLimit,
153 : : int64_t stepLimit,
154 : : TheoryRewriteMode tmode)
155 : : {
156 : 577840 : bool success = false;
157 : : // first, try the basic utility
158 [ + + ]: 577840 : if (d_trrc.prove(cdp, eqi[0], eqi[1], tmode))
159 : : {
160 [ + - ]: 111315 : Trace("rpc") << "...success (basic)" << std::endl;
161 : 111315 : success = true;
162 : : }
163 : : else
164 : : {
165 : : // prove the equality
166 [ + + ]: 529260 : for (int64_t i = 0; i <= recLimit; i++)
167 : : {
168 [ + - ]: 526288 : Trace("rpc-debug") << "* Try recursion depth " << i << std::endl;
169 [ + + ]: 526288 : if (proveEq(cdp, eqi, i, stepLimit))
170 : : {
171 [ + - ]: 452480 : Trace("rpc") << "...success" << std::endl;
172 : 452480 : success = true;
173 : 452480 : break;
174 : : }
175 [ + + ]: 73808 : else if (!d_currFailResource)
176 : : {
177 [ + - ]: 22146 : Trace("rpc-debug") << "...fail independent of depth (" << i << ")"
178 : 11073 : << std::endl;
179 : : // if it was not due to a resource limit, we know that we will always
180 : : // fail at higher recursion limit, so we abort here for the sake of
181 : : // performance.
182 : 11073 : break;
183 : : }
184 : : }
185 : : }
186 [ + + ]: 577840 : if (success)
187 : : {
188 : : // if eqi was converted, update the proof to account for this
189 [ + + ]: 563795 : if (eq != eqi)
190 : : {
191 : 6249 : d_trrc.ensureProofForEncodeTransform(cdp, eq, eqi);
192 : : }
193 : 563795 : return true;
194 : : }
195 : 14045 : return false;
196 : : }
197 : :
198 : 12351 : Node RewriteDbProofCons::preprocessClosureEq(CDProof* cdp,
199 : : const Node& a,
200 : : const Node& b)
201 : : {
202 : : // if it is a single step rewrite, do not preprocess
203 : 12351 : theory::Rewriter* rr = d_env.getRewriter();
204 : 12351 : ProofRewriteRule prid = rr->findRule(a, b, theory::TheoryRewriteCtx::PRE_DSL);
205 [ + + ]: 12351 : if (prid != ProofRewriteRule::NONE)
206 : : {
207 : : // a simple theory rewrite happens to solve it, do not continue
208 : 7330 : return Node::null();
209 : : }
210 : : // Ensure patterns are removed by calling d_rdnc postConvert (single step),
211 : : // which also ensures differences e.g. LAMBDA vs FUNCTION_ARRAY_CONST are
212 : : // resolved. We do not apply convert recursively here.
213 : 5021 : Node ai = d_rdnc.postConvert(a);
214 : 5021 : Node bi = d_rdnc.postConvert(b);
215 : : // The kinds must match.
216 [ + + ]: 5021 : if (ai.getKind() != bi.getKind())
217 : : {
218 : 63 : return Node::null();
219 : : }
220 : : // only apply this to standard binders (those with 2 children)
221 [ + - ][ - + ]: 4958 : if (ai.getNumChildren() != 2 || bi.getNumChildren() != 2)
[ - + ]
222 : : {
223 : 0 : return Node::null();
224 : : }
225 : 4958 : Node eq;
226 : 4958 : Node eqConv = ai.eqNode(bi);
227 [ + + ]: 4958 : if (ai[0] == bi[0])
228 : : {
229 : 4365 : std::vector<Node> cargs;
230 : 4365 : ProofRule cr = expr::getCongRule(ai, cargs);
231 : : // remains to prove their bodies are equal
232 : 4365 : eq = ai[1].eqNode(bi[1]);
233 : 8730 : cdp->addStep(eqConv, cr, {eq}, cargs);
234 : 4365 : }
235 [ + + ]: 593 : else if (ai[0].getNumChildren() == bi[0].getNumChildren())
236 : : {
237 : 529 : size_t nchild = ai[0].getNumChildren();
238 : 529 : std::vector<Node> vars;
239 : 529 : std::vector<Node> subs;
240 : 529 : std::unordered_set<Node> uvars;
241 [ + + ]: 1477 : for (size_t i = 0; i < nchild; i++)
242 : : {
243 : : // rare corner case: don't use if duplicate variables
244 [ - + ]: 1018 : if (!uvars.insert(ai[0][i]).second)
245 : : {
246 : 70 : return Node::null();
247 : : }
248 [ + + ]: 1018 : if (ai[0][i] != bi[0][i])
249 : : {
250 [ + + ]: 5045 : if (!CVC5_EQUAL(ai[0][i].getType(), bi[0][i].getType()))
251 : : {
252 : 70 : return Node::null();
253 : : }
254 : 939 : vars.emplace_back(ai[0][i]);
255 : 939 : subs.emplace_back(bi[0][i]);
256 : : }
257 : : }
258 [ - + ]: 459 : if (vars.empty())
259 : : {
260 : 0 : return Node::null();
261 : : }
262 : 459 : NodeManager* nm = nodeManager();
263 : 459 : std::vector<Node> aeArgs;
264 : 459 : aeArgs.push_back(ai);
265 : 459 : aeArgs.push_back(nm->mkNode(Kind::SEXPR, vars));
266 : 459 : aeArgs.push_back(nm->mkNode(Kind::SEXPR, subs));
267 : 459 : ProofChecker* pc = d_env.getProofNodeManager()->getChecker();
268 : 918 : Node res = pc->checkDebug(ProofRule::ALPHA_EQUIV, {}, aeArgs);
269 [ + - ]: 459 : if (!res.isNull())
270 : : {
271 [ - + ][ - + ]: 459 : Assert(res.getKind() == Kind::EQUAL);
[ - - ]
272 : 459 : cdp->addStep(res, ProofRule::ALPHA_EQUIV, {}, aeArgs);
273 : : // Remains to prove that the result of applying alpha equivalence to the
274 : : // left hand side is equal to the right hand side. This may be a
275 : : // reflexive equality when ALPHA_EQUIV alone suffices. Note that when this
276 : : // occurs eq is not a free assumption in cdp. Proof generation will
277 : : // easily succeed in proving eq by REFL, but this will not be used
278 : : // in the final proof.
279 : 459 : eq = res[1].eqNode(bi);
280 [ + + ]: 459 : if (res != eqConv)
281 : : {
282 [ + + ][ - - ]: 36 : cdp->addStep(eqConv, ProofRule::TRANS, {res, eq}, {});
283 : : }
284 : : }
285 : : else
286 : : {
287 : 0 : return Node::null();
288 : : }
289 [ + - ][ + - ]: 669 : }
[ + + ][ + + ]
[ + + ]
290 [ + - ]: 64 : else if (ai[0].getNumChildren() > bi[0].getNumChildren())
291 : : {
292 : : // maybe unused variables on the left hand side
293 : 64 : Node aiu = rr->rewriteViaRule(ProofRewriteRule::QUANT_UNUSED_VARS, ai);
294 [ + + ]: 64 : if (!aiu.isNull())
295 : : {
296 [ - + ][ - + ]: 38 : Assert(aiu != ai);
[ - - ]
297 : 38 : Node eqq = ai.eqNode(aiu);
298 : 38 : cdp->addTheoryRewriteStep(eqq, ProofRewriteRule::QUANT_UNUSED_VARS);
299 : : // remains to prove the result of removing variables is equal to
300 : : // the right hand side.
301 : 38 : eq = aiu.eqNode(bi);
302 [ + + ][ - - ]: 114 : cdp->addStep(eqConv, ProofRule::TRANS, {eqq, eq}, {});
303 : 38 : }
304 : : else
305 : : {
306 : 26 : return Node::null();
307 : : }
308 [ + + ]: 64 : }
309 : : else
310 : : {
311 : 0 : return Node::null();
312 : : }
313 : 4862 : std::vector<Node> transEq;
314 [ + + ]: 4862 : if (ai != a)
315 : : {
316 : 626 : Node aeq = a.eqNode(ai);
317 : 1252 : cdp->addStep(aeq, ProofRule::ENCODE_EQ_INTRO, {}, {a});
318 : 626 : transEq.push_back(aeq);
319 : 626 : }
320 : 4862 : transEq.push_back(eqConv);
321 [ + + ]: 4862 : if (bi != b)
322 : : {
323 : 655 : Node beq = b.eqNode(bi);
324 : 1310 : cdp->addStep(beq, ProofRule::ENCODE_EQ_INTRO, {}, {b});
325 : 655 : Node beqs = bi.eqNode(b);
326 : 1310 : cdp->addStep(beqs, ProofRule::SYMM, {beq}, {});
327 : 655 : transEq.push_back(beqs);
328 : 655 : }
329 [ + + ]: 4862 : if (transEq.size() > 1)
330 : : {
331 : 655 : Node eqo = a.eqNode(b);
332 : 655 : cdp->addStep(eqo, ProofRule::TRANS, transEq, {});
333 : 655 : }
334 : 4862 : return eq;
335 : 5021 : }
336 : :
337 : 526288 : bool RewriteDbProofCons::proveEq(CDProof* cdp,
338 : : const Node& eqi,
339 : : int64_t recLimit,
340 : : int64_t stepLimit)
341 : : {
342 : : // add one to recursion limit, since it is decremented whenever we
343 : : // initiate the getMatches routine.
344 : 526288 : d_currRecLimit = recLimit + 1;
345 : 526288 : d_currStepLimit = stepLimit;
346 : 526288 : d_currFailResource = false;
347 : : RewriteProofStatus id;
348 [ + + ]: 526288 : if (!proveInternalBase(eqi, id))
349 : : {
350 [ + - ]: 524265 : Trace("rpc-debug") << "- prove internal" << std::endl;
351 : : // Otherwise, we call the main prove internal method, which recurisvely
352 : : // tries to find a matched conclusion whose conditions can be proven
353 : 524265 : id = proveInternal(eqi);
354 [ + - ]: 524265 : Trace("rpc-debug") << "- finished prove internal" << std::endl;
355 : : }
356 : : // if a proof was provided, fill it in
357 [ + + ][ + - ]: 526288 : if (id != RewriteProofStatus::FAIL && cdp != nullptr)
358 : : {
359 : 452480 : ++d_statTotalInputSuccess;
360 [ + - ]: 452480 : Trace("rpc-debug") << "- ensure proof" << std::endl;
361 : 452480 : ensureProofInternal(cdp, eqi);
362 : 452480 : AlwaysAssert(cdp->hasStep(eqi)) << eqi;
363 [ + - ]: 452480 : Trace("rpc-debug") << "- finish ensure proof" << std::endl;
364 : 452480 : return true;
365 : : }
366 : 73808 : return false;
367 : : }
368 : :
369 : 1546808 : RewriteProofStatus RewriteDbProofCons::proveInternal(const Node& eqi)
370 : : {
371 : 1546808 : d_currProving.insert(eqi);
372 : 1546808 : ++d_statTotalAttempts;
373 : : // eqi should not hold trivially and should not be cached
374 [ + - ]: 1546808 : Trace("rpc-debug2") << "proveInternal " << eqi << std::endl;
375 : : // Otherwise, call the get matches routine. This will call notifyMatch below
376 : : // for each matching rewrite rule conclusion in the database
377 : : // decrease the recursion depth
378 [ - + ][ - + ]: 1546808 : Assert(eqi.getKind() == Kind::EQUAL);
[ - - ]
379 : : // first, try congruence if possible, which does not count towards recursion
380 : : // limit.
381 : 1546808 : RewriteProofStatus retId = proveInternalViaStrategy(eqi);
382 : 1546808 : d_currProving.erase(eqi);
383 : 1546808 : return retId;
384 : : }
385 : :
386 : 1546808 : RewriteProofStatus RewriteDbProofCons::proveInternalViaStrategy(const Node& eqi)
387 : : {
388 [ - + ][ - + ]: 1546808 : Assert(eqi.getKind() == Kind::EQUAL);
[ - - ]
389 [ + + ]: 1546808 : if (proveWithRule(RewriteProofStatus::CONG, eqi, {}, {}, false, false, true))
390 : : {
391 [ + - ]: 33262 : Trace("rpc-debug2") << "...proved via congruence" << std::endl;
392 : 33262 : return RewriteProofStatus::CONG;
393 : : }
394 [ + + ]: 1513546 : if (proveWithRule(
395 : : RewriteProofStatus::CONG_EVAL, eqi, {}, {}, false, false, true))
396 : : {
397 [ + - ]: 1724 : Trace("rpc-debug2") << "...proved via congruence + evaluation" << std::endl;
398 : 1724 : return RewriteProofStatus::CONG_EVAL;
399 : : }
400 : : // maybe by absorb?
401 [ + + ]: 1511822 : if (proveWithRule(
402 : : RewriteProofStatus::ABSORB, eqi, {}, {}, false, false, true))
403 : : {
404 : 14474 : return RewriteProofStatus::ABSORB;
405 : : }
406 : : // standard normalization
407 [ + + ]: 1497348 : if (proveWithRule(
408 : : RewriteProofStatus::ACI_NORM, eqi, {}, {}, false, false, true))
409 : : {
410 : 75299 : return RewriteProofStatus::ACI_NORM;
411 : : }
412 : : // if arithmetic, maybe holds by arithmetic normalization?
413 [ + + ]: 1422049 : if (proveWithRule(
414 : : RewriteProofStatus::ARITH_POLY_NORM, eqi, {}, {}, false, false, true))
415 : : {
416 : 160713 : return RewriteProofStatus::ARITH_POLY_NORM;
417 : : }
418 : : // flattening
419 [ + + ]: 1261336 : if (proveWithRule(
420 : : RewriteProofStatus::FLATTEN, eqi, {}, {}, false, false, true))
421 : : {
422 : 864 : return RewriteProofStatus::FLATTEN;
423 : : }
424 : : // Maybe holds via a THEORY_REWRITE that has been marked with
425 : : // TheoryRewriteCtx::DSL_SUBCALL.
426 [ + + ]: 1260472 : if (d_tmode == TheoryRewriteMode::STANDARD)
427 : : {
428 [ + + ]: 1188448 : if (proveWithRule(RewriteProofStatus::THEORY_REWRITE,
429 : : eqi,
430 : : {},
431 : : {},
432 : : false,
433 : : false,
434 : : true))
435 : : {
436 : 2366 : return RewriteProofStatus::THEORY_REWRITE;
437 : : }
438 : : }
439 [ + - ]: 1258106 : Trace("rpc-debug2") << "...not proved via builtin tactic" << std::endl;
440 : 1258106 : Node prevTarget = d_target;
441 : 1258106 : d_target = eqi;
442 : 1258106 : d_db->getMatches(eqi[0], &d_notify);
443 : 1258106 : d_target = prevTarget;
444 : : // check if we determined the proof in the above call, which is the case
445 : : // if we succeeded, or we are already marked as a failure at a lower depth.
446 : 1258106 : std::unordered_map<Node, ProvenInfo>::iterator it = d_pcache.find(eqi);
447 [ + + ]: 1258106 : if (it != d_pcache.end())
448 : : {
449 [ + + ]: 736746 : if (it->second.d_id != RewriteProofStatus::FAIL)
450 : : {
451 : 280704 : return it->second.d_id;
452 : : }
453 [ - + ]: 456042 : else if (it->second.d_failMaxDepth == -1)
454 : : {
455 : 0 : return it->second.d_id;
456 : : }
457 [ + + ]: 456042 : else if (d_currRecLimit <= it->second.d_failMaxDepth)
458 : : {
459 : 49969 : d_currFailResource = true;
460 : 49969 : return it->second.d_id;
461 : : }
462 : : }
463 : : // if target is (= (= t1 t2) true), maybe try showing (= t1 t2); otherwise
464 : : // try showing (= target true)
465 : 927433 : RewriteProofStatus eqTrueId = eqi[1] == d_true
466 [ + + ]: 927433 : ? RewriteProofStatus::TRUE_INTRO
467 : 927433 : : RewriteProofStatus::TRUE_ELIM;
468 [ + + ]: 927433 : if (proveWithRule(eqTrueId, eqi, {}, {}, false, false, true))
469 : : {
470 [ + - ]: 29435 : Trace("rpc-debug2") << "...proved via " << eqTrueId << std::endl;
471 : 29435 : return eqTrueId;
472 : : }
473 : 1795996 : Trace("rpc-fail") << "FAIL: cannot prove " << eqi[0] << " == " << eqi[1]
474 : 897998 : << std::endl;
475 : : // store failure, and its maximum depth
476 : 897998 : ProvenInfo& pi = d_pcache[eqi];
477 : 897998 : pi.d_id = RewriteProofStatus::FAIL;
478 : 897998 : pi.d_failMaxDepth = d_currRecLimit;
479 : 897998 : return RewriteProofStatus::FAIL;
480 : 1258106 : }
481 : :
482 : 1560706 : bool RewriteDbProofCons::notifyMatch(const Node& s,
483 : : const Node& n,
484 : : std::vector<Node>& vars,
485 : : std::vector<Node>& subs)
486 : : {
487 : : // if we reach our step limit, do not continue trying
488 [ + - ]: 3121412 : Trace("rpc-debug2") << "[steps remaining: " << d_currStepLimit << "]"
489 : 1560706 : << std::endl;
490 [ + - ]: 3121412 : Trace("rpc-debug2") << "notifyMatch: " << s << " from " << n << " via "
491 : 1560706 : << vars << " -> " << subs << std::endl;
492 [ - + ][ - + ]: 1560706 : Assert(d_target.getKind() == Kind::EQUAL);
[ - - ]
493 [ - + ][ - + ]: 1560706 : Assert(s.getType().isComparableTo(n.getType()));
[ - - ]
494 [ - + ][ - + ]: 1560706 : Assert(vars.size() == subs.size());
[ - - ]
495 [ + + ]: 1560706 : if (d_currFixedPointId != ProofRewriteRule::NONE)
496 : : {
497 [ + - ]: 160610 : Trace("rpc-debug2") << "Part of fixed point for rule " << d_currFixedPointId
498 : 80305 : << std::endl;
499 : 80305 : const RewriteProofRule& rpr = d_db->getRule(d_currFixedPointId);
500 : : // get the conclusion
501 : 80305 : Node target = rpr.getConclusion(true);
502 : : // apply substitution, which may notice vars may be out of order wrt rule
503 : : // var list
504 : 80305 : target = expr::narySubstitute(target, vars, subs);
505 : : // it may be impossible to construct the conclusion due to null terminators
506 : : // for approximate types, return false in this case
507 [ + + ]: 80305 : if (target.isNull())
508 : : {
509 : : // note that we return false here, indicating that we don't want any
510 : : // more matches, since we have failed for the current fixed point rule.
511 : 40 : return false;
512 : : }
513 : : // We now prove with the given rule. this should only fail if there are
514 : : // conditions on the rule which fail. Notice we never allow recursion here.
515 : : // We also don't permit inflection matching (which regardless should not
516 : : // apply).
517 [ + - ]: 80265 : if (proveWithRule(RewriteProofStatus::DSL,
518 : : target,
519 : : vars,
520 : : subs,
521 : : false,
522 : : false,
523 : : false,
524 : : d_currFixedPointId))
525 : : {
526 : : // successfully proved, store in temporary variable
527 : 80265 : d_currFixedPointConc = target;
528 : 80265 : d_currFixedPointSubs = subs;
529 : : }
530 : : // regardless, no further matches, due to semantics of fixed point which
531 : : // limits to first match
532 : 80265 : return false;
533 : 80305 : }
534 [ - + ][ - + ]: 1480401 : Assert(d_target[0] == s);
[ - - ]
535 : 1480401 : bool recurse = d_currRecLimit > 0;
536 : : // get the rule identifiers for the conclusion
537 : 1480401 : const std::vector<ProofRewriteRule>& ids = d_db->getRuleIdsForHead(n);
538 [ - + ][ - + ]: 1480401 : Assert(!ids.empty());
[ - - ]
539 : : // check each rule instance, succeed if one proves
540 [ + + ]: 2867308 : for (ProofRewriteRule id : ids)
541 : : {
542 : : // try to prove target with the current rule, using inflection matching
543 : : // and fixed point semantics
544 [ + + ]: 1667611 : if (proveWithRule(RewriteProofStatus::DSL,
545 : 1667611 : d_target,
546 : : vars,
547 : : subs,
548 : : true,
549 : : true,
550 : : recurse,
551 : : id))
552 : : {
553 : : // if successful, we do not want to be notified of further matches
554 : : // and return false here.
555 : 280704 : return false;
556 : : }
557 : : // notice that we do not cache a failure here since we only know that the
558 : : // current rule was not able to prove the current target
559 : : }
560 : : // want to keep getting notify calls
561 : 1199697 : return true;
562 : : }
563 : :
564 : 12616666 : bool RewriteDbProofCons::proveWithRule(RewriteProofStatus id,
565 : : const Node& target,
566 : : const std::vector<Node>& vars,
567 : : const std::vector<Node>& subs,
568 : : bool doInflectMatch,
569 : : bool doFixedPoint,
570 : : bool doRecurse,
571 : : ProofRewriteRule r)
572 : : {
573 [ + - ][ + - ]: 12616666 : Assert(!target.isNull() && target.getKind() == Kind::EQUAL)
[ - + ][ - - ]
574 [ - + ][ - + ]: 12616666 : << "Unknown " << target << " with rule " << id << " " << r << std::endl;
[ - - ]
575 [ + - ]: 25233332 : Trace("rpc-debug2") << "Check rule "
576 [ - - ]: 12616666 : << (id == RewriteProofStatus::DSL ? toString(r)
577 : 0 : : toString(id))
578 : 12616666 : << std::endl;
579 : 12616666 : std::vector<Node> vcs;
580 : : // the implied substitution if we have a rule with free variables on RHS
581 : 12616666 : std::vector<Node> impliedVs;
582 : 12616666 : std::vector<Node> impliedSs;
583 : 12616666 : Node transEq;
584 : 12616666 : ProvenInfo pic;
585 : : // whether we require decrementing the recursion limit to apply this rule
586 : 12616666 : bool decRecLimit = true;
587 [ + + ]: 12616666 : if (id == RewriteProofStatus::CONG)
588 : : {
589 : 1546808 : size_t nchild = target[0].getNumChildren();
590 [ + + ][ + + ]: 3091216 : if (nchild == 0 || nchild != target[1].getNumChildren()
[ - - ]
591 : 3091216 : || target[0].getOperator() != target[1].getOperator())
592 : : {
593 : : // cannot show congruence between different operators
594 : 1260418 : return false;
595 : : }
596 : 286390 : pic.d_id = id;
597 [ + + ]: 779552 : for (size_t i = 0; i < nchild; i++)
598 : : {
599 : : // for closures, their first argument (the bound variable list) must be
600 : : // equivalent, and should not be given as a child proof.
601 [ + + ][ + + ]: 523923 : if (i == 0 && target[0].isClosure())
[ + + ][ + + ]
[ - - ]
602 : : {
603 [ + + ]: 681 : if (target[0][0] != target[1][0])
604 : : {
605 : 30761 : return false;
606 : : }
607 : 222 : continue;
608 : : }
609 [ + + ]: 523242 : if (!target[0][i].getType().isComparableTo(target[1][i].getType()))
610 : : {
611 : : // type error on children (required for certain polymorphic operators)
612 : 30302 : return false;
613 : : }
614 : 985880 : Node eq = target[0][i].eqNode(target[1][i]);
615 : 492940 : vcs.push_back(eq);
616 : 492940 : pic.d_vars.push_back(eq);
617 : 492940 : }
618 : : // congruence (f(a) = f(b)) <= (a = b) is treated as a "propagation", i.e.
619 : : // it does not require decrementing the recursion limit, as a heuristic.
620 : 255629 : decRecLimit = false;
621 : : }
622 [ + + ]: 11069858 : else if (id == RewriteProofStatus::CONG_EVAL)
623 : : {
624 : 1513546 : size_t nchild = target[0].getNumChildren();
625 : : // evaluate the right hand side
626 : 1513546 : Node r2 = doEvaluate(target[1]);
627 [ + + ][ + + ]: 1513546 : if (nchild == 0 || r2.isNull())
[ + + ]
628 : : {
629 : 912413 : return false;
630 : : }
631 : 601133 : Node rr1 = rewriteConcrete(target[0]);
632 [ + + ]: 601133 : if (rr1 != r2)
633 : : {
634 : 311076 : return false;
635 : : }
636 : 290057 : pic.d_id = id;
637 : : // if all children rewrite to a constant, try proving equalities
638 : : // on those children
639 : 290057 : std::vector<Node> rchildren;
640 [ + + ]: 418100 : for (size_t i = 0; i < nchild; i++)
641 : : {
642 : 721364 : Node rr = rewriteConcrete(target[0][i]);
643 [ + + ]: 360682 : if (!rr.isConst())
644 : : {
645 : 232639 : return false;
646 : : }
647 : 256086 : Node eq = target[0][i].eqNode(rr);
648 : 128043 : vcs.push_back(eq);
649 : 128043 : pic.d_vars.push_back(eq);
650 : 128043 : rchildren.push_back(rr);
651 [ + + ]: 360682 : }
652 : : // must check if it truly evaluates. This can fail if the evaluator does
653 : : // not support constant folding for the operator in question, which is the
654 : : // case e.g. for operators that return regular expressions, datatypes,
655 : : // sequences, sets.
656 [ + + ]: 57418 : if (target[0].getMetaKind() == metakind::PARAMETERIZED)
657 : : {
658 : 1245 : rchildren.insert(rchildren.begin(), target[0].getOperator());
659 : : }
660 : 57418 : NodeManager* nm = nodeManager();
661 : 57418 : Node tappc = nm->mkNode(target[0].getKind(), rchildren);
662 [ + + ]: 57418 : if (doEvaluate(tappc) != r2)
663 : : {
664 : 2606 : return false;
665 : : }
666 [ + + ][ + + ]: 2297718 : }
[ + + ][ + + ]
667 [ + + ]: 9556312 : else if (id == RewriteProofStatus::TRUE_ELIM)
668 : : {
669 [ - + ]: 481463 : if (target[1] == d_true)
670 : : {
671 : : // don't do for equals true, avoids unbounded recursion
672 : 0 : return false;
673 : : }
674 : 481463 : pic.d_id = id;
675 : 481463 : Node eq = target.eqNode(d_true);
676 : 481463 : vcs.push_back(eq);
677 : 481463 : pic.d_vars.push_back(eq);
678 : 481463 : }
679 [ + + ]: 9074849 : else if (id == RewriteProofStatus::TRUE_INTRO)
680 : : {
681 : 445970 : if (target[1] != d_true || target[0].getKind() != Kind::EQUAL)
682 : : {
683 : : // only works for (= (= t1 t2) true)
684 : 101565 : return false;
685 : : }
686 : 344405 : pic.d_id = id;
687 : 344405 : Node eq = target[0];
688 : 344405 : vcs.push_back(eq);
689 : 344405 : pic.d_vars.push_back(eq);
690 : : // also treated as a "propagation" heuristic
691 : 344405 : decRecLimit = false;
692 : 344405 : }
693 [ + + ]: 8628879 : else if (id == RewriteProofStatus::ABSORB)
694 : : {
695 : : Node zero = expr::getZeroElement(
696 : 3023644 : nodeManager(), target[0].getKind(), target[0].getType());
697 [ + + ]: 1511822 : if (zero != target[1])
698 : : {
699 : 1469152 : return false;
700 : : }
701 [ + + ]: 42670 : if (!expr::isAbsorb(target[0], target[1]))
702 : : {
703 : 28196 : return false;
704 : : }
705 : 14474 : pic.d_id = id;
706 [ + + ]: 1511822 : }
707 [ + + ]: 7117057 : else if (id == RewriteProofStatus::ACI_NORM)
708 : : {
709 [ + + ]: 1497348 : if (!expr::isACINorm(target[0], target[1]))
710 : : {
711 : 1422049 : return false;
712 : : }
713 : 75299 : pic.d_id = id;
714 : : }
715 [ + + ]: 5619709 : else if (id == RewriteProofStatus::ARITH_POLY_NORM)
716 : : {
717 [ + + ]: 1422049 : if (target[0].getType().isBoolean())
718 : : {
719 : 1192553 : Rational rx, ry;
720 [ + + ]: 1192553 : if (!theory::arith::PolyNorm::isArithPolyNormRel(
721 : : target[0], target[1], rx, ry))
722 : : {
723 : 1107862 : return false;
724 : : }
725 : : Node premise = theory::arith::PolyNorm::getArithPolyNormRelPremise(
726 : 169382 : target[0], target[1], rx, ry);
727 : 84691 : ProvenInfo ppremise;
728 : 84691 : ppremise.d_id = id;
729 : 84691 : d_pcache[premise] = ppremise;
730 : 84691 : pic.d_id = id;
731 : 84691 : pic.d_vars.push_back(premise);
732 [ + + ][ + + ]: 2300415 : }
733 : : else
734 : : {
735 [ + + ]: 229496 : if (!theory::arith::PolyNorm::isArithPolyNorm(target[0], target[1]))
736 : : {
737 : 153474 : return false;
738 : : }
739 : 76022 : pic.d_id = id;
740 : : }
741 : : }
742 [ + + ]: 4197660 : else if (id == RewriteProofStatus::FLATTEN)
743 : : {
744 : 1261336 : Node an = doFlatten(target[0]);
745 [ + + ]: 1261336 : if (an == target[0])
746 : : {
747 : 1251507 : return false;
748 : : }
749 [ + - ]: 9829 : if (an != target[1])
750 : : {
751 : 9829 : transEq = an.eqNode(target[1]);
752 : 9829 : vcs.push_back(transEq);
753 : : }
754 : 9829 : pic.d_id = id;
755 [ + + ]: 1261336 : }
756 [ + + ]: 2936324 : else if (id == RewriteProofStatus::THEORY_REWRITE)
757 : : {
758 : 1188448 : ProofRewriteRule prid = d_env.getRewriter()->findRule(
759 : : target[0], target[1], theory::TheoryRewriteCtx::DSL_SUBCALL);
760 [ + + ]: 1188448 : if (prid == ProofRewriteRule::NONE)
761 : : {
762 : 1186082 : return false;
763 : : }
764 : 2366 : pic.d_id = id;
765 : 2366 : pic.d_dslId = prid;
766 : : }
767 : : else
768 : : {
769 [ - + ][ - + ]: 1747876 : Assert(id == RewriteProofStatus::DSL);
[ - - ]
770 : 1747876 : const RewriteProofRule& rpr = d_db->getRule(r);
771 : : // does it conclusion match what we are trying to show?
772 : 1747876 : Node conc = rpr.getConclusion();
773 [ + - ][ + - ]: 1747876 : Assert(conc.getKind() == Kind::EQUAL && target.getKind() == Kind::EQUAL);
[ - + ][ - + ]
[ - - ]
774 : : // get rule conclusion, which may incorporate fixed point semantics when
775 : : // doFixedPoint is true. This stores the rule for the conclusion in pic,
776 : : // which is either r or RewriteProofStatus::TRANS.
777 : 1747876 : Node stgt = getRuleConclusion(rpr, vars, subs, pic, doFixedPoint);
778 [ + - ][ - + ]: 1747876 : Trace("rpc-debug2") << " RHS: " << conc[1] << std::endl;
[ - - ]
779 [ + - ]: 1747876 : Trace("rpc-debug2") << "Substituted RHS: " << stgt << std::endl;
780 [ + - ][ - + ]: 1747876 : Trace("rpc-debug2") << " Target RHS: " << target[1] << std::endl;
[ - - ]
781 : : // check if conclusion is null
782 [ + + ]: 1747876 : if (stgt.isNull())
783 : : {
784 : : // this is likely due to not finding a null terminator for a gradual
785 : : // type term
786 [ + - ]: 232 : Trace("rpc-debug2") << "...fail (no construct conclusion)" << std::endl;
787 : 232 : return false;
788 : : }
789 [ + + ]: 1747644 : if (expr::hasBoundVar(stgt))
790 : : {
791 : 136463 : rpr.getConditionalDefinitions(vars, subs, impliedVs, impliedSs);
792 [ + - ]: 272926 : Trace("rpc-debug2") << " Implied definitions: " << impliedVs << " -> "
793 : 136463 : << impliedSs << std::endl;
794 [ + + ]: 136463 : if (!impliedVs.empty())
795 : : {
796 : : // evaluate them
797 [ + + ]: 127363 : for (Node& s : impliedSs)
798 : : {
799 : 75406 : s = evaluate(s, {}, {});
800 : : }
801 : 51957 : stgt = expr::narySubstitute(stgt, impliedVs, impliedSs);
802 [ + - ]: 103914 : Trace("rpc-debug2") << " Implied definitions (post-eval): " << impliedVs
803 : 51957 : << " -> " << impliedSs << std::endl;
804 [ + - ]: 103914 : Trace("rpc-debug2")
805 : 51957 : << "Substituted RHS (post-eval): " << stgt << std::endl;
806 : : }
807 : : }
808 : : // inflection substitution, used if conclusion does not exactly match
809 : 1747644 : std::unordered_map<Node, std::pair<Node, Node>> isubs;
810 [ + + ]: 1747644 : if (stgt != target[1])
811 : : {
812 [ - + ]: 1424131 : if (!doInflectMatch)
813 : : {
814 [ - - ]: 0 : Trace("rpc-debug2") << "...fail (no inflection)" << std::endl;
815 : 0 : return false;
816 : : }
817 : : // The conclusion term may actually change type. Note that we must rewrite
818 : : // the terms, since they may involve operators with abstract type that
819 : : // evaluate to terms with concrete types.
820 [ + + ]: 4272393 : if (!rewriteConcrete(stgt).getType().isComparableTo(
821 : 2848262 : rewriteConcrete(target[1]).getType()))
822 : : {
823 [ + - ]: 1010 : Trace("rpc-debug2") << "...fail (types)" << std::endl;
824 : 1010 : return false;
825 : : }
826 : : // the missing transitivity link is a subgoal to prove
827 : 1423121 : transEq = stgt.eqNode(target[1]);
828 [ + - ]: 1423121 : Trace("rpc-debug2") << " Try transitive with " << transEq << std::endl;
829 : : }
830 : : // do its conditions hold?
831 : : // Get the conditions, substituted { vars -> subs } and with side conditions
832 : : // evaluated.
833 [ + + ]: 1746634 : if (!impliedVs.empty())
834 : : {
835 : 51957 : std::vector<Node> vsall = vars;
836 : 51957 : std::vector<Node> subsall = subs;
837 : 51957 : vsall.insert(vsall.end(), impliedVs.begin(), impliedVs.end());
838 : 51957 : subsall.insert(subsall.end(), impliedSs.begin(), impliedSs.end());
839 [ - + ]: 51957 : if (!rpr.getObligations(vsall, subsall, vcs))
840 : : {
841 : : // cannot get conditions, likely due to failed side condition
842 [ - - ]: 0 : Trace("rpc-debug2") << "...fail (obligations)" << std::endl;
843 : 0 : return false;
844 : : }
845 [ + - ][ + - ]: 51957 : }
846 [ - + ]: 1694677 : else if (!rpr.getObligations(vars, subs, vcs))
847 : : {
848 : : // cannot get conditions, likely due to failed side condition
849 [ - - ]: 0 : Trace("rpc-debug2") << "...fail (obligations)" << std::endl;
850 : 0 : return false;
851 : : }
852 : : // Prove transitive equality last. We choose this order since the
853 : : // transitive equality is expected to be the hardest to prove. Also, the
854 : : // conditions may guard instances where the RHS is not well typed (e.g.
855 : : // bv-eq-extract-elim1,2,3).
856 [ + + ]: 1746634 : if (!transEq.isNull())
857 : : {
858 : 1423121 : vcs.push_back(transEq);
859 : : }
860 [ + + ][ + + ]: 1750128 : }
[ + + ]
861 : : // First, check which premises are non-trivial, and if there is a trivial
862 : : // failure. Those that are non-trivial are added to condToProve.
863 : 3145624 : std::vector<Node> condToProve;
864 [ + + ]: 4621786 : for (const Node& cond : vcs)
865 : : {
866 [ - + ][ - + ]: 3068346 : Assert(cond.getKind() == Kind::EQUAL);
[ - - ]
867 : : // substitute to get the condition-to-prove
868 : : RewriteProofStatus cid;
869 : : // check whether condition is already known to hold or not hold
870 [ + + ]: 3068346 : if (proveInternalBase(cond, cid))
871 : : {
872 [ + + ]: 1076011 : if (cid == RewriteProofStatus::FAIL)
873 : : {
874 : : // does not hold, we fail
875 [ + - ]: 1767000 : Trace("rpc-debug2") << "...fail (simple condition failure for " << cond
876 : 883500 : << ")" << std::endl;
877 : 1592184 : return false;
878 : : }
879 : : // already holds, continue
880 : 192511 : continue;
881 : : }
882 [ + + ][ + + ]: 1992335 : if (!doRecurse || (decRecLimit && d_currRecLimit == 0))
[ + + ]
883 : : {
884 : 708684 : d_currFailResource = true;
885 : : // we can't apply recursion, return false
886 [ + - ]: 708684 : Trace("rpc-debug2") << "...fail (recursion limit)" << std::endl;
887 : 708684 : return false;
888 : : }
889 : : // save, to check below
890 : 1283651 : condToProve.push_back(cond);
891 : : }
892 : : // if we have any sub-conditions to prove, we require decrementing the
893 : : // recursion limit
894 [ + + ]: 1553440 : if (!condToProve.empty())
895 : : {
896 : : // we could only add condToProve if d_currRecLimit>0 above.
897 [ + + ][ + - ]: 1018450 : Assert(!decRecLimit || d_currRecLimit > 0);
[ - + ][ - + ]
[ - - ]
898 [ + + ]: 1018450 : if (decRecLimit)
899 : : {
900 : 816184 : d_currRecLimit--;
901 [ + + ]: 816184 : if (d_currStepLimit == 0)
902 : : {
903 : 42 : d_currFailResource = true;
904 : 42 : return false;
905 : : }
906 : 816142 : d_currStepLimit--;
907 : : }
908 [ + - ]: 2036816 : Trace("rpc-debug") << "Recurse rule "
909 [ - - ]: 1018408 : << (id == RewriteProofStatus::DSL ? toString(r)
910 : 0 : : toString(id))
911 : 1018408 : << std::endl;
912 : 1018408 : bool recSuccess = true;
913 : : // if no trivial failures, go back and try to recursively prove
914 [ + + ]: 1166659 : for (const Node& cond : condToProve)
915 : : {
916 [ + - ]: 1022543 : Trace("rpc-infer-sc") << "Check condition: " << cond << std::endl;
917 : : // recursively check if the condition holds
918 : 1022543 : RewriteProofStatus cid = proveInternal(cond);
919 [ + + ]: 1022543 : if (cid == RewriteProofStatus::FAIL)
920 : : {
921 : : // print reason for failure
922 [ + - ]: 1748584 : Trace("rpc-infer-debug")
923 : 874292 : << "required: " << cond << " for " << id << std::endl;
924 : 874292 : recSuccess = false;
925 : 874292 : break;
926 : : }
927 : : }
928 [ + + ]: 1018408 : if (decRecLimit)
929 : : {
930 : 816142 : d_currRecLimit++;
931 : : }
932 [ + + ]: 1018408 : if (!recSuccess)
933 : : {
934 : 874292 : return false;
935 : : }
936 : : }
937 : : // successfully found instance of rule
938 [ - + ]: 679106 : if (TraceIsOn("rpc-infer"))
939 : : {
940 [ - - ]: 0 : Trace("rpc-infer") << "INFER " << target << " by " << id
941 [ - - ]: 0 : << (transEq.isNull() ? "" : " + TRANS") << std::endl;
942 : : }
943 : : // cache the success
944 : 679106 : ProvenInfo* pi = &d_pcache[target];
945 [ + + ]: 679106 : if (!transEq.isNull())
946 : : {
947 [ + - ]: 86012 : Trace("rpc-debug2") << "..." << target << " proved by TRANS" << std::endl;
948 : 172024 : Node transEqStart = target[0].eqNode(transEq[0]);
949 : : // proves both
950 : 86012 : pi->d_id = RewriteProofStatus::TRANS;
951 : 86012 : pi->d_vars.clear();
952 : 86012 : pi->d_vars.push_back(transEqStart);
953 : 86012 : pi->d_vars.push_back(transEq);
954 [ + - ]: 172024 : Trace("rpc-debug2") << "...original equality was " << transEqStart
955 : 86012 : << std::endl;
956 : : // we also prove the original
957 : 86012 : pi = &d_pcache[transEqStart];
958 : 86012 : }
959 : 679106 : pi->d_id = pic.d_id;
960 : 679106 : pi->d_dslId = pic.d_dslId;
961 [ + + ]: 679106 : if (pic.isInternalRule())
962 : : {
963 : 317974 : pi->d_vars = pic.d_vars;
964 : : }
965 : : else
966 : : {
967 : 361132 : pi->d_vars = vars;
968 : 361132 : pi->d_subs = subs;
969 [ + + ]: 361132 : if (!impliedVs.empty())
970 : : {
971 : 2196 : pi->d_vars.insert(pi->d_vars.end(), impliedVs.begin(), impliedVs.end());
972 : 2196 : pi->d_subs.insert(pi->d_subs.end(), impliedSs.begin(), impliedSs.end());
973 : : }
974 : : }
975 [ + - ]: 1358212 : Trace("rpc-debug2") << "...target proved by " << d_pcache[target].d_id
976 : 679106 : << std::endl;
977 : : // success
978 : 679106 : return true;
979 : 12616666 : }
980 : :
981 : 3594634 : bool RewriteDbProofCons::proveInternalBase(const Node& eqi,
982 : : RewriteProofStatus& idb)
983 : : {
984 [ + - ]: 3594634 : Trace("rpc-debug2") << "Prove internal base: " << eqi << "?" << std::endl;
985 [ - + ][ - + ]: 3594634 : Assert(eqi.getKind() == Kind::EQUAL);
[ - - ]
986 : : // if we are currently trying to prove this, fail
987 [ + + ]: 3594634 : if (d_currProving.find(eqi) != d_currProving.end())
988 : : {
989 [ + - ]: 482885 : Trace("rpc-debug2") << "...fail (already proving)" << std::endl;
990 : 482885 : idb = RewriteProofStatus::FAIL;
991 : 482885 : return true;
992 : : }
993 : : // already cached?
994 : 3111749 : std::unordered_map<Node, ProvenInfo>::iterator it = d_pcache.find(eqi);
995 [ + + ]: 3111749 : if (it != d_pcache.end())
996 : : {
997 [ + + ]: 826130 : if (it->second.d_id != RewriteProofStatus::FAIL)
998 : : {
999 : : // proof exists, return
1000 : 130690 : idb = it->second.d_id;
1001 [ + - ]: 130690 : Trace("rpc-debug2") << "...success, already exists" << std::endl;
1002 : 130690 : return true;
1003 : : }
1004 [ + + ]: 695440 : if (it->second.d_failMaxDepth == -1)
1005 : : {
1006 : 147620 : idb = it->second.d_id;
1007 [ + - ]: 147620 : Trace("rpc-debug2") << "...fail (depth independent)" << std::endl;
1008 : 147620 : return true;
1009 : : }
1010 [ + + ]: 547820 : if (d_currRecLimit <= it->second.d_failMaxDepth)
1011 : : {
1012 : 42754 : idb = it->second.d_id;
1013 [ + - ]: 42754 : Trace("rpc-debug2") << "...fail (at higher depth)" << std::endl;
1014 : 42754 : return true;
1015 : : }
1016 [ + - ]: 505066 : Trace("rpc-debug2") << "...unknown (already fail)" << std::endl;
1017 : : // Will not succeed below, since we know we've already tried. Hence, we
1018 : : // are in a situation where we have yet to succeed to prove eqi for some
1019 : : // depth, but we are currently trying at a higher maximum depth.
1020 : 505066 : return false;
1021 : : }
1022 : : // reflexivity, applied potentially to non-Booleans
1023 [ + + ]: 2285619 : if (eqi[0] == eqi[1])
1024 : : {
1025 : 28235 : ProvenInfo& pi = d_pcache[eqi];
1026 : 28235 : idb = RewriteProofStatus::REFL;
1027 : 28235 : pi.d_id = idb;
1028 [ + - ]: 28235 : Trace("rpc-debug2") << "...success, refl" << std::endl;
1029 : 28235 : return true;
1030 : : }
1031 : : // non-well-typed equalities cannot be proven
1032 : : // also, variables cannot be rewritten
1033 [ + + ][ - - ]: 2257384 : if (eqi.getTypeOrNull().isNull()
1034 : 2257384 : || (eqi[0].isVar() && !eqi[0].getTypeOrNull().isBoolean()))
1035 : : {
1036 [ + - ]: 118100 : Trace("rpc-debug2") << "...fail ("
1037 [ - - ][ - + ]: 59050 : << (eqi[0].isVar() ? "variable" : "ill-typed") << ")"
[ - - ]
1038 : 59050 : << std::endl;
1039 : 59050 : ProvenInfo& pi = d_pcache[eqi];
1040 : 59050 : idb = RewriteProofStatus::FAIL;
1041 : 59050 : pi.d_failMaxDepth = -1;
1042 : 59050 : pi.d_id = idb;
1043 : 59050 : return true;
1044 : : }
1045 : : // evaluate the two sides of the equality, without help of the rewriter
1046 [ + + ]: 13190004 : Node ev[2];
1047 : 2198334 : bool evalSuccess = true;
1048 [ + + ]: 2401654 : for (size_t i = 0; i < 2; i++)
1049 : : {
1050 : 2348138 : ev[i] = doEvaluate(eqi[i]);
1051 [ + - ][ - + ]: 4696276 : Trace("rpc-debug2") << "...evaluate " << eqi[i] << " to " << ev[i]
[ - - ]
1052 : 2348138 : << std::endl;
1053 [ + + ]: 2348138 : if (ev[i].isNull())
1054 : : {
1055 : : // does not evaluate
1056 : : // If it rewrites to false, then it is obviously infeasible. Notice that
1057 : : // rewriting is more expensive than evaluation, so we do it as a second
1058 : : // resort.
1059 [ + + ]: 2144818 : Node lhs = i == 1 ? ev[0] : eqi[0];
1060 : 2144818 : Node eq = lhs.eqNode(eqi[1]);
1061 : :
1062 [ - + ]: 2144818 : if (eq.getTypeOrNull().isNull())
1063 : : {
1064 : 0 : ProvenInfo& pi = d_pcache[eqi];
1065 : 0 : idb = RewriteProofStatus::FAIL;
1066 : 0 : pi.d_failMaxDepth = -1;
1067 : 0 : pi.d_id = idb;
1068 [ - - ]: 0 : Trace("rpc-debug2") << "...fail, ill-typed equality" << std::endl;
1069 : 0 : return true;
1070 : : }
1071 : 2144818 : Node eqr = rewriteConcrete(eq);
1072 [ + + ]: 2144818 : if (eqr.isConst())
1073 : : {
1074 : : // definitely not true
1075 [ + + ]: 1133029 : if (!eqr.getConst<bool>())
1076 : : {
1077 : 42642 : ProvenInfo& pi = d_pcache[eqi];
1078 [ + - ][ - - ]: 85284 : Trace("rpc-debug2") << "fail, infeasible due to rewriting: " << eqi[0]
1079 [ - + ][ - + ]: 42642 : << " == " << eqi[1] << std::endl;
[ - - ]
1080 : 42642 : idb = RewriteProofStatus::FAIL;
1081 : 42642 : pi.d_failMaxDepth = -1;
1082 : 42642 : pi.d_id = idb;
1083 : 42642 : return true;
1084 : : }
1085 : : // NOTE: if eqr does not rewrite to true, it still could be true, hence
1086 : : // we fail
1087 : : }
1088 : 2102176 : evalSuccess = false;
1089 : 2102176 : break;
1090 [ + + ][ + + ]: 6434454 : }
[ + + ]
1091 : : }
1092 [ + + ]: 2155692 : if (evalSuccess)
1093 : : {
1094 : 53516 : ProvenInfo& pi = d_pcache[eqi];
1095 : : // we can evaluate both sides, check to see if the values are the same
1096 [ + + ]: 53516 : if (ev[0] == ev[1])
1097 : : {
1098 [ + - ]: 35476 : Trace("rpc-debug2") << "...success, eval" << std::endl;
1099 : 35476 : idb = RewriteProofStatus::EVAL;
1100 : : }
1101 : : else
1102 : : {
1103 [ + - ]: 36080 : Trace("rpc-debug2") << "...fail (eval " << ev[0] << " and " << ev[1]
1104 : 18040 : << ")" << std::endl;
1105 : 18040 : idb = RewriteProofStatus::FAIL;
1106 : : // failure relies on nothing, depth is 0
1107 : 18040 : pi.d_failMaxDepth = -1;
1108 : : }
1109 : : // cache it
1110 : 53516 : pi.d_id = idb;
1111 : 53516 : return true;
1112 : : }
1113 [ + + ]: 2102176 : if (eqi[0].isConst())
1114 : : {
1115 [ + - ]: 90642 : Trace("rpc-debug2") << "...fail (constant head)" << std::endl;
1116 : 90642 : ProvenInfo& pi = d_pcache[eqi];
1117 : 90642 : idb = RewriteProofStatus::FAIL;
1118 : 90642 : pi.d_failMaxDepth = -1;
1119 : 90642 : pi.d_id = idb;
1120 : 90642 : return true;
1121 : : }
1122 [ + - ]: 2011534 : Trace("rpc-debug2") << "...unknown (default)" << std::endl;
1123 : : // otherwise, we fail to either prove or disprove the equality
1124 : 2011534 : return false;
1125 [ + + ][ - - ]: 6595002 : }
1126 : :
1127 : 452480 : bool RewriteDbProofCons::ensureProofInternal(CDProof* cdp, const Node& eqi)
1128 : : {
1129 : : // note we could use single internal cdp to improve subproof sharing
1130 : 452480 : NodeManager* nm = nodeManager();
1131 : 452480 : std::unordered_map<TNode, bool> visited;
1132 : 452480 : std::unordered_map<TNode, std::vector<Node>> premises;
1133 : 452480 : std::unordered_map<TNode, std::vector<Node>> pfArgs;
1134 : 452480 : std::unordered_map<TNode, bool>::iterator it;
1135 : : bool inserted;
1136 : 452480 : std::unordered_map<Node, ProvenInfo>::iterator itd;
1137 : 452480 : std::vector<Node>::iterator itv;
1138 : 452480 : std::vector<TNode> visit;
1139 : 452480 : TNode cur;
1140 : 452480 : visit.push_back(eqi);
1141 : : do
1142 : : {
1143 : 1619131 : cur = visit.back();
1144 : 1619131 : visit.pop_back();
1145 : 1619131 : std::tie(it, inserted) = visited.emplace(cur, false);
1146 : 1619131 : itd = d_pcache.find(cur);
1147 [ - + ][ - + ]: 1619131 : Assert(itd != d_pcache.end());
[ - - ]
1148 : 1619131 : ProvenInfo& pcur = itd->second;
1149 [ - + ][ - + ]: 1619131 : Assert(cur.getKind() == Kind::EQUAL);
[ - - ]
1150 [ + + ]: 1619131 : if (inserted)
1151 : : {
1152 [ + - ]: 808969 : Trace("rpc-debug") << "Ensure proof for " << cur << std::endl;
1153 : 808969 : visit.push_back(cur);
1154 : : // may already have a proof rule from a previous call
1155 [ + + ]: 808969 : if (cdp->hasStep(cur))
1156 : : {
1157 : 98 : it->second = true;
1158 [ + - ]: 98 : Trace("rpc-debug") << "...already proven" << std::endl;
1159 : : }
1160 : : else
1161 : : {
1162 [ - + ][ - + ]: 808871 : Assert(pcur.d_id != RewriteProofStatus::FAIL);
[ - - ]
1163 [ + - ]: 808871 : Trace("rpc-debug") << "...proved via " << pcur.d_id << std::endl;
1164 [ + + ]: 808871 : if (pcur.d_id == RewriteProofStatus::REFL)
1165 : : {
1166 : 13199 : it->second = true;
1167 : : // trivial proof
1168 [ - + ][ - + ]: 13199 : Assert(cur[0] == cur[1]);
[ - - ]
1169 : 26398 : cdp->addStep(cur, ProofRule::REFL, {}, {cur[0]});
1170 : : }
1171 [ + + ]: 795672 : else if (pcur.d_id == RewriteProofStatus::EVAL)
1172 : : {
1173 : 20063 : it->second = true;
1174 : : // NOTE: this could just evaluate the equality itself
1175 [ - + ][ - + ]: 20063 : Assert(cur.getKind() == Kind::EQUAL);
[ - - ]
1176 : 20063 : std::vector<Node> transc;
1177 [ + + ]: 60189 : for (size_t i = 0; i < 2; ++i)
1178 : : {
1179 : 80252 : Node curv = doEvaluate(cur[i]);
1180 [ + + ]: 40126 : if (curv == cur[i])
1181 : : {
1182 : 17494 : continue;
1183 : : }
1184 : 22632 : Node eq = cur[i].eqNode(curv);
1185 : : // flip orientation for second child
1186 [ + + ][ + + ]: 22632 : transc.push_back(i == 1 ? curv.eqNode(cur[i]) : eq);
[ - - ]
1187 : : // trivial evaluation, add evaluation method id
1188 : 45264 : cdp->addStep(eq, ProofRule::EVALUATE, {}, {cur[i]});
1189 [ + + ]: 40126 : }
1190 [ + + ]: 20063 : if (transc.size() == 2)
1191 : : {
1192 : : // do transitivity if both sides evaluate
1193 : 2569 : cdp->addStep(cur, ProofRule::TRANS, transc, {});
1194 : : }
1195 : 20063 : }
1196 : : else
1197 : : {
1198 : 775609 : std::vector<Node>& ps = premises[cur];
1199 : 775609 : std::vector<Node>& pfac = pfArgs[cur];
1200 [ + + ]: 775609 : if (pcur.isInternalRule())
1201 : : {
1202 : : // premises are the steps, stored in d_vars
1203 : 487869 : ps.insert(ps.end(), pcur.d_vars.begin(), pcur.d_vars.end());
1204 : : }
1205 : : else
1206 : : {
1207 [ - + ][ - + ]: 287740 : Assert(cur.getKind() == Kind::EQUAL);
[ - - ]
1208 [ - + ][ - + ]: 287740 : Assert(pcur.d_dslId != ProofRewriteRule::NONE);
[ - - ]
1209 : : // add the DSL proof rule we used
1210 : 287740 : pfac.push_back(
1211 : 575480 : nm->mkConstInt(Rational(static_cast<uint32_t>(pcur.d_dslId))));
1212 [ + + ]: 287740 : if (pcur.d_id == RewriteProofStatus::DSL)
1213 : : {
1214 : 286141 : const RewriteProofRule& rpr = d_db->getRule(pcur.d_dslId);
1215 : : // compute premises based on the used substitution
1216 : : // build the substitution context
1217 : 286141 : const std::vector<Node>& vs = rpr.getVarList();
1218 [ - + ][ - + ]: 286141 : Assert(pcur.d_vars.size() == vs.size());
[ - - ]
1219 : 286141 : std::vector<Node> rsubs;
1220 : : // must order the variables to match order of rewrite rule
1221 [ + + ]: 822983 : for (const Node& v : vs)
1222 : : {
1223 : 536842 : itv = std::find(pcur.d_vars.begin(), pcur.d_vars.end(), v);
1224 : 536842 : size_t d = std::distance(pcur.d_vars.begin(), itv);
1225 [ - + ][ - + ]: 536842 : Assert(d < pcur.d_subs.size());
[ - - ]
1226 : 536842 : rsubs.push_back(pcur.d_subs[d]);
1227 : : }
1228 : : // get the conditions, store into premises of cur.
1229 [ - + ]: 286141 : if (!rpr.getObligations(vs, rsubs, ps))
1230 : : {
1231 : 0 : DebugUnhandled() << "failed a side condition?";
1232 : : return false;
1233 : : }
1234 : 286141 : pfac.insert(pfac.end(), rsubs.begin(), rsubs.end());
1235 [ + - ]: 286141 : }
1236 : : else
1237 : : {
1238 [ - + ][ - + ]: 1599 : Assert(pcur.d_id == RewriteProofStatus::THEORY_REWRITE);
[ - - ]
1239 : 1599 : pfac.push_back(cur);
1240 : : }
1241 : : }
1242 : : // recurse on premises
1243 : 775609 : visit.insert(visit.end(), ps.begin(), ps.end());
1244 : : }
1245 : : }
1246 : : }
1247 [ + + ]: 810162 : else if (!it->second)
1248 : : {
1249 : : // Now, add the proof rule. We do this after its children proofs already
1250 : : // exist.
1251 : 775609 : it->second = true;
1252 [ - + ][ - + ]: 775609 : Assert(premises.find(cur) != premises.end());
[ - - ]
1253 : 775609 : std::vector<Node>& ps = premises[cur];
1254 : : // get the conclusion
1255 : 775609 : Node conc;
1256 : 775609 : RewriteProofStatus status = pcur.d_id;
1257 [ + + ]: 775609 : if (status == RewriteProofStatus::FLATTEN)
1258 : : {
1259 : 864 : Kind ck = cur[0].getKind();
1260 [ - + ]: 1462 : status = (ck == Kind::ADD || ck == Kind::NONLINEAR_MULT)
1261 [ + + ]: 1462 : ? RewriteProofStatus::ARITH_POLY_NORM
1262 : : : RewriteProofStatus::ACI_NORM;
1263 : : }
1264 [ + + ]: 775609 : if (status == RewriteProofStatus::TRANS)
1265 : : {
1266 : 85901 : conc = ps[0][0].eqNode(ps.back()[1]);
1267 : 85901 : cdp->addStep(conc, ProofRule::TRANS, ps, {});
1268 : : }
1269 [ + + ]: 689708 : else if (status == RewriteProofStatus::CONG)
1270 : : {
1271 : : // get the appropriate CONG rule
1272 : 33196 : std::vector<Node> cargs;
1273 : 33196 : ProofRule cr = expr::getCongRule(cur[0], cargs);
1274 : 33196 : cdp->addStep(cur, cr, ps, cargs);
1275 : 33196 : }
1276 [ + + ]: 656512 : else if (status == RewriteProofStatus::CONG_EVAL)
1277 : : {
1278 : : // congruence + evaluation, given we are trying to prove
1279 : : // (f t1 ... tn) == c
1280 : : // This tactic checks if t1 ... tn rewrite to constants c1 ... cn.
1281 : : // If so, we try to show subgoals
1282 : : // t1 == c1 ... tn == cn
1283 : : // The final proof is a congruence step + evaluation:
1284 : : // (f t1 ... tn) == (f c1 ... cn) == c.
1285 : 1563 : Node lhs = cur[0];
1286 : 1563 : std::vector<Node> lhsTgtc;
1287 [ + + ]: 1563 : if (cur[0].getMetaKind() == metakind::PARAMETERIZED)
1288 : : {
1289 : 78 : lhsTgtc.push_back(cur[0].getOperator());
1290 : : }
1291 [ + + ]: 4592 : for (const Node& eq : pcur.d_vars)
1292 : : {
1293 [ - + ][ - + ]: 3029 : Assert(eq.getKind() == Kind::EQUAL);
[ - - ]
1294 : 3029 : lhsTgtc.push_back(eq[1]);
1295 : : }
1296 : 1563 : Node lhsTgt = nm->mkNode(cur[0].getKind(), lhsTgtc);
1297 : 3126 : Node rhs = doEvaluate(cur[1]);
1298 [ - + ][ - + ]: 1563 : Assert(!rhs.isNull());
[ - - ]
1299 : 1563 : Node eq1 = lhs.eqNode(lhsTgt);
1300 : 1563 : Node eq2 = lhsTgt.eqNode(rhs);
1301 : 6252 : std::vector<Node> transChildren = {eq1, eq2};
1302 : : // get the appropriate CONG rule
1303 : 1563 : std::vector<Node> cargs;
1304 : 1563 : ProofRule cr = expr::getCongRule(eq1[0], cargs);
1305 : 1563 : cdp->addStep(eq1, cr, ps, cargs);
1306 : 3126 : cdp->addStep(eq2, ProofRule::EVALUATE, {}, {lhsTgt});
1307 [ - + ]: 1563 : if (rhs != cur[1])
1308 : : {
1309 : 0 : cdp->addStep(cur[1].eqNode(rhs), ProofRule::EVALUATE, {}, {cur[1]});
1310 : 0 : transChildren.push_back(rhs.eqNode(cur[1]));
1311 : : }
1312 : 1563 : cdp->addStep(cur, ProofRule::TRANS, transChildren, {});
1313 : 1563 : }
1314 [ + + ]: 654949 : else if (status == RewriteProofStatus::TRUE_ELIM)
1315 : : {
1316 : 15139 : conc = ps[0][0];
1317 : 15139 : cdp->addStep(conc, ProofRule::TRUE_ELIM, ps, {});
1318 : : }
1319 [ + + ]: 639810 : else if (status == RewriteProofStatus::TRUE_INTRO)
1320 : : {
1321 : 14197 : conc = ps[0].eqNode(d_true);
1322 : 14197 : cdp->addStep(conc, ProofRule::TRUE_INTRO, ps, {});
1323 : : }
1324 [ + + ]: 625613 : else if (status == RewriteProofStatus::ABSORB)
1325 : : {
1326 : 28632 : cdp->addStep(cur, ProofRule::ABSORB, {}, {cur});
1327 : : }
1328 [ + + ]: 611297 : else if (status == RewriteProofStatus::ACI_NORM)
1329 : : {
1330 : 151734 : cdp->addStep(cur, ProofRule::ACI_NORM, {}, {cur});
1331 : : }
1332 [ + + ]: 535430 : else if (status == RewriteProofStatus::ARITH_POLY_NORM)
1333 : : {
1334 : : TypeNode tn =
1335 : 414731 : pcur.d_vars.empty() ? cur[0].getType() : cur[0][0].getType();
1336 : 245487 : bool isBitVec = (tn.isBitVector());
1337 : 245487 : ProofRule pr =
1338 [ + + ]: 245487 : isBitVec ? ProofRule::BV_POLY_NORM : ProofRule::ARITH_POLY_NORM;
1339 [ + + ]: 245487 : if (pcur.d_vars.empty())
1340 : : {
1341 : 321730 : cdp->addStep(cur, pr, {}, {cur});
1342 : : }
1343 : : else
1344 : : {
1345 [ + + ]: 84622 : ProofRule prr = isBitVec ? ProofRule::BV_POLY_NORM_EQ
1346 : : : ProofRule::ARITH_POLY_NORM_REL;
1347 : 169244 : cdp->addStep(pcur.d_vars[0], pr, {}, {pcur.d_vars[0]});
1348 : 253866 : cdp->addStep(cur, prr, {pcur.d_vars[0]}, {cur});
1349 : : }
1350 : 245487 : }
1351 [ + + ]: 289943 : else if (status == RewriteProofStatus::DSL_FIXED_POINT)
1352 : : {
1353 : 2203 : const RewriteProofRule& rpr = d_db->getRule(pcur.d_dslId);
1354 : 2203 : const std::vector<size_t>& path = rpr.getPathToContextVar();
1355 : : // We only want to rewrite on the relevant path. So for example
1356 : : // if our context is lambda x. (or C x), then we only apply
1357 : : // rewrites on the path that traverses the second child of
1358 : : // ors, recurisvely.
1359 : 2203 : bool emptyPath = path.empty();
1360 : 2203 : WithinPathTermContext wptc(path);
1361 : : TConvProofGenerator tcpg(d_env,
1362 : : nullptr,
1363 : : TConvPolicy::FIXPOINT,
1364 : : TConvCachePolicy::NEVER,
1365 : : "DslFixedPointTConv",
1366 [ + + ]: 4406 : emptyPath ? nullptr : &wptc);
1367 [ + - ]: 4406 : Trace("rpc-debug") << "Prove fixed point " << pcur.d_dslId
1368 : 2203 : << " via:" << std::endl;
1369 [ + - ]: 2203 : Trace("rpc-debug") << "- path size is " << path.size() << std::endl;
1370 [ + - ]: 2203 : Trace("rpc-debug") << "- conclusion: " << cur << std::endl;
1371 : 2203 : size_t tc = 1;
1372 [ + + ]: 10146 : for (const Node& s : pcur.d_vars)
1373 : : {
1374 [ + - ]: 7943 : Trace("rpc-debug") << " - step: " << s << std::endl;
1375 : : // Fixed-point steps are an explicit rewrite chain. Register them as
1376 : : // pre-rewrites so they are applied in the recorded order before
1377 : : // child rewriting changes the current redex.
1378 [ + + ][ + - ]: 7943 : tcpg.addRewriteStep(
1379 : : s[0], s[1], cdp, true, TrustId::NONE, false, emptyPath ? 0 : tc);
1380 : : // the next rewrite should be applied at the depth that adds the
1381 : : // length of the path.
1382 : 7943 : tc += path.size();
1383 : : }
1384 : 2203 : std::shared_ptr<ProofNode> pfn = tcpg.getProofFor(cur);
1385 [ - + ][ - + ]: 2203 : Assert(pfn != nullptr);
[ - - ]
1386 : 2203 : cdp->addProof(pfn);
1387 : 2203 : }
1388 [ + + ]: 287740 : else if (status == RewriteProofStatus::DSL
1389 [ + - ]: 1599 : || status == RewriteProofStatus::THEORY_REWRITE)
1390 : : {
1391 [ - + ][ - + ]: 287740 : Assert(pfArgs.find(cur) != pfArgs.end());
[ - - ]
1392 [ - + ][ - + ]: 287740 : Assert(pcur.d_dslId != ProofRewriteRule::NONE);
[ - - ]
1393 : 287740 : const std::vector<Node>& args = pfArgs[cur];
1394 : : ProofRule pfr;
1395 [ + + ]: 287740 : if (status == RewriteProofStatus::DSL)
1396 : : {
1397 : 286141 : std::vector<Node> subs(args.begin() + 1, args.end());
1398 : 286141 : const RewriteProofRule& rpr = d_db->getRule(pcur.d_dslId);
1399 : 286141 : conc = rpr.getConclusionFor(subs);
1400 [ + - ]: 286141 : Trace("rpc-debug") << "Finalize proof for " << cur << std::endl;
1401 [ + - ]: 286141 : Trace("rpc-debug") << "Proved: " << cur << std::endl;
1402 [ + - ]: 286141 : Trace("rpc-debug") << "From: " << conc << std::endl;
1403 : 286141 : pfr = ProofRule::DSL_REWRITE;
1404 : 286141 : cdp->addStep(conc, pfr, ps, args);
1405 : 286141 : }
1406 : : else
1407 : : {
1408 [ - + ][ - + ]: 1599 : Assert(status == RewriteProofStatus::THEORY_REWRITE);
[ - - ]
1409 : : // Use the utility, possibly to do macro expansion.
1410 : : // We use a fresh CDProof to avoid duplicate substeps.
1411 : 3198 : CDProof cdpt(d_env);
1412 : 1599 : d_trrc.ensureProofForTheoryRewrite(&cdpt, pcur.d_dslId, cur);
1413 : 1599 : cdp->addProof(cdpt.getProofFor(cur));
1414 : 1599 : }
1415 : : }
1416 : 775609 : }
1417 [ + + ]: 1619131 : } while (!visit.empty());
1418 : 452480 : return true;
1419 : 452480 : }
1420 : :
1421 : 3960791 : Node RewriteDbProofCons::doEvaluate(const Node& n)
1422 : : {
1423 : : // Only possible to evaluate if we rewrite to a constant. This is worthwhile
1424 : : // to check since the rewrite of n has likely already been computed, whereas
1425 : : // the evaluator below is not (globally) cached. We can do this optimization
1426 : : // only if the term does not contain abstract subterms, which should not be
1427 : : // sent to the rewriter.
1428 [ + + ]: 3960791 : if (!expr::hasAbstractSubterm(n))
1429 : : {
1430 : 3960595 : Node nc = rewrite(n);
1431 [ + + ]: 3960595 : if (!nc.isConst())
1432 : : {
1433 : 2507216 : return Node::null();
1434 : : }
1435 [ + + ]: 3960595 : }
1436 : 1453575 : auto [itv, inserted] = d_evalCache.emplace(n, Node());
1437 [ + + ]: 1453575 : if (inserted)
1438 : : {
1439 : 683234 : itv->second = d_eval.eval(n, {}, {});
1440 : : }
1441 : 1453575 : return itv->second;
1442 : : }
1443 : :
1444 : 1747876 : Node RewriteDbProofCons::getRuleConclusion(const RewriteProofRule& rpr,
1445 : : const std::vector<Node>& vars,
1446 : : const std::vector<Node>& subs,
1447 : : ProvenInfo& pi,
1448 : : bool doFixedPoint)
1449 : : {
1450 : 1747876 : pi.d_id = RewriteProofStatus::DSL;
1451 : 1747876 : pi.d_dslId = rpr.getId();
1452 : 1747876 : Node conc = rpr.getConclusion(true);
1453 : 1747876 : Node concRhs = conc[1];
1454 [ + - ]: 3495752 : Trace("rpc-ctx") << "***GET CONCLUSION " << pi.d_dslId << " for " << vars
1455 : 1747876 : << " -> " << subs << std::endl;
1456 : : // if fixed point, we continue applying
1457 [ + + ][ + + ]: 1747876 : if (doFixedPoint && rpr.isFixedPoint())
[ + + ]
1458 : : {
1459 [ - + ][ - + ]: 25111 : Assert(d_currFixedPointId == ProofRewriteRule::NONE);
[ - - ]
1460 [ - + ][ - + ]: 25111 : Assert(d_currFixedPointConc.isNull());
[ - - ]
1461 : 25111 : d_currFixedPointId = rpr.getId();
1462 : 25111 : Node context = rpr.getContext();
1463 [ - + ][ - + ]: 25111 : Assert(!context.isNull());
[ - - ]
1464 [ + - ]: 25111 : Trace("rpc-ctx") << "Context is " << context << std::endl;
1465 : : // check if stgt also rewrites with the same rule?
1466 : : bool continueFixedPoint;
1467 : 25111 : std::vector<Node> steps;
1468 : 25111 : std::vector<std::vector<Node>> stepsSubs;
1469 : : // start from the source, match again to start the chain. Notice this is
1470 : : // required for uniformity since we want to successfully cache the first
1471 : : // step, independent of the target.
1472 : 25111 : Node ssrc = expr::narySubstitute(conc[0], vars, subs);
1473 : 25111 : Node stgt = ssrc;
1474 : 105376 : do
1475 : : {
1476 [ + - ]: 105376 : Trace("rpc-ctx") << "Get matches " << stgt << std::endl;
1477 [ + - ]: 105376 : Trace("rpc-ctx") << "Conclusion is " << concRhs << std::endl;
1478 : 105376 : continueFixedPoint = false;
1479 : 105376 : rpr.getMatches(stgt, &d_notify);
1480 [ + - ]: 210752 : Trace("rpc-ctx") << "...conclusion is " << d_currFixedPointConc
1481 : 105376 : << std::endl;
1482 [ + + ]: 105376 : if (!d_currFixedPointConc.isNull())
1483 : : {
1484 : : // currently avoid accidental loops: arbitrarily bound to 1000
1485 : 80265 : continueFixedPoint = steps.size() <= s_fixedPointLimit;
1486 [ - + ][ - + ]: 80265 : Assert(d_currFixedPointConc.getKind() == Kind::EQUAL);
[ - - ]
1487 : 80265 : stepsSubs.emplace_back(d_currFixedPointSubs.begin(),
1488 : 80265 : d_currFixedPointSubs.end());
1489 : 80265 : stgt = d_currFixedPointConc[1];
1490 : : // For example, we have now computed
1491 : : // (str.len (str.++ x y z)) --> (+ (str.len x) (str.len (str.++ y z)))
1492 : : // where stgt is the RHS. We now want to continue to rewrite the right
1493 : : // hand side, where to find the next target term to rewrite, we match
1494 : : // the context of the rule to the RHS.
1495 : : // In particular, given a context (+ (str.len S0) ?0), we would match
1496 : : // ?0 to (str.len (str.++ y z)). This indicates that the user suggests
1497 : : // that (str.len (str.++ y z)) is the term to continue to rewrite.
1498 : : // We update stgt to this term to proceed with the loop.
1499 : 80265 : std::unordered_map<Node, Node> msubs;
1500 : 80265 : expr::match(context[1], stgt, msubs);
1501 [ + - ]: 160530 : Trace("rpc-ctx") << "Matching context " << context << " with " << stgt
1502 : 80265 : << " gives " << msubs[context[0][0]] << std::endl;
1503 : 80265 : stgt = msubs[context[0][0]];
1504 [ - + ][ - + ]: 80265 : Assert(!stgt.isNull());
[ - - ]
1505 : 80265 : steps.push_back(stgt);
1506 : 80265 : }
1507 [ + + ]: 105376 : d_currFixedPointConc = Node::null();
1508 : : } while (continueFixedPoint);
1509 : :
1510 : 25111 : Node prev = ssrc;
1511 : 25111 : Node placeholder = context[0][0];
1512 : 25111 : Node body = context[1];
1513 : 25111 : Node currConc = body;
1514 : 25111 : Node currContext = placeholder;
1515 : 25111 : std::vector<Node> rews;
1516 [ + + ]: 105376 : for (size_t i = 0, size = steps.size(); i < size; ++i)
1517 : : {
1518 : 80265 : const std::vector<Node>& stepSubs = stepsSubs[i];
1519 : 80265 : Node step = steps[i];
1520 : 80265 : Node source = expr::narySubstitute(conc[0], vars, stepSubs);
1521 : 80265 : Node target = expr::narySubstitute(body, vars, stepSubs);
1522 : 80265 : target = target.substitute(TNode(placeholder), TNode(step));
1523 [ + - ]: 160530 : Trace("rpc-ctx") << "Step " << source << " == " << target << " from "
1524 : 0 : << body << " " << vars << " -> " << stepSubs << ", "
1525 : 80265 : << placeholder << " -> " << step << std::endl;
1526 : 80265 : Node req = source.eqNode(target);
1527 : 80265 : rews.push_back(req);
1528 : : // will prove this via a DSL rewrite
1529 : 80265 : ProvenInfo& dpi = d_pcache[req];
1530 : 80265 : dpi.d_id = pi.d_id;
1531 : 80265 : dpi.d_dslId = pi.d_dslId;
1532 : 80265 : dpi.d_vars = vars;
1533 : 80265 : dpi.d_subs = stepSubs;
1534 : 80265 : currConc = expr::narySubstitute(currConc, vars, stepSubs);
1535 : 80265 : Node prevConc = currConc;
1536 [ + + ]: 80265 : if (i < size - 1)
1537 : : {
1538 : 55194 : currConc = currConc.substitute(TNode(placeholder), TNode(body));
1539 : : }
1540 : 160530 : Node stepConc = prevConc.substitute(TNode(placeholder), TNode(step));
1541 : 80265 : prev = stepConc;
1542 : 80265 : }
1543 : :
1544 : 25111 : d_currFixedPointId = ProofRewriteRule::NONE;
1545 : : // add the transistivity rule here if needed
1546 [ + + ]: 25111 : if (rews.size() >= 2)
1547 : : {
1548 : 11495 : pi.d_id = RewriteProofStatus::DSL_FIXED_POINT;
1549 : : // store steps in d_vars
1550 : 11495 : pi.d_vars = rews;
1551 [ + - ]: 11495 : Trace("rpc-ctx") << "***RETURN fixed point " << rews << std::endl;
1552 : : // return the end of the chain, which will be used for constrained
1553 : : // matching
1554 : 11495 : return prev;
1555 : : }
1556 [ + + ][ + + ]: 140061 : }
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ]
1557 : :
1558 : 1736381 : Node ret = expr::narySubstitute(concRhs, vars, subs);
1559 [ + - ]: 1736381 : Trace("rpc-ctx") << "***RETURN " << ret << std::endl;
1560 : 1736381 : return ret;
1561 : 1747876 : }
1562 : :
1563 : 5954895 : Node RewriteDbProofCons::rewriteConcrete(const Node& n)
1564 : : {
1565 [ + + ]: 5954895 : if (expr::hasAbstractSubterm(n))
1566 : : {
1567 : 7504 : return n;
1568 : : }
1569 : 5947391 : return rewrite(n);
1570 : : }
1571 : :
1572 : 1261336 : Node RewriteDbProofCons::doFlatten(const Node& n)
1573 : : {
1574 : 1261336 : Kind k = n.getKind();
1575 : : // must be able to prove with ACI_NORM or ARITH_POLY_NORM
1576 [ + + ][ + + ]: 2444340 : if (expr::isAssocCommIdem(k) || expr::isAssoc(k) || k == Kind::ADD
1577 [ + + ][ + + ]: 2444340 : || k == Kind::NONLINEAR_MULT)
[ + + ]
1578 : : {
1579 : 129746 : return expr::algorithm::flatten(nodeManager(), n);
1580 : : }
1581 : 1131590 : return n;
1582 : : }
1583 : :
1584 : : } // namespace rewriter
1585 : : } // namespace cvc5::internal
|
