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