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 : : * Base solver for the theory of strings. This class implements term
11 : : * indexing and constant inference for the theory of strings.
12 : : */
13 : :
14 : : #include "theory/strings/base_solver.h"
15 : :
16 : : #include "expr/sequence.h"
17 : : #include "options/quantifiers_options.h"
18 : : #include "options/strings_options.h"
19 : : #include "theory/rewriter.h"
20 : : #include "theory/strings/theory_strings_utils.h"
21 : : #include "theory/strings/word.h"
22 : : #include "util/cardinality.h"
23 : : #include "util/rational.h"
24 : : #include "util/string.h"
25 : :
26 : : using namespace std;
27 : : using namespace cvc5::context;
28 : : using namespace cvc5::internal::kind;
29 : :
30 : : namespace cvc5::internal {
31 : : namespace theory {
32 : : namespace strings {
33 : :
34 : 49981 : BaseSolver::BaseSolver(Env& env,
35 : : SolverState& s,
36 : : InferenceManager& im,
37 : 49981 : TermRegistry& tr)
38 : : : EnvObj(env),
39 : 49981 : d_state(s),
40 : 49981 : d_im(im),
41 : 49981 : d_termReg(tr),
42 : 49981 : d_congruent(context()),
43 : 99962 : d_strUnitOobEq(userContext())
44 : : {
45 : 49981 : d_false = nodeManager()->mkConst(false);
46 : 49981 : d_cardSize = options().strings.stringsAlphaCard;
47 : 49981 : }
48 : :
49 : 49636 : BaseSolver::~BaseSolver() {}
50 : :
51 : : /**
52 : : * Implements union find, with path compression
53 : : */
54 : 11537 : Node getRep(const Node& n, std::map<Node, Node>& rep)
55 : : {
56 : 11537 : std::map<Node, Node>::iterator it = rep.find(n);
57 [ + + ]: 11537 : if (it == rep.end())
58 : : {
59 : 11290 : return n;
60 : : }
61 [ - + ][ - + ]: 247 : Assert(n != it->second);
[ - - ]
62 : 247 : Node r = getRep(it->second, rep);
63 : 247 : rep[n] = r;
64 : 247 : return r;
65 : 247 : }
66 : :
67 : 100873 : void BaseSolver::checkInit()
68 : : {
69 : : // build term index
70 : 100873 : d_eqcInfo.clear();
71 : 100873 : d_termIndex.clear();
72 : 100873 : d_stringLikeEqc.clear();
73 : :
74 : 100873 : const std::set<Node>& rlvSet = d_termReg.getRelevantTermSet();
75 : :
76 [ + - ]: 100873 : Trace("strings-base") << "BaseSolver::checkInit" << std::endl;
77 : : // count of congruent, non-congruent per operator (independent of type),
78 : : // for debugging.
79 : 100873 : std::map<Kind, std::pair<uint32_t, uint32_t>> congruentCount;
80 : 100873 : eq::EqualityEngine* ee = d_state.getEqualityEngine();
81 : 100873 : eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee);
82 [ + + ]: 4370260 : while (!eqcs_i.isFinished())
83 : : {
84 : 4269387 : Node eqc = (*eqcs_i);
85 : 4269387 : TypeNode tn = eqc.getType();
86 [ + + ]: 4269387 : if (!tn.isRegExp())
87 : : {
88 : 4151116 : Node emps;
89 : : // get the term index for type tn
90 : 4151116 : std::map<Kind, TermIndex>& tti = d_termIndex[tn];
91 [ + + ]: 4151116 : if (tn.isStringLike())
92 : : {
93 : 1620820 : d_stringLikeEqc.push_back(eqc);
94 : 1620820 : emps = Word::mkEmptyWord(tn);
95 : : }
96 : 4151116 : Node var;
97 : 4151116 : eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, ee);
98 : 4151116 : std::vector<Node> prevConstLike;
99 : 4151116 : bool isString = eqc.getType().isString();
100 : : // have we found a constant in this equivalence class
101 : 4151116 : bool foundConst = false;
102 [ + + ]: 26528221 : for (; !eqc_i.isFinished(); ++eqc_i)
103 : : {
104 : 22377105 : Node n = *eqc_i;
105 : 22377105 : Kind k = n.getKind();
106 [ + - ]: 22377105 : Trace("strings-base") << "initialize term: " << n << std::endl;
107 : : // process constant-like terms
108 [ + + ]: 22377105 : if (utils::isConstantLike(n))
109 : : {
110 : : // compare against the other constant-like terms in this equivalence
111 : : // class
112 [ + + ]: 896796 : for (const Node& prev : prevConstLike)
113 : : {
114 [ - + ]: 3136 : if (processConstantLike(n, prev))
115 : : {
116 : : // in conflict, return
117 : 0 : return;
118 : : }
119 : : }
120 [ + + ][ + - ]: 893660 : bool addToConstLike = isString && !foundConst;
121 : : // update best content
122 [ + + ][ - + ]: 893660 : if (prevConstLike.empty() || n.isConst())
[ + + ]
123 : : {
124 : 890524 : d_eqcInfo[eqc].d_bestContent = n;
125 : 890524 : d_eqcInfo[eqc].d_bestScore = 0;
126 : 890524 : d_eqcInfo[eqc].d_base = n;
127 : 890524 : d_eqcInfo[eqc].d_exp = Node::null();
128 [ + + ]: 890524 : if (n.isConst())
129 : : {
130 : : // only keep the current
131 : 885501 : prevConstLike.clear();
132 : 885501 : foundConst = true;
133 : : }
134 : : }
135 : : // Determine if we need to track n to compare it to other constant
136 : : // like terms in this equivalence class. This is done if we do not
137 : : // have any other constant-like terms we are tracking, or if we have
138 : : // not yet encountered a constant and we are a string equivalence
139 : : // class. This is because all *pairs* of str.unit must be compared
140 : : // to one another, whereas since seq.unit is injective, we can
141 : : // compare seq.unit with a single representative seq.unit term.
142 [ + + ][ - + ]: 893660 : if (prevConstLike.empty() || addToConstLike)
[ + + ]
143 : : {
144 : 890524 : prevConstLike.push_back(n);
145 : : }
146 : : }
147 : :
148 [ + + ]: 22377105 : if (tn.isInteger())
149 : : {
150 : : // do nothing
151 : 5191955 : continue;
152 : : }
153 [ + + ]: 17185150 : else if (d_congruent.find(n) != d_congruent.end())
154 : : {
155 : : // skip congruent terms
156 : 2009869 : congruentCount[k].first++;
157 : 2009869 : continue;
158 : : }
159 : :
160 : 15175281 : congruentCount[k].second++;
161 : :
162 : : // process indexing
163 [ + + ]: 15175281 : if (n.getNumChildren() > 0)
164 : : {
165 [ + + ]: 12242725 : if (k == Kind::EQUAL)
166 : : {
167 : 10167894 : continue;
168 : : }
169 : :
170 : 2074831 : std::vector<Node> c;
171 : 4149662 : Node nc = tti[k].add(n, 0, d_state, emps, false, c);
172 [ + + ]: 2074831 : if (nc != n)
173 : : {
174 [ + - ]: 420250 : Trace("strings-base-debug")
175 : 210125 : << "...found congruent term " << nc << std::endl;
176 : : // check if we have inferred a new equality by removal of empty
177 : : // components
178 : 210125 : if (k == Kind::STRING_CONCAT && !d_state.areEqual(nc, n))
179 : : {
180 : 25395 : std::vector<Node> exp;
181 : : // the number of empty components of n, nc
182 : 25395 : size_t count[2] = {0, 0};
183 : : // We are explaining equal components, which may end up producing
184 : : // cycles in the explanation, e.g. explaining
185 : : // (= (str.++ s t) (str.++ t s)) when s is equal to t,
186 : : // we would add (= s t) and (= t s) to the explanation. This leads
187 : : // to issues in proofs since we are treating explanations as
188 : : // substitutions. To address this we track a representative of
189 : : // the terms occurring in our explanation, such that after adding
190 : : // (= s t), expRep[s] = expRep[t] = s, and hence (= t s) is
191 : : // recognized as redundant. This also can lead to shorter
192 : : // explanations.
193 : 25395 : std::map<Node, Node> expRep;
194 : 25395 : std::map<Node, Node>::iterator itra, itrb;
195 : 94368 : while (count[0] < nc.getNumChildren()
196 [ + + ][ + + ]: 94368 : || count[1] < n.getNumChildren())
[ + + ]
197 : : {
198 : : // explain empty prefixes
199 [ + + ]: 206919 : for (unsigned t = 0; t < 2; t++)
200 : : {
201 [ + + ]: 137946 : Node nn = t == 0 ? nc : n;
202 : 137946 : while (count[t] < nn.getNumChildren()
203 [ + + ][ + - ]: 516293 : && (nn[count[t]] == emps
[ + + ][ - - ]
204 : 330464 : || d_state.areEqual(nn[count[t]], emps)))
205 : : {
206 [ + - ]: 47883 : if (nn[count[t]] != emps)
207 : : {
208 : 47883 : exp.push_back(nn[count[t]].eqNode(emps));
209 : : }
210 : 47883 : count[t]++;
211 : : }
212 : 137946 : }
213 [ + - ]: 137946 : Trace("strings-base-debug") << " counts = " << count[0] << ", "
214 : 68973 : << count[1] << std::endl;
215 : : // explain equal components
216 [ + + ]: 68973 : if (count[0] < nc.getNumChildren())
217 : : {
218 [ - + ][ - + ]: 48376 : Assert(count[1] < n.getNumChildren());
[ - - ]
219 [ + + ]: 48376 : if (nc[count[0]] != n[count[1]])
220 : : {
221 : 5645 : Node a = nc[count[0]];
222 : 5645 : Node b = n[count[1]];
223 : 5645 : Node ra = getRep(a, expRep);
224 : 5645 : Node rb = getRep(b, expRep);
225 : : // if they do not already have an equal representative
226 [ + + ]: 5645 : if (ra != rb)
227 : : {
228 : : // update the representative
229 : 5401 : expRep[rb] = ra;
230 : 5401 : exp.push_back(a.eqNode(b));
231 : : }
232 : 5645 : }
233 : 48376 : count[0]++;
234 : 48376 : count[1]++;
235 : : }
236 : : }
237 : : // infer the equality
238 : 25395 : d_im.sendInference(
239 : 50790 : exp, n.eqNode(nc), InferenceId::STRINGS_I_NORM);
240 : 25395 : }
241 : : else
242 : : {
243 : : // We cannot mark one of the terms as reduced here (via
244 : : // ExtTheory::markCongruent) since extended function terms
245 : : // rely on reductions to other extended function terms. We
246 : : // may have a pair of extended function terms f(a)=f(b) where
247 : : // the reduction of argument a depends on the term b.
248 : : // Thus, marking f(b) as reduced by virtue of the fact we
249 : : // have f(a) is incorrect, since then we are effectively
250 : : // assuming that the reduction of f(a) depends on itself.
251 : : }
252 : : // this node is congruent to another one, we can ignore it
253 : 210125 : if (rlvSet.find(n) != rlvSet.end()
254 [ + + ][ + + ]: 210125 : && rlvSet.find(nc) == rlvSet.end())
[ + + ]
255 : : {
256 : : // If `n` is a relevant term and `nc` is not, then we change
257 : : // the term at its index to `n` and mark `nc` as congruent.
258 : : // This ensures that if we have mutliple congruent terms, we
259 : : // reason about one of the relevant ones (if available).
260 : 303 : tti[k].add(n, 0, d_state, emps, true, c);
261 : 303 : std::swap(nc, n);
262 : : }
263 [ + - ]: 420250 : Trace("strings-base-debug")
264 : 0 : << " congruent term : " << n << " (via " << nc << ")"
265 : 210125 : << std::endl;
266 : 210125 : d_congruent.insert(n);
267 : 210125 : congruentCount[k].first++;
268 : : }
269 [ + + ][ + + ]: 1864706 : else if (k == Kind::STRING_CONCAT && c.size() == 1)
[ + + ]
270 : : {
271 [ + - ]: 177186 : Trace("strings-base-debug")
272 : 0 : << " congruent term by singular : " << n << " " << c[0]
273 : 88593 : << std::endl;
274 : : // singular case
275 [ + + ]: 88593 : if (!d_state.areEqual(c[0], n))
276 : : {
277 : 45656 : Node ns;
278 : 45656 : std::vector<Node> exp;
279 : : // explain empty components
280 : 45656 : bool foundNEmpty = false;
281 [ + + ]: 149447 : for (const Node& nnc : n)
282 : : {
283 [ + + ]: 103791 : if (d_state.areEqual(nnc, emps))
284 : : {
285 [ + - ]: 58135 : if (nnc != emps)
286 : : {
287 : 58135 : exp.push_back(nnc.eqNode(emps));
288 : : }
289 : : }
290 : : else
291 : : {
292 [ - + ][ - + ]: 45656 : Assert(!foundNEmpty);
[ - - ]
293 : 45656 : ns = nnc;
294 : 45656 : foundNEmpty = true;
295 : : }
296 : 103791 : }
297 [ - + ][ - + ]: 45656 : AlwaysAssert(foundNEmpty);
[ - - ]
298 : : // infer the equality
299 : 45656 : d_im.sendInference(
300 : 91312 : exp, n.eqNode(ns), InferenceId::STRINGS_I_NORM_S);
301 : 45656 : }
302 : 88593 : d_congruent.insert(n);
303 : : }
304 : 2074831 : }
305 [ + + ]: 2932556 : else if (!n.isConst())
306 : : {
307 : : // We mark all but the oldest variable in the equivalence class as
308 : : // congruent.
309 [ + + ]: 2386198 : if (var.isNull())
310 : : {
311 : 1606285 : var = n;
312 : : }
313 [ + + ]: 779913 : else if (var > n)
314 : : {
315 [ + - ]: 876844 : Trace("strings-base-debug")
316 : 438422 : << " congruent variable : " << var << std::endl;
317 : 438422 : d_congruent.insert(var);
318 : 438422 : var = n;
319 : : }
320 : : else
321 : : {
322 [ + - ]: 682982 : Trace("strings-base-debug")
323 : 341491 : << " congruent variable : " << n << std::endl;
324 : 341491 : d_congruent.insert(n);
325 : : }
326 : : }
327 [ + - ][ + ]: 22377105 : }
328 [ + - ][ + - ]: 4151116 : }
[ + - ]
329 : 4269387 : ++eqcs_i;
330 [ + - ][ + - ]: 4269387 : }
331 [ - + ]: 100873 : if (TraceIsOn("strings-base"))
332 : : {
333 : 0 : for (const std::pair<const Kind, std::pair<uint32_t, uint32_t>>& cc :
334 [ - - ]: 0 : congruentCount)
335 : : {
336 [ - - ]: 0 : Trace("strings-base")
337 : 0 : << " Terms[" << cc.first << "] = " << cc.second.second << "/"
338 : 0 : << (cc.second.first + cc.second.second) << std::endl;
339 : : }
340 : : }
341 [ + - ]: 100873 : Trace("strings-base") << "BaseSolver::checkInit finished" << std::endl;
342 [ + - ]: 100873 : }
343 : :
344 : 3136 : bool BaseSolver::processConstantLike(Node a, Node b)
345 : : {
346 : : // we have either (seq.unit x) = C, or (seq.unit x) = (seq.unit y)
347 : : // where C is a sequence constant.
348 [ + + ][ - + ]: 3136 : Node cval = b.isConst() ? b : (a.isConst() ? a : Node::null());
349 : 3136 : std::vector<Node> exp;
350 : 3136 : exp.push_back(b.eqNode(a));
351 : 3136 : Node s, t;
352 [ + + ]: 3136 : if (cval.isNull())
353 : : {
354 : : // injectivity of seq.unit
355 : 1961 : s = b[0];
356 : 1961 : t = a[0];
357 : : }
358 : : else
359 : : {
360 : : // should not have two constants in the same equivalence class
361 : 1175 : std::vector<Node> cchars = Word::getChars(cval);
362 [ + - ]: 1175 : if (cchars.size() == 1)
363 : : {
364 [ + - ]: 1175 : Node oval = b.isConst() ? a : b;
365 [ - + ][ - - ]: 1175 : Assert(oval.getKind() == Kind::SEQ_UNIT
[ - + ][ - + ]
[ - - ]
366 : : || oval.getKind() == Kind::STRING_UNIT);
367 : 1175 : s = oval[0];
368 : 1175 : t = Word::getNth(cchars[0], 0);
369 : : // oval is congruent (ignored) in this context
370 : 1175 : d_congruent.insert(oval);
371 : 1175 : }
372 : : else
373 : : {
374 : : // (seq.unit x) = C => false if |C| != 1.
375 : 0 : d_im.sendInference(
376 : 0 : exp, d_false, InferenceId::STRINGS_UNIT_CONST_CONFLICT);
377 : 0 : return true;
378 : : }
379 [ + - ]: 1175 : }
380 [ + - ]: 6272 : Trace("strings-base") << "Process constant-like pair " << s << ", " << t
381 : 3136 : << " from " << a << ", " << b << std::endl;
382 [ + + ]: 3136 : if (!d_state.areEqual(s, t))
383 : : {
384 [ - + ][ - + ]: 226 : Assert(s.getType() == t.getType());
[ - - ]
385 : 226 : Node eq = s.eqNode(t);
386 [ - + ]: 226 : if (a.getType().isString())
387 : : {
388 : : // String unit is not injective, due to invalid code points.
389 : : // We do an inference scheme in two parts.
390 : : // for (str.unit x), (str.unit y): x = y or x != y
391 [ - - ]: 0 : if (!d_state.areDisequal(s, t))
392 : : {
393 : 0 : d_im.sendSplit(s, t, InferenceId::STRINGS_UNIT_SPLIT);
394 [ - - ]: 0 : Trace("strings-base") << "...split" << std::endl;
395 : : }
396 [ - - ]: 0 : else if (d_strUnitOobEq.find(eq) == d_strUnitOobEq.end())
397 : : {
398 : : // cache that we have performed this inference
399 : 0 : Node eqSym = t.eqNode(s);
400 : 0 : d_strUnitOobEq.insert(eq);
401 : 0 : d_strUnitOobEq.insert(eqSym);
402 : 0 : exp.push_back(eq.notNode());
403 : : // (str.unit x) = (str.unit y) ^ x != y =>
404 : : // x or y is not a valid code point
405 : 0 : Node scr = utils::mkCodeRange(s, d_cardSize);
406 : 0 : Node tcr = utils::mkCodeRange(t, d_cardSize);
407 : : Node conc =
408 : 0 : nodeManager()->mkNode(Kind::OR, scr.notNode(), tcr.notNode());
409 : : // We do not explain exp for two reasons. First, we are
410 : : // caching this inference based on the user context and thus
411 : : // it should not depend on the current explanation. Second,
412 : : // s or t may be concrete integers corresponding to code
413 : : // points of string constants, and thus are not guaranteed to
414 : : // be terms in the equality engine.
415 : 0 : NodeManager* nm = nodeManager();
416 : : // We must send this lemma immediately, since otherwise if buffered,
417 : : // this lemma may be dropped if there is a fact or conflict that
418 : : // preempts it.
419 : 0 : Node lem = nm->mkNode(Kind::IMPLIES, nm->mkAnd(exp), conc);
420 : 0 : d_im.lemma(lem, InferenceId::STRINGS_UNIT_INJ_OOB);
421 [ - - ]: 0 : Trace("strings-base") << "...oob split" << std::endl;
422 : 0 : }
423 : : else
424 : : {
425 [ - - ]: 0 : Trace("strings-base") << "...already sent oob" << std::endl;
426 : : }
427 : : }
428 : : else
429 : : {
430 : : // (seq.unit x) = (seq.unit y) => x=y, or
431 : : // (seq.unit x) = (seq.unit c) => x=c
432 : : // Must send this as lemma since it may impact other theories, or
433 : : // imply length constraints if the conclusion involves strings/sequences.
434 : 226 : d_im.sendInference(exp, eq, InferenceId::STRINGS_UNIT_INJ, false, true);
435 [ + - ]: 226 : Trace("strings-base") << "...inj seq" << std::endl;
436 : : }
437 : 226 : }
438 : : else
439 : : {
440 [ + - ]: 2910 : Trace("strings-base") << "...equal" << std::endl;
441 : : }
442 : 3136 : return false;
443 : 3136 : }
444 : :
445 : 82834 : void BaseSolver::checkConstantEquivalenceClasses()
446 : : {
447 : : // do fixed point
448 : 82834 : size_t prevSize = 0;
449 : 82834 : std::vector<Node> vecc;
450 : : do
451 : : {
452 : 82842 : vecc.clear();
453 [ + - ]: 165684 : Trace("strings-base-debug")
454 : 82842 : << "Check constant equivalence classes..." << std::endl;
455 : 82842 : prevSize = d_eqcInfo.size();
456 : 82842 : for (std::pair<const TypeNode, std::map<Kind, TermIndex>>& tindex :
457 [ + + ]: 361250 : d_termIndex)
458 : : {
459 : 195566 : checkConstantEquivalenceClasses(
460 : 195566 : &tindex.second[Kind::STRING_CONCAT], vecc, true);
461 : : }
462 [ + - ][ + + ]: 82842 : } while (!d_im.hasProcessed() && d_eqcInfo.size() > prevSize);
[ + + ]
463 : :
464 [ + - ]: 82834 : if (!d_im.hasProcessed())
465 : : {
466 : : // now, go back and set "most content" terms
467 : 82834 : vecc.clear();
468 : 82834 : for (std::pair<const TypeNode, std::map<Kind, TermIndex>>& tindex :
469 [ + + ]: 361202 : d_termIndex)
470 : : {
471 : 195534 : checkConstantEquivalenceClasses(
472 : 195534 : &tindex.second[Kind::STRING_CONCAT], vecc, false);
473 : : }
474 : : }
475 : 82834 : }
476 : :
477 : 1772274 : void BaseSolver::checkConstantEquivalenceClasses(TermIndex* ti,
478 : : std::vector<Node>& vecc,
479 : : bool ensureConst,
480 : : bool isConst)
481 : : {
482 : 1772274 : Node n = ti->d_data;
483 [ + + ]: 1772274 : if (!n.isNull())
484 : : {
485 : : // construct the constant if applicable
486 : 859722 : Node c;
487 [ + + ]: 859722 : if (isConst)
488 : : {
489 : 122720 : c = d_termReg.mkNConcat(vecc, n.getType());
490 : : }
491 : 859722 : if (!isConst || !d_state.areEqual(n, c))
492 : : {
493 [ - + ]: 737032 : if (TraceIsOn("strings-debug"))
494 : : {
495 [ - - ]: 0 : Trace("strings-debug")
496 : 0 : << "Constant eqc : " << c << " for " << n << std::endl;
497 [ - - ]: 0 : Trace("strings-debug") << " ";
498 [ - - ]: 0 : for (const Node& v : vecc)
499 : : {
500 [ - - ]: 0 : Trace("strings-debug") << v << " ";
501 : : }
502 [ - - ]: 0 : Trace("strings-debug") << std::endl;
503 : : }
504 : 737032 : size_t countc = 0;
505 : 737032 : std::vector<Node> exp;
506 : : // non-constant vector
507 : 737032 : std::vector<Node> vecnc;
508 : 737032 : size_t contentSize = 0;
509 [ + + ]: 2513139 : for (size_t count = 0, nchild = n.getNumChildren(); count < nchild;
510 : : ++count)
511 : : {
512 : : // Add explanations for the empty children
513 : 1776107 : Node emps;
514 [ + + ]: 1776107 : if (d_state.isEqualEmptyWord(n[count], emps))
515 : : {
516 : 76291 : d_im.addToExplanation(n[count], emps, exp);
517 : 76291 : continue;
518 : : }
519 [ + + ]: 1699816 : else if (vecc[countc].isNull())
520 : : {
521 [ - + ][ - + ]: 1623471 : Assert(!isConst);
[ - - ]
522 : : // no constant for this component, leave it as is
523 : 1623471 : vecnc.push_back(n[count]);
524 : 1623471 : continue;
525 : : }
526 : : // if we are not entirely a constant
527 [ + + ]: 76345 : if (!isConst)
528 : : {
529 : : // use the constant component
530 : 76285 : vecnc.push_back(vecc[countc]);
531 [ - + ][ - + ]: 76285 : Assert(vecc[countc].isConst());
[ - - ]
532 : 76285 : contentSize += Word::getLength(vecc[countc]);
533 : : }
534 [ + - ]: 152690 : Trace("strings-debug")
535 [ - + ][ - - ]: 76345 : << "...explain " << n[count] << " " << vecc[countc] << std::endl;
536 [ - + ]: 76345 : if (!d_state.areEqual(n[count], vecc[countc]))
537 : : {
538 : 0 : Node nrr = d_state.getRepresentative(n[count]);
539 : 0 : Assert(!d_eqcInfo[nrr].d_bestContent.isNull()
540 : : && d_eqcInfo[nrr].d_bestContent.isConst());
541 : : // must flatten to avoid nested AND in explanations
542 : 0 : utils::flattenOp(Kind::AND, d_eqcInfo[nrr].d_exp, exp);
543 : : // now explain equality to base
544 : 0 : d_im.addToExplanation(n[count], d_eqcInfo[nrr].d_base, exp);
545 : 0 : }
546 : : else
547 : : {
548 : 76345 : d_im.addToExplanation(n[count], vecc[countc], exp);
549 : : }
550 : 76345 : countc++;
551 [ + + ]: 1776107 : }
552 : : // exp contains an explanation of n==c
553 [ + + ][ + - ]: 737032 : Assert(!isConst || countc == vecc.size());
[ - + ][ - + ]
[ - - ]
554 [ + + ]: 737032 : if (!isConst)
555 : : {
556 : : // no use storing something with no content
557 [ + + ]: 737002 : if (contentSize > 0)
558 : : {
559 : 144574 : Node nr = d_state.getRepresentative(n);
560 : 72287 : BaseEqcInfo& bei = d_eqcInfo[nr];
561 : 72287 : if (!bei.d_bestContent.isConst()
562 [ + + ][ + + ]: 72287 : && (bei.d_bestContent.isNull() || contentSize > bei.d_bestScore))
[ + + ][ + + ]
563 : : {
564 : : // The equivalence class is not entailed to be equal to a constant
565 : : // and we found a better concatenation
566 : 66495 : Node nct = d_termReg.mkNConcat(vecnc, n.getType());
567 [ - + ][ - + ]: 66495 : Assert(!nct.isConst());
[ - - ]
568 : 66495 : bei.d_bestContent = nct;
569 : 66495 : bei.d_bestScore = contentSize;
570 : 66495 : bei.d_base = n;
571 [ + + ]: 66495 : if (!exp.empty())
572 : : {
573 : 26688 : bei.d_exp = utils::mkAnd(nodeManager(), exp);
574 : : }
575 [ + - ]: 132990 : Trace("strings-debug")
576 : 0 : << "Set eqc best content " << n << " to " << nct
577 : 66495 : << ", explanation = " << bei.d_exp << std::endl;
578 : : // we have e.g. (= x (str.++ "A" x)), which is a conflict.
579 [ + + ]: 227252 : for (const Node& nctc : nct)
580 : : {
581 [ + + ]: 160813 : if (d_state.areEqual(nctc, nr))
582 : : {
583 : 56 : d_im.sendInference(exp,
584 : 112 : nctc.eqNode(n).notNode(),
585 : : InferenceId::STRINGS_I_CYCLE_CONFLICT);
586 : 56 : return;
587 : : }
588 [ + + ]: 160813 : }
589 [ + + ]: 66495 : }
590 [ + + ]: 72287 : }
591 : : }
592 [ - + ]: 30 : else if (d_state.hasTerm(c))
593 : : {
594 : 0 : d_im.sendInference(exp, n.eqNode(c), InferenceId::STRINGS_I_CONST_MERGE);
595 : 0 : return;
596 : : }
597 [ + - ]: 30 : else if (!d_im.hasProcessed())
598 : : {
599 : 60 : Node nr = d_state.getRepresentative(n);
600 : 30 : BaseEqcInfo& bei = d_eqcInfo[nr];
601 [ + + ]: 30 : if (!bei.d_bestContent.isConst())
602 : : {
603 : 10 : bei.d_bestContent = c;
604 : 10 : bei.d_base = n;
605 : 10 : bei.d_exp = utils::mkAnd(nodeManager(), exp);
606 [ + - ]: 20 : Trace("strings-debug")
607 : 0 : << "Set eqc const " << n << " to " << c
608 : 10 : << ", explanation = " << bei.d_exp << std::endl;
609 : : }
610 [ - + ]: 20 : else if (c != bei.d_bestContent)
611 : : {
612 : : // conflict
613 [ - - ]: 0 : Trace("strings-debug")
614 : 0 : << "Conflict, other constant was " << bei.d_bestContent
615 : 0 : << ", this constant was " << c << std::endl;
616 [ - - ]: 0 : if (bei.d_exp.isNull())
617 : : {
618 : : // n==c ^ n == c' => false
619 : 0 : d_im.addToExplanation(n, bei.d_bestContent, exp);
620 : : }
621 : : else
622 : : {
623 : : // n==c ^ n == d_base == c' => false
624 : 0 : exp.push_back(bei.d_exp);
625 : 0 : d_im.addToExplanation(n, bei.d_base, exp);
626 : : }
627 : 0 : d_im.sendInference(exp, d_false, InferenceId::STRINGS_I_CONST_CONFLICT);
628 : 0 : return;
629 : : }
630 : : else
631 : : {
632 [ + - ]: 20 : Trace("strings-debug") << "Duplicate constant." << std::endl;
633 : : }
634 [ + - ]: 30 : }
635 [ + + ][ + + ]: 737088 : }
636 [ + + ]: 859722 : }
637 [ + + ]: 3514791 : for (std::pair<const TNode, TermIndex>& p : ti->d_children)
638 : : {
639 : 1742685 : std::map<Node, BaseEqcInfo>::const_iterator it = d_eqcInfo.find(p.first);
640 [ + + ][ + + ]: 1742685 : if (it != d_eqcInfo.end() && it->second.d_bestContent.isConst())
[ + + ]
641 : : {
642 : 344125 : vecc.push_back(it->second.d_bestContent);
643 : 344125 : checkConstantEquivalenceClasses(&p.second, vecc, ensureConst, isConst);
644 : 344125 : vecc.pop_back();
645 : : }
646 [ + + ]: 1398560 : else if (!ensureConst)
647 : : {
648 : : // can still proceed, with null
649 : 1037049 : vecc.push_back(Node::null());
650 : 1037049 : checkConstantEquivalenceClasses(&p.second, vecc, ensureConst, false);
651 : 1037049 : vecc.pop_back();
652 : : }
653 [ + + ]: 1742685 : if (d_im.hasProcessed())
654 : : {
655 : 112 : break;
656 : : }
657 : : }
658 [ + + ]: 1772274 : }
659 : :
660 : 34385 : void BaseSolver::checkCardinality()
661 : : {
662 : : // This will create a partition of eqc, where each collection has length that
663 : : // are pairwise propagated to be equal. We do not require disequalities
664 : : // between the lengths of each collection, since we split on disequalities
665 : : // between lengths of string terms that are disequal (DEQ-LENGTH-SP).
666 : 34385 : std::map<TypeNode, std::vector<std::vector<Node> > > cols;
667 : 34385 : std::map<TypeNode, std::vector<Node> > lts;
668 : 34385 : d_state.separateByLengthTyped(d_stringLikeEqc, cols, lts);
669 [ + + ]: 41540 : for (std::pair<const TypeNode, std::vector<std::vector<Node> > >& c : cols)
670 : : {
671 : 7155 : checkCardinalityType(c.first, c.second, lts[c.first]);
672 : : }
673 : 34385 : }
674 : :
675 : 7155 : BaseSolver::CardinalityResponse BaseSolver::getCardinalityReq(
676 : : TypeNode tn, size_t& typeCardSize) const
677 : : {
678 [ + + ]: 7155 : if (tn.isString()) // string-only
679 : : {
680 : 6799 : typeCardSize = d_cardSize;
681 : 6799 : return CardinalityResponse::REQ;
682 : : }
683 [ - + ][ - + ]: 356 : Assert(tn.isSequence());
[ - - ]
684 : 356 : TypeNode etn = tn.getSequenceElementType();
685 [ + + ]: 356 : if (!d_env.isFiniteType(etn))
686 : : {
687 : : // infinite cardinality, we are fine
688 : 234 : return CardinalityResponse::NO_REQ;
689 : : }
690 : : // we check the cardinality class of the type, assuming that FMF is
691 : : // disabled.
692 [ + - ]: 122 : if (isCardinalityClassFinite(etn.getCardinalityClass(), false))
693 : : {
694 : 122 : Cardinality c = etn.getCardinality();
695 : 122 : bool smallCardinality = false;
696 [ + - ]: 122 : if (!c.isLargeFinite())
697 : : {
698 : 122 : Integer ci = c.getFiniteCardinality();
699 [ + - ]: 122 : if (ci.fitsUnsignedInt())
700 : : {
701 : 122 : smallCardinality = true;
702 : 122 : typeCardSize = ci.toUnsignedInt();
703 : : }
704 : 122 : }
705 [ - + ]: 122 : if (!smallCardinality)
706 : : {
707 : : // if it is large finite, then there is no way we could have
708 : : // constructed that many terms in memory, hence there is nothing
709 : : // to do.
710 : 0 : return CardinalityResponse::NO_REQ;
711 : : }
712 [ + - ]: 122 : }
713 : : else
714 : : {
715 : 0 : Assert(options().quantifiers.finiteModelFind);
716 : : // we are in a case where the cardinality of the type is infinite
717 : : // if not FMF, and finite given the Env's option value for FMF. In this
718 : : // case, FMF must be true, and the cardinality is finite and dynamic
719 : : // (i.e. it depends on the model's finite interpretation for uninterpreted
720 : : // sorts). We do not know how to handle this case, we set incomplete.
721 : : // TODO (cvc4-projects #23): how to handle sequence for finite types?
722 : 0 : d_im.setModelUnsound(IncompleteId::SEQ_FINITE_DYNAMIC_CARDINALITY);
723 : 0 : return CardinalityResponse::UNHANDLED;
724 : : }
725 : 122 : return CardinalityResponse::REQ;
726 : 356 : }
727 : :
728 : 23621 : bool BaseSolver::isCardinalityOk(size_t typeCardSize,
729 : : Node lr,
730 : : size_t eqcCount,
731 : : size_t& lenNeed) const
732 : : {
733 [ + - ]: 47242 : Trace("strings-card") << "isCardinalityOk? " << typeCardSize << " "
734 : 23621 : << eqcCount << std::endl;
735 [ + + ]: 23621 : if (eqcCount <= 1)
736 : : {
737 : 16660 : return true;
738 : : }
739 [ + + ]: 6961 : if (typeCardSize == 1)
740 : : {
741 : : // For string-like types of cardinality 1, there is only a single
742 : : // element of any length, thus we return false and set lenNeed to zero.
743 : : // We will add a split in checkCardinalityType.
744 : 2 : lenNeed = 0;
745 : 2 : return false;
746 : : }
747 : 6959 : lenNeed = 1;
748 : 6959 : double curr = static_cast<double>(eqcCount);
749 [ + + ]: 10666 : while (curr > typeCardSize)
750 : : {
751 : 3707 : curr = curr / static_cast<double>(typeCardSize);
752 : 3707 : lenNeed++;
753 : : }
754 [ + - ]: 13918 : Trace("strings-card")
755 : 0 : << "Need length " << lenNeed
756 : 0 : << " for this number of strings (where alphabet size is " << typeCardSize
757 : 6959 : << ")." << std::endl;
758 : 6959 : NodeManager* nm = nodeManager();
759 : : // check if we need to split
760 : 6959 : bool needsSplit = true;
761 [ + + ]: 6959 : if (lr.isConst())
762 : : {
763 : : // if constant, compare
764 : 13648 : Node cmp = nm->mkNode(Kind::GEQ, lr, nm->mkConstInt(Rational(lenNeed)));
765 : 6824 : cmp = rewrite(cmp);
766 : 6824 : needsSplit = !cmp.getConst<bool>();
767 : 6824 : }
768 : : else
769 : : {
770 : : // find the minimimum constant that we are unknown to be disequal from, or
771 : : // otherwise stop if we increment such that cardinality does not apply.
772 : : // We always start with r=1 since by the invariants of our term registry,
773 : : // a term is either equal to the empty string, or has length >= 1.
774 : 135 : size_t r = 1;
775 : 135 : bool success = true;
776 [ - + ][ - - ]: 135 : while (r < lenNeed && success)
777 : : {
778 : 0 : Node rr = nm->mkConstInt(Rational(r));
779 [ - - ]: 0 : if (d_state.areDisequal(rr, lr))
780 : : {
781 : 0 : r++;
782 : : }
783 : : else
784 : : {
785 : 0 : success = false;
786 : : }
787 : 0 : }
788 [ + - ]: 135 : if (r > 0)
789 : : {
790 [ + - ]: 270 : Trace("strings-card")
791 : 0 : << "Symbolic length " << lr << " must be at least " << r
792 : 135 : << " due to constant disequalities." << std::endl;
793 : : }
794 : 135 : needsSplit = r < lenNeed;
795 : : }
796 : 6959 : return !needsSplit;
797 : : }
798 : 0 : bool BaseSolver::isCardinalityOk(size_t typeCardSize,
799 : : Node lr,
800 : : size_t eqcCount) const
801 : : {
802 : : size_t lenNeed;
803 : 0 : return isCardinalityOk(typeCardSize, lr, eqcCount, lenNeed);
804 : : }
805 : :
806 : 7155 : void BaseSolver::checkCardinalityType(TypeNode tn,
807 : : std::vector<std::vector<Node>>& cols,
808 : : std::vector<Node>& lts)
809 : : {
810 [ + - ]: 14310 : Trace("strings-card") << "Check cardinality (type " << tn << ")..."
811 : 7155 : << std::endl;
812 : :
813 : 7155 : NodeManager* nm = nodeManager();
814 : : size_t typeCardSize;
815 : 7155 : CardinalityResponse cr = getCardinalityReq(tn, typeCardSize);
816 [ + + ]: 7155 : if (cr == CardinalityResponse::NO_REQ)
817 : : {
818 : : // no requirements, return
819 : 3943 : return;
820 : : }
821 [ - + ]: 6921 : else if (cr == CardinalityResponse::UNHANDLED)
822 : : {
823 : : // we are in a case where the cardinality of the type is infinite
824 : : // if not FMF, and finite given the Env's option value for FMF. In this
825 : : // case, FMF must be true, and the cardinality is finite and dynamic
826 : : // (i.e. it depends on the model's finite interpretation for uninterpreted
827 : : // sorts). We do not know how to handle this case, we set incomplete.
828 : : // TODO (cvc4-projects #23): how to handle sequence for finite types?
829 : 0 : d_im.setModelUnsound(IncompleteId::SEQ_FINITE_DYNAMIC_CARDINALITY);
830 : 0 : return;
831 : : }
832 : : // for each collection
833 [ + + ]: 26833 : for (unsigned i = 0, csize = cols.size(); i < csize; ++i)
834 : : {
835 : 23621 : Node lr = lts[i];
836 [ + - ]: 47242 : Trace("strings-card") << "Number of strings with length equal to " << lr
837 : 23621 : << " is " << cols[i].size() << std::endl;
838 : 23621 : size_t lenNeed = 0;
839 [ + + ]: 23621 : if (isCardinalityOk(typeCardSize, lr, cols[i].size(), lenNeed))
840 : : {
841 : : // based on cardinality, we are ok
842 : 19912 : continue;
843 : : }
844 : : // first, try to split to merge equivalence classes
845 : 3709 : for (std::vector<Node>::iterator itr1 = cols[i].begin();
846 [ + + ]: 42132 : itr1 != cols[i].end();
847 : 38423 : ++itr1)
848 : : {
849 [ + + ]: 1019717 : for (std::vector<Node>::iterator itr2 = itr1 + 1; itr2 != cols[i].end();
850 : 977592 : ++itr2)
851 : : {
852 [ + + ]: 981294 : if (!d_state.areDisequal(*itr1, *itr2))
853 : : {
854 : : // add split lemma
855 [ + - ]: 3702 : if (d_im.sendSplit(*itr1, *itr2, InferenceId::STRINGS_CARD_SP))
856 : : {
857 : 3702 : return;
858 : : }
859 : : }
860 : : }
861 : : }
862 : : // otherwise, we need a length constraint
863 : 7 : EqcInfo* ei = d_state.getOrMakeEqcInfo(lr, true);
864 [ + - ]: 14 : Trace("strings-card") << "Previous cardinality used for " << lr << " is "
865 : 7 : << ((int)ei->d_cardinalityLemK.get() - 1)
866 : 7 : << std::endl;
867 [ + - ]: 7 : if (lenNeed + 1 > ei->d_cardinalityLemK.get())
868 : : {
869 : 7 : Node k_node = nm->mkConstInt(Rational(lenNeed));
870 : : // add cardinality lemma
871 : 7 : Node dist = nm->mkNode(Kind::DISTINCT, cols[i]);
872 : 7 : std::vector<Node> expn;
873 : 7 : expn.push_back(dist);
874 : 7 : for (std::vector<Node>::iterator itr1 = cols[i].begin();
875 [ + + ]: 238 : itr1 != cols[i].end();
876 : 231 : ++itr1)
877 : : {
878 : 231 : Node len = nm->mkNode(Kind::STRING_LENGTH, *itr1);
879 [ + - ]: 231 : if (len != lr)
880 : : {
881 : 231 : Node len_eq_lr = len.eqNode(lr);
882 : 231 : expn.push_back(len_eq_lr);
883 : 231 : }
884 : 231 : }
885 : 7 : Node len = nm->mkNode(Kind::STRING_LENGTH, cols[i][0]);
886 : 14 : Node cons = nm->mkNode(Kind::GEQ, len, k_node);
887 : 7 : cons = rewrite(cons);
888 : 7 : ei->d_cardinalityLemK.set(lenNeed + 1);
889 [ - + ][ - - ]: 7 : if (!cons.isConst() || !cons.getConst<bool>())
[ + - ]
890 : : {
891 : 7 : d_im.sendInference(
892 : : expn, expn, cons, InferenceId::STRINGS_CARDINALITY, false, true);
893 : 7 : return;
894 : : }
895 [ - + ][ - + ]: 35 : }
[ - + ][ - + ]
[ - + ]
896 [ - + ][ + ]: 23621 : }
897 [ + - ]: 3212 : Trace("strings-card") << "...end check cardinality" << std::endl;
898 : : }
899 : :
900 : 3552110 : bool BaseSolver::isCongruent(Node n)
901 : : {
902 : 3552110 : return d_congruent.find(n) != d_congruent.end();
903 : : }
904 : :
905 : 3553753 : Node BaseSolver::getConstantEqc(Node eqc)
906 : : {
907 : 3553753 : std::map<Node, BaseEqcInfo>::const_iterator it = d_eqcInfo.find(eqc);
908 [ + + ][ + + ]: 3553753 : if (it != d_eqcInfo.end() && it->second.d_bestContent.isConst())
[ + + ]
909 : : {
910 : 673208 : return it->second.d_bestContent;
911 : : }
912 : 2880545 : return Node::null();
913 : : }
914 : :
915 : 103803 : Node BaseSolver::explainConstantEqc(Node n, Node eqc, std::vector<Node>& exp)
916 : : {
917 : 103803 : std::map<Node, BaseEqcInfo>::const_iterator it = d_eqcInfo.find(eqc);
918 [ + - ]: 103803 : if (it != d_eqcInfo.end())
919 : : {
920 : 103803 : BaseEqcInfo& bei = d_eqcInfo[eqc];
921 [ - + ]: 103803 : if (!bei.d_bestContent.isConst())
922 : : {
923 : 0 : return Node::null();
924 : : }
925 [ - + ]: 103803 : if (!bei.d_exp.isNull())
926 : : {
927 : 0 : utils::flattenOp(Kind::AND, bei.d_exp, exp);
928 : : }
929 [ + - ]: 103803 : if (!bei.d_base.isNull())
930 : : {
931 : 103803 : d_im.addToExplanation(n, bei.d_base, exp);
932 : : }
933 : 103803 : return bei.d_bestContent;
934 : : }
935 : 0 : return Node::null();
936 : : }
937 : :
938 : 1805359 : Node BaseSolver::explainBestContentEqc(Node n, Node eqc, std::vector<Node>& exp)
939 : : {
940 : 1805359 : std::map<Node, BaseEqcInfo>::const_iterator it = d_eqcInfo.find(eqc);
941 [ + + ]: 1805359 : if (it != d_eqcInfo.end())
942 : : {
943 : 953968 : BaseEqcInfo& bei = d_eqcInfo[eqc];
944 [ - + ][ - + ]: 953968 : Assert(!bei.d_bestContent.isNull());
[ - - ]
945 [ + + ]: 953968 : if (!bei.d_exp.isNull())
946 : : {
947 : 63269 : utils::flattenOp(Kind::AND, bei.d_exp, exp);
948 : : }
949 [ + - ]: 953968 : if (!bei.d_base.isNull())
950 : : {
951 : 953968 : d_im.addToExplanation(n, bei.d_base, exp);
952 : : }
953 : 953968 : return bei.d_bestContent;
954 : : }
955 : :
956 : 851391 : return Node::null();
957 : : }
958 : :
959 : 80760 : const std::vector<Node>& BaseSolver::getStringLikeEqc() const
960 : : {
961 : 80760 : return d_stringLikeEqc;
962 : : }
963 : :
964 : 7169542 : Node BaseSolver::TermIndex::add(TNode n,
965 : : unsigned index,
966 : : const SolverState& s,
967 : : Node er,
968 : : bool overwrite,
969 : : std::vector<Node>& c)
970 : : {
971 [ + + ]: 7169542 : if (index == n.getNumChildren())
972 : : {
973 [ + + ][ + + ]: 2075134 : if (overwrite || d_data.isNull())
[ + + ]
974 : : {
975 : 1865009 : d_data = n;
976 : : }
977 : 2075134 : return d_data;
978 : : }
979 [ - + ][ - + ]: 5094408 : Assert(index < n.getNumChildren());
[ - - ]
980 : 5094408 : TNode nir = s.getRepresentative(n[index]);
981 : : // if it is empty, and doing CONCAT, ignore
982 [ + + ][ + + ]: 5094408 : if (nir == er && n.getKind() == Kind::STRING_CONCAT)
[ + + ]
983 : : {
984 : 550727 : return add(n, index + 1, s, er, overwrite, c);
985 : : }
986 : 4543681 : c.push_back(nir);
987 : 4543681 : return d_children[nir].add(n, index + 1, s, er, overwrite, c);
988 : 5094408 : }
989 : :
990 : : } // namespace strings
991 : : } // namespace theory
992 : : } // namespace cvc5::internal
|
