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