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 : 28852 : BaseSolver::BaseSolver(Env& env,
35 : : SolverState& s,
36 : : InferenceManager& im,
37 : 28852 : TermRegistry& tr)
38 : : : EnvObj(env),
39 : 28852 : d_state(s),
40 : 28852 : d_im(im),
41 : 28852 : d_termReg(tr),
42 : 28852 : d_congruent(context()),
43 : 57704 : d_strUnitOobEq(userContext())
44 : : {
45 : 28852 : d_false = nodeManager()->mkConst(false);
46 : 28852 : d_cardSize = options().strings.stringsAlphaCard;
47 : 28852 : }
48 : :
49 : 28839 : BaseSolver::~BaseSolver() {}
50 : :
51 : : /**
52 : : * Implements union find, with path compression
53 : : */
54 : 14126 : Node getRep(const Node& n, std::map<Node, Node>& rep)
55 : : {
56 : 14126 : std::map<Node, Node>::iterator it = rep.find(n);
57 [ + + ]: 14126 : if (it == rep.end())
58 : : {
59 : 14000 : return n;
60 : : }
61 [ - + ][ - + ]: 126 : Assert(n != it->second);
[ - - ]
62 : 126 : Node r = getRep(it->second, rep);
63 : 126 : rep[n] = r;
64 : 126 : return r;
65 : 126 : }
66 : :
67 : 91011 : void BaseSolver::checkInit()
68 : : {
69 : : // build term index
70 : 91011 : d_eqcInfo.clear();
71 : 91011 : d_termIndex.clear();
72 : 91011 : d_stringLikeEqc.clear();
73 : :
74 : 91011 : const std::set<Node>& rlvSet = d_termReg.getRelevantTermSet();
75 : :
76 [ + - ]: 91011 : Trace("strings-base") << "BaseSolver::checkInit" << std::endl;
77 : : // count of congruent, non-congruent per operator (independent of type),
78 : : // for debugging.
79 : 91011 : std::map<Kind, std::pair<uint32_t, uint32_t>> congruentCount;
80 : 91011 : eq::EqualityEngine* ee = d_state.getEqualityEngine();
81 : 91011 : eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee);
82 [ + + ]: 4209341 : while (!eqcs_i.isFinished())
83 : : {
84 : 4118330 : Node eqc = (*eqcs_i);
85 : 4118330 : TypeNode tn = eqc.getType();
86 [ + + ]: 4118330 : if (!tn.isRegExp())
87 : : {
88 : 3995783 : Node emps;
89 : : // get the term index for type tn
90 : 3995783 : std::map<Kind, TermIndex>& tti = d_termIndex[tn];
91 [ + + ]: 3995783 : if (tn.isStringLike())
92 : : {
93 : 1591838 : d_stringLikeEqc.push_back(eqc);
94 : 1591838 : emps = Word::mkEmptyWord(tn);
95 : : }
96 : 3995783 : Node var;
97 : 3995783 : eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, ee);
98 : 3995783 : std::vector<Node> prevConstLike;
99 : 3995783 : bool isString = eqc.getType().isString();
100 : : // have we found a constant in this equivalence class
101 : 3995783 : bool foundConst = false;
102 [ + + ]: 26765377 : for (; !eqc_i.isFinished(); ++eqc_i)
103 : : {
104 : 22769594 : Node n = *eqc_i;
105 : 22769594 : Kind k = n.getKind();
106 [ + - ]: 22769594 : Trace("strings-base") << "initialize term: " << n << std::endl;
107 : : // process constant-like terms
108 [ + + ]: 22769594 : if (utils::isConstantLike(n))
109 : : {
110 : : // compare against the other constant-like terms in this equivalence
111 : : // class
112 [ + + ]: 885218 : for (const Node& prev : prevConstLike)
113 : : {
114 [ - + ]: 3056 : if (processConstantLike(n, prev))
115 : : {
116 : : // in conflict, return
117 : 0 : return;
118 : : }
119 : : }
120 [ + + ][ + - ]: 882162 : bool addToConstLike = isString && !foundConst;
121 : : // update best content
122 [ + + ][ - + ]: 882162 : if (prevConstLike.empty() || n.isConst())
[ + + ]
123 : : {
124 : 879106 : d_eqcInfo[eqc].d_bestContent = n;
125 : 879106 : d_eqcInfo[eqc].d_bestScore = 0;
126 : 879106 : d_eqcInfo[eqc].d_base = n;
127 : 879106 : d_eqcInfo[eqc].d_exp = Node::null();
128 [ + + ]: 879106 : if (n.isConst())
129 : : {
130 : : // only keep the current
131 : 874029 : prevConstLike.clear();
132 : 874029 : 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 [ + + ][ - + ]: 882162 : if (prevConstLike.empty() || addToConstLike)
[ + + ]
143 : : {
144 : 879106 : prevConstLike.push_back(n);
145 : : }
146 : : }
147 : :
148 [ + + ]: 22769594 : if (tn.isInteger())
149 : : {
150 : : // do nothing
151 : 5345039 : continue;
152 : : }
153 [ + + ]: 17424555 : else if (d_congruent.find(n) != d_congruent.end())
154 : : {
155 : : // skip congruent terms
156 : 2104796 : congruentCount[k].first++;
157 : 2104796 : continue;
158 : : }
159 : :
160 : 15319759 : congruentCount[k].second++;
161 : :
162 : : // process indexing
163 [ + + ]: 15319759 : if (n.getNumChildren() > 0)
164 : : {
165 [ + + ]: 12431022 : if (k == Kind::EQUAL)
166 : : {
167 : 10311476 : continue;
168 : : }
169 : :
170 : 2119546 : std::vector<Node> c;
171 : 4239092 : Node nc = tti[k].add(n, 0, d_state, emps, false, c);
172 [ + + ]: 2119546 : if (nc != n)
173 : : {
174 [ + - ]: 414486 : Trace("strings-base-debug")
175 : 207243 : << "...found congruent term " << nc << std::endl;
176 : : // check if we have inferred a new equality by removal of empty
177 : : // components
178 : 207243 : if (k == Kind::STRING_CONCAT && !d_state.areEqual(nc, n))
179 : : {
180 : 21442 : std::vector<Node> exp;
181 : : // the number of empty components of n, nc
182 : 21442 : 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 : 21442 : std::map<Node, Node> expRep;
194 : 21442 : std::map<Node, Node>::iterator itra, itrb;
195 : 82108 : while (count[0] < nc.getNumChildren()
196 [ + + ][ + + ]: 82108 : || count[1] < n.getNumChildren())
[ + + ]
197 : : {
198 : : // explain empty prefixes
199 [ + + ]: 181998 : for (unsigned t = 0; t < 2; t++)
200 : : {
201 [ + + ]: 121332 : Node nn = t == 0 ? nc : n;
202 : 121332 : while (count[t] < nn.getNumChildren()
203 [ + + ][ + - ]: 450749 : && (nn[count[t]] == emps
[ + + ][ - - ]
204 : 288728 : || d_state.areEqual(nn[count[t]], emps)))
205 : : {
206 [ + - ]: 40689 : if (nn[count[t]] != emps)
207 : : {
208 : 40689 : exp.push_back(nn[count[t]].eqNode(emps));
209 : : }
210 : 40689 : count[t]++;
211 : : }
212 : 121332 : }
213 [ + - ]: 121332 : Trace("strings-base-debug") << " counts = " << count[0] << ", "
214 : 60666 : << count[1] << std::endl;
215 : : // explain equal components
216 [ + + ]: 60666 : if (count[0] < nc.getNumChildren())
217 : : {
218 [ - + ][ - + ]: 43009 : Assert(count[1] < n.getNumChildren());
[ - - ]
219 [ + + ]: 43009 : if (nc[count[0]] != n[count[1]])
220 : : {
221 : 7000 : Node a = nc[count[0]];
222 : 7000 : Node b = n[count[1]];
223 : 7000 : Node ra = getRep(a, expRep);
224 : 7000 : Node rb = getRep(b, expRep);
225 : : // if they do not already have an equal representative
226 [ + + ]: 7000 : if (ra != rb)
227 : : {
228 : : // update the representative
229 : 6902 : expRep[rb] = ra;
230 : 6902 : exp.push_back(a.eqNode(b));
231 : : }
232 : 7000 : }
233 : 43009 : count[0]++;
234 : 43009 : count[1]++;
235 : : }
236 : : }
237 : : // infer the equality
238 : 21442 : d_im.sendInference(
239 : 42884 : exp, n.eqNode(nc), InferenceId::STRINGS_I_NORM);
240 : 21442 : }
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 : 207243 : if (rlvSet.find(n) != rlvSet.end()
254 [ + + ][ + + ]: 207243 : && 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 : 114 : tti[k].add(n, 0, d_state, emps, true, c);
261 : 114 : std::swap(nc, n);
262 : : }
263 [ + - ]: 414486 : Trace("strings-base-debug") << " congruent term : " << n
264 : 207243 : << " (via " << nc << ")" << std::endl;
265 : 207243 : d_congruent.insert(n);
266 : 207243 : congruentCount[k].first++;
267 : : }
268 [ + + ][ + + ]: 1912303 : else if (k == Kind::STRING_CONCAT && c.size() == 1)
[ + + ]
269 : : {
270 [ + - ]: 172318 : Trace("strings-base-debug")
271 : 0 : << " congruent term by singular : " << n << " " << c[0]
272 : 86159 : << std::endl;
273 : : // singular case
274 [ + + ]: 86159 : if (!d_state.areEqual(c[0], n))
275 : : {
276 : 42423 : Node ns;
277 : 42423 : std::vector<Node> exp;
278 : : // explain empty components
279 : 42423 : bool foundNEmpty = false;
280 [ + + ]: 138468 : for (const Node& nnc : n)
281 : : {
282 [ + + ]: 96045 : if (d_state.areEqual(nnc, emps))
283 : : {
284 [ + - ]: 53622 : if (nnc != emps)
285 : : {
286 : 53622 : exp.push_back(nnc.eqNode(emps));
287 : : }
288 : : }
289 : : else
290 : : {
291 [ - + ][ - + ]: 42423 : Assert(!foundNEmpty);
[ - - ]
292 : 42423 : ns = nnc;
293 : 42423 : foundNEmpty = true;
294 : : }
295 : 96045 : }
296 [ - + ][ - + ]: 42423 : AlwaysAssert(foundNEmpty);
[ - - ]
297 : : // infer the equality
298 : 42423 : d_im.sendInference(
299 : 84846 : exp, n.eqNode(ns), InferenceId::STRINGS_I_NORM_S);
300 : 42423 : }
301 : 86159 : d_congruent.insert(n);
302 : : }
303 : 2119546 : }
304 [ + + ]: 2888737 : else if (!n.isConst())
305 : : {
306 : : // We mark all but the oldest variable in the equivalence class as
307 : : // congruent.
308 [ + + ]: 2356521 : if (var.isNull())
309 : : {
310 : 1577624 : var = n;
311 : : }
312 [ + + ]: 778897 : else if (var > n)
313 : : {
314 [ + - ]: 879382 : Trace("strings-base-debug")
315 : 439691 : << " congruent variable : " << var << std::endl;
316 : 439691 : d_congruent.insert(var);
317 : 439691 : var = n;
318 : : }
319 : : else
320 : : {
321 [ + - ]: 678412 : Trace("strings-base-debug")
322 : 339206 : << " congruent variable : " << n << std::endl;
323 : 339206 : d_congruent.insert(n);
324 : : }
325 : : }
326 [ + - ][ + ]: 22769594 : }
327 [ + - ][ + - ]: 3995783 : }
[ + - ]
328 : 4118330 : ++eqcs_i;
329 [ + - ][ + - ]: 4118330 : }
330 [ - + ]: 91011 : if (TraceIsOn("strings-base"))
331 : : {
332 : 0 : for (const std::pair<const Kind, std::pair<uint32_t, uint32_t>>& cc :
333 [ - - ]: 0 : congruentCount)
334 : : {
335 [ - - ]: 0 : Trace("strings-base")
336 : 0 : << " Terms[" << cc.first << "] = " << cc.second.second << "/"
337 : 0 : << (cc.second.first + cc.second.second) << std::endl;
338 : : }
339 : : }
340 [ + - ]: 91011 : Trace("strings-base") << "BaseSolver::checkInit finished" << std::endl;
341 [ + - ]: 91011 : }
342 : :
343 : 3056 : bool BaseSolver::processConstantLike(Node a, Node b)
344 : : {
345 : : // we have either (seq.unit x) = C, or (seq.unit x) = (seq.unit y)
346 : : // where C is a sequence constant.
347 [ + + ][ - + ]: 3056 : Node cval = b.isConst() ? b : (a.isConst() ? a : Node::null());
348 : 3056 : std::vector<Node> exp;
349 : 3056 : exp.push_back(b.eqNode(a));
350 : 3056 : Node s, t;
351 [ + + ]: 3056 : if (cval.isNull())
352 : : {
353 : : // injectivity of seq.unit
354 : 1871 : s = b[0];
355 : 1871 : t = a[0];
356 : : }
357 : : else
358 : : {
359 : : // should not have two constants in the same equivalence class
360 : 1185 : std::vector<Node> cchars = Word::getChars(cval);
361 [ + - ]: 1185 : if (cchars.size() == 1)
362 : : {
363 [ + - ]: 1185 : Node oval = b.isConst() ? a : b;
364 [ - + ][ - - ]: 1185 : Assert(oval.getKind() == Kind::SEQ_UNIT
[ - + ][ - + ]
[ - - ]
365 : : || oval.getKind() == Kind::STRING_UNIT);
366 : 1185 : s = oval[0];
367 : 1185 : t = Word::getNth(cchars[0], 0);
368 : : // oval is congruent (ignored) in this context
369 : 1185 : d_congruent.insert(oval);
370 : 1185 : }
371 : : else
372 : : {
373 : : // (seq.unit x) = C => false if |C| != 1.
374 : 0 : d_im.sendInference(
375 : 0 : exp, d_false, InferenceId::STRINGS_UNIT_CONST_CONFLICT);
376 : 0 : return true;
377 : : }
378 [ + - ]: 1185 : }
379 [ + - ]: 6112 : Trace("strings-base") << "Process constant-like pair " << s << ", " << t
380 : 3056 : << " from " << a << ", " << b << std::endl;
381 [ + + ]: 3056 : if (!d_state.areEqual(s, t))
382 : : {
383 [ - + ][ - + ]: 678 : AssertEqual(s.getType(), t.getType());
[ - - ]
384 : 226 : Node eq = s.eqNode(t);
385 [ - + ]: 226 : if (a.getType().isString())
386 : : {
387 : : // String unit is not injective, due to invalid code points.
388 : : // We do an inference scheme in two parts.
389 : : // for (str.unit x), (str.unit y): x = y or x != y
390 [ - - ]: 0 : if (!d_state.areDisequal(s, t))
391 : : {
392 : 0 : d_im.sendSplit(s, t, InferenceId::STRINGS_UNIT_SPLIT);
393 [ - - ]: 0 : Trace("strings-base") << "...split" << std::endl;
394 : : }
395 [ - - ]: 0 : else if (d_strUnitOobEq.find(eq) == d_strUnitOobEq.end())
396 : : {
397 : : // cache that we have performed this inference
398 : 0 : Node eqSym = t.eqNode(s);
399 : 0 : d_strUnitOobEq.insert(eq);
400 : 0 : d_strUnitOobEq.insert(eqSym);
401 : 0 : exp.push_back(eq.notNode());
402 : : // (str.unit x) = (str.unit y) ^ x != y =>
403 : : // x or y is not a valid code point
404 : 0 : Node scr = utils::mkCodeRange(s, d_cardSize);
405 : 0 : Node tcr = utils::mkCodeRange(t, d_cardSize);
406 : : Node conc =
407 : 0 : nodeManager()->mkNode(Kind::OR, {scr.notNode(), tcr.notNode()});
408 : : // We do not explain exp for two reasons. First, we are
409 : : // caching this inference based on the user context and thus
410 : : // it should not depend on the current explanation. Second,
411 : : // s or t may be concrete integers corresponding to code
412 : : // points of string constants, and thus are not guaranteed to
413 : : // be terms in the equality engine.
414 : 0 : NodeManager* nm = nodeManager();
415 : : // We must send this lemma immediately, since otherwise if buffered,
416 : : // this lemma may be dropped if there is a fact or conflict that
417 : : // preempts it.
418 : 0 : Node lem = nm->mkNode(Kind::IMPLIES, nm->mkAnd(exp), conc);
419 : 0 : d_im.lemma(lem, InferenceId::STRINGS_UNIT_INJ_OOB);
420 [ - - ]: 0 : Trace("strings-base") << "...oob split" << std::endl;
421 : 0 : }
422 : : else
423 : : {
424 [ - - ]: 0 : Trace("strings-base") << "...already sent oob" << std::endl;
425 : : }
426 : : }
427 : : else
428 : : {
429 : : // (seq.unit x) = (seq.unit y) => x=y, or
430 : : // (seq.unit x) = (seq.unit c) => x=c
431 : : // Must send this as lemma since it may impact other theories, or
432 : : // imply length constraints if the conclusion involves strings/sequences.
433 : 226 : d_im.sendInference(exp, eq, InferenceId::STRINGS_UNIT_INJ, false, true);
434 [ + - ]: 226 : Trace("strings-base") << "...inj seq" << std::endl;
435 : : }
436 : 226 : }
437 : : else
438 : : {
439 [ + - ]: 2830 : Trace("strings-base") << "...equal" << std::endl;
440 : : }
441 : 3056 : return false;
442 : 3056 : }
443 : :
444 : 73696 : void BaseSolver::checkConstantEquivalenceClasses()
445 : : {
446 : : // do fixed point
447 : 73696 : size_t prevSize = 0;
448 : 73696 : std::vector<Node> vecc;
449 : : do
450 : : {
451 : 73704 : vecc.clear();
452 [ + - ]: 147408 : Trace("strings-base-debug")
453 : 73704 : << "Check constant equivalence classes..." << std::endl;
454 : 73704 : prevSize = d_eqcInfo.size();
455 : 73704 : for (std::pair<const TypeNode, std::map<Kind, TermIndex>>& tindex :
456 [ + + ]: 335683 : d_termIndex)
457 : : {
458 : 188275 : checkConstantEquivalenceClasses(
459 : 188275 : &tindex.second[Kind::STRING_CONCAT], vecc, true);
460 : : }
461 [ + - ][ + + ]: 73704 : } while (!d_im.hasProcessed() && d_eqcInfo.size() > prevSize);
[ + + ]
462 : :
463 [ + - ]: 73696 : if (!d_im.hasProcessed())
464 : : {
465 : : // now, go back and set "most content" terms
466 : 73696 : vecc.clear();
467 : 73696 : for (std::pair<const TypeNode, std::map<Kind, TermIndex>>& tindex :
468 [ + + ]: 335635 : d_termIndex)
469 : : {
470 : 188243 : checkConstantEquivalenceClasses(
471 : 188243 : &tindex.second[Kind::STRING_CONCAT], vecc, false);
472 : : }
473 : : }
474 : 73696 : }
475 : :
476 : 1766840 : void BaseSolver::checkConstantEquivalenceClasses(TermIndex* ti,
477 : : std::vector<Node>& vecc,
478 : : bool ensureConst,
479 : : bool isConst)
480 : : {
481 : 1766840 : Node n = ti->d_data;
482 [ + + ]: 1766840 : if (!n.isNull())
483 : : {
484 : : // construct the constant if applicable
485 : 848151 : Node c;
486 [ + + ]: 848151 : if (isConst)
487 : : {
488 : 127518 : c = d_termReg.mkNConcat(vecc, n.getType());
489 : : }
490 : 848151 : if (!isConst || !d_state.areEqual(n, c))
491 : : {
492 [ - + ]: 720663 : if (TraceIsOn("strings-debug"))
493 : : {
494 [ - - ]: 0 : Trace("strings-debug")
495 : 0 : << "Constant eqc : " << c << " for " << n << std::endl;
496 [ - - ]: 0 : Trace("strings-debug") << " ";
497 [ - - ]: 0 : for (const Node& v : vecc)
498 : : {
499 [ - - ]: 0 : Trace("strings-debug") << v << " ";
500 : : }
501 [ - - ]: 0 : Trace("strings-debug") << std::endl;
502 : : }
503 : 720663 : size_t countc = 0;
504 : 720663 : std::vector<Node> exp;
505 : : // non-constant vector
506 : 720663 : std::vector<Node> vecnc;
507 : 720663 : size_t contentSize = 0;
508 [ + + ]: 2526952 : for (size_t count = 0, nchild = n.getNumChildren(); count < nchild;
509 : : ++count)
510 : : {
511 : : // Add explanations for the empty children
512 : 1806289 : Node emps;
513 [ + + ]: 1806289 : if (d_state.isEqualEmptyWord(n[count], emps))
514 : : {
515 : 81325 : d_im.addToExplanation(n[count], emps, exp);
516 : 81325 : continue;
517 : : }
518 [ + + ]: 1724964 : else if (vecc[countc].isNull())
519 : : {
520 [ - + ][ - + ]: 1640043 : Assert(!isConst);
[ - - ]
521 : : // no constant for this component, leave it as is
522 : 1640043 : vecnc.push_back(n[count]);
523 : 1640043 : continue;
524 : : }
525 : : // if we are not entirely a constant
526 [ + + ]: 84921 : if (!isConst)
527 : : {
528 : : // use the constant component
529 : 84861 : vecnc.push_back(vecc[countc]);
530 [ - + ][ - + ]: 84861 : Assert(vecc[countc].isConst());
[ - - ]
531 : 84861 : contentSize += Word::getLength(vecc[countc]);
532 : : }
533 [ + - ]: 169842 : Trace("strings-debug")
534 [ - + ][ - - ]: 84921 : << "...explain " << n[count] << " " << vecc[countc] << std::endl;
535 [ - + ]: 84921 : if (!d_state.areEqual(n[count], vecc[countc]))
536 : : {
537 : 0 : Node nrr = d_state.getRepresentative(n[count]);
538 : 0 : Assert(!d_eqcInfo[nrr].d_bestContent.isNull()
539 : : && d_eqcInfo[nrr].d_bestContent.isConst());
540 : : // must flatten to avoid nested AND in explanations
541 : 0 : utils::flattenOp(Kind::AND, d_eqcInfo[nrr].d_exp, exp);
542 : : // now explain equality to base
543 : 0 : d_im.addToExplanation(n[count], d_eqcInfo[nrr].d_base, exp);
544 : 0 : }
545 : : else
546 : : {
547 : 84921 : d_im.addToExplanation(n[count], vecc[countc], exp);
548 : : }
549 : 84921 : countc++;
550 [ + + ]: 1806289 : }
551 : : // exp contains an explanation of n==c
552 [ + + ][ + - ]: 720663 : Assert(!isConst || countc == vecc.size());
[ - + ][ - + ]
[ - - ]
553 [ + + ]: 720663 : if (!isConst)
554 : : {
555 : : // no use storing something with no content
556 [ + + ]: 720633 : if (contentSize > 0)
557 : : {
558 : 160898 : Node nr = d_state.getRepresentative(n);
559 : 80449 : BaseEqcInfo& bei = d_eqcInfo[nr];
560 : 80449 : if (!bei.d_bestContent.isConst()
561 [ + + ][ + + ]: 80449 : && (bei.d_bestContent.isNull() || contentSize > bei.d_bestScore))
[ + + ][ + + ]
562 : : {
563 : : // The equivalence class is not entailed to be equal to a constant
564 : : // and we found a better concatenation
565 : 73797 : Node nct = d_termReg.mkNConcat(vecnc, n.getType());
566 [ - + ][ - + ]: 73797 : Assert(!nct.isConst());
[ - - ]
567 : 73797 : bei.d_bestContent = nct;
568 : 73797 : bei.d_bestScore = contentSize;
569 : 73797 : bei.d_base = n;
570 [ + + ]: 73797 : if (!exp.empty())
571 : : {
572 : 31371 : bei.d_exp = utils::mkAnd(nodeManager(), exp);
573 : : }
574 [ + - ]: 147594 : Trace("strings-debug")
575 : 0 : << "Set eqc best content " << n << " to " << nct
576 : 73797 : << ", explanation = " << bei.d_exp << std::endl;
577 : : // we have e.g. (= x (str.++ "A" x)), which is a conflict.
578 [ + + ]: 256666 : for (const Node& nctc : nct)
579 : : {
580 [ + + ]: 182897 : if (d_state.areEqual(nctc, nr))
581 : : {
582 : 28 : d_im.sendInference(exp,
583 : 56 : nctc.eqNode(n).notNode(),
584 : : InferenceId::STRINGS_I_CYCLE_CONFLICT);
585 : 28 : return;
586 : : }
587 [ + + ]: 182897 : }
588 [ + + ]: 73797 : }
589 [ + + ]: 80449 : }
590 : : }
591 [ - + ]: 30 : else if (d_state.hasTerm(c))
592 : : {
593 : 0 : d_im.sendInference(
594 : 0 : 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(
628 : 0 : exp, d_false, InferenceId::STRINGS_I_CONST_CONFLICT);
629 : 0 : return;
630 : : }
631 : : else
632 : : {
633 [ + - ]: 20 : Trace("strings-debug") << "Duplicate constant." << std::endl;
634 : : }
635 [ + - ]: 30 : }
636 [ + + ][ + + ]: 720691 : }
637 [ + + ]: 848151 : }
638 [ + + ]: 3518198 : for (std::pair<const TNode, TermIndex>& p : ti->d_children)
639 : : {
640 : 1751442 : std::map<Node, BaseEqcInfo>::const_iterator it = d_eqcInfo.find(p.first);
641 [ + + ][ + + ]: 1751442 : if (it != d_eqcInfo.end() && it->second.d_bestContent.isConst())
[ + + ]
642 : : {
643 : 366785 : vecc.push_back(it->second.d_bestContent);
644 : 366785 : checkConstantEquivalenceClasses(&p.second, vecc, ensureConst, isConst);
645 : 366785 : vecc.pop_back();
646 : : }
647 [ + + ]: 1384657 : else if (!ensureConst)
648 : : {
649 : : // can still proceed, with null
650 : 1023537 : vecc.push_back(Node::null());
651 : 1023537 : checkConstantEquivalenceClasses(&p.second, vecc, ensureConst, false);
652 : 1023537 : vecc.pop_back();
653 : : }
654 [ + + ]: 1751442 : if (d_im.hasProcessed())
655 : : {
656 : 56 : break;
657 : : }
658 : : }
659 [ + + ]: 1766840 : }
660 : :
661 : 24162 : void BaseSolver::checkCardinality()
662 : : {
663 : : // This will create a partition of eqc, where each collection has length that
664 : : // are pairwise propagated to be equal. We do not require disequalities
665 : : // between the lengths of each collection, since we split on disequalities
666 : : // between lengths of string terms that are disequal (DEQ-LENGTH-SP).
667 : 24162 : std::map<TypeNode, std::vector<std::vector<Node>>> cols;
668 : 24162 : std::map<TypeNode, std::vector<Node>> lts;
669 : 24162 : d_state.separateByLengthTyped(d_stringLikeEqc, cols, lts);
670 [ + + ]: 31085 : for (std::pair<const TypeNode, std::vector<std::vector<Node>>>& c : cols)
671 : : {
672 : 6923 : checkCardinalityType(c.first, c.second, lts[c.first]);
673 : : }
674 : 24162 : }
675 : :
676 : 6923 : BaseSolver::CardinalityResponse BaseSolver::getCardinalityReq(
677 : : TypeNode tn, size_t& typeCardSize) const
678 : : {
679 [ + + ]: 6923 : if (tn.isString()) // string-only
680 : : {
681 : 6542 : typeCardSize = d_cardSize;
682 : 6542 : return CardinalityResponse::REQ;
683 : : }
684 [ - + ][ - + ]: 381 : Assert(tn.isSequence());
[ - - ]
685 : 381 : TypeNode etn = tn.getSequenceElementType();
686 [ + + ]: 381 : if (!d_env.isFiniteType(etn))
687 : : {
688 : : // infinite cardinality, we are fine
689 : 261 : return CardinalityResponse::NO_REQ;
690 : : }
691 : : // we check the cardinality class of the type, assuming that FMF is
692 : : // disabled.
693 [ + - ]: 120 : if (isCardinalityClassFinite(etn.getCardinalityClass(), false))
694 : : {
695 : 120 : Cardinality c = etn.getCardinality();
696 : 120 : bool smallCardinality = false;
697 [ + - ]: 120 : if (!c.isLargeFinite())
698 : : {
699 : 120 : Integer ci = c.getFiniteCardinality();
700 [ + - ]: 120 : if (ci.fitsUnsignedInt())
701 : : {
702 : 120 : smallCardinality = true;
703 : 120 : typeCardSize = ci.toUnsignedInt();
704 : : }
705 : 120 : }
706 [ - + ]: 120 : if (!smallCardinality)
707 : : {
708 : : // if it is large finite, then there is no way we could have
709 : : // constructed that many terms in memory, hence there is nothing
710 : : // to do.
711 : 0 : return CardinalityResponse::NO_REQ;
712 : : }
713 [ + - ]: 120 : }
714 : : else
715 : : {
716 : 0 : Assert(options().quantifiers.finiteModelFind);
717 : : // we are in a case where the cardinality of the type is infinite
718 : : // if not FMF, and finite given the Env's option value for FMF. In this
719 : : // case, FMF must be true, and the cardinality is finite and dynamic
720 : : // (i.e. it depends on the model's finite interpretation for uninterpreted
721 : : // sorts). We do not know how to handle this case, we set incomplete.
722 : : // TODO (cvc4-projects #23): how to handle sequence for finite types?
723 : 0 : d_im.setModelUnsound(IncompleteId::SEQ_FINITE_DYNAMIC_CARDINALITY);
724 : 0 : return CardinalityResponse::UNHANDLED;
725 : : }
726 : 120 : return CardinalityResponse::REQ;
727 : 381 : }
728 : :
729 : 22880 : bool BaseSolver::isCardinalityOk(size_t typeCardSize,
730 : : Node lr,
731 : : size_t eqcCount,
732 : : size_t& lenNeed) const
733 : : {
734 [ + - ]: 45760 : Trace("strings-card") << "isCardinalityOk? " << typeCardSize << " "
735 : 22880 : << eqcCount << std::endl;
736 [ + + ]: 22880 : if (eqcCount <= 1)
737 : : {
738 : 16012 : return true;
739 : : }
740 [ + + ]: 6868 : if (typeCardSize == 1)
741 : : {
742 : : // For string-like types of cardinality 1, there is only a single
743 : : // element of any length, thus we return false and set lenNeed to zero.
744 : : // We will add a split in checkCardinalityType.
745 : 2 : lenNeed = 0;
746 : 2 : return false;
747 : : }
748 : 6866 : lenNeed = 1;
749 : 6866 : double curr = static_cast<double>(eqcCount);
750 [ + + ]: 10573 : while (curr > typeCardSize)
751 : : {
752 : 3707 : curr = curr / static_cast<double>(typeCardSize);
753 : 3707 : lenNeed++;
754 : : }
755 [ + - ]: 13732 : Trace("strings-card")
756 : 0 : << "Need length " << lenNeed
757 : 0 : << " for this number of strings (where alphabet size is " << typeCardSize
758 : 6866 : << ")." << std::endl;
759 : 6866 : NodeManager* nm = nodeManager();
760 : : // check if we need to split
761 : 6866 : bool needsSplit = true;
762 [ + + ]: 6866 : if (lr.isConst())
763 : : {
764 : : // if constant, compare
765 : 13376 : Node cmp = nm->mkNode(Kind::GEQ, lr, nm->mkConstInt(Rational(lenNeed)));
766 : 6688 : cmp = rewrite(cmp);
767 : 6688 : needsSplit = !cmp.getConst<bool>();
768 : 6688 : }
769 : : else
770 : : {
771 : : // find the minimimum constant that we are unknown to be disequal from, or
772 : : // otherwise stop if we increment such that cardinality does not apply.
773 : : // We always start with r=1 since by the invariants of our term registry,
774 : : // a term is either equal to the empty string, or has length >= 1.
775 : 178 : size_t r = 1;
776 : 178 : bool success = true;
777 [ - + ][ - - ]: 178 : while (r < lenNeed && success)
778 : : {
779 : 0 : Node rr = nm->mkConstInt(Rational(r));
780 [ - - ]: 0 : if (d_state.areDisequal(rr, lr))
781 : : {
782 : 0 : r++;
783 : : }
784 : : else
785 : : {
786 : 0 : success = false;
787 : : }
788 : 0 : }
789 [ + - ]: 178 : if (r > 0)
790 : : {
791 [ + - ]: 356 : Trace("strings-card")
792 : 0 : << "Symbolic length " << lr << " must be at least " << r
793 : 178 : << " due to constant disequalities." << std::endl;
794 : : }
795 : 178 : needsSplit = r < lenNeed;
796 : : }
797 : 6866 : return !needsSplit;
798 : : }
799 : 0 : bool BaseSolver::isCardinalityOk(size_t typeCardSize,
800 : : Node lr,
801 : : size_t eqcCount) const
802 : : {
803 : : size_t lenNeed;
804 : 0 : return isCardinalityOk(typeCardSize, lr, eqcCount, lenNeed);
805 : : }
806 : :
807 : 6923 : void BaseSolver::checkCardinalityType(TypeNode tn,
808 : : std::vector<std::vector<Node>>& cols,
809 : : std::vector<Node>& lts)
810 : : {
811 [ + - ]: 13846 : Trace("strings-card") << "Check cardinality (type " << tn << ")..."
812 : 6923 : << std::endl;
813 : :
814 : 6923 : NodeManager* nm = nodeManager();
815 : : size_t typeCardSize;
816 : 6923 : CardinalityResponse cr = getCardinalityReq(tn, typeCardSize);
817 [ + + ]: 6923 : if (cr == CardinalityResponse::NO_REQ)
818 : : {
819 : : // no requirements, return
820 : 3970 : return;
821 : : }
822 [ - + ]: 6662 : else if (cr == CardinalityResponse::UNHANDLED)
823 : : {
824 : : // we are in a case where the cardinality of the type is infinite
825 : : // if not FMF, and finite given the Env's option value for FMF. In this
826 : : // case, FMF must be true, and the cardinality is finite and dynamic
827 : : // (i.e. it depends on the model's finite interpretation for uninterpreted
828 : : // sorts). We do not know how to handle this case, we set incomplete.
829 : : // TODO (cvc4-projects #23): how to handle sequence for finite types?
830 : 0 : d_im.setModelUnsound(IncompleteId::SEQ_FINITE_DYNAMIC_CARDINALITY);
831 : 0 : return;
832 : : }
833 : : // for each collection
834 [ + + ]: 25833 : for (unsigned i = 0, csize = cols.size(); i < csize; ++i)
835 : : {
836 : 22880 : Node lr = lts[i];
837 [ + - ]: 45760 : Trace("strings-card") << "Number of strings with length equal to " << lr
838 : 22880 : << " is " << cols[i].size() << std::endl;
839 : 22880 : size_t lenNeed = 0;
840 [ + + ]: 22880 : if (isCardinalityOk(typeCardSize, lr, cols[i].size(), lenNeed))
841 : : {
842 : : // based on cardinality, we are ok
843 : 19171 : continue;
844 : : }
845 : : // first, try to split to merge equivalence classes
846 : 3709 : for (std::vector<Node>::iterator itr1 = cols[i].begin();
847 [ + + ]: 42132 : itr1 != cols[i].end();
848 : 38423 : ++itr1)
849 : : {
850 [ + + ]: 1019717 : for (std::vector<Node>::iterator itr2 = itr1 + 1; itr2 != cols[i].end();
851 : 977592 : ++itr2)
852 : : {
853 [ + + ]: 981294 : if (!d_state.areDisequal(*itr1, *itr2))
854 : : {
855 : : // add split lemma
856 [ + - ]: 3702 : if (d_im.sendSplit(*itr1, *itr2, InferenceId::STRINGS_CARD_SP))
857 : : {
858 : 3702 : return;
859 : : }
860 : : }
861 : : }
862 : : }
863 : : // otherwise, we need a length constraint
864 : 7 : EqcInfo* ei = d_state.getOrMakeEqcInfo(lr, true);
865 [ + - ]: 14 : Trace("strings-card") << "Previous cardinality used for " << lr << " is "
866 : 7 : << ((int)ei->d_cardinalityLemK.get() - 1)
867 : 7 : << std::endl;
868 [ + - ]: 7 : if (lenNeed + 1 > ei->d_cardinalityLemK.get())
869 : : {
870 : 7 : Node k_node = nm->mkConstInt(Rational(lenNeed));
871 : : // add cardinality lemma
872 : 7 : Node dist = nm->mkNode(Kind::DISTINCT, cols[i]);
873 : 7 : std::vector<Node> expn;
874 : 7 : expn.push_back(dist);
875 : 7 : for (std::vector<Node>::iterator itr1 = cols[i].begin();
876 [ + + ]: 238 : itr1 != cols[i].end();
877 : 231 : ++itr1)
878 : : {
879 : 231 : Node len = nm->mkNode(Kind::STRING_LENGTH, *itr1);
880 [ + - ]: 231 : if (len != lr)
881 : : {
882 : 231 : Node len_eq_lr = len.eqNode(lr);
883 : 231 : expn.push_back(len_eq_lr);
884 : 231 : }
885 : 231 : }
886 : 7 : Node len = nm->mkNode(Kind::STRING_LENGTH, cols[i][0]);
887 : 14 : Node cons = nm->mkNode(Kind::GEQ, len, k_node);
888 : 7 : cons = rewrite(cons);
889 : 7 : ei->d_cardinalityLemK.set(lenNeed + 1);
890 [ - + ][ - - ]: 7 : if (!cons.isConst() || !cons.getConst<bool>())
[ + - ]
891 : : {
892 : 7 : d_im.sendInference(
893 : : expn, expn, cons, InferenceId::STRINGS_CARDINALITY, false, true);
894 : 7 : return;
895 : : }
896 [ - + ][ - + ]: 35 : }
[ - + ][ - + ]
[ - + ]
897 [ - + ][ + ]: 22880 : }
898 [ + - ]: 2953 : Trace("strings-card") << "...end check cardinality" << std::endl;
899 : : }
900 : :
901 : 3525242 : bool BaseSolver::isCongruent(Node n)
902 : : {
903 : 3525242 : return d_congruent.find(n) != d_congruent.end();
904 : : }
905 : :
906 : 3851460 : Node BaseSolver::getConstantEqc(Node eqc)
907 : : {
908 : 3851460 : std::map<Node, BaseEqcInfo>::const_iterator it = d_eqcInfo.find(eqc);
909 [ + + ][ + + ]: 3851460 : if (it != d_eqcInfo.end() && it->second.d_bestContent.isConst())
[ + + ]
910 : : {
911 : 736116 : return it->second.d_bestContent;
912 : : }
913 : 3115344 : return Node::null();
914 : : }
915 : :
916 : 135829 : Node BaseSolver::explainConstantEqc(Node n, Node eqc, std::vector<Node>& exp)
917 : : {
918 : 135829 : std::map<Node, BaseEqcInfo>::const_iterator it = d_eqcInfo.find(eqc);
919 [ + - ]: 135829 : if (it != d_eqcInfo.end())
920 : : {
921 : 135829 : BaseEqcInfo& bei = d_eqcInfo[eqc];
922 [ - + ]: 135829 : if (!bei.d_bestContent.isConst())
923 : : {
924 : 0 : return Node::null();
925 : : }
926 [ - + ]: 135829 : if (!bei.d_exp.isNull())
927 : : {
928 : 0 : utils::flattenOp(Kind::AND, bei.d_exp, exp);
929 : : }
930 [ + - ]: 135829 : if (!bei.d_base.isNull())
931 : : {
932 : 135829 : d_im.addToExplanation(n, bei.d_base, exp);
933 : : }
934 : 135829 : return bei.d_bestContent;
935 : : }
936 : 0 : return Node::null();
937 : : }
938 : :
939 : 1982446 : Node BaseSolver::explainBestContentEqc(Node n, Node eqc, std::vector<Node>& exp)
940 : : {
941 : 1982446 : std::map<Node, BaseEqcInfo>::const_iterator it = d_eqcInfo.find(eqc);
942 [ + + ]: 1982446 : if (it != d_eqcInfo.end())
943 : : {
944 : 1033372 : BaseEqcInfo& bei = d_eqcInfo[eqc];
945 [ - + ][ - + ]: 1033372 : Assert(!bei.d_bestContent.isNull());
[ - - ]
946 [ + + ]: 1033372 : if (!bei.d_exp.isNull())
947 : : {
948 : 65853 : utils::flattenOp(Kind::AND, bei.d_exp, exp);
949 : : }
950 [ + - ]: 1033372 : if (!bei.d_base.isNull())
951 : : {
952 : 1033372 : d_im.addToExplanation(n, bei.d_base, exp);
953 : : }
954 : 1033372 : return bei.d_bestContent;
955 : : }
956 : :
957 : 949074 : return Node::null();
958 : : }
959 : :
960 : 71154 : const std::vector<Node>& BaseSolver::getStringLikeEqc() const
961 : : {
962 : 71154 : return d_stringLikeEqc;
963 : : }
964 : :
965 : 7427549 : Node BaseSolver::TermIndex::add(TNode n,
966 : : unsigned index,
967 : : const SolverState& s,
968 : : Node er,
969 : : bool overwrite,
970 : : std::vector<Node>& c)
971 : : {
972 [ + + ]: 7427549 : if (index == n.getNumChildren())
973 : : {
974 [ + + ][ + + ]: 2119660 : if (overwrite || d_data.isNull())
[ + + ]
975 : : {
976 : 1912417 : d_data = n;
977 : : }
978 : 2119660 : return d_data;
979 : : }
980 [ - + ][ - + ]: 5307889 : Assert(index < n.getNumChildren());
[ - - ]
981 : 5307889 : TNode nir = s.getRepresentative(n[index]);
982 : : // if it is empty, and doing CONCAT, ignore
983 [ + + ][ + + ]: 5307889 : if (nir == er && n.getKind() == Kind::STRING_CONCAT)
[ + + ]
984 : : {
985 : 550913 : return add(n, index + 1, s, er, overwrite, c);
986 : : }
987 : 4756976 : c.push_back(nir);
988 : 4756976 : return d_children[nir].add(n, index + 1, s, er, overwrite, c);
989 : 5307889 : }
990 : :
991 : : } // namespace strings
992 : : } // namespace theory
993 : : } // namespace cvc5::internal
|
