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