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 : : * Sequences solver for seq.nth/seq.update.
11 : : */
12 : :
13 : : #include "theory/strings/array_solver.h"
14 : :
15 : : #include "expr/sequence.h"
16 : : #include "theory/strings/arith_entail.h"
17 : : #include "theory/strings/theory_strings_utils.h"
18 : : #include "theory/strings/word.h"
19 : : #include "util/rational.h"
20 : : #include "util/string.h"
21 : :
22 : : using namespace cvc5::context;
23 : : using namespace cvc5::internal::kind;
24 : :
25 : : namespace cvc5::internal {
26 : : namespace theory {
27 : : namespace strings {
28 : :
29 : 28738 : ArraySolver::ArraySolver(Env& env,
30 : : SolverState& s,
31 : : InferenceManager& im,
32 : : TermRegistry& tr,
33 : : BaseSolver& bs,
34 : : CoreSolver& cs,
35 : : ExtfSolver& es,
36 : 28738 : ExtTheory& extt)
37 : : : EnvObj(env),
38 : 28738 : d_state(s),
39 : 28738 : d_im(im),
40 : 28738 : d_termReg(tr),
41 : 28738 : d_bsolver(bs),
42 : 28738 : d_csolver(cs),
43 : 28738 : d_esolver(es),
44 : 28738 : d_coreSolver(env, s, im, tr, es, extt),
45 : 57476 : d_eqProc(context())
46 : : {
47 : 28738 : NodeManager* nm = nodeManager();
48 : 28738 : d_zero = nm->mkConstInt(Rational(0));
49 : 28738 : }
50 : :
51 : 28725 : ArraySolver::~ArraySolver() {}
52 : :
53 : 389 : void ArraySolver::checkArrayConcat()
54 : : {
55 [ + + ]: 389 : if (!d_termReg.hasSeqUpdate())
56 : : {
57 [ + - ]: 164 : Trace("seq-array") << "No seq.update/seq.nth terms, skipping check..."
58 : 82 : << std::endl;
59 : 82 : return;
60 : : }
61 : 307 : d_currTerms.clear();
62 [ + - ]: 307 : Trace("seq-array") << "ArraySolver::checkArrayConcat..." << std::endl;
63 : : // Get the set of relevant terms. The core array solver requires knowing this
64 : : // set to ensure its write model is only over relevant terms.
65 : 307 : std::vector<Node> terms = d_esolver.getRelevantActive();
66 : 307 : checkTerms(terms);
67 : 307 : }
68 : :
69 : 245 : void ArraySolver::checkArray()
70 : : {
71 [ + + ]: 245 : if (!d_termReg.hasSeqUpdate())
72 : : {
73 [ + - ]: 164 : Trace("seq-array") << "No seq.update/seq.nth terms, skipping check..."
74 : 82 : << std::endl;
75 : 82 : return;
76 : : }
77 [ + - ]: 163 : Trace("seq-array") << "ArraySolver::checkArray..." << std::endl;
78 : 163 : d_coreSolver.check(d_currTerms[Kind::SEQ_NTH],
79 : 326 : d_currTerms[Kind::STRING_UPDATE]);
80 : : }
81 : :
82 : 170 : void ArraySolver::checkArrayEager()
83 : : {
84 [ - + ]: 170 : if (!d_termReg.hasSeqUpdate())
85 : : {
86 [ - - ]: 0 : Trace("seq-array") << "No seq.update/seq.nth terms, skipping check..."
87 : 0 : << std::endl;
88 : 0 : return;
89 : : }
90 [ + - ]: 170 : Trace("seq-array") << "ArraySolver::checkArray..." << std::endl;
91 : : // get the set of relevant terms, for reasons described above
92 : 170 : std::vector<Node> terms = d_esolver.getRelevantActive();
93 : 170 : std::vector<Node> nthTerms;
94 : 170 : std::vector<Node> updateTerms;
95 [ + + ]: 1019 : for (const Node& n : terms)
96 : : {
97 : 849 : Kind k = n.getKind();
98 [ + + ]: 849 : if (k == Kind::STRING_UPDATE)
99 : : {
100 : 149 : updateTerms.push_back(n);
101 : : }
102 [ + + ]: 700 : else if (k == Kind::SEQ_NTH)
103 : : {
104 : 458 : nthTerms.push_back(n);
105 : : }
106 : : }
107 : 170 : d_coreSolver.check(nthTerms, updateTerms);
108 : 170 : }
109 : :
110 : 307 : void ArraySolver::checkTerms(const std::vector<Node>& terms)
111 : : {
112 : : // get all the active update terms that have not been reduced in the
113 : : // current context by context-dependent simplification
114 : 307 : std::unordered_set<Node> processed;
115 [ + + ]: 4269 : for (const Node& t : terms)
116 : : {
117 : 3962 : bool checkInv = false;
118 : 3962 : Kind k = t.getKind();
119 [ + - ]: 3962 : Trace("seq-array-debug") << "check term " << t << "..." << std::endl;
120 [ + + ]: 3962 : if (k == Kind::STRING_UPDATE)
121 : : {
122 [ + + ]: 598 : if (!d_termReg.isHandledUpdateOrSubstr(t))
123 : : {
124 : : // not handled by procedure
125 [ + - ]: 98 : Trace("seq-array-debug") << "...unhandled" << std::endl;
126 : 98 : continue;
127 : : }
128 : : // for update terms, also check the inverse inference
129 : 500 : checkInv = true;
130 : : }
131 [ + + ]: 3364 : else if (k != Kind::SEQ_NTH)
132 : : {
133 : 446 : continue;
134 : : }
135 : :
136 [ + + ]: 3418 : if (d_bsolver.isCongruent(t))
137 : : {
138 : 890 : continue;
139 : : }
140 : :
141 : : // check the normal inference
142 : 2528 : checkTerm(t, false);
143 [ + + ]: 2528 : if (checkInv)
144 : : {
145 : 424 : checkTerm(t, true);
146 : : }
147 : : }
148 : 307 : }
149 : :
150 : 2952 : void ArraySolver::checkTerm(Node t, bool checkInv)
151 : : {
152 : 2952 : NodeManager* nm = nodeManager();
153 : 2952 : Kind k = t.getKind();
154 : 5904 : Node r = d_state.getRepresentative(t[0]);
155 : 2952 : Node rself;
156 : 2952 : NormalForm& nf = d_csolver.getNormalForm(r);
157 [ + - ]: 2952 : Trace("seq-array-debug") << "...normal form " << nf.d_nf << std::endl;
158 : 2952 : std::vector<Node> nfChildren;
159 : :
160 [ + + ]: 2952 : if (k == Kind::SEQ_NTH)
161 : : {
162 : : // The core solver must process all `nth` terms
163 : 2104 : d_currTerms[Kind::SEQ_NTH].push_back(t);
164 : : }
165 : :
166 [ + + ]: 2952 : if (checkInv)
167 : : {
168 [ - + ]: 424 : if (k != Kind::STRING_UPDATE)
169 : : {
170 : 0 : return;
171 : : }
172 : : // If the term we are updating is atomic, but the update itself
173 : : // not atomic, then we will apply the inverse version of the update
174 : : // concat rule, based on the normal form of the term itself.
175 : 424 : rself = d_state.getRepresentative(t);
176 : 424 : NormalForm& nfSelf = d_csolver.getNormalForm(rself);
177 [ + + ]: 424 : if (nfSelf.d_nf.size() > 1)
178 : : {
179 : 90 : nfChildren.insert(
180 : 90 : nfChildren.end(), nfSelf.d_nf.begin(), nfSelf.d_nf.end());
181 : : }
182 : : else
183 : : {
184 : 379 : return;
185 : : }
186 : : }
187 : : else
188 : : {
189 [ + + ]: 2528 : if (nf.d_nf.empty())
190 : : {
191 : : // updates should have been reduced (UPD_EMPTYSTR)
192 [ - + ][ - + ]: 4 : Assert(k != Kind::STRING_UPDATE);
[ - - ]
193 [ + - ]: 4 : Trace("seq-array-debug") << "...empty" << std::endl;
194 : 4 : return;
195 : : }
196 [ + + ]: 2524 : else if (nf.d_nf.size() == 1)
197 : : {
198 [ + - ]: 2091 : Trace("seq-array-debug") << "...norm form size 1" << std::endl;
199 : : // NOTE: could split on n=0 if needed, do not introduce ITE
200 : 2091 : Kind ck = nf.d_nf[0].getKind();
201 : 2091 : bool cIsConst = nf.d_nf[0].isConst();
202 : : // Note that (seq.unit c) is rewritten to CONST_SEQUENCE{c}, hence we
203 : : // check two cases here. It is important for completeness of this schema
204 : : // to handle this differently from STRINGS_ARRAY_UPDATE_CONCAT /
205 : : // STRINGS_ARRAY_NTH_CONCAT. Otherwise we would conclude a trivial
206 : : // equality when update/nth is applied to a constant of length one.
207 [ + - ]: 1672 : if (ck == Kind::SEQ_UNIT || ck == Kind::STRING_UNIT
208 [ + + ][ + + ]: 3763 : || (cIsConst && Word::getLength(nf.d_nf[0]) == 1))
[ + - ][ + + ]
[ + + ][ - - ]
209 : : {
210 [ + - ]: 446 : Trace("seq-array-debug") << "...unit case" << std::endl;
211 : : // do we know whether n = 0 ?
212 : : // x = (seq.unit m) => (seq.update x n z) = ite(n=0, z, (seq.unit m))
213 : : // x = (seq.unit m) ^ n=0 => (seq.nth x n) = m
214 : : InferenceId iid;
215 : 446 : Node eq;
216 : 446 : std::vector<Node> exp;
217 : 446 : std::vector<Node> nexp;
218 : 446 : d_im.addToExplanation(t[0], nf.d_nf[0], exp);
219 : 446 : d_im.addToExplanation(r, t[0], exp);
220 [ + + ]: 446 : if (k == Kind::STRING_UPDATE)
221 : : {
222 : 7 : iid = InferenceId::STRINGS_ARRAY_UPDATE_UNIT;
223 [ + + ][ - - ]: 49 : eq = nm->mkNode(
224 : : Kind::ITE,
225 : 35 : {t[1].eqNode(d_zero), t.eqNode(t[2]), t.eqNode(nf.d_nf[0])});
226 : : }
227 : : else
228 : : {
229 [ + + ]: 439 : if (d_state.areDisequal(t[1], d_zero))
230 : : {
231 : : // n is known to be disequal from zero, skip
232 : 56 : return;
233 : : }
234 [ - + ][ - + ]: 383 : Assert(k == Kind::SEQ_NTH);
[ - - ]
235 : 383 : Node val;
236 [ + + ]: 383 : if (cIsConst)
237 : : {
238 : 20 : val = Word::getNth(nf.d_nf[0], 0);
239 : : }
240 : : else
241 : : {
242 : 363 : val = nf.d_nf[0][0];
243 : : }
244 : 383 : iid = InferenceId::STRINGS_ARRAY_NTH_UNIT;
245 : 383 : eq = t.eqNode(val);
246 [ + + ]: 383 : if (t[1] != d_zero)
247 : : {
248 : 292 : exp.push_back(t[1].eqNode(d_zero));
249 : 292 : nexp.push_back(t[1].eqNode(d_zero));
250 : : }
251 : 383 : }
252 [ + + ]: 390 : if (d_eqProc.find(eq) == d_eqProc.end())
253 : : {
254 : 271 : d_eqProc.insert(eq);
255 : 271 : d_im.sendInference(exp, nexp, eq, iid);
256 : : }
257 : 390 : return;
258 : 446 : }
259 [ + - ]: 1645 : else if (!cIsConst)
260 : : {
261 [ + + ]: 1645 : if (k == Kind::STRING_UPDATE)
262 : : {
263 : : // If the term we are updating is atomic, but the update itself
264 : : // not atomic, then we will apply the inverse version of the update
265 : : // concat rule, based on the normal form of the term itself.
266 : 374 : rself = d_state.getRepresentative(t);
267 : 374 : NormalForm& nfSelf = d_csolver.getNormalForm(rself);
268 [ + + ]: 374 : if (nfSelf.d_nf.size() == 1)
269 : : {
270 : : // otherwise, if the normal form is not a constant word, and we
271 : : // are an atomic update term, then this term will be given to the
272 : : // core array solver.
273 : 372 : d_currTerms[k].push_back(t);
274 : : }
275 : : }
276 : 1645 : return;
277 : : }
278 : : else
279 : : {
280 : : // if the normal form is a constant word, it is treated as a
281 : : // concatenation. We split per character and case split on whether the
282 : : // nth/update falls on each character below, which must have a size
283 : : // greater than one.
284 : 0 : std::vector<Node> chars = Word::getChars(nf.d_nf[0]);
285 : 0 : Assert(chars.size() > 1);
286 : 0 : nfChildren.insert(nfChildren.end(), chars.begin(), chars.end());
287 : 0 : }
288 : : }
289 : : else
290 : : {
291 : 433 : nfChildren.insert(nfChildren.end(), nf.d_nf.begin(), nf.d_nf.end());
292 : : }
293 : : }
294 : : // otherwise, we are the concatenation of the components
295 : : // NOTE: for nth, split on index vs component lengths, do not introduce ITE
296 : 478 : std::vector<Node> cond;
297 : 478 : std::vector<Node> cchildren;
298 : 478 : std::vector<Node> lacc;
299 : 478 : SkolemCache* skc = d_termReg.getSkolemCache();
300 [ + + ]: 1574 : for (const Node& c : nfChildren)
301 : : {
302 [ + - ]: 1096 : Trace("seq-array-debug") << "...process " << c << std::endl;
303 : 1096 : Node clen = nm->mkNode(Kind::STRING_LENGTH, c);
304 : 1096 : Node currIndex = t[1];
305 : 1096 : Node currSum = d_zero;
306 [ + + ]: 1096 : if (!lacc.empty())
307 : : {
308 [ + + ]: 618 : currSum = lacc.size() == 1 ? lacc[0] : nm->mkNode(Kind::ADD, lacc);
309 : 618 : currIndex = nm->mkNode(Kind::SUB, currIndex, currSum);
310 : : }
311 : 1096 : Node cc;
312 [ + + ][ + + ]: 1096 : if (k == Kind::STRING_UPDATE && checkInv)
313 : : {
314 : : // component for the reverse form of the update inference is a fresh
315 : : // variable, in particular, the purification variable for the substring
316 : : // of the term we are updating.
317 : 180 : Node sstr = nm->mkNode(Kind::STRING_SUBSTR, t[0], currSum, clen);
318 : 90 : cc = skc->mkSkolemCached(sstr, SkolemCache::SK_PURIFY, "z");
319 : 90 : }
320 : : // If it is a constant of length one, then the update/nth is determined
321 : : // in this interval. Notice this is done here as
322 : : // an optimization to short cut introducing terms like
323 : : // (seq.nth (seq.unit c) i), which by construction is only relevant in
324 : : // the context where i = 0, hence we replace by c here.
325 [ - + ]: 1006 : else if (c.isConst())
326 : : {
327 [ - - ]: 0 : if (Word::getLength(c) == 1)
328 : : {
329 [ - - ]: 0 : if (k == Kind::STRING_UPDATE)
330 : : {
331 : 0 : cc = nm->mkNode(Kind::ITE, t[1].eqNode(d_zero), t[2], c);
332 : : }
333 : : else
334 : : {
335 : 0 : cc = Word::getNth(c, 0);
336 : : }
337 : : }
338 : : }
339 : : // if we did not process as a constant of length one
340 [ + + ]: 1096 : if (cc.isNull())
341 : : {
342 [ + + ]: 1006 : if (k == Kind::STRING_UPDATE)
343 : : {
344 : 86 : cc = nm->mkNode(Kind::STRING_UPDATE, c, currIndex, t[2]);
345 : : }
346 : : else
347 : : {
348 [ - + ][ - + ]: 920 : Assert(k == Kind::SEQ_NTH);
[ - - ]
349 : 920 : cc = nm->mkNode(Kind::SEQ_NTH, c, currIndex);
350 : : }
351 : : }
352 [ + - ]: 1096 : Trace("seq-array-debug") << "......component " << cc << std::endl;
353 : 1096 : cchildren.push_back(cc);
354 : 1096 : lacc.push_back(clen);
355 [ + + ]: 1096 : if (k == Kind::SEQ_NTH)
356 : : {
357 : : Node currSumPost =
358 [ + + ]: 920 : lacc.size() == 1 ? lacc[0] : nm->mkNode(Kind::ADD, lacc);
359 : 1840 : Node cf = nm->mkNode(Kind::LT, t[1], currSumPost);
360 [ + - ]: 920 : Trace("seq-array-debug") << "......condition " << cf << std::endl;
361 : 920 : cond.push_back(cf);
362 : 920 : }
363 [ + - ][ + + ]: 176 : else if (k == Kind::STRING_UPDATE && checkInv)
364 : : {
365 : 180 : Node ccu = nm->mkNode(Kind::STRING_UPDATE, cc, currIndex, t[2]);
366 : 90 : Node eq = c.eqNode(ccu);
367 [ + - ]: 90 : Trace("seq-array-debug") << "......condition " << eq << std::endl;
368 : 90 : cond.push_back(eq);
369 : 90 : }
370 : 1096 : }
371 : : // z = (seq.++ x y) =>
372 : : // (seq.update z n l) =
373 : : // (seq.++ (seq.update x n 1) (seq.update y (- n len(x)) 1))
374 : : // z = (seq.++ x y) ^ (>= n 0) ^ (< n (+ (str.len x) (str.len y)))) =>
375 : : // (seq.nth z n) =
376 : : // (ite (< n (str.len x)) (seq.nth x n)
377 : : // (seq.nth y (- n (str.len x))))
378 : : InferenceId iid;
379 : 478 : std::vector<Node> exp;
380 : 478 : std::vector<Node> nexp;
381 : 478 : Node eq;
382 [ + + ]: 478 : if (k == Kind::STRING_UPDATE)
383 : : {
384 : 88 : Node finalc = utils::mkConcat(cchildren, t.getType());
385 [ + + ]: 88 : if (checkInv)
386 : : {
387 : 45 : eq = t[0].eqNode(finalc);
388 : 45 : cond.push_back(eq);
389 : 45 : eq = nm->mkAnd(cond);
390 : : }
391 : : else
392 : : {
393 : 43 : eq = t.eqNode(finalc);
394 : : }
395 : : // Must rewrite the equality to ensure terms are in rewritten form. This
396 : : // is important since this inference may be processed as a fact.
397 : 88 : eq = rewrite(eq);
398 [ + + ]: 88 : iid = checkInv ? InferenceId::STRINGS_ARRAY_UPDATE_CONCAT_INVERSE
399 : : : InferenceId::STRINGS_ARRAY_UPDATE_CONCAT;
400 : 88 : }
401 : : else
402 : : {
403 : 390 : std::reverse(cchildren.begin(), cchildren.end());
404 : 390 : std::reverse(cond.begin(), cond.end());
405 : 390 : eq = t.eqNode(cchildren[0]);
406 [ + + ]: 920 : for (size_t i = 1, ncond = cond.size(); i < ncond; i++)
407 : : {
408 : 530 : eq = nm->mkNode(Kind::ITE, cond[i], t.eqNode(cchildren[i]), eq);
409 : : }
410 : : Node inBoundsCond =
411 : 780 : nm->mkNode(Kind::AND, nm->mkNode(Kind::GEQ, t[1], d_zero), cond[0]);
412 : 390 : exp.push_back(inBoundsCond);
413 : 390 : nexp.push_back(inBoundsCond);
414 : 390 : iid = InferenceId::STRINGS_ARRAY_NTH_CONCAT;
415 : 390 : }
416 [ + + ]: 478 : if (checkInv)
417 : : {
418 : 45 : NormalForm& nfSelf = d_csolver.getNormalForm(rself);
419 : 45 : exp.insert(exp.end(), nfSelf.d_exp.begin(), nfSelf.d_exp.end());
420 : 45 : d_im.addToExplanation(t, nfSelf.d_base, exp);
421 : : }
422 : : else
423 : : {
424 : 433 : exp.insert(exp.end(), nf.d_exp.begin(), nf.d_exp.end());
425 : 433 : d_im.addToExplanation(t[0], nf.d_base, exp);
426 : : }
427 [ + + ]: 478 : if (d_eqProc.find(eq) == d_eqProc.end())
428 : : {
429 : 349 : d_eqProc.insert(eq);
430 [ + - ]: 349 : Trace("seq-array") << "- send lemma - " << eq << std::endl;
431 : 349 : d_im.sendInference(exp, nexp, eq, iid);
432 : : }
433 [ + + ][ + + ]: 7900 : }
[ + + ]
434 : :
435 : 100 : const std::map<Node, Node>& ArraySolver::getWriteModel(Node eqc)
436 : : {
437 : 100 : return d_coreSolver.getWriteModel(eqc);
438 : : }
439 : :
440 : 62 : const std::map<Node, Node>& ArraySolver::getConnectedSequences()
441 : : {
442 : 62 : return d_coreSolver.getConnectedSequences();
443 : : }
444 : :
445 : : } // namespace strings
446 : : } // namespace theory
447 : : } // namespace cvc5::internal
|
