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