Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Gereon Kremer, Aina Niemetz
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 by the authors listed in the file AUTHORS
8 : : * in the top-level source directory and their institutional affiliations.
9 : : * All rights reserved. See the file COPYING in the top-level source
10 : : * directory for licensing information.
11 : : * ****************************************************************************
12 : : *
13 : : * Implementation of inference to proof conversion.
14 : : */
15 : :
16 : : #include "theory/strings/infer_proof_cons.h"
17 : :
18 : : #include "expr/node_algorithm.h"
19 : : #include "expr/skolem_manager.h"
20 : : #include "options/smt_options.h"
21 : : #include "options/strings_options.h"
22 : : #include "proof/proof_node_algorithm.h"
23 : : #include "proof/proof_node_manager.h"
24 : : #include "smt/env.h"
25 : : #include "theory/builtin/proof_checker.h"
26 : : #include "theory/rewriter.h"
27 : : #include "theory/strings/core_solver.h"
28 : : #include "theory/strings/regexp_operation.h"
29 : : #include "theory/strings/theory_strings_utils.h"
30 : : #include "theory/strings/word.h"
31 : : #include "util/statistics_registry.h"
32 : :
33 : : using namespace cvc5::internal::kind;
34 : :
35 : : namespace cvc5::internal {
36 : : namespace theory {
37 : : namespace strings {
38 : :
39 : : /**
40 : : * Counts the number of times we traverse beneath a "non-core" operator.
41 : : * This is used to reason about substitutions that assume reasoning about
42 : : * concatentation and (dis)equalities only.
43 : : */
44 : : class StringCoreTermContext : public TermContext
45 : : {
46 : : public:
47 : 6063 : StringCoreTermContext() {}
48 : : /** The initial value: not nested. */
49 : 12126 : uint32_t initialValue() const override { return 0; }
50 : : /** Compute the value of the index^th child of t whose hash is tval */
51 : 164716 : uint32_t computeValue(TNode t, uint32_t tval, size_t index) const override
52 : : {
53 [ + + ]: 164716 : if (tval < 2)
54 : : {
55 : 131528 : Kind k = t.getKind();
56 : : // kinds we wish to substitute beneath
57 [ + + ][ + + ]: 131528 : if (k == Kind::NOT || k == Kind::EQUAL || k == Kind::STRING_CONCAT)
[ + + ]
58 : : {
59 : 88092 : return tval;
60 : : }
61 : 43436 : return tval + 1;
62 : : }
63 : 33188 : return 2;
64 : : }
65 : : };
66 : :
67 : 22554 : InferProofCons::InferProofCons(Env& env,
68 : : context::Context* c,
69 : 22554 : SequencesStatistics& statistics)
70 : 22554 : : EnvObj(env), d_lazyFactMap(c), d_statistics(statistics)
71 : : {
72 : 22554 : }
73 : :
74 : 40875 : void InferProofCons::notifyFact(const InferInfo& ii)
75 : : {
76 : 40875 : Node fact = ii.d_conc;
77 [ + - ]: 81750 : Trace("strings-ipc-notify")
78 : 40875 : << "InferProofCons::notifyFact: " << ii << std::endl;
79 [ + + ]: 40875 : if (d_lazyFactMap.find(fact) != d_lazyFactMap.end())
80 : : {
81 [ + - ]: 461 : Trace("strings-ipc-notify") << "...duplicate!" << std::endl;
82 : 461 : return;
83 : : }
84 : 40414 : Node symFact = CDProof::getSymmFact(fact);
85 [ + + ][ + + ]: 40414 : if (!symFact.isNull() && d_lazyFactMap.find(symFact) != d_lazyFactMap.end())
[ + + ]
86 : : {
87 [ + - ]: 67 : Trace("strings-ipc-notify") << "...duplicate (sym)!" << std::endl;
88 : 67 : return;
89 : : }
90 : 80694 : std::shared_ptr<InferInfo> iic = std::make_shared<InferInfo>(ii);
91 : 40347 : d_lazyFactMap.insert(ii.d_conc, iic);
92 : : }
93 : :
94 : 18169 : void InferProofCons::notifyLemma(const InferInfo& ii)
95 : : {
96 : 18169 : d_lazyFactMap[ii.d_conc] = std::make_shared<InferInfo>(ii);
97 : 18169 : }
98 : :
99 : 24512 : void InferProofCons::packArgs(Node conc,
100 : : InferenceId infer,
101 : : bool isRev,
102 : : const std::vector<Node>& exp,
103 : : std::vector<Node>& args)
104 : : {
105 : 24512 : NodeManager* nm = conc.getNodeManager();
106 : 24512 : args.push_back(conc);
107 : 24512 : args.push_back(mkInferenceIdNode(nm, infer));
108 : 24512 : args.push_back(nm->mkConst(isRev));
109 : : // The vector exp is stored as arguments; its flatten form are premises. We
110 : : // need both since the grouping of exp is important, e.g. { (and a b), c }
111 : : // is different from { a, b, c } in the convert routine, since positions
112 : : // of formulas in exp have special meaning.
113 : 24512 : args.insert(args.end(), exp.begin(), exp.end());
114 : 24512 : }
115 : :
116 : 9551 : bool InferProofCons::unpackArgs(const std::vector<Node>& args,
117 : : Node& conc,
118 : : InferenceId& infer,
119 : : bool& isRev,
120 : : std::vector<Node>& exp)
121 : : {
122 [ - + ][ - + ]: 9551 : Assert(args.size() >= 3);
[ - - ]
123 : 9551 : conc = args[0];
124 [ - + ]: 9551 : if (!getInferenceId(args[1], infer))
125 : : {
126 : 0 : return false;
127 : : }
128 : 9551 : isRev = args[2].getConst<bool>();
129 : 9551 : exp.insert(exp.end(), args.begin() + 3, args.end());
130 : 9551 : return true;
131 : : }
132 : :
133 : : /** convert
134 : : *
135 : : * This method converts this call to instructions on what the proof rule
136 : : * step(s) are for concluding the conclusion of the inference. This
137 : : * information is either:
138 : : *
139 : : * (A) stored in the argument ps, which consists of:
140 : : * - A proof rule identifier (ProofStep::d_rule).
141 : : * - The premises of the proof step (ProofStep::d_children).
142 : : * - Arguments to the proof step (ProofStep::d_args).
143 : : *
144 : : * (B) If the proof for the inference cannot be captured by a single
145 : : * step, then the d_rule field of ps is not set, and useBuffer is set to
146 : : * true. In this case, the argument psb is updated to contain (possibly
147 : : * multiple) proof steps for how to construct a proof for the given inference.
148 : : * In particular, psb will contain a set of steps that form a proof
149 : : * whose conclusion is conc and whose free assumptions are exp.
150 : : */
151 : 9551 : bool InferProofCons::convert(Env& env,
152 : : InferenceId infer,
153 : : bool isRev,
154 : : Node conc,
155 : : const std::vector<Node>& exp,
156 : : CDProof* pf)
157 : : {
158 : : // now go back and convert it to proof steps and add to proof
159 : 9551 : bool useBuffer = false;
160 : 19102 : ProofStep ps;
161 : : // ensure proof steps are unique
162 : 19102 : TheoryProofStepBuffer psb(pf->getManager()->getChecker(), true);
163 : : // Must flatten children with respect to AND to be ready to explain.
164 : : // We store the index where each flattened vector begins, since some
165 : : // explanations are grouped together using AND.
166 : 19102 : std::vector<size_t> startExpIndex;
167 [ + + ]: 30874 : for (const Node& ec : exp)
168 : : {
169 : : // store the index in the flattened vector
170 : 21323 : startExpIndex.push_back(ps.d_children.size());
171 : 21323 : utils::flattenOp(Kind::AND, ec, ps.d_children);
172 : : }
173 : : // debug print
174 [ - + ]: 9551 : if (TraceIsOn("strings-ipc-debug"))
175 : : {
176 [ - - ]: 0 : Trace("strings-ipc-debug") << "InferProofCons::convert: " << infer
177 [ - - ]: 0 : << (isRev ? " :rev " : " ") << conc << std::endl;
178 [ - - ]: 0 : for (const Node& ec : ps.d_children)
179 : : {
180 [ - - ]: 0 : Trace("strings-ipc-debug") << " e: " << ec << std::endl;
181 : : }
182 : : }
183 : : // try to find a set of proof steps to incorporate into the buffer
184 : 9551 : psb.clear();
185 : : // explicitly add ASSUME steps to the proof step buffer for premises of the
186 : : // inference, so that they will not be overwritten in the reconstruction
187 : : // below
188 [ + + ]: 31606 : for (const Node& ec : ps.d_children)
189 : : {
190 [ + - ]: 22055 : Trace("strings-ipc-debug") << "Explicit add " << ec << std::endl;
191 : 44110 : psb.addStep(ProofRule::ASSUME, {}, {ec}, ec);
192 : : }
193 : 9551 : NodeManager* nm = conc.getNodeManager();
194 : 19102 : Node nodeIsRev = nm->mkConst(isRev);
195 [ + + ][ + + ]: 9551 : switch (infer)
[ + + ][ - + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + ]
196 : : {
197 : : // ========================== equal by substitution+rewriting
198 : 2634 : case InferenceId::STRINGS_EXTF:
199 : : case InferenceId::STRINGS_EXTF_N:
200 : : case InferenceId::STRINGS_I_NORM_S:
201 : : case InferenceId::STRINGS_I_CONST_MERGE:
202 : : case InferenceId::STRINGS_I_NORM:
203 : : case InferenceId::STRINGS_LEN_NORM:
204 : : case InferenceId::STRINGS_NORMAL_FORM:
205 : : case InferenceId::STRINGS_CODE_PROXY:
206 : : {
207 : 2634 : size_t idMax = 0;
208 : : // These three inference assume the substitution is applied to the
209 : : // *arguments* of extended functions and the length function, so we
210 : : // will allow the substitutions to fire in term context value one.
211 [ + + ]: 2634 : if (infer == InferenceId::STRINGS_EXTF
212 [ + + ]: 2037 : || infer == InferenceId::STRINGS_EXTF_N
213 [ + + ]: 1289 : || infer == InferenceId::STRINGS_LEN_NORM)
214 : : {
215 : 1395 : idMax = 1;
216 : : }
217 : : // apply the substitution to conclude conc = conc', where conc' is the
218 : : // result of applying the substitution to conc'. This method further
219 : : // concludes conc from conc'. It then remains to prove conc' below.
220 : : Node concr =
221 : 5268 : convertCoreSubs(env, pf, psb, conc, ps.d_children, 0, idMax, true);
222 [ + - ]: 2634 : Trace("strings-ipc-core") << "Rewrote conclusion" << std::endl;
223 [ + - ]: 2634 : Trace("strings-ipc-core") << "- " << conc << std::endl;
224 [ + - ]: 2634 : Trace("strings-ipc-core") << "- to " << concr << std::endl;
225 [ + - ]: 2634 : if (psb.applyPredIntro(concr, {}))
226 : : {
227 : 2634 : useBuffer = true;
228 : : }
229 : : }
230 : 2634 : break;
231 : : // ========================== substitution + rewriting
232 : 80 : case InferenceId::STRINGS_RE_NF_CONFLICT:
233 : : case InferenceId::STRINGS_EXTF_D:
234 : : case InferenceId::STRINGS_EXTF_D_N:
235 : : case InferenceId::STRINGS_I_CONST_CONFLICT:
236 : : case InferenceId::STRINGS_UNIT_CONST_CONFLICT:
237 : : case InferenceId::STRINGS_ARITH_BOUND_CONFLICT:
238 : : {
239 [ + - ]: 80 : if (!ps.d_children.empty())
240 : : {
241 : 160 : std::vector<Node> exps(ps.d_children.begin(), ps.d_children.end() - 1);
242 : 160 : Node psrc = ps.d_children[ps.d_children.size() - 1];
243 : : // we apply the substitution on the purified form to get the
244 : : // original conclusion
245 [ + + ]: 80 : if (psb.applyPredTransform(psrc, conc, exps))
246 : : {
247 : 25 : useBuffer = true;
248 : : }
249 : : else
250 : : {
251 : : // More aggressive: lift to original form and use extended rewriting.
252 : : // A common case that this covers is arithmetic bound conflicts like
253 : : // (= (str.len @purifyN) 5) where @purifyN is the purification skolem
254 : : // for (str.++ "ABCDEF" x).
255 : 110 : Node psrco = SkolemManager::getOriginalForm(psrc);
256 [ + + ]: 55 : if (psb.applyPredTransform(psrco,
257 : : conc,
258 : : exps,
259 : : MethodId::SB_DEFAULT,
260 : : MethodId::SBA_SEQUENTIAL,
261 : : MethodId::RW_EXT_REWRITE))
262 : : {
263 : 50 : useBuffer = psb.applyPredTransform(psrc, psrco, {});
264 : : }
265 : : }
266 : : // Maybe involves AND_ELIM?
267 [ + + ]: 80 : if (!useBuffer)
268 : : {
269 : 5 : Node res = psb.applyPredElim(psrc, exps);
270 : 5 : useBuffer = convertAndElim(nm, res, conc, psb);
271 : : }
272 : : }
273 : : else
274 : : {
275 : : // use the predicate version?
276 : 0 : ps.d_args.push_back(conc);
277 : 0 : ps.d_rule = ProofRule::MACRO_SR_PRED_INTRO;
278 : : }
279 : : }
280 : 80 : break;
281 : : // ========================== rewrite pred
282 : 265 : case InferenceId::STRINGS_EXTF_EQ_REW:
283 : : {
284 : : // the last child is the predicate we are operating on, move to front
285 : 265 : Node src = ps.d_children[ps.d_children.size() - 1];
286 [ + - ]: 530 : Trace("strings-ipc-core")
287 : 0 : << "Generate proof for STRINGS_EXTF_EQ_REW, starting with " << src
288 : 265 : << std::endl;
289 : : // apply the substitution using the proper contextual information
290 : : // using the utility method
291 : 265 : std::vector<Node> expe(ps.d_children.begin(), ps.d_children.end() - 1);
292 : 265 : Node mainEqSRew = convertCoreSubs(env, pf, psb, src, expe, 1, 1);
293 [ + - ]: 265 : Trace("strings-ipc-core") << "...after subs: " << mainEqSRew << std::endl;
294 : 265 : mainEqSRew = psb.applyPredElim(mainEqSRew, {});
295 [ + - ]: 530 : Trace("strings-ipc-core")
296 : 265 : << "...after pred elim: " << mainEqSRew << std::endl;
297 [ - + ]: 265 : if (mainEqSRew == conc)
298 : : {
299 [ - - ]: 0 : Trace("strings-ipc-core") << "...success" << std::endl;
300 : 0 : useBuffer = true;
301 : 0 : break;
302 : : }
303 [ - + ]: 265 : else if (mainEqSRew.getKind() != Kind::EQUAL)
304 : : {
305 : : // Note this can happen in rare cases where substitution+rewriting
306 : : // is more powerful than congruence+rewriting. We fail to reconstruct
307 : : // the proof in this case.
308 [ - - ]: 0 : Trace("strings-ipc-core")
309 : 0 : << "...failed, not equality after rewriting" << std::endl;
310 : 0 : break;
311 : : }
312 : : // may need the "extended equality rewrite"
313 : : Node mainEqSRew2 = psb.applyPredElim(mainEqSRew,
314 : : {},
315 : : MethodId::SB_DEFAULT,
316 : : MethodId::SBA_SEQUENTIAL,
317 : 530 : MethodId::RW_REWRITE_EQ_EXT);
318 [ + - ]: 530 : Trace("strings-ipc-core")
319 : 265 : << "...after extended equality rewrite: " << mainEqSRew2 << std::endl;
320 : : // it may have rewritten to an AND, in which case we get the conjunct
321 [ + + ]: 265 : if (convertAndElim(nm, mainEqSRew2, conc, psb))
322 : : {
323 : 210 : useBuffer = true;
324 : 210 : break;
325 : : }
326 : : // rewrite again with default rewriter
327 : 110 : Node mainEqSRew3 = psb.applyPredElim(mainEqSRew2, {});
328 : 55 : useBuffer = (mainEqSRew3 == conc);
329 : : }
330 : 55 : break;
331 : : // ========================== extensionality
332 : 40 : case InferenceId::STRINGS_DEQ_EXTENSIONALITY:
333 : : {
334 : 40 : ps.d_rule = ProofRule::STRING_EXT;
335 : : }
336 : 40 : break;
337 : : // ========================== substitution+rewriting, CONCAT_EQ, ...
338 : 4131 : case InferenceId::STRINGS_F_CONST:
339 : : case InferenceId::STRINGS_F_UNIFY:
340 : : case InferenceId::STRINGS_F_ENDPOINT_EMP:
341 : : case InferenceId::STRINGS_F_ENDPOINT_EQ:
342 : : case InferenceId::STRINGS_F_NCTN:
343 : : case InferenceId::STRINGS_N_EQ_CONF:
344 : : case InferenceId::STRINGS_N_CONST:
345 : : case InferenceId::STRINGS_N_UNIFY:
346 : : case InferenceId::STRINGS_N_ENDPOINT_EMP:
347 : : case InferenceId::STRINGS_N_ENDPOINT_EQ:
348 : : case InferenceId::STRINGS_N_NCTN:
349 : : case InferenceId::STRINGS_SSPLIT_CST_PROP:
350 : : case InferenceId::STRINGS_SSPLIT_VAR_PROP:
351 : : case InferenceId::STRINGS_SSPLIT_CST:
352 : : case InferenceId::STRINGS_SSPLIT_VAR:
353 : : {
354 [ + - ]: 8262 : Trace("strings-ipc-core") << "Generate core rule for " << infer
355 : 4131 : << " (rev=" << isRev << ")" << std::endl;
356 : : // All of the above inferences have the form:
357 : : // (explanation for why t and s have the same prefix/suffix) ^
358 : : // t = s ^
359 : : // (length constraint)?
360 : : // We call t=s the "main equality" below. The length constraint is
361 : : // optional, which we split on below.
362 : 4131 : size_t nchild = ps.d_children.size();
363 : 4131 : size_t mainEqIndex = 0;
364 : 4131 : bool mainEqIndexSet = false;
365 : : // the length constraint
366 : 4131 : std::vector<Node> lenConstraint;
367 : : // these inferences have a length constraint as the last explain
368 [ + + ][ + + ]: 4131 : if (infer == InferenceId::STRINGS_N_UNIFY || infer == InferenceId::STRINGS_F_UNIFY
369 [ + + ][ + + ]: 2830 : || infer == InferenceId::STRINGS_SSPLIT_CST || infer == InferenceId::STRINGS_SSPLIT_VAR
370 [ + + ]: 2030 : || infer == InferenceId::STRINGS_SSPLIT_VAR_PROP
371 [ + + ]: 1676 : || infer == InferenceId::STRINGS_SSPLIT_CST_PROP)
372 : : {
373 [ + - ]: 2625 : if (exp.size() >= 2)
374 : : {
375 [ - + ][ - + ]: 2625 : Assert(exp.size() <= startExpIndex.size());
[ - - ]
376 : : // The index of the "main" equality is the last equality before
377 : : // the length explanation.
378 : 2625 : mainEqIndex = startExpIndex[exp.size() - 1] - 1;
379 : 2625 : mainEqIndexSet = true;
380 : : // the remainder is the length constraint
381 : 2625 : lenConstraint.insert(lenConstraint.end(),
382 : 2625 : ps.d_children.begin() + mainEqIndex + 1,
383 : 7875 : ps.d_children.end());
384 : : }
385 : : }
386 [ + - ]: 1506 : else if (nchild >= 1)
387 : : {
388 : : // The index of the main equality is the last child.
389 : 1506 : mainEqIndex = nchild - 1;
390 : 1506 : mainEqIndexSet = true;
391 : : }
392 : 4131 : Node mainEq;
393 [ + - ]: 4131 : if (mainEqIndexSet)
394 : : {
395 : 4131 : mainEq = ps.d_children[mainEqIndex];
396 [ + - ]: 8262 : Trace("strings-ipc-core") << "Main equality " << mainEq << " at index "
397 : 4131 : << mainEqIndex << std::endl;
398 : : }
399 [ + - ][ - + ]: 4131 : if (mainEq.isNull() || mainEq.getKind() != Kind::EQUAL)
[ - + ]
400 : : {
401 [ - - ]: 0 : Trace("strings-ipc-core")
402 : 0 : << "...failed to find main equality" << std::endl;
403 : 0 : break;
404 : : }
405 : : // apply MACRO_SR_PRED_ELIM using equalities up to the main eq
406 : : // we purify the core substitution
407 : : std::vector<Node> pcsr(ps.d_children.begin(),
408 : 4131 : ps.d_children.begin() + mainEqIndex);
409 : 4131 : Node pmainEq = mainEq;
410 : : // if there are substitutions to apply
411 [ + + ]: 4131 : if (mainEqIndex > 0)
412 : : {
413 : : // Compute which equalities we want to flip their substitution.
414 : : // Currently this is only an issue if e.g. (= (str.++ a a) (str.++ b c))
415 : : // where we conclude (= a c) from an explanation (= a b) via
416 : : // STRINGS_F_UNIFY, which would otherwise conclude (= b c) if a -> b
417 : : // was processed as a substitution.
418 : : // In contrast, normal form inferences are truly processed as
419 : : // substitutions in the strings core solver, whereas flat form
420 : : // inferences simply consider unification without substitutions, leading
421 : : // to issues like the one above.
422 : : std::vector<Node> rexp(ps.d_children.begin(),
423 : 3164 : ps.d_children.begin() + mainEqIndex);
424 [ + + ]: 3164 : if (infer == InferenceId::STRINGS_F_UNIFY
425 [ + + ]: 2995 : || infer == InferenceId::STRINGS_F_ENDPOINT_EQ)
426 : : {
427 [ + - ]: 756 : Trace("strings-ipc-core")
428 : 378 : << "...check reorient substitution" << std::endl;
429 [ - + ][ - + ]: 378 : Assert(conc.getKind() == Kind::EQUAL);
[ - - ]
430 : : // maybe reorient?
431 [ + + ]: 869 : for (size_t i = 0; i < mainEqIndex; i++)
432 : : {
433 [ - + ][ - + ]: 491 : Assert(rexp[i].getKind() == Kind::EQUAL);
[ - - ]
434 : 491 : if (rexp[i][0] == conc[0] || rexp[i][0] == conc[1])
435 : : {
436 : 9 : rexp[i] = rexp[i][1].eqNode(rexp[i][0]);
437 [ + - ]: 18 : Trace("strings-ipc-core")
438 : 9 : << "...reorient to " << rexp[i] << std::endl;
439 : : }
440 : : }
441 : : }
442 : : // apply substitution using the util method below
443 : 3164 : pmainEq = convertCoreSubs(env, pf, psb, mainEq, rexp, 0, 0);
444 : : }
445 [ + - ]: 8262 : Trace("strings-ipc-core")
446 : 4131 : << "Main equality after subs " << pmainEq << std::endl;
447 : : // now, conclude the proper equality
448 : 8262 : Node mainEqSRew = psb.applyPredElim(pmainEq, {});
449 [ - + ]: 4131 : if (mainEqSRew == conc)
450 : : {
451 [ - - ]: 0 : Trace("strings-ipc-core") << "...success after rewrite!" << std::endl;
452 : 0 : useBuffer = true;
453 : 0 : break;
454 : : }
455 [ + - ]: 8262 : Trace("strings-ipc-core")
456 : 4131 : << "Main equality after subs+rewrite " << mainEqSRew << std::endl;
457 : : // may need to splice constants
458 : 8262 : mainEqSRew = spliceConstants(
459 : 4131 : env, ProofRule::CONCAT_EQ, psb, mainEqSRew, conc, isRev);
460 : : // now, apply CONCAT_EQ to get the remainder
461 : 4131 : std::vector<Node> childrenCeq;
462 : 4131 : childrenCeq.push_back(mainEqSRew);
463 : 4131 : std::vector<Node> argsCeq;
464 : 4131 : argsCeq.push_back(nodeIsRev);
465 : 4131 : Node mainEqCeq = psb.tryStep(ProofRule::CONCAT_EQ, childrenCeq, argsCeq);
466 [ + - ]: 8262 : Trace("strings-ipc-core")
467 : 4131 : << "Main equality after CONCAT_EQ " << mainEqCeq << std::endl;
468 [ + - ][ - + ]: 4131 : if (mainEqCeq.isNull() || mainEqCeq.getKind() != Kind::EQUAL)
[ - + ]
469 : : {
470 : : // fail
471 : 0 : break;
472 : : }
473 : : // get the heads of the equality
474 : 4131 : std::vector<Node> tvec;
475 : 4131 : std::vector<Node> svec;
476 : 4131 : theory::strings::utils::getConcat(mainEqCeq[0], tvec);
477 : 4131 : theory::strings::utils::getConcat(mainEqCeq[1], svec);
478 [ + + ]: 4131 : Node t0 = tvec[isRev ? tvec.size() - 1 : 0];
479 [ + + ]: 4131 : Node s0 = svec[isRev ? svec.size() - 1 : 0];
480 : : // Now, mainEqCeq is an equality t ++ ... == s ++ ... where the
481 : : // inference involved t and s.
482 [ + + ]: 4131 : if (infer == InferenceId::STRINGS_N_ENDPOINT_EQ
483 [ + - ]: 3418 : || infer == InferenceId::STRINGS_N_ENDPOINT_EMP
484 [ + + ]: 3418 : || infer == InferenceId::STRINGS_F_ENDPOINT_EQ
485 [ - + ]: 3164 : || infer == InferenceId::STRINGS_F_ENDPOINT_EMP)
486 : : {
487 : : // Should be equal to conclusion already, or rewrite to it.
488 : : // Notice that this step is necessary to handle the "rproc"
489 : : // optimization in processSimpleNEq. Alternatively, this could
490 : : // possibly be done by CONCAT_EQ with !isRev.
491 : 1934 : std::vector<Node> cexp;
492 [ + - ]: 967 : if (psb.applyPredTransform(mainEqCeq,
493 : : conc,
494 : : cexp,
495 : : MethodId::SB_DEFAULT,
496 : : MethodId::SBA_SEQUENTIAL,
497 : : MethodId::RW_REWRITE_EQ_EXT))
498 : : {
499 [ + - ]: 1934 : Trace("strings-ipc-core") << "Transformed to " << conc
500 : 967 : << " via pred transform" << std::endl;
501 : : // success
502 : 967 : useBuffer = true;
503 [ + - ]: 967 : Trace("strings-ipc-core") << "...success!" << std::endl;
504 : 967 : }
505 : : // Otherwise, note that EMP rules conclude ti = "" where
506 : : // t1 ++ ... ++ tn == "". However, these are very rarely applied, let
507 : : // alone for 2+ children. This case is intentionally unhandled here.
508 : : }
509 [ + + ]: 3164 : else if (infer == InferenceId::STRINGS_F_NCTN
510 [ + + ]: 2960 : || infer == InferenceId::STRINGS_N_NCTN)
511 : : {
512 : : // May require extended equality rewrite, applied after the rewrite
513 : : // above. Notice we need both in sequence since ext equality rewriting
514 : : // is not recursive.
515 : 768 : std::vector<Node> argsERew;
516 : 384 : addMethodIds(nm,
517 : : argsERew,
518 : : MethodId::SB_DEFAULT,
519 : : MethodId::SBA_SEQUENTIAL,
520 : : MethodId::RW_REWRITE_EQ_EXT);
521 : : Node mainEqERew =
522 : 1920 : psb.tryStep(ProofRule::MACRO_SR_PRED_ELIM, {mainEqCeq}, argsERew);
523 [ + - ]: 384 : if (mainEqERew == conc)
524 : : {
525 : 384 : useBuffer = true;
526 [ + - ]: 384 : Trace("strings-ipc-core") << "...success!" << std::endl;
527 : 384 : }
528 : : }
529 : : else
530 : : {
531 : : // may need to apply symmetry
532 : 5560 : if ((infer == InferenceId::STRINGS_SSPLIT_CST
533 [ + + ]: 2025 : || infer == InferenceId::STRINGS_SSPLIT_CST_PROP)
534 [ + + ][ + + ]: 4805 : && t0.isConst())
[ + + ]
535 : : {
536 [ - + ][ - + ]: 665 : Assert(!s0.isConst());
[ - - ]
537 : 1330 : mainEqCeq = psb.tryStep(ProofRule::SYMM, {mainEqCeq}, {});
538 : 665 : std::swap(t0, s0);
539 : : }
540 [ + + ][ + + ]: 2780 : if (infer == InferenceId::STRINGS_N_UNIFY || infer == InferenceId::STRINGS_F_UNIFY)
541 : : {
542 [ - + ]: 1301 : if (conc.getKind() != Kind::EQUAL)
543 : : {
544 : 0 : break;
545 : : }
546 : : // one side should match, the other side could be a split constant
547 : 1301 : if (conc[0] != t0 && conc[1] != s0)
548 : : {
549 : 1322 : mainEqCeq = psb.tryStep(ProofRule::SYMM, {mainEqCeq}, {});
550 : 661 : std::swap(t0, s0);
551 : : }
552 [ - + ][ - + ]: 1301 : Assert(conc[0].isConst() == t0.isConst());
[ - - ]
553 [ - + ][ - + ]: 1301 : Assert(conc[1].isConst() == s0.isConst());
[ - - ]
554 : : }
555 : 2780 : ProofRule rule = ProofRule::UNKNOWN;
556 : : // the form of the required length constraint expected by the proof
557 : 2780 : Node lenReq;
558 : 2780 : bool lenSuccess = false;
559 [ + + ][ + + ]: 2780 : if (infer == InferenceId::STRINGS_N_UNIFY || infer == InferenceId::STRINGS_F_UNIFY)
560 : : {
561 : : // first, splice if necessary
562 : 2602 : mainEqCeq = spliceConstants(
563 : 1301 : env, ProofRule::CONCAT_UNIFY, psb, mainEqCeq, conc, isRev);
564 : : // the required premise for unify is always len(x) = len(y),
565 : : // however the explanation may not be literally this. Thus, we
566 : : // need to reconstruct a proof from the given explanation.
567 : : // it should be the case that lenConstraint => lenReq.
568 : : // We use terms in the conclusion equality, not t0, s0 here.
569 : 2602 : lenReq = nm->mkNode(Kind::STRING_LENGTH, conc[0])
570 : 1301 : .eqNode(nm->mkNode(Kind::STRING_LENGTH, conc[1]));
571 : 1301 : lenSuccess = convertLengthPf(lenReq, lenConstraint, psb);
572 : 1301 : rule = ProofRule::CONCAT_UNIFY;
573 : : }
574 [ + + ]: 1479 : else if (infer == InferenceId::STRINGS_SSPLIT_VAR)
575 : : {
576 : : // may have to flip
577 : 90 : Assert(conc.getKind() == Kind::AND && conc[0].getKind() == Kind::OR
578 : : && conc[0][0].getKind() == Kind::EQUAL);
579 [ + + ]: 45 : if (conc[0][0][0] != t0)
580 : : {
581 : 64 : mainEqCeq = psb.tryStep(ProofRule::SYMM, {mainEqCeq}, {});
582 : 32 : std::swap(t0, s0);
583 : : }
584 : : // it should be the case that lenConstraint => lenReq
585 : 90 : lenReq = nm->mkNode(Kind::STRING_LENGTH, t0)
586 : 90 : .eqNode(nm->mkNode(Kind::STRING_LENGTH, s0))
587 : 45 : .notNode();
588 : 45 : lenSuccess = convertLengthPf(lenReq, lenConstraint, psb);
589 : 45 : rule = ProofRule::CONCAT_SPLIT;
590 : : }
591 [ + + ]: 1434 : else if (infer == InferenceId::STRINGS_SSPLIT_CST)
592 : : {
593 : : // first, splice if necessary
594 : 1510 : mainEqCeq = spliceConstants(
595 : 755 : env, ProofRule::CONCAT_CSPLIT, psb, mainEqCeq, conc, isRev);
596 : : // it should be the case that lenConstraint => lenReq
597 : 1510 : lenReq = nm->mkNode(Kind::STRING_LENGTH, t0)
598 : 1510 : .eqNode(nm->mkConstInt(Rational(0)))
599 : 755 : .notNode();
600 : 755 : lenSuccess = convertLengthPf(lenReq, lenConstraint, psb);
601 : 755 : rule = ProofRule::CONCAT_CSPLIT;
602 : : }
603 [ + + ]: 679 : else if (infer == InferenceId::STRINGS_SSPLIT_VAR_PROP)
604 : : {
605 : : // it should be the case that lenConstraint => lenReq
606 [ + - ]: 500 : for (unsigned r = 0; r < 2; r++)
607 : : {
608 : 1500 : lenReq = nm->mkNode(Kind::GT,
609 : 1000 : nm->mkNode(Kind::STRING_LENGTH, t0),
610 : 1500 : nm->mkNode(Kind::STRING_LENGTH, s0));
611 [ + + ]: 500 : if (convertLengthPf(lenReq, lenConstraint, psb))
612 : : {
613 : 354 : lenSuccess = true;
614 : 354 : break;
615 : : }
616 [ + - ]: 146 : if (r == 0)
617 : : {
618 : : // may be the other direction
619 : 292 : mainEqCeq = psb.tryStep(ProofRule::SYMM, {mainEqCeq}, {});
620 : 146 : std::swap(t0, s0);
621 : : }
622 : : }
623 : 354 : rule = ProofRule::CONCAT_LPROP;
624 : : }
625 [ + + ]: 325 : else if (infer == InferenceId::STRINGS_SSPLIT_CST_PROP)
626 : : {
627 : : // it should be the case that lenConstraint => lenReq
628 : 340 : lenReq = nm->mkNode(Kind::STRING_LENGTH, t0)
629 : 340 : .eqNode(nm->mkConstInt(Rational(0)))
630 : 170 : .notNode();
631 : 170 : lenSuccess = convertLengthPf(lenReq, lenConstraint, psb);
632 : 170 : rule = ProofRule::CONCAT_CPROP;
633 : : }
634 [ + + ]: 155 : else if (infer == InferenceId::STRINGS_N_CONST
635 [ - + ]: 90 : || infer == InferenceId::STRINGS_F_CONST
636 [ - - ]: 0 : || infer == InferenceId::STRINGS_N_EQ_CONF)
637 : : {
638 : : // first, splice if necessary
639 : 310 : mainEqCeq = spliceConstants(
640 : 155 : env, ProofRule::CONCAT_UNIFY, psb, mainEqCeq, conc, isRev);
641 : : // Should be a constant conflict. We use CONCAT_UNIFY to infer an
642 : : // equality between string or sequence values, which will rewrite to
643 : : // false below, justifed by EVALUATE or DISTINCT_VALUES after
644 : : // elaboration.
645 : 155 : rule = ProofRule::CONCAT_UNIFY;
646 : 310 : std::vector<Node> tvecs, svecs;
647 : 155 : theory::strings::utils::getConcat(mainEqCeq[0], tvecs);
648 : 155 : theory::strings::utils::getConcat(mainEqCeq[1], svecs);
649 [ + + ]: 155 : t0 = tvecs[isRev ? tvecs.size() - 1 : 0];
650 [ + + ]: 155 : s0 = svecs[isRev ? svecs.size() - 1 : 0];
651 : : // add length requirement, which due to the splicing above should hold
652 : 310 : lenReq = nm->mkNode(Kind::STRING_LENGTH, t0)
653 : 155 : .eqNode(nm->mkNode(Kind::STRING_LENGTH, s0));
654 : : // should be shown by evaluation
655 : 155 : lenSuccess = psb.applyPredIntro(lenReq, {});
656 : : // will conclude an equality between string/sequence values, which
657 : : // will rewrite to false.
658 : : }
659 [ - + ]: 2780 : if (!lenSuccess)
660 : : {
661 [ - - ]: 0 : Trace("strings-ipc-core")
662 : 0 : << "...failed due to length constraint" << std::endl;
663 : 0 : break;
664 : : }
665 [ + - ]: 2780 : if (rule != ProofRule::UNKNOWN)
666 : : {
667 [ + - ]: 5560 : Trace("strings-ipc-core")
668 : 2780 : << "Core rule length requirement is " << lenReq << std::endl;
669 : : // apply the given rule
670 : 5560 : std::vector<Node> childrenMain;
671 : 2780 : childrenMain.push_back(mainEqCeq);
672 : 2780 : childrenMain.push_back(lenReq);
673 : 5560 : std::vector<Node> argsMain;
674 : 2780 : argsMain.push_back(nodeIsRev);
675 : 5560 : Node mainEqMain = psb.tryStep(rule, childrenMain, argsMain);
676 [ + - ]: 5560 : Trace("strings-ipc-core") << "Main equality after " << rule << " "
677 : 2780 : << mainEqMain << std::endl;
678 : : // either equal or rewrites to it
679 : 5560 : std::vector<Node> cexp;
680 [ + - ]: 2780 : if (psb.applyPredTransform(mainEqMain, conc, cexp))
681 : : {
682 : : // requires that length success is also true
683 : 2780 : useBuffer = true;
684 [ + - ]: 2780 : Trace("strings-ipc-core") << "...success" << std::endl;
685 : : }
686 : : else
687 : : {
688 [ - - ]: 0 : Trace("strings-ipc-core") << "...fail" << std::endl;
689 : : }
690 : : }
691 : : else
692 : : {
693 : : // should always have given a rule to try above
694 : 0 : Assert(false) << "No reconstruction rule given for " << infer;
695 : : }
696 : : }
697 : : }
698 : 4131 : break;
699 : : // ========================== Disequalities
700 : 30 : case InferenceId::STRINGS_DEQ_DISL_FIRST_CHAR_STRING_SPLIT:
701 : : case InferenceId::STRINGS_DEQ_DISL_STRINGS_SPLIT:
702 : : {
703 [ + - ]: 30 : if (conc.getKind() != Kind::AND || conc.getNumChildren() != 2
704 [ + - ][ - + ]: 60 : || conc[0].getKind() != Kind::EQUAL
[ - - ]
705 : 60 : || !conc[0][0].getType().isStringLike()
706 [ + - ][ + - ]: 60 : || conc[1].getKind() != Kind::EQUAL
[ - - ]
707 : 60 : || conc[1][0].getKind() != Kind::STRING_LENGTH)
708 : : {
709 [ - - ]: 0 : Trace("strings-ipc-deq") << "malformed application" << std::endl;
710 : 0 : Assert(false) << "unexpected conclusion " << conc << " for " << infer;
711 : : }
712 : : else
713 : : {
714 : : Node lenReq = nm->mkNode(
715 : 90 : Kind::GEQ, nm->mkNode(Kind::STRING_LENGTH, conc[0][0]), conc[1][1]);
716 [ + - ]: 60 : Trace("strings-ipc-deq")
717 : 30 : << "length requirement is " << lenReq << std::endl;
718 [ + - ]: 30 : if (convertLengthPf(lenReq, ps.d_children, psb))
719 : : {
720 [ + - ]: 30 : Trace("strings-ipc-deq") << "...success length" << std::endl;
721 : : // make the proof
722 : 60 : std::vector<Node> childrenMain;
723 : 30 : childrenMain.push_back(lenReq);
724 : 60 : std::vector<Node> argsMain;
725 : 30 : argsMain.push_back(nodeIsRev);
726 : : Node mainConc =
727 : 30 : psb.tryStep(ProofRule::STRING_DECOMPOSE, childrenMain, argsMain);
728 [ + - ]: 60 : Trace("strings-ipc-deq")
729 : 30 : << "...main conclusion is " << mainConc << std::endl;
730 : 30 : useBuffer = (mainConc == conc);
731 [ + - ]: 30 : if (!useBuffer)
732 : : {
733 : : // Should be made equal by transformation. This step is necessary
734 : : // if rewriting was used to change the skolem introduced in the
735 : : // conclusion.
736 : 30 : useBuffer = psb.applyPredTransform(mainConc, conc, {});
737 : : }
738 [ + - ]: 60 : Trace("strings-ipc-deq")
739 : 30 : << "...success is " << useBuffer << std::endl;
740 : : }
741 : : else
742 : : {
743 : 0 : Assert(false)
744 : 0 : << "Failed to convert length " << lenReq << " " << ps.d_children;
745 : : Trace("strings-ipc-deq") << "...fail length" << std::endl;
746 : : }
747 : : }
748 : : }
749 : 30 : break;
750 : : // ========================== Boolean split
751 : 0 : case InferenceId::STRINGS_CARD_SP:
752 : : case InferenceId::STRINGS_LEN_SPLIT:
753 : : case InferenceId::STRINGS_LEN_SPLIT_EMP:
754 : : case InferenceId::STRINGS_DEQ_DISL_EMP_SPLIT:
755 : : case InferenceId::STRINGS_DEQ_DISL_FIRST_CHAR_EQ_SPLIT:
756 : : case InferenceId::STRINGS_DEQ_STRINGS_EQ:
757 : : case InferenceId::STRINGS_DEQ_LENS_EQ:
758 : : case InferenceId::STRINGS_DEQ_LENGTH_SP:
759 : : case InferenceId::STRINGS_UNIT_SPLIT:
760 : : {
761 [ - - ]: 0 : if (conc.getKind() != Kind::OR)
762 : : {
763 : : // This should never happen. If it does, we resort to using
764 : : // THEORY_INFERENCE_STRINGS below (in production mode).
765 : 0 : Assert(false) << "Expected OR conclusion for " << infer;
766 : : }
767 : : else
768 : : {
769 : 0 : ps.d_rule = ProofRule::SPLIT;
770 : 0 : Assert(ps.d_children.empty());
771 : 0 : ps.d_args.push_back(conc[0]);
772 : : }
773 : : }
774 : 0 : break;
775 : : // ========================== Regular expression unfolding
776 : 322 : case InferenceId::STRINGS_RE_UNFOLD_POS:
777 : : case InferenceId::STRINGS_RE_UNFOLD_NEG:
778 : : {
779 [ - + ][ - + ]: 322 : Assert (!ps.d_children.empty());
[ - - ]
780 : 322 : size_t nchild = ps.d_children.size();
781 : 644 : Node mem = ps.d_children[nchild-1];
782 [ - + ]: 322 : if (nchild>1)
783 : : {
784 : : // if more than one, apply MACRO_SR_PRED_ELIM
785 : 0 : std::vector<Node> tcs;
786 : 0 : tcs.insert(tcs.end(),
787 : : ps.d_children.begin(),
788 : 0 : ps.d_children.begin() + (nchild-1));
789 : 0 : mem = psb.applyPredElim(mem, tcs);
790 : 0 : useBuffer = true;
791 : : }
792 : 322 : ProofRule r = ProofRule::UNKNOWN;
793 : 644 : std::vector<Node> args;
794 [ - + ]: 322 : if (mem.isNull())
795 : : {
796 : : // failed to eliminate above
797 : 0 : Assert(false) << "Failed to apply MACRO_SR_PRED_ELIM for RE unfold";
798 : : useBuffer = false;
799 : : }
800 [ + + ]: 322 : else if (infer == InferenceId::STRINGS_RE_UNFOLD_POS)
801 : : {
802 : 287 : r = ProofRule::RE_UNFOLD_POS;
803 : : }
804 : : else
805 : : {
806 : 35 : r = ProofRule::RE_UNFOLD_NEG;
807 : : // it may be an optimized form of concat simplification
808 : 70 : Assert(mem.getKind() == Kind::NOT
809 : : && mem[0].getKind() == Kind::STRING_IN_REGEXP);
810 [ + - ]: 35 : if (mem[0][1].getKind() == Kind::REGEXP_CONCAT)
811 : : {
812 : : bool isCRev;
813 : 105 : Node reLen = RegExpOpr::getRegExpConcatFixed(mem[0][1], isCRev);
814 : : // if we can find a fixed length for a component, use the optimized
815 : : // version
816 [ + - ]: 35 : if (!reLen.isNull())
817 : : {
818 : 35 : r = ProofRule::RE_UNFOLD_NEG_CONCAT_FIXED;
819 : 35 : args.push_back(nm->mkConst(isCRev));
820 : : }
821 : : }
822 : : }
823 [ - + ]: 322 : if (useBuffer)
824 : : {
825 : 0 : mem = psb.tryStep(r, {mem}, args);
826 : : // should match the conclusion
827 : 0 : useBuffer = (mem==conc);
828 : : }
829 : : else
830 : : {
831 : 322 : ps.d_rule = r;
832 : 322 : ps.d_args = args;
833 : : }
834 : : }
835 : 322 : break;
836 : : // ========================== Reduction
837 : 130 : case InferenceId::STRINGS_CTN_POS:
838 : : case InferenceId::STRINGS_CTN_NEG_EQUAL:
839 : : {
840 [ - + ]: 130 : if (ps.d_children.size() != 1)
841 : : {
842 : 0 : break;
843 : : }
844 : 130 : bool polarity = ps.d_children[0].getKind() != Kind::NOT;
845 [ + - ]: 130 : Node atom = polarity ? ps.d_children[0] : ps.d_children[0][0];
846 : 130 : std::vector<Node> args;
847 : 130 : args.push_back(atom);
848 : 260 : Node res = psb.tryStep(ProofRule::STRING_EAGER_REDUCTION, {}, args);
849 [ - + ]: 130 : if (res.isNull())
850 : : {
851 : 0 : break;
852 : : }
853 : : // ite( contains(x,t), x = k1 ++ t ++ k2, x != t )
854 : 130 : std::vector<Node> tiChildren;
855 : 130 : tiChildren.push_back(ps.d_children[0]);
856 : : Node ctnt =
857 : : psb.tryStep(polarity ? ProofRule::TRUE_INTRO : ProofRule::FALSE_INTRO,
858 : : tiChildren,
859 [ + - ]: 260 : {});
860 [ + - ][ - + ]: 130 : if (ctnt.isNull() || ctnt.getKind() != Kind::EQUAL)
[ - + ]
861 : : {
862 : 0 : break;
863 : : }
864 : 260 : std::vector<Node> tchildren;
865 : 130 : tchildren.push_back(ctnt);
866 : : // apply substitution { contains(x,t) -> true|false } and rewrite to get
867 : : // conclusion x = k1 ++ t ++ k2 or x != t.
868 [ + - ]: 130 : if (psb.applyPredTransform(res, conc, tchildren))
869 : : {
870 : 130 : useBuffer = true;
871 : : }
872 : : }
873 : 130 : break;
874 : :
875 : 1325 : case InferenceId::STRINGS_REDUCTION:
876 : : {
877 : 1325 : size_t nchild = conc.getNumChildren();
878 : 1325 : Node mainEq;
879 [ - + ]: 1325 : if (conc.getKind() == Kind::EQUAL)
880 : : {
881 : 0 : mainEq = conc;
882 : : }
883 : 3975 : else if (conc.getKind() == Kind::AND
884 [ + - ][ + - ]: 1325 : && conc[nchild - 1].getKind() == Kind::EQUAL)
[ + - ][ + - ]
[ - - ]
885 : : {
886 : 1325 : mainEq = conc[nchild - 1];
887 : : }
888 [ - + ]: 1325 : if (mainEq.isNull())
889 : : {
890 [ - - ]: 0 : Trace("strings-ipc-red") << "Bad Reduction: " << conc << std::endl;
891 : 0 : Assert(false) << "Unexpected reduction " << conc;
892 : : break;
893 : : }
894 : 2650 : std::vector<Node> argsRed;
895 : : // the left hand side of the last conjunct is the term we are reducing
896 : 1325 : argsRed.push_back(mainEq[0]);
897 : 3975 : Node red = psb.tryStep(ProofRule::STRING_REDUCTION, {}, argsRed);
898 [ + - ]: 1325 : Trace("strings-ipc-red") << "Reduction : " << red << std::endl;
899 [ + - ]: 1325 : if (!red.isNull())
900 : : {
901 [ + + ]: 1325 : if (red == conc)
902 : : {
903 [ + - ]: 143 : Trace("strings-ipc-red") << "...success!" << std::endl;
904 : 143 : useBuffer = true;
905 : : }
906 : : else
907 : : {
908 : 2364 : std::vector<Node> cexp;
909 : : // get the equalities where the reduction is different
910 : 2364 : std::vector<Node> matchConds;
911 : 1182 : expr::getConversionConditions(red, conc, matchConds);
912 [ + - ]: 2364 : Trace("strings-ipc-red")
913 : 1182 : << "...need to prove " << matchConds << std::endl;
914 : : // To simplify the proof transformation step below, we manually
915 : : // unpurify skolems from the concluded reduction. This
916 : : // make it more likely the applyPredTransform step does not have to
917 : : // resort to original forms. In particular, the strings rewriter
918 : : // currently does not respect the property that if
919 : : // t ---> c for constant c, then getOriginalForm(t) ---> c. This
920 : : // means we should attempt to replay the term which was used by the
921 : : // strings skolem cache to justify k = c, which is its unpurified
922 : : // form t, not its original form.
923 [ + + ]: 2898 : for (const Node& mc : matchConds)
924 : : {
925 : 3432 : Node mcu = SkolemManager::getUnpurifiedForm(mc[0]);
926 [ + - ]: 1716 : if (mcu != mc[0])
927 : : {
928 : 3432 : Node mceq = mc[0].eqNode(mcu);
929 : 3432 : psb.addStep(ProofRule::SKOLEM_INTRO, {}, {mc[0]}, mceq);
930 : 1716 : cexp.push_back(mceq);
931 : : }
932 : : }
933 : : // either equal or rewrites to it
934 [ + - ]: 1182 : if (psb.applyPredTransform(red, conc, cexp))
935 : : {
936 [ + - ]: 1182 : Trace("strings-ipc-red") << "...success!" << std::endl;
937 : 1182 : useBuffer = true;
938 : : }
939 : : else
940 : : {
941 [ - - ]: 0 : Trace("strings-ipc-red") << "...failed to reduce" << std::endl;
942 : : }
943 : : }
944 : : }
945 : : }
946 : 1325 : break;
947 : : // ========================== code injectivity
948 : 71 : case InferenceId::STRINGS_CODE_INJ:
949 : : {
950 : 71 : ps.d_rule = ProofRule::STRING_CODE_INJ;
951 : 142 : Assert(conc.getKind() == Kind::OR && conc.getNumChildren() == 3
952 : : && conc[2].getKind() == Kind::EQUAL);
953 : 71 : ps.d_args.push_back(conc[2][0]);
954 : 71 : ps.d_args.push_back(conc[2][1]);
955 : : }
956 : 71 : break;
957 : : // ========================== unit injectivity
958 : 45 : case InferenceId::STRINGS_UNIT_INJ:
959 : : {
960 [ - + ][ - + ]: 45 : Assert(conc.getKind() == Kind::EQUAL);
[ - - ]
961 [ + - ][ + - ]: 90 : Assert(ps.d_children.size() == 1
[ - + ][ - - ]
962 : : && ps.d_children[0].getKind() == Kind::EQUAL);
963 : : Node concS =
964 : 135 : psb.tryStep(ProofRule::STRING_SEQ_UNIT_INJ, ps.d_children, {});
965 [ + - ]: 45 : if (!concS.isNull())
966 : : {
967 : : // may need to apply symmetry
968 [ + + ]: 45 : if (concS != conc)
969 : : {
970 : 40 : Node ss = psb.tryStep(ProofRule::SYMM, {concS}, {});
971 : 10 : useBuffer = (ss == conc);
972 : : }
973 : : else
974 : : {
975 : 35 : useBuffer = true;
976 : : }
977 : : }
978 : : }
979 : 45 : break;
980 : : // ========================== prefix conflict
981 : 189 : case InferenceId::STRINGS_PREFIX_CONFLICT:
982 : : case InferenceId::STRINGS_PREFIX_CONFLICT_MIN:
983 : : {
984 [ + - ]: 189 : Trace("strings-ipc-prefix") << "Prefix conflict..." << std::endl;
985 : 189 : std::vector<Node> eqs;
986 [ + + ]: 532 : for (const Node& e : ps.d_children)
987 : : {
988 : 343 : Kind ek = e.getKind();
989 [ + + ]: 343 : if (ek == Kind::EQUAL)
990 : : {
991 [ + - ]: 234 : Trace("strings-ipc-prefix") << "- equality : " << e << std::endl;
992 : 234 : eqs.push_back(e);
993 : : }
994 [ + - ]: 109 : else if (ek == Kind::STRING_IN_REGEXP)
995 : : {
996 : : // unfold it and extract the equality
997 : 109 : std::vector<Node> children;
998 : 109 : children.push_back(e);
999 : 109 : std::vector<Node> args;
1000 : 109 : Node eunf = psb.tryStep(ProofRule::RE_UNFOLD_POS, children, args);
1001 [ + - ]: 218 : Trace("strings-ipc-prefix")
1002 : 109 : << "--- " << e << " unfolds to " << eunf << std::endl;
1003 [ - + ]: 109 : if (eunf.isNull())
1004 : : {
1005 : 0 : continue;
1006 : : }
1007 [ + - ]: 109 : else if (eunf.getKind() == Kind::AND)
1008 : : {
1009 : : // equality is the first conjunct
1010 : 109 : std::vector<Node> childrenAE;
1011 : 109 : childrenAE.push_back(eunf);
1012 : 109 : std::vector<Node> argsAE;
1013 : 109 : argsAE.push_back(nm->mkConstInt(Rational(0)));
1014 : 109 : Node eunfAE = psb.tryStep(ProofRule::AND_ELIM, childrenAE, argsAE);
1015 [ + - ]: 218 : Trace("strings-ipc-prefix")
1016 : 109 : << "--- and elim to " << eunfAE << std::endl;
1017 [ + - ][ - + ]: 109 : if (eunfAE.isNull() || eunfAE.getKind() != Kind::EQUAL)
[ - + ]
1018 : : {
1019 : 0 : Assert(false)
1020 : 0 : << "Unexpected unfolded premise " << eunf << " for " << infer;
1021 : : continue;
1022 : : }
1023 [ + - ]: 218 : Trace("strings-ipc-prefix")
1024 : 109 : << "- equality : " << eunfAE << std::endl;
1025 : 109 : eqs.push_back(eunfAE);
1026 : : }
1027 [ - - ]: 0 : else if (eunf.getKind() == Kind::EQUAL)
1028 : : {
1029 [ - - ]: 0 : Trace("strings-ipc-prefix") << "- equality : " << eunf << std::endl;
1030 : 0 : eqs.push_back(eunf);
1031 : : }
1032 : : }
1033 : : else
1034 : : {
1035 : : // not sure how to use this assumption
1036 : 0 : Assert(false) << "Unexpected premise " << e << " for " << infer;
1037 : : }
1038 : : }
1039 [ - + ]: 189 : if (eqs.empty())
1040 : : {
1041 : 0 : break;
1042 : : }
1043 : : // connect via transitivity
1044 : 189 : Node curr = eqs[0];
1045 : 189 : std::vector<Node> subs;
1046 [ + + ]: 343 : for (size_t i = 1, esize = eqs.size(); i < esize; i++)
1047 : : {
1048 : 154 : Node prev = curr;
1049 : 154 : curr = convertTrans(curr, eqs[i], psb);
1050 : : // if it is not a transitive step, it corresponds to a substitution
1051 [ + + ]: 154 : if (curr.isNull())
1052 : : {
1053 : 45 : curr = prev;
1054 : : // This is an equality between a variable and a concatention or
1055 : : // constant term (for example see below).
1056 : : // orient the substitution properly
1057 [ - + ][ - - ]: 90 : if (!eqs[i][1].isConst()
1058 [ - + ][ - - ]: 90 : && eqs[i][1].getKind() != Kind::STRING_CONCAT)
[ - + ][ + - ]
[ - - ]
1059 : : {
1060 : 0 : subs.push_back(eqs[i][1].eqNode(eqs[i][0]));
1061 : : }
1062 : : else
1063 : : {
1064 : 45 : subs.push_back(eqs[i]);
1065 : : }
1066 : 45 : continue;
1067 : : }
1068 [ + - ]: 109 : Trace("strings-ipc-prefix") << "- Via trans: " << curr << std::endl;
1069 : : }
1070 [ - + ]: 189 : if (curr.isNull())
1071 : : {
1072 : 0 : break;
1073 : : }
1074 : : // Substitution is applied in reverse order
1075 : : // An example of this inference that uses a substituion is the conflict:
1076 : : // (str.in_re w (re.++ (re.* re.allchar) (str.to_re "ABC")))
1077 : : // (= w (str.++ z y x))
1078 : : // (= x "D")
1079 : : // where we apply w -> (str.++ z y x), then x -> "D" to the first
1080 : : // predicate to obtain a conflict by rewriting (predicate elim).
1081 : 189 : std::reverse(subs.begin(), subs.end());
1082 [ + - ]: 378 : Trace("strings-ipc-prefix")
1083 : 189 : << "- Possible conflicting equality : " << curr << std::endl;
1084 : : Node concE = psb.applyPredElim(curr,
1085 : : subs,
1086 : : MethodId::SB_DEFAULT,
1087 : : MethodId::SBA_SEQUENTIAL,
1088 : 378 : MethodId::RW_EXT_REWRITE);
1089 [ + - ]: 378 : Trace("strings-ipc-prefix")
1090 : 189 : << "- After pred elim: " << concE << std::endl;
1091 [ + - ]: 189 : if (concE == conc)
1092 : : {
1093 [ + - ]: 189 : Trace("strings-ipc-prefix") << "...success!" << std::endl;
1094 : 189 : useBuffer = true;
1095 : : }
1096 : : }
1097 : 189 : break;
1098 : : // ========================== regular expressions
1099 : 35 : case InferenceId::STRINGS_RE_INTER_INCLUDE:
1100 : : case InferenceId::STRINGS_RE_INTER_CONF:
1101 : : case InferenceId::STRINGS_RE_INTER_INFER:
1102 : : {
1103 : 35 : std::vector<Node> reiExp;
1104 : 35 : std::vector<Node> reis;
1105 : 35 : std::vector<Node> reiChildren;
1106 : 35 : std::vector<Node> reiChildrenOrig;
1107 : 35 : Node x;
1108 : : // make the regular expression intersection that summarizes all
1109 : : // memberships in the explanation
1110 [ + + ]: 105 : for (const Node& c : ps.d_children)
1111 : : {
1112 : 70 : bool polarity = c.getKind() != Kind::NOT;
1113 [ + + ]: 70 : Node catom = polarity ? c : c[0];
1114 [ - + ]: 70 : if (catom.getKind() != Kind::STRING_IN_REGEXP)
1115 : : {
1116 : 0 : Assert(c.getKind() == Kind::EQUAL);
1117 [ - - ]: 0 : if (c.getKind() == Kind::EQUAL)
1118 : : {
1119 : 0 : reiExp.push_back(c);
1120 : : }
1121 : 0 : continue;
1122 : : }
1123 [ + + ]: 70 : if (x.isNull())
1124 : : {
1125 : : // just take the first LHS; others should be equated to it by exp
1126 : 35 : x = catom[0];
1127 : : }
1128 : : Node rcurr =
1129 : 175 : polarity ? catom[1] : nm->mkNode(Kind::REGEXP_COMPLEMENT, catom[1]);
1130 : 70 : reis.push_back(rcurr);
1131 : 210 : Node mem = nm->mkNode(Kind::STRING_IN_REGEXP, catom[0], rcurr);
1132 : 70 : reiChildren.push_back(mem);
1133 : 70 : reiChildrenOrig.push_back(c);
1134 : : }
1135 : : // go back and justify each premise
1136 : 35 : bool successChildren = true;
1137 [ + + ]: 105 : for (size_t i = 0, nchild = reiChildren.size(); i < nchild; i++)
1138 : : {
1139 [ - + ]: 70 : if (!psb.applyPredTransform(reiChildrenOrig[i], reiChildren[i], reiExp))
1140 : : {
1141 [ - - ]: 0 : Trace("strings-ipc-re")
1142 : 0 : << "... failed to justify child " << reiChildren[i] << " from "
1143 : 0 : << reiChildrenOrig[i] << std::endl;
1144 : 0 : successChildren = false;
1145 : 0 : break;
1146 : : }
1147 : : }
1148 [ - + ]: 35 : if (!successChildren)
1149 : : {
1150 : 0 : break;
1151 : : }
1152 : 105 : Node mem = psb.tryStep(ProofRule::RE_INTER, reiChildren, {});
1153 [ + - ]: 70 : Trace("strings-ipc-re")
1154 : 35 : << "Regular expression summary: " << mem << std::endl;
1155 : : // the conclusion is rewritable to the premises via rewriting?
1156 [ + - ]: 35 : if (psb.applyPredTransform(mem, conc, {}))
1157 : : {
1158 [ + - ]: 35 : Trace("strings-ipc-re") << "... success!" << std::endl;
1159 : 35 : useBuffer = true;
1160 : : }
1161 : : else
1162 : : {
1163 [ - - ]: 0 : Trace("strings-ipc-re")
1164 : 0 : << "...failed to rewrite to conclusion" << std::endl;
1165 : : }
1166 : : }
1167 : 35 : break;
1168 : 5 : case InferenceId::STRINGS_I_CYCLE_E:
1169 : : {
1170 [ - + ][ - + ]: 5 : Assert(ps.d_children.size() == 1);
[ - - ]
1171 : 5 : Node concE = psb.applyPredElim(ps.d_children[0],
1172 : : {},
1173 : : MethodId::SB_DEFAULT,
1174 : : MethodId::SBA_SEQUENTIAL,
1175 : 20 : MethodId::RW_EXT_REWRITE);
1176 [ + - ]: 5 : Trace("strings-ipc-debug") << "... elim to " << concE << std::endl;
1177 [ - + ]: 5 : if (concE != conc)
1178 : : {
1179 [ - - ]: 0 : if (concE.getKind() == Kind::AND)
1180 : : {
1181 [ - - ]: 0 : for (size_t i = 0, nchild = concE.getNumChildren(); i < nchild; i++)
1182 : : {
1183 [ - - ]: 0 : if (concE[i] == conc)
1184 : : {
1185 : 0 : Node ni = nm->mkConstInt(Rational(i));
1186 : 0 : psb.addStep(ProofRule::AND_ELIM, {concE}, {ni}, conc);
1187 : 0 : useBuffer = true;
1188 : 0 : break;
1189 : : }
1190 : : }
1191 : : }
1192 : : }
1193 : : else
1194 : : {
1195 : 5 : useBuffer = true;
1196 : : }
1197 : : }
1198 : 5 : break;
1199 : 10 : case InferenceId::STRINGS_CTN_DECOMPOSE:
1200 : : {
1201 [ - + ]: 10 : if (ps.d_children.size() != 2)
1202 : : {
1203 : 0 : break;
1204 : : }
1205 : 10 : Node ctn = ps.d_children[0];
1206 [ - + ]: 10 : if (ctn.getKind() != Kind::STRING_CONTAINS)
1207 : : {
1208 : 0 : break;
1209 : : }
1210 : 40 : Node pconc = psb.tryStep(ProofRule::STRING_EAGER_REDUCTION, {}, {ctn});
1211 [ + - ]: 10 : Trace("strings-ipc-cons") << "Eager reduction: " << pconc << std::endl;
1212 : 30 : Node pelim = psb.applyPredElim(pconc, {ctn}, MethodId::SB_LITERAL);
1213 [ + - ]: 10 : Trace("strings-ipc-cons") << "After rewriting: " << pelim << std::endl;
1214 [ - + ]: 10 : if (pelim.getKind() != Kind::EQUAL)
1215 : : {
1216 : 0 : break;
1217 : : }
1218 : 20 : Node tgt = ps.d_children[1];
1219 : 40 : Node pelim2 = psb.applyPredElim(tgt, {pelim});
1220 [ + - ]: 10 : Trace("strings-ipc-cons") << "After elim: " << pelim << std::endl;
1221 [ + - ]: 10 : if (pelim2 == conc)
1222 : : {
1223 : 10 : useBuffer = true;
1224 : : }
1225 : : }
1226 : 10 : break;
1227 : : // ========================== unknown and currently unsupported
1228 : 239 : case InferenceId::STRINGS_CARDINALITY:
1229 : : case InferenceId::STRINGS_I_CYCLE:
1230 : : case InferenceId::STRINGS_INFER_EMP:
1231 : : case InferenceId::STRINGS_RE_DELTA:
1232 : : case InferenceId::STRINGS_RE_DELTA_CONF:
1233 : : case InferenceId::STRINGS_RE_DERIVE:
1234 : : case InferenceId::STRINGS_FLOOP:
1235 : : case InferenceId::STRINGS_FLOOP_CONFLICT:
1236 : : case InferenceId::STRINGS_DEQ_NORM_EMP:
1237 : : case InferenceId::STRINGS_CTN_TRANS:
1238 : : default:
1239 : : // do nothing, these will be converted to THEORY_INFERENCE_STRINGS below
1240 : : // since the rule is unknown.
1241 : 239 : break;
1242 : : }
1243 : :
1244 : : // now see if we would succeed with the checker-to-try
1245 : 9551 : bool success = false;
1246 [ + + ]: 9551 : if (ps.d_rule != ProofRule::UNKNOWN)
1247 : : {
1248 [ + - ]: 866 : Trace("strings-ipc") << "For " << infer << ", try proof rule " << ps.d_rule
1249 : 433 : << "...";
1250 [ - + ][ - + ]: 433 : Assert(ps.d_rule != ProofRule::UNKNOWN);
[ - - ]
1251 : 866 : Node pconc = psb.tryStep(ps.d_rule, ps.d_children, ps.d_args);
1252 [ + - ][ - + ]: 433 : if (pconc.isNull() || pconc != conc)
[ - + ]
1253 : : {
1254 [ - - ]: 0 : Trace("strings-ipc") << "failed, pconc is " << pconc << " (expected "
1255 : 0 : << conc << ")" << std::endl;
1256 : 0 : ps.d_rule = ProofRule::UNKNOWN;
1257 : : }
1258 : : else
1259 : : {
1260 : : // successfully set up a single step proof in ps
1261 : 433 : success = true;
1262 [ + - ]: 433 : Trace("strings-ipc") << "success!" << std::endl;
1263 : : }
1264 : : }
1265 [ + + ]: 9118 : else if (useBuffer)
1266 : : {
1267 : : // successfully set up a multi step proof in psb
1268 : 8879 : success = true;
1269 : : }
1270 : : else
1271 : : {
1272 [ + - ]: 478 : Trace("strings-ipc") << "For " << infer << " " << conc
1273 : 239 : << ", no proof rule, failed" << std::endl;
1274 : : }
1275 [ + + ]: 9551 : if (!success)
1276 : : {
1277 : : // debug print
1278 [ - + ]: 239 : if (TraceIsOn("strings-ipc-fail"))
1279 : : {
1280 [ - - ]: 0 : Trace("strings-ipc-fail")
1281 : 0 : << "InferProofCons::convert: Failed " << infer
1282 [ - - ]: 0 : << (isRev ? " :rev " : " ") << conc << std::endl;
1283 [ - - ]: 0 : for (const Node& ec : exp)
1284 : : {
1285 [ - - ]: 0 : Trace("strings-ipc-fail") << " e: " << ec << std::endl;
1286 : : }
1287 : : }
1288 : : // untrustworthy conversion, the argument of THEORY_INFERENCE_STRINGS is
1289 : : // its conclusion
1290 : 239 : ps.d_args.clear();
1291 : 239 : ps.d_args.push_back(mkTrustId(nm, TrustId::THEORY_INFERENCE_STRINGS));
1292 : 239 : ps.d_args.push_back(conc);
1293 : : // use the trust rule
1294 : 239 : ps.d_rule = ProofRule::TRUST;
1295 : : }
1296 [ - + ]: 9551 : if (TraceIsOn("strings-ipc-debug"))
1297 : : {
1298 [ - - ]: 0 : if (useBuffer)
1299 : : {
1300 [ - - ]: 0 : Trace("strings-ipc-debug")
1301 : 0 : << "InferProofCons::convert returned buffer with "
1302 : 0 : << psb.getNumSteps() << " steps:" << std::endl;
1303 : 0 : const std::vector<std::pair<Node, ProofStep>>& steps = psb.getSteps();
1304 [ - - ]: 0 : for (const std::pair<Node, ProofStep>& step : steps)
1305 : : {
1306 [ - - ]: 0 : Trace("strings-ipc-debug")
1307 : 0 : << "- " << step.first << " via " << step.second << std::endl;
1308 : : }
1309 : : }
1310 : : else
1311 : : {
1312 [ - - ]: 0 : Trace("strings-ipc-debug")
1313 : 0 : << "InferProofCons::convert returned " << ps << std::endl;
1314 : : }
1315 : : }
1316 : : // make the proof based on the step or the buffer
1317 [ + + ]: 9551 : if (useBuffer)
1318 : : {
1319 [ - + ]: 8879 : if (!pf->addSteps(psb))
1320 : : {
1321 : 0 : return false;
1322 : : }
1323 : : }
1324 : : else
1325 : : {
1326 [ - + ]: 672 : if (!pf->addStep(conc, ps))
1327 : : {
1328 : 0 : return false;
1329 : : }
1330 : : }
1331 : 9551 : return true;
1332 : : }
1333 : :
1334 : 2801 : bool InferProofCons::convertLengthPf(Node lenReq,
1335 : : const std::vector<Node>& lenExp,
1336 : : TheoryProofStepBuffer& psb)
1337 : : {
1338 [ + + ]: 5339 : for (const Node& le : lenExp)
1339 : : {
1340 [ + + ]: 3801 : if (lenReq == le)
1341 : : {
1342 : 1263 : return true;
1343 : : }
1344 : : }
1345 [ + - ]: 3076 : Trace("strings-ipc-len") << "Must explain " << lenReq << " by " << lenExp
1346 : 1538 : << std::endl;
1347 [ + + ]: 1976 : for (const Node& le : lenExp)
1348 : : {
1349 : : // probably rewrites to it?
1350 : 1830 : std::vector<Node> exp;
1351 [ + + ]: 1830 : if (psb.applyPredTransform(le, lenReq, exp))
1352 : : {
1353 [ + - ]: 740 : Trace("strings-ipc-len") << "...success by rewrite" << std::endl;
1354 : 740 : return true;
1355 : : }
1356 : : // maybe x != "" => len(x) != 0
1357 : 1090 : std::vector<Node> children;
1358 : 1090 : children.push_back(le);
1359 : 1090 : std::vector<Node> args;
1360 : 1090 : Node res = psb.tryStep(ProofRule::STRING_LENGTH_NON_EMPTY, children, args);
1361 [ + + ]: 1090 : if (res == lenReq)
1362 : : {
1363 [ + - ]: 652 : Trace("strings-ipc-len") << "...success by LENGTH_NON_EMPTY" << std::endl;
1364 : 652 : return true;
1365 : : }
1366 : : }
1367 [ + - ]: 146 : Trace("strings-ipc-len") << "...failed" << std::endl;
1368 : 146 : return false;
1369 : : }
1370 : :
1371 : 154 : Node InferProofCons::convertTrans(Node eqa,
1372 : : Node eqb,
1373 : : TheoryProofStepBuffer& psb)
1374 : : {
1375 [ + - ][ - + ]: 154 : if (eqa.getKind() != Kind::EQUAL || eqb.getKind() != Kind::EQUAL)
[ - + ]
1376 : : {
1377 : 0 : return Node::null();
1378 : : }
1379 [ + + ]: 244 : for (uint32_t i = 0; i < 2; i++)
1380 : : {
1381 : 353 : Node eqaSym = i == 0 ? eqa[1].eqNode(eqa[0]) : eqa;
1382 [ + + ]: 381 : for (uint32_t j = 0; j < 2; j++)
1383 : : {
1384 : 383 : Node eqbSym = j == 0 ? eqb : eqb[1].eqNode(eqb[0]);
1385 [ + + ]: 291 : if (eqa[i] == eqb[j])
1386 : : {
1387 : 109 : std::vector<Node> children;
1388 : 109 : children.push_back(eqaSym);
1389 : 109 : children.push_back(eqbSym);
1390 : 109 : return psb.tryStep(ProofRule::TRANS, children, {});
1391 : : }
1392 : : }
1393 : : }
1394 : 45 : return Node::null();
1395 : : }
1396 : :
1397 : 270 : bool InferProofCons::convertAndElim(NodeManager* nm,
1398 : : const Node& src,
1399 : : const Node& tgt,
1400 : : TheoryProofStepBuffer& psb)
1401 : : {
1402 [ + + ]: 270 : if (src == tgt)
1403 : : {
1404 : 190 : return true;
1405 : : }
1406 [ + - ]: 160 : Trace("strings-ipc-debug")
1407 : 80 : << "AND_ELIM " << src << " => " << tgt << "?" << std::endl;
1408 : 160 : Node stgt;
1409 [ + + ][ + - ]: 80 : if (src.getKind() == Kind::NOT && src[0].getKind() == Kind::OR)
[ + + ][ + + ]
[ - - ]
1410 : : {
1411 : : // handles case of ~(L1 or ... or Ln) where tgt is ~Li.
1412 [ + - ]: 10 : for (size_t i = 0, nchild = src[0].getNumChildren(); i < nchild; i++)
1413 : : {
1414 : 20 : Node sn = src[0][i].negate();
1415 [ + + ]: 10 : if (CDProof::isSame(sn, tgt))
1416 : : {
1417 : 15 : Node snn = src[0][i].notNode();
1418 : 10 : Node ni = nm->mkConstInt(Rational(i));
1419 : 15 : psb.addStep(ProofRule::NOT_OR_ELIM, {src}, {ni}, snn);
1420 : : // double negation elimination if necessary
1421 [ - + ]: 5 : if (snn != sn)
1422 : : {
1423 : 0 : psb.addStep(ProofRule::NOT_NOT_ELIM, {snn}, {}, sn);
1424 : : }
1425 : 5 : stgt = sn;
1426 : 5 : break;
1427 : : }
1428 : : }
1429 : : }
1430 [ + + ]: 75 : else if (src.getKind() == Kind::AND)
1431 : : {
1432 : : // otherwise check case of (L1 and ... and Ln) => Li
1433 [ + - ]: 25 : for (size_t i = 0, nchild = src.getNumChildren(); i < nchild; i++)
1434 : : {
1435 [ + + ]: 25 : if (CDProof::isSame(src[i], tgt))
1436 : : {
1437 : 40 : Node ni = nm->mkConstInt(Rational(i));
1438 : 60 : psb.addStep(ProofRule::AND_ELIM, {src}, {ni}, src[i]);
1439 : 20 : stgt = src[i];
1440 : 20 : break;
1441 : : }
1442 : : }
1443 : : }
1444 [ + + ]: 80 : if (!stgt.isNull())
1445 : : {
1446 [ - + ][ - + ]: 25 : Assert(CDProof::isSame(stgt, tgt));
[ - - ]
1447 [ + + ]: 25 : if (stgt != tgt)
1448 : : {
1449 : 10 : psb.addStep(ProofRule::SYMM, {stgt}, {}, tgt);
1450 : : }
1451 : 25 : return true;
1452 : : }
1453 : 55 : return false;
1454 : : }
1455 : :
1456 : 6063 : Node InferProofCons::convertCoreSubs(Env& env,
1457 : : CDProof* pf,
1458 : : TheoryProofStepBuffer& psb,
1459 : : const Node& src,
1460 : : const std::vector<Node>& exp,
1461 : : size_t minIndex,
1462 : : size_t maxIndex,
1463 : : bool proveSrc)
1464 : : {
1465 : : // set up the conversion proof generator with string core term context
1466 : 12126 : StringCoreTermContext sctc;
1467 : : TConvProofGenerator tconv(env,
1468 : : nullptr,
1469 : : TConvPolicy::FIXPOINT,
1470 : : TConvCachePolicy::NEVER,
1471 : : "StrTConv",
1472 : 18189 : &sctc);
1473 : : // add the rewrites for nested contexts up to idMax.
1474 [ + + ]: 13521 : for (size_t i = minIndex; i <= maxIndex; i++)
1475 : : {
1476 [ + + ]: 23171 : for (const Node& s : exp)
1477 : : {
1478 [ + - ]: 31426 : Trace("strings-ipc-subs")
1479 : 15713 : << "--- rewrite " << s << ", id " << i << std::endl;
1480 [ - + ][ - + ]: 15713 : Assert(s.getKind() == Kind::EQUAL);
[ - - ]
1481 [ + - ]: 15713 : tconv.addRewriteStep(s[0], s[1], pf, false, TrustId::NONE, false, i);
1482 : : }
1483 : : }
1484 : 12126 : std::shared_ptr<ProofNode> pfn = tconv.getProofForRewriting(src);
1485 : 12126 : Node res = pfn->getResult();
1486 [ - + ][ - + ]: 6063 : Assert(res.getKind() == Kind::EQUAL);
[ - - ]
1487 [ + + ]: 6063 : if (res[0] != res[1])
1488 : : {
1489 [ - + ][ - + ]: 5899 : Assert(res[0] == src);
[ - - ]
1490 [ + - ]: 5899 : Trace("strings-ipc-subs") << "Substitutes: " << res << std::endl;
1491 : 5899 : pf->addProof(pfn);
1492 : : // The proof step buffer is tracking unique conclusions, we (dummy) mark
1493 : : // that we have a proof of res via the proof above to ensure we do not
1494 : : // reprove it.
1495 : 11798 : psb.addStep(ProofRule::ASSUME, {}, {res}, res);
1496 [ + + ]: 5899 : if (proveSrc)
1497 : : {
1498 [ + + ][ - - ]: 7740 : psb.addStep(ProofRule::EQ_RESOLVE, {res[1], res[1].eqNode(src)}, {}, src);
1499 : : }
1500 : : else
1501 : : {
1502 [ + + ][ - - ]: 9957 : psb.addStep(ProofRule::EQ_RESOLVE, {src, res}, {}, res[1]);
1503 : : }
1504 : 5899 : return res[1];
1505 : : }
1506 : 164 : return src;
1507 : : }
1508 : :
1509 : 6342 : Node InferProofCons::spliceConstants(Env& env,
1510 : : ProofRule rule,
1511 : : TheoryProofStepBuffer& psb,
1512 : : const Node& eq,
1513 : : const Node& conc,
1514 : : bool isRev)
1515 : : {
1516 [ - + ][ - + ]: 6342 : Assert(eq.getKind() == Kind::EQUAL);
[ - - ]
1517 [ + - ]: 12684 : Trace("strings-ipc-splice")
1518 : 6342 : << "Splice " << rule << " (" << isRev << ") for " << eq << std::endl;
1519 : 12684 : std::vector<Node> tvec;
1520 : 12684 : std::vector<Node> svec;
1521 : 6342 : theory::strings::utils::getConcat(eq[0], tvec);
1522 : 6342 : theory::strings::utils::getConcat(eq[1], svec);
1523 : 6342 : size_t nts = tvec.size();
1524 : 6342 : size_t nss = svec.size();
1525 [ + + ]: 6342 : size_t n = nts > nss ? nss : nts;
1526 [ + - ]: 8500 : for (size_t i = 0; i < n; i++)
1527 : : {
1528 [ + + ]: 8500 : size_t ti = isRev ? nts - i - 1 : i;
1529 [ + + ]: 8500 : size_t si = isRev ? nss - i - 1 : i;
1530 : 8500 : Node currT = tvec[ti];
1531 : 8500 : Node currS = svec[si];
1532 [ + + ]: 8500 : if (currT == currS)
1533 : : {
1534 : 2158 : continue;
1535 : : }
1536 [ + + ]: 6342 : if (rule == ProofRule::CONCAT_EQ)
1537 : : {
1538 [ + + ][ + + ]: 4131 : if (!currT.isConst() || !currS.isConst())
[ + + ]
1539 : : {
1540 : : // no need to splice
1541 : 7243 : return eq;
1542 : : }
1543 : : // remove the common prefix
1544 : : // get the equal prefix/suffix, strip and add the remainders
1545 : : size_t sindex;
1546 : 1214 : Node currR = Word::splitConstant(currT, currS, sindex, isRev);
1547 [ + + ]: 607 : if (currR.isNull())
1548 : : {
1549 : : // no need to splice
1550 : 195 : return eq;
1551 : : }
1552 [ + + ]: 412 : size_t index = sindex == 1 ? si : ti;
1553 [ + + ]: 412 : std::vector<Node>& vec = sindex == 1 ? svec : tvec;
1554 [ + + ]: 412 : Node o = sindex == 1 ? currT : currS;
1555 : 412 : vec[index] = o;
1556 [ + + ]: 412 : vec.insert(vec.begin() + index + (isRev ? 0 : 1), currR);
1557 : : }
1558 [ + - ]: 1456 : else if (rule == ProofRule::CONCAT_UNIFY && !conc.isNull()
1559 [ + + ][ + + ]: 3667 : && conc.getKind() == Kind::EQUAL)
[ + + ]
1560 : : {
1561 [ + - ]: 2602 : Trace("strings-ipc-splice")
1562 : 0 : << "Splice cprop at " << currT << " / " << currS
1563 : 1301 : << ", for conclusion " << conc << std::endl;
1564 [ + + ]: 3903 : for (size_t j = 0; j < 2; j++)
1565 : : {
1566 [ + + ]: 2602 : Node src = j == 0 ? currT : currS;
1567 [ + + ]: 2602 : Node tgt = j == 0 ? conc[0] : conc[1];
1568 [ + + ]: 2602 : if (src == tgt)
1569 : : {
1570 : 2592 : continue;
1571 : : }
1572 [ + - ][ - + ]: 10 : if (!src.isConst() || !tgt.isConst())
[ - + ]
1573 : : {
1574 : 0 : Assert(false) << "Non-constant for unify";
1575 : : return eq;
1576 : : }
1577 [ + - ]: 10 : size_t index = j == 0 ? ti : si;
1578 [ + - ]: 10 : std::vector<Node>& vec = j == 0 ? tvec : svec;
1579 : 10 : size_t lentgt = Word::getLength(tgt);
1580 : 10 : size_t len = Word::getLength(src);
1581 [ - + ]: 10 : if (len <= lentgt)
1582 : : {
1583 : 0 : Assert(false) << "Smaller source for unify";
1584 : : return eq;
1585 : : }
1586 [ + - ]: 10 : if (isRev)
1587 : : {
1588 : 10 : vec[index] = Word::suffix(src, lentgt);
1589 : 10 : vec.insert(vec.begin() + index, Word::prefix(src, len - lentgt));
1590 : : }
1591 : : else
1592 : : {
1593 : 0 : vec[index] = Word::prefix(src, lentgt);
1594 : 0 : vec.insert(vec.begin() + index + 1, Word::suffix(src, len - lentgt));
1595 : : }
1596 : : }
1597 : : }
1598 [ + + ]: 910 : else if (rule == ProofRule::CONCAT_CSPLIT)
1599 : : {
1600 [ - + ]: 755 : if (!currS.isConst())
1601 : : {
1602 : 0 : Assert(false) << "Non-constant for csplit";
1603 : : return eq;
1604 : : }
1605 : : // split the first character
1606 : 755 : size_t len = Word::getLength(currS);
1607 [ + + ]: 755 : if (len == 1)
1608 : : {
1609 : : // not needed
1610 : 553 : return eq;
1611 : : }
1612 [ + + ]: 202 : if (isRev)
1613 : : {
1614 : 122 : svec[si] = Word::suffix(currS, 1);
1615 : 122 : svec.insert(svec.begin() + si, Word::prefix(currS, len - 1));
1616 : : }
1617 : : else
1618 : : {
1619 : 80 : svec[si] = Word::prefix(currS, 1);
1620 : 80 : svec.insert(svec.begin() + si + 1, Word::suffix(currS, len - 1));
1621 : : }
1622 : : }
1623 [ + - ]: 155 : else if (rule == ProofRule::CONCAT_UNIFY && conc.isConst()
1624 [ + - ][ + - ]: 310 : && !conc.getConst<bool>())
[ + - ]
1625 : : {
1626 [ + - ][ - + ]: 155 : if (!currT.isConst() || !currS.isConst())
[ - + ]
1627 : : {
1628 : 0 : Assert(false) << "Non-constants for concat conflict";
1629 : 90 : return eq;
1630 : : }
1631 : : // isolate a disequal prefix by taking maximal prefix/suffix
1632 : 155 : size_t lens = Word::getLength(currS);
1633 : 155 : size_t lent = Word::getLength(currT);
1634 [ + + ]: 155 : if (lens == lent)
1635 : : {
1636 : : // no need
1637 : 90 : return eq;
1638 : : }
1639 [ + + ]: 65 : std::vector<Node>& vec = lens > lent ? svec : tvec;
1640 [ + + ]: 65 : Node curr = lens > lent ? currS : currT;
1641 [ + + ]: 65 : size_t index = lens > lent ? si : ti;
1642 [ + + ]: 65 : size_t smallLen = lens > lent ? lent : lens;
1643 [ + + ]: 65 : size_t diffLen = lens > lent ? (lens - lent) : (lent - lens);
1644 : 65 : vec[index] =
1645 : 130 : isRev ? Word::suffix(curr, smallLen) : Word::prefix(curr, smallLen);
1646 : : vec.insert(
1647 [ + + ]: 65 : vec.begin() + index + (isRev ? 0 : 1),
1648 : 130 : isRev ? Word::prefix(curr, diffLen) : Word::suffix(curr, diffLen));
1649 : : }
1650 : : else
1651 : : {
1652 : 0 : Assert(false) << "Unknown rule to splice " << rule;
1653 : : return eq;
1654 : : }
1655 : 3960 : TypeNode stype = eq[0].getType();
1656 : 3960 : Node tr = utils::mkConcat(tvec, stype);
1657 : 3960 : Node sr = utils::mkConcat(svec, stype);
1658 : 3960 : Node eqr = tr.eqNode(sr);
1659 [ + - ]: 1980 : Trace("strings-ipc-splice") << "...splice to " << eqr << std::endl;
1660 : 3960 : std::vector<Node> cexp;
1661 [ - + ]: 1980 : if (!psb.applyPredTransform(eq, eqr, cexp))
1662 : : {
1663 : 0 : Assert(false) << "Failed to show " << eqr << " spliced from " << eq;
1664 : : return eq;
1665 : : }
1666 : 1980 : return eqr;
1667 : : }
1668 : : // no change
1669 : 0 : return eq;
1670 : : }
1671 : :
1672 : 24512 : std::shared_ptr<ProofNode> InferProofCons::getProofFor(Node fact)
1673 : : {
1674 : : // get the inference
1675 : 24512 : NodeInferInfoMap::iterator it = d_lazyFactMap.find(fact);
1676 [ - + ]: 24512 : if (it == d_lazyFactMap.end())
1677 : : {
1678 : 0 : Node factSym = CDProof::getSymmFact(fact);
1679 [ - - ]: 0 : if (!factSym.isNull())
1680 : : {
1681 : : // Use the symmetric fact. There is no need to explictly make a
1682 : : // SYMM proof, as this is handled by CDProof::getProofFor below.
1683 : 0 : it = d_lazyFactMap.find(factSym);
1684 : : }
1685 : : }
1686 [ - + ][ - + ]: 24512 : AlwaysAssert(it != d_lazyFactMap.end());
[ - - ]
1687 : 49024 : std::shared_ptr<InferInfo> ii = (*it).second;
1688 [ - + ][ - + ]: 24512 : Assert(ii->d_conc == fact);
[ - - ]
1689 : : // make a placeholder proof using STRINGS_INFERENCE, which is reconstructed
1690 : : // during post-process
1691 : 73536 : CDProof pf(d_env);
1692 : 49024 : std::vector<Node> args;
1693 : 24512 : packArgs(ii->d_conc, ii->getId(), ii->d_idRev, ii->d_premises, args);
1694 : : // must flatten
1695 : 24512 : std::vector<Node> exp;
1696 [ + + ]: 78475 : for (const Node& ec : ii->d_premises)
1697 : : {
1698 : 53963 : utils::flattenOp(Kind::AND, ec, exp);
1699 : : }
1700 : 24512 : pf.addStep(fact, ProofRule::MACRO_STRING_INFERENCE, exp, args);
1701 : 49024 : return pf.getProofFor(fact);
1702 : : }
1703 : :
1704 : 0 : std::string InferProofCons::identify() const
1705 : : {
1706 : 0 : return "strings::InferProofCons";
1707 : : }
1708 : :
1709 : : } // namespace strings
1710 : : } // namespace theory
1711 : : } // namespace cvc5::internal
|
