Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Hans-Joerg Schurr, Aina Niemetz
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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 : : * The module for basic (non-DSL-dependent) automatic reconstructing proofs of
14 : : * THEORY_REWRITE steps.
15 : : */
16 : :
17 : : #include "rewriter/basic_rewrite_rcons.h"
18 : :
19 : : #include "expr/nary_term_util.h"
20 : : #include "proof/conv_proof_generator.h"
21 : : #include "proof/proof_checker.h"
22 : : #include "proof/proof_node_algorithm.h"
23 : : #include "rewriter/rewrite_db_term_process.h"
24 : : #include "rewriter/rewrites.h"
25 : : #include "smt/env.h"
26 : : #include "theory/arith/arith_poly_norm.h"
27 : : #include "theory/arith/arith_proof_utilities.h"
28 : : #include "theory/booleans/theory_bool_rewriter.h"
29 : : #include "theory/bv/theory_bv_rewrite_rules.h"
30 : : #include "theory/rewriter.h"
31 : : #include "theory/strings/arith_entail.h"
32 : : #include "theory/strings/strings_entail.h"
33 : : #include "theory/strings/theory_strings_utils.h"
34 : : #include "util/rational.h"
35 : :
36 : : using namespace cvc5::internal::kind;
37 : :
38 : : namespace cvc5::internal {
39 : : namespace rewriter {
40 : :
41 : 0 : std::ostream& operator<<(std::ostream& os, TheoryRewriteMode tm)
42 : : {
43 [ - - ][ - - ]: 0 : switch (tm)
44 : : {
45 : 0 : case TheoryRewriteMode::STANDARD: return os << "STANDARD";
46 : 0 : case TheoryRewriteMode::RESORT: return os << "RESORT";
47 : 0 : case TheoryRewriteMode::NEVER: return os << "NEVER";
48 : : }
49 : 0 : Unreachable();
50 : : return os;
51 : : }
52 : :
53 : 3187 : BasicRewriteRCons::BasicRewriteRCons(Env& env) : EnvObj(env)
54 : : {
55 : :
56 : 3187 : }
57 : :
58 : 320369 : bool BasicRewriteRCons::prove(CDProof* cdp,
59 : : Node a,
60 : : Node b,
61 : : std::vector<std::shared_ptr<ProofNode>>& subgoals,
62 : : TheoryRewriteMode tmode)
63 : : {
64 : 640738 : Node eq = a.eqNode(b);
65 [ + - ]: 320369 : Trace("trewrite-rcons") << "Reconstruct " << eq << std::endl;
66 : 640738 : Node lhs = eq[0];
67 : 640738 : Node rhs = eq[1];
68 : : // this probably should never happen
69 [ - + ]: 320369 : if (eq[0] == eq[1])
70 : : {
71 [ - - ]: 0 : Trace("trewrite-rcons") << "...REFL" << std::endl;
72 : 0 : cdp->addStep(eq, ProofRule::REFL, {}, {eq[0]});
73 : 0 : return true;
74 : : }
75 : : // first, check that maybe its just an evaluation step
76 [ + + ][ + + ]: 640738 : if (tryRule(cdp, eq, ProofRule::EVALUATE, {eq[0]}))
[ - - ]
77 : : {
78 [ + - ]: 27751 : Trace("trewrite-rcons") << "...EVALUATE" << std::endl;
79 : 27751 : return true;
80 : : }
81 : :
82 : : // try theory rewrite (pre-rare)
83 [ + + ]: 292618 : if (tmode == TheoryRewriteMode::STANDARD)
84 : : {
85 [ + + ]: 289926 : if (tryTheoryRewrite(cdp, eq, theory::TheoryRewriteCtx::PRE_DSL, subgoals))
86 : : {
87 [ + - ]: 9218 : Trace("trewrite-rcons")
88 : 4609 : << "Reconstruct (pre) " << eq << " via theory rewrite" << std::endl;
89 : 4609 : return true;
90 : : }
91 : : }
92 [ + - ]: 288009 : Trace("trewrite-rcons") << "...(fail)" << std::endl;
93 : 288009 : return false;
94 : : }
95 : :
96 : 7021 : bool BasicRewriteRCons::postProve(
97 : : CDProof* cdp,
98 : : Node a,
99 : : Node b,
100 : : std::vector<std::shared_ptr<ProofNode>>& subgoals,
101 : : TheoryRewriteMode tmode)
102 : : {
103 : 7021 : Node eq = a.eqNode(b);
104 : : // try theory rewrite (post-rare), which may try both pre and post if
105 : : // the proof-granularity mode is dsl-rewrite-strict.
106 : 7021 : bool success = false;
107 [ - + ]: 7021 : if (tmode == TheoryRewriteMode::RESORT)
108 : : {
109 [ - - ]: 0 : if (tryTheoryRewrite(cdp, eq, theory::TheoryRewriteCtx::PRE_DSL, subgoals))
110 : : {
111 : 0 : success = true;
112 : : }
113 : : }
114 [ + - ]: 7021 : if (!success && tmode != TheoryRewriteMode::NEVER
115 [ + - ][ + + ]: 14042 : && tryTheoryRewrite(
[ + + ]
116 : : cdp, eq, theory::TheoryRewriteCtx::POST_DSL, subgoals))
117 : : {
118 : 683 : success = true;
119 : : }
120 [ + + ]: 7021 : if (success)
121 : : {
122 [ + - ]: 1366 : Trace("trewrite-rcons")
123 : 683 : << "Reconstruct (post) " << eq << " via theory rewrite" << std::endl;
124 : : }
125 : : else
126 : : {
127 [ + - ]: 6338 : Trace("trewrite-rcons") << "...(fail)" << std::endl;
128 : : }
129 : 14042 : return success;
130 : : }
131 : :
132 : 325661 : bool BasicRewriteRCons::tryRule(CDProof* cdp,
133 : : Node eq,
134 : : ProofRule r,
135 : : const std::vector<Node>& args,
136 : : bool addStep)
137 : : {
138 [ + - ]: 325661 : Trace("trewrite-rcons-debug") << "Try " << r << std::endl;
139 : 325661 : ProofChecker* pc = d_env.getProofNodeManager()->getChecker();
140 : : // do not provide expected, as this will always succeed if proof checking
141 : : // is disabled
142 : 976983 : Node res = pc->checkDebug(r, {}, args, Node::null(), "trewrite-rcons");
143 [ + + ][ + + ]: 325661 : if (!res.isNull() && res == eq)
[ + + ]
144 : : {
145 [ + + ]: 33043 : if (addStep)
146 : : {
147 : 27751 : cdp->addStep(eq, r, {}, args);
148 : : }
149 : 33043 : return true;
150 : : }
151 : 292618 : return false;
152 : : }
153 : :
154 : 2654 : void BasicRewriteRCons::ensureProofForEncodeTransform(CDProof* cdp,
155 : : const Node& eq,
156 : : const Node& eqi)
157 : : {
158 : 5308 : ProofRewriteDbNodeConverter rdnc(d_env);
159 : 5308 : std::shared_ptr<ProofNode> pfn = rdnc.convert(eq);
160 : 5308 : Node equiv = eq.eqNode(eqi);
161 [ - + ][ - + ]: 2654 : Assert(pfn->getResult() == equiv);
[ - - ]
162 : 2654 : cdp->addProof(pfn);
163 : 2654 : Node equivs = eqi.eqNode(eq);
164 : 5308 : cdp->addStep(equivs, ProofRule::SYMM, {equiv}, {});
165 [ + + ][ - - ]: 7962 : cdp->addStep(eq, ProofRule::EQ_RESOLVE, {eqi, equivs}, {});
166 : 2654 : }
167 : :
168 : 6062 : void BasicRewriteRCons::ensureProofForTheoryRewrite(
169 : : CDProof* cdp,
170 : : ProofRewriteRule id,
171 : : const Node& eq,
172 : : std::vector<std::shared_ptr<ProofNode>>& subgoals)
173 : : {
174 : 6062 : bool handledMacro = false;
175 [ + + ][ + + ]: 6062 : switch (id)
176 : : {
177 : 573 : case ProofRewriteRule::MACRO_BOOL_NNF_NORM:
178 [ + - ]: 573 : if (ensureProofMacroBoolNnfNorm(cdp, eq))
179 : : {
180 : 573 : handledMacro = true;
181 : : }
182 : 573 : break;
183 : 1337 : case ProofRewriteRule::MACRO_ARITH_STRING_PRED_ENTAIL:
184 [ + - ]: 1337 : if (ensureProofMacroArithStringPredEntail(cdp, eq))
185 : : {
186 : 1337 : handledMacro = true;
187 : : }
188 : 1337 : break;
189 : 10 : case ProofRewriteRule::MACRO_SUBSTR_STRIP_SYM_LENGTH:
190 [ + - ]: 10 : if (ensureProofMacroSubstrStripSymLength(cdp, eq))
191 : : {
192 : 10 : handledMacro = true;
193 : : }
194 : 10 : break;
195 : 4142 : default: break;
196 : : }
197 [ + + ]: 6062 : if (handledMacro)
198 : : {
199 : 1920 : std::shared_ptr<ProofNode> pfn = cdp->getProofFor(eq);
200 [ + - ]: 1920 : Trace("brc-macro") << "...proof is " << *pfn.get() << std::endl;
201 : 1920 : expr::getSubproofRule(pfn, ProofRule::TRUST, subgoals);
202 : 1920 : return;
203 : : }
204 : : // default, just add the rewrite
205 : 4142 : std::vector<Node> args;
206 : 4142 : args.push_back(
207 : 8284 : nodeManager()->mkConstInt(Rational(static_cast<uint32_t>(id))));
208 : 4142 : args.push_back(eq);
209 : 4142 : cdp->addStep(eq, ProofRule::THEORY_REWRITE, {}, args);
210 : : }
211 : :
212 : 573 : bool BasicRewriteRCons::ensureProofMacroBoolNnfNorm(CDProof* cdp,
213 : : const Node& eq)
214 : : {
215 : 1146 : Trace("brc-macro") << "Expand Bool NNF norm " << eq[0] << " == " << eq[1]
216 : 573 : << std::endl;
217 : : // Call the utility again with proof tracking and construct the term
218 : : // conversion proof. This proof itself may have trust steps in it.
219 : 1719 : TConvProofGenerator tcpg(d_env, nullptr);
220 : : Node nr = theory::booleans::TheoryBoolRewriter::computeNnfNorm(
221 : 1146 : nodeManager(), eq[0], &tcpg);
222 : 573 : std::shared_ptr<ProofNode> pfn = tcpg.getProofFor(eq);
223 [ + - ]: 573 : Trace("brc-macro") << "...proof is " << *pfn.get() << std::endl;
224 : 573 : cdp->addProof(pfn);
225 : 1146 : return true;
226 : : }
227 : :
228 : 1337 : bool BasicRewriteRCons::ensureProofMacroArithStringPredEntail(CDProof* cdp,
229 : : const Node& eq)
230 : : {
231 [ - + ][ - + ]: 1337 : Assert(eq.getKind() == Kind::EQUAL);
[ - - ]
232 [ + - ]: 1337 : Trace("brc-macro") << "Expand entailment for " << eq << std::endl;
233 : 2674 : theory::strings::ArithEntail ae(nullptr);
234 : 2674 : Node lhs = eq[0];
235 : 2674 : Node eqi = eq;
236 : : // First normalize LT/GT/LEQ to GEQ.
237 [ + + ][ + + ]: 1337 : if (lhs.getKind() != Kind::EQUAL && lhs.getKind() != Kind::GEQ)
[ + + ]
238 : : {
239 : 122 : Node lhsn = ae.normalizeGeq(lhs);
240 : 61 : Node eqLhs = lhs.eqNode(lhsn);
241 : 61 : cdp->addTrustedStep(
242 : : eqLhs, TrustId::MACRO_THEORY_REWRITE_RCONS_SIMPLE, {}, {});
243 : 61 : eqi = lhsn.eqNode(eq[1]);
244 [ + + ][ - - ]: 183 : cdp->addStep(eq, ProofRule::TRANS, {eqLhs, eqi}, {});
245 [ + - ]: 61 : Trace("brc-macro") << "- GEQ normalize is " << eqi << std::endl;
246 : : }
247 : : // Then do basic length intro, which rewrites (str.len (str.++ x y))
248 : : // to (+ (str.len x) (str.len y)).
249 : 4011 : TConvProofGenerator tcpg(d_env, nullptr);
250 : 2674 : Node eqii = ae.rewriteLengthIntro(eqi, &tcpg);
251 [ + + ]: 1337 : if (eqii != eqi)
252 : : {
253 : 1048 : Node equiv = eqi.eqNode(eqii);
254 : 1048 : std::shared_ptr<ProofNode> pfn = tcpg.getProofFor(equiv);
255 : 524 : cdp->addProof(pfn);
256 : 524 : Node equivs = eqii.eqNode(eqi);
257 : 1048 : cdp->addStep(equivs, ProofRule::SYMM, {equiv}, {});
258 [ + + ][ - - ]: 1572 : cdp->addStep(eqi, ProofRule::EQ_RESOLVE, {eqii, equivs}, {});
259 [ + - ]: 524 : Trace("brc-macro") << "- length intro is " << eqii << std::endl;
260 : : // now, must prove eqii
261 : : }
262 : 1337 : lhs = eqii[0];
263 : 2674 : Node exp;
264 : 2674 : Node ret = ae.rewritePredViaEntailment(lhs, exp, true);
265 [ - + ][ - + ]: 1337 : Assert(ret == eqii[1]);
[ - - ]
266 [ + - ]: 1337 : Trace("brc-macro") << "- explanation is " << exp << std::endl;
267 : : // if trivially true equality
268 [ + + ]: 1337 : if (exp.isNull())
269 : : {
270 : : // explanation true if we are an equality that is trivially true
271 [ - + ][ - + ]: 1022 : Assert(eqii[0].getKind() == Kind::EQUAL);
[ - - ]
272 [ + + ]: 1022 : if (eqii[0][0] == eqii[0][1])
273 : : {
274 : 2040 : cdp->addStep(eqii[0], ProofRule::REFL, {}, {eqii[0][0]});
275 : : }
276 : : else
277 : : {
278 [ - + ][ - + ]: 2 : Assert(theory::arith::PolyNorm::isArithPolyNorm(eqii[0][0], eqii[0][1]));
[ - - ]
279 : : // prove via ARITH_POLY_NORM.
280 : 4 : cdp->addStep(eqii[0], ProofRule::ARITH_POLY_NORM, {}, {eqii[0]});
281 : : }
282 : 2044 : cdp->addStep(eqii, ProofRule::TRUE_INTRO, {eqii[0]}, {});
283 : 1022 : return true;
284 : : }
285 : 630 : Node expRew = ae.rewriteArith(exp);
286 : 630 : Node zero = nodeManager()->mkConstInt(Rational(0));
287 : 945 : Node geq = nodeManager()->mkNode(Kind::GEQ, expRew, zero);
288 [ + - ]: 315 : Trace("brc-macro") << "- rewritten predicate is " << geq << std::endl;
289 : 630 : Node approx = ae.findApprox(expRew, true);
290 [ - + ]: 315 : if (approx.isNull())
291 : : {
292 [ - - ]: 0 : Trace("brc-macro") << "...failed to find approximation" << std::endl;
293 : 0 : Assert(false);
294 : : return false;
295 : : }
296 : 630 : Node truen = nodeManager()->mkConst(true);
297 : 630 : Node approxRew = ae.rewriteArith(approx);
298 : 945 : Node approxGeq = nodeManager()->mkNode(Kind::GEQ, approx, zero);
299 : 945 : Node approxRewGeq = nodeManager()->mkNode(Kind::GEQ, approxRew, zero);
300 [ + - ]: 630 : Trace("brc-macro") << "- approximation predicate is " << approxGeq
301 : 315 : << std::endl;
302 : 630 : std::vector<Node> transEq;
303 [ + + ]: 315 : if (expRew != approx)
304 : : {
305 : 208 : Node aeq = geq.eqNode(approxGeq);
306 : : // (>= expRew 0) = (>= approx 0)
307 [ + - ]: 208 : Trace("brc-macro") << "- prove " << aeq << " via pred-safe-approx"
308 : 104 : << std::endl;
309 : 104 : cdp->addTheoryRewriteStep(aeq,
310 : : ProofRewriteRule::ARITH_STRING_PRED_SAFE_APPROX);
311 : 104 : transEq.push_back(aeq);
312 : : }
313 [ + + ]: 315 : if (approx != approxRew)
314 : : {
315 : 104 : Node areq = approxGeq.eqNode(approxRewGeq);
316 [ + - ]: 208 : Trace("brc-macro") << "- prove " << areq << " via arith-poly-norm"
317 : 104 : << std::endl;
318 [ - + ]: 104 : if (!ensureProofArithPolyNormRel(cdp, areq))
319 : : {
320 [ - - ]: 0 : Trace("brc-macro") << "...failed to show normalization" << std::endl;
321 : 0 : Assert(false);
322 : : return false;
323 : : }
324 : 104 : transEq.push_back(areq);
325 : : }
326 : : // (>= approx 0) = true
327 : 630 : Node teq = approxRewGeq.eqNode(truen);
328 : 945 : Node ev = evaluate(approxRewGeq, {}, {});
329 [ + + ]: 315 : if (ev == truen)
330 : : {
331 [ + - ]: 171 : Trace("brc-macro") << "- prove " << teq << " via evaluate" << std::endl;
332 : 342 : cdp->addStep(teq, ProofRule::EVALUATE, {}, {approxRewGeq});
333 : : }
334 : : else
335 : : {
336 [ + - ]: 144 : Trace("brc-macro") << "- prove " << teq << " via pred-entail" << std::endl;
337 : 144 : cdp->addTheoryRewriteStep(teq, ProofRewriteRule::ARITH_STRING_PRED_ENTAIL);
338 : : }
339 : 315 : transEq.push_back(teq);
340 : : // put the above three steps together with TRANS
341 [ + + ]: 315 : if (transEq.size() > 1)
342 : : {
343 : 104 : teq = geq.eqNode(truen);
344 : 104 : cdp->addStep(teq, ProofRule::TRANS, transEq, {});
345 : : }
346 : :
347 : : // now have (>= expRew 0) = true, stored in teq
348 : :
349 [ - + ]: 315 : if (lhs == expRew)
350 : : {
351 [ - - ]: 0 : Trace("brc-macro") << "...success (no normalization)" << std::endl;
352 : 0 : return true;
353 : : }
354 [ + + ]: 315 : if (!ret.getConst<bool>())
355 : : {
356 [ + - ]: 61 : Trace("brc-macro") << "- false case, setting up conflict" << std::endl;
357 : 122 : cdp->addStep(geq, ProofRule::TRUE_ELIM, {teq}, {});
358 [ - + ][ - + ]: 61 : Assert(exp.getKind() == Kind::SUB);
[ - - ]
359 [ + - ][ + - ]: 122 : Node posTerm = exp[0].getKind() == Kind::SUB ? exp[0][0] : exp[0];
[ - - ]
360 : 61 : Assert(posTerm == lhs[0] || posTerm == lhs[1]);
361 : 61 : bool isLhs = posTerm == lhs[0];
362 [ + - ]: 61 : Trace("brc-macro") << "- isLhs is " << isLhs << std::endl;
363 : 61 : std::vector<Node> children;
364 : 61 : children.push_back(geq);
365 : 61 : children.push_back(lhs);
366 : 61 : std::vector<Node> args;
367 : : // Must flip signs to ensure it is <=, as required by
368 : : // MACRO_ARITH_SCALE_SUM_UB. This rule sums inequalities based on the
369 : : // coefficients in args.
370 : 61 : args.push_back(nodeManager()->mkConstInt(Rational(-1)));
371 [ + + ]: 61 : args.push_back(nodeManager()->mkConstInt(Rational(isLhs ? 1 : -1)));
372 [ + - ]: 122 : Trace("brc-macro") << "- compute sum bound for " << children << " " << args
373 : 61 : << std::endl;
374 : 61 : Node sumBound = theory::arith::expandMacroSumUb(children, args, cdp);
375 [ + - ]: 61 : Trace("brc-macro") << "- sum bound is " << sumBound << std::endl;
376 [ - + ]: 61 : if (sumBound.isNull())
377 : : {
378 [ - - ]: 0 : Trace("brc-macro") << "...failed to show normalization" << std::endl;
379 : 0 : Assert(false);
380 : : return false;
381 : : }
382 [ - + ][ - + ]: 61 : Assert(sumBound.getNumChildren() == 2);
[ - - ]
383 : 122 : Node py = nodeManager()->mkNode(Kind::SUB, sumBound[0], sumBound[1]);
384 : 61 : theory::arith::PolyNorm pn = theory::arith::PolyNorm::mkPolyNorm(py);
385 : 61 : Rational pyr;
386 [ - + ]: 61 : if (!pn.isConstant(pyr))
387 : : {
388 [ - - ]: 0 : Trace("brc-macro") << "...failed to prove constant after normalization"
389 : 0 : << std::endl;
390 : 0 : Assert(false);
391 : : return false;
392 : : }
393 : : Node cpred = nodeManager()->mkNode(
394 : 122 : sumBound.getKind(), nodeManager()->mkConstInt(pyr), zero);
395 : 61 : Node peq = sumBound.eqNode(cpred);
396 [ - + ]: 61 : if (!ensureProofArithPolyNormRel(cdp, peq))
397 : : {
398 [ - - ]: 0 : Trace("brc-macro") << "...failed to show normalization" << std::endl;
399 : 0 : Assert(false);
400 : : return false;
401 : : }
402 : 122 : Node cceq = cpred.eqNode(ret);
403 : 122 : cdp->addStep(cceq, ProofRule::EVALUATE, {}, {cpred});
404 : 122 : Node sumEqFalse = sumBound.eqNode(ret);
405 [ + + ][ - - ]: 183 : cdp->addStep(sumEqFalse, ProofRule::TRANS, {peq, cceq}, {});
406 : 122 : Node notSum = sumBound.notNode();
407 : 122 : cdp->addStep(notSum, ProofRule::FALSE_ELIM, {sumEqFalse}, {});
408 [ + + ][ - - ]: 183 : cdp->addStep(ret, ProofRule::CONTRA, {sumBound, notSum}, {});
409 : 61 : Node notLhs = lhs.notNode();
410 : 183 : cdp->addStep(notLhs, ProofRule::SCOPE, {ret}, {lhs});
411 : 122 : cdp->addStep(eqii, ProofRule::FALSE_INTRO, {notLhs}, {});
412 : : }
413 : : else
414 : : {
415 [ + - ]: 254 : Trace("brc-macro") << "- true case, prove equal" << std::endl;
416 [ - + ][ - + ]: 254 : Assert(lhs.getKind() == Kind::GEQ);
[ - - ]
417 : : // should be able to show equivalence by polynomial normalization
418 : 254 : Node peq = lhs.eqNode(geq);
419 [ - + ]: 254 : if (!ensureProofArithPolyNormRel(cdp, peq))
420 : : {
421 [ - - ]: 0 : Trace("brc-macro") << "...failed to show normalization (true case) "
422 : 0 : << lhs << " and " << geq << std::endl;
423 : 0 : Assert(false);
424 : : return false;
425 : : }
426 [ + + ][ - - ]: 762 : cdp->addStep(eqii, ProofRule::TRANS, {peq, teq}, {});
427 : : }
428 [ + - ]: 315 : Trace("brc-macro") << "...success" << std::endl;
429 : 315 : return true;
430 : : }
431 : :
432 : 10 : bool BasicRewriteRCons::ensureProofMacroSubstrStripSymLength(CDProof* cdp,
433 : : const Node& eq)
434 : : {
435 : 10 : NodeManager* nm = NodeManager::currentNM();
436 [ + - ]: 10 : Trace("brc-macro") << "Expand substring strip for " << eq << std::endl;
437 [ - + ][ - + ]: 10 : Assert(eq.getKind() == Kind::EQUAL);
[ - - ]
438 : 20 : Node lhs = eq[0];
439 [ - + ][ - + ]: 10 : Assert(lhs.getKind() == Kind::STRING_SUBSTR);
[ - - ]
440 : : theory::strings::Rewrite rule;
441 : : // call the same utility that proved it
442 : 20 : theory::strings::ArithEntail ae(nullptr);
443 : 10 : theory::strings::StringsEntail sent(nullptr, ae, nullptr);
444 : 20 : std::vector<Node> ch1;
445 : 20 : std::vector<Node> ch2;
446 : 20 : Node rhs = sent.rewriteViaMacroSubstrStripSymLength(lhs, rule, ch1, ch2);
447 [ + - ]: 10 : Trace("brc-macro") << "...was via string rewrite rule " << rule << std::endl;
448 [ - + ][ - + ]: 10 : Assert(rhs == eq[1]);
[ - - ]
449 : 20 : TypeNode stype = lhs.getType();
450 : 20 : Node cm1 = theory::strings::utils::mkConcat(ch1, stype);
451 : 20 : Node cm2 = theory::strings::utils::mkConcat(ch2, stype);
452 : 20 : Node cm;
453 : : // depending on the rule, are either stripping from front or back
454 [ + + ]: 10 : if (rule == theory::strings::Rewrite::SS_STRIP_END_PT)
455 : : {
456 : 8 : cm = nm->mkNode(Kind::STRING_CONCAT, cm1, cm2);
457 : : }
458 : : else
459 : : {
460 : 2 : cm = nm->mkNode(Kind::STRING_CONCAT, cm2, cm1);
461 : : }
462 [ - + ]: 10 : if (cm == lhs[0])
463 : : {
464 : 0 : return false;
465 : : }
466 : 30 : Node eq1 = nm->mkNode(Kind::EQUAL, lhs[0], cm);
467 : : // It is likely provable by ACI_NORM. However, if it involves splitting
468 : : // word constants, we require going through the rewrite term converter.
469 [ + - ]: 10 : if (expr::isACINorm(lhs[0], cm))
470 : : {
471 : 20 : cdp->addStep(eq1, ProofRule::ACI_NORM, {}, {eq1});
472 [ + - ]: 10 : Trace("brc-macro") << "- via ACI_NORM " << eq1 << std::endl;
473 : : }
474 : : else
475 : : {
476 : : // ----------------- via encode transform
477 : : // (t = s) = (r = r)
478 : : // ----- REFL ------------------ SYMM
479 : : // r = r (r = r) = (t = s)
480 : : // ---------------------------------- EQ_RESOLVE
481 : : // t = s
482 : 0 : RewriteDbNodeConverter rdnc(nodeManager());
483 : 0 : Node eq1t = rdnc.convert(eq1);
484 : 0 : Assert(eq1t.getKind() == Kind::EQUAL);
485 [ - - ]: 0 : if (eq1t[0] != eq1t[1])
486 : : {
487 : 0 : return false;
488 : : }
489 : 0 : Node equiv = eq1.eqNode(eq1t);
490 : 0 : ensureProofForEncodeTransform(cdp, eq1, eq1t);
491 : 0 : Node equivs = eq1t.eqNode(eq1);
492 : 0 : cdp->addStep(equivs, ProofRule::SYMM, {equiv}, {});
493 : 0 : cdp->addStep(eq1t, ProofRule::REFL, {}, {eq1t[0]});
494 : 0 : cdp->addStep(eq1, ProofRule::EQ_RESOLVE, {eq1t, equivs}, {});
495 : : }
496 : 20 : std::vector<Node> cargs;
497 : 10 : ProofRule cr = expr::getCongRule(lhs, cargs);
498 : 30 : Node eq2 = lhs[1].eqNode(lhs[1]);
499 : 30 : Node eq3 = lhs[2].eqNode(lhs[2]);
500 : 20 : cdp->addStep(eq2, ProofRule::REFL, {}, {lhs[1]});
501 : 20 : cdp->addStep(eq3, ProofRule::REFL, {}, {lhs[2]});
502 : 30 : Node lhsm = nm->mkNode(Kind::STRING_SUBSTR, cm, lhs[1], lhs[2]);
503 : 20 : Node eqLhs = lhs.eqNode(lhsm);
504 [ + + ][ - - ]: 40 : cdp->addStep(eqLhs, cr, {eq1, eq2, eq3}, cargs);
505 : 10 : Node eqm = lhsm.eqNode(rhs);
506 : : // Note that this is not marked simple, since it may require length
507 : : // entailment to prove.
508 : : // Note that there are three cases of string rewrites handled by this macro,
509 : : // where we expect this trusted step to be filled by one of 3 RARE rewrites,
510 : : // namely:
511 : : // str-substr-len-include, str-substr-len-include-pre, str-substr-len-skip.
512 : 10 : cdp->addTrustedStep(eqm, TrustId::MACRO_THEORY_REWRITE_RCONS, {}, {});
513 [ + - ]: 10 : Trace("brc-macro") << "- rely on rewrite " << eqm << std::endl;
514 [ + + ][ - - ]: 30 : cdp->addStep(eq, ProofRule::TRANS, {eqLhs, eqm}, {});
515 : 10 : return true;
516 : : }
517 : :
518 : 419 : bool BasicRewriteRCons::ensureProofArithPolyNormRel(CDProof* cdp,
519 : : const Node& eq)
520 : : {
521 [ + - ]: 419 : Trace("brc-macro") << "Ensure arith poly norm rel: " << eq << std::endl;
522 : 838 : Rational rx, ry;
523 [ - + ]: 419 : if (!theory::arith::PolyNorm::isArithPolyNormRel(eq[0], eq[1], rx, ry))
524 : : {
525 [ - - ]: 0 : Trace("brc-macro") << "...fail rule" << std::endl;
526 : 0 : return false;
527 : : }
528 : : Node premise =
529 : 1257 : theory::arith::PolyNorm::getArithPolyNormRelPremise(eq[0], eq[1], rx, ry);
530 [ + - ]: 838 : Trace("brc-macro") << "Show " << premise << " by arith poly norm"
531 : 419 : << std::endl;
532 [ + + ][ - + ]: 838 : if (!cdp->addStep(premise, ProofRule::ARITH_POLY_NORM, {}, {premise}))
[ - - ]
533 : : {
534 [ - - ]: 0 : Trace("brc-macro") << "...fail premise" << std::endl;
535 : 0 : return false;
536 : : }
537 : 838 : Node kn = ProofRuleChecker::mkKindNode(eq[0].getKind());
538 : 1257 : if (!cdp->addStep(eq, ProofRule::ARITH_POLY_NORM_REL, {premise}, {kn}))
539 : : {
540 [ - - ]: 0 : Trace("brc-macro") << "...fail application" << std::endl;
541 : 0 : return false;
542 : : }
543 : 419 : return true;
544 : : }
545 : :
546 : 296947 : bool BasicRewriteRCons::tryTheoryRewrite(
547 : : CDProof* cdp,
548 : : const Node& eq,
549 : : theory::TheoryRewriteCtx ctx,
550 : : std::vector<std::shared_ptr<ProofNode>>& subgoals)
551 : : {
552 [ - + ][ - + ]: 296947 : Assert(eq.getKind() == Kind::EQUAL);
[ - - ]
553 : 296947 : ProofRewriteRule prid = d_env.getRewriter()->findRule(eq[0], eq[1], ctx);
554 [ + + ]: 296947 : if (prid != ProofRewriteRule::NONE)
555 : : {
556 : : // Do not add the step in the call to tryStep, instead we add it via
557 : : // ensureProofForTheoryRewrite.
558 [ + + ][ + - ]: 15876 : if (tryRule(cdp,
[ - - ]
559 : : eq,
560 : : ProofRule::THEORY_REWRITE,
561 : : {mkRewriteRuleNode(prid), eq},
562 : 10584 : false))
563 : : {
564 : : // Theory rewrites may require macro expansion
565 : 5292 : ensureProofForTheoryRewrite(cdp, prid, eq, subgoals);
566 : 5292 : return true;
567 : : }
568 : : }
569 : 291655 : return false;
570 : : }
571 : :
572 : : } // namespace rewriter
573 : : } // namespace cvc5::internal
|
