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 : : * Implementation of the theory of strings.
11 : : */
12 : :
13 : : #include "theory/strings/sequences_rewriter.h"
14 : :
15 : : #include "expr/attribute.h"
16 : : #include "expr/node_builder.h"
17 : : #include "expr/sequence.h"
18 : : #include "theory/rewriter.h"
19 : : #include "theory/strings/arith_entail.h"
20 : : #include "theory/strings/regexp_entail.h"
21 : : #include "theory/strings/skolem_cache.h"
22 : : #include "theory/strings/strings_rewriter.h"
23 : : #include "theory/strings/theory_strings_utils.h"
24 : : #include "theory/strings/word.h"
25 : : #include "util/rational.h"
26 : : #include "util/regexp.h"
27 : : #include "util/statistics_registry.h"
28 : : #include "util/string.h"
29 : :
30 : : using namespace std;
31 : : using namespace cvc5::internal::kind;
32 : :
33 : : namespace cvc5::internal {
34 : : namespace theory {
35 : : namespace strings {
36 : :
37 : 47367 : SequencesRewriter::SequencesRewriter(NodeManager* nm,
38 : : ArithEntail& ae,
39 : : StringsEntail& se,
40 : 47367 : HistogramStat<Rewrite>* statistics)
41 : : : TheoryRewriter(nm),
42 : 47367 : d_statistics(statistics),
43 : 47367 : d_arithEntail(ae),
44 : 47367 : d_stringsEntail(se)
45 : : {
46 : 47367 : d_sigmaStar = nm->mkNode(Kind::REGEXP_STAR, nm->mkNode(Kind::REGEXP_ALLCHAR));
47 : 47367 : d_true = nm->mkConst(true);
48 : 47367 : d_false = nm->mkConst(false);
49 : 47367 : registerProofRewriteRule(ProofRewriteRule::RE_LOOP_ELIM,
50 : : TheoryRewriteCtx::PRE_DSL);
51 : 47367 : registerProofRewriteRule(ProofRewriteRule::RE_EQ_ELIM,
52 : : TheoryRewriteCtx::PRE_DSL);
53 : 47367 : registerProofRewriteRule(ProofRewriteRule::MACRO_RE_INTER_UNION_INCLUSION,
54 : : TheoryRewriteCtx::PRE_DSL);
55 : 47367 : registerProofRewriteRule(ProofRewriteRule::STR_IN_RE_EVAL,
56 : : TheoryRewriteCtx::DSL_SUBCALL);
57 : 47367 : registerProofRewriteRule(ProofRewriteRule::STR_IN_RE_CONSUME,
58 : : TheoryRewriteCtx::PRE_DSL);
59 : 47367 : registerProofRewriteRule(ProofRewriteRule::STR_IN_RE_CONCAT_STAR_CHAR,
60 : : TheoryRewriteCtx::PRE_DSL);
61 : 47367 : registerProofRewriteRule(ProofRewriteRule::STR_IN_RE_SIGMA,
62 : : TheoryRewriteCtx::PRE_DSL);
63 : 47367 : registerProofRewriteRule(ProofRewriteRule::STR_IN_RE_SIGMA_STAR,
64 : : TheoryRewriteCtx::PRE_DSL);
65 : 47367 : registerProofRewriteRule(ProofRewriteRule::MACRO_SUBSTR_STRIP_SYM_LENGTH,
66 : : TheoryRewriteCtx::POST_DSL);
67 : 47367 : registerProofRewriteRule(ProofRewriteRule::STR_CTN_MULTISET_SUBSET,
68 : : TheoryRewriteCtx::DSL_SUBCALL);
69 : 47367 : registerProofRewriteRule(ProofRewriteRule::MACRO_STR_EQ_LEN_UNIFY_PREFIX,
70 : : TheoryRewriteCtx::POST_DSL);
71 : 47367 : registerProofRewriteRule(ProofRewriteRule::MACRO_STR_EQ_LEN_UNIFY,
72 : : TheoryRewriteCtx::POST_DSL);
73 : 47367 : registerProofRewriteRule(ProofRewriteRule::STR_INDEXOF_RE_EVAL,
74 : : TheoryRewriteCtx::POST_DSL);
75 : 47367 : registerProofRewriteRule(ProofRewriteRule::STR_REPLACE_RE_EVAL,
76 : : TheoryRewriteCtx::POST_DSL);
77 : 47367 : registerProofRewriteRule(ProofRewriteRule::STR_REPLACE_RE_ALL_EVAL,
78 : : TheoryRewriteCtx::POST_DSL);
79 : 47367 : registerProofRewriteRule(ProofRewriteRule::MACRO_STR_CONST_NCTN_CONCAT,
80 : : TheoryRewriteCtx::DSL_SUBCALL);
81 : 47367 : registerProofRewriteRule(ProofRewriteRule::MACRO_STR_IN_RE_INCLUSION,
82 : : TheoryRewriteCtx::POST_DSL);
83 : 47367 : registerProofRewriteRule(ProofRewriteRule::MACRO_STR_STRIP_ENDPOINTS,
84 : : TheoryRewriteCtx::POST_DSL);
85 : 47367 : registerProofRewriteRule(ProofRewriteRule::MACRO_STR_SPLIT_CTN,
86 : : TheoryRewriteCtx::POST_DSL);
87 : : // MACRO_RE_INTER_UNION_CONST_ELIM should always be called at post-dsl
88 : : // as it is partly subsumed by RARE rewrites for intersection.
89 : 47367 : registerProofRewriteRule(ProofRewriteRule::MACRO_RE_INTER_UNION_CONST_ELIM,
90 : : TheoryRewriteCtx::POST_DSL);
91 : 47367 : registerProofRewriteRule(ProofRewriteRule::MACRO_STR_COMPONENT_CTN,
92 : : TheoryRewriteCtx::POST_DSL);
93 : 47367 : registerProofRewriteRule(ProofRewriteRule::SEQ_EVAL_OP,
94 : : TheoryRewriteCtx::DSL_SUBCALL);
95 : : // make back pointer to this (for rewriting contains)
96 : 47367 : se.d_rewriter = this;
97 : 47367 : }
98 : :
99 : 942390 : Node SequencesRewriter::rewriteViaRule(ProofRewriteRule id, const Node& n)
100 : : {
101 [ + + ][ + + ]: 942390 : switch (id)
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ - ]
102 : : {
103 : 19869 : case ProofRewriteRule::RE_LOOP_ELIM: return rewriteViaReLoopElim(n);
104 : 19820 : case ProofRewriteRule::RE_EQ_ELIM: return rewriteViaReEqElim(n);
105 : 19857 : case ProofRewriteRule::MACRO_RE_INTER_UNION_INCLUSION:
106 : 19857 : return rewriteViaMacroReInterUnionInclusion(n);
107 : 83 : case ProofRewriteRule::RE_INTER_INCLUSION:
108 : : case ProofRewriteRule::RE_UNION_INCLUSION:
109 : 83 : return rewriteViaReInterUnionInclusion(id, n);
110 : 83332 : case ProofRewriteRule::STR_IN_RE_EVAL: return rewriteViaStrInReEval(n);
111 : 19711 : case ProofRewriteRule::STR_IN_RE_CONSUME:
112 : 19711 : return rewriteViaStrInReConsume(n);
113 : 19520 : case ProofRewriteRule::STR_IN_RE_CONCAT_STAR_CHAR:
114 : 19520 : return rewriteViaStrInReConcatStarChar(n);
115 : 19409 : case ProofRewriteRule::STR_IN_RE_SIGMA: return rewriteViaStrInReSigma(n);
116 : 19399 : case ProofRewriteRule::STR_IN_RE_SIGMA_STAR:
117 : 19399 : return rewriteViaStrInReSigmaStar(n);
118 : 397 : case ProofRewriteRule::MACRO_SUBSTR_STRIP_SYM_LENGTH:
119 : : {
120 : : // Rewrite without using the rewriter as a subutility, which ensures
121 : : // that we can reconstruct the reasoning in a proof.
122 : : Rewrite rule;
123 : 397 : ArithEntail ae(nodeManager(), nullptr);
124 : 397 : StringsEntail sent(nullptr, ae);
125 : 397 : return rewriteViaMacroSubstrStripSymLength(n, rule, sent);
126 : 397 : }
127 : 82870 : case ProofRewriteRule::STR_CTN_MULTISET_SUBSET:
128 : : {
129 : : // don't use this just for evaluation
130 : 248610 : if (n.getKind() == Kind::STRING_CONTAINS
131 : 82870 : && (!n[0].isConst() || !n[1].isConst()))
132 : : {
133 [ + + ]: 8649 : if (d_stringsEntail.checkMultisetSubset(n[0], n[1]))
134 : : {
135 : 1670 : return d_nm->mkConst(false);
136 : : }
137 : : }
138 : : }
139 : 82035 : break;
140 : 367 : case ProofRewriteRule::MACRO_STR_EQ_LEN_UNIFY_PREFIX:
141 : : {
142 [ + + ]: 367 : if (n.getKind() == Kind::EQUAL)
143 : : {
144 : 66 : return rewriteViaStrEqLenUnifyPrefix(n);
145 : : }
146 : : }
147 : 301 : break;
148 : 337 : case ProofRewriteRule::MACRO_STR_EQ_LEN_UNIFY:
149 : : {
150 [ + + ]: 337 : if (n.getKind() == Kind::EQUAL)
151 : : {
152 : : Rewrite rule;
153 : 36 : return rewriteViaStrEqLenUnify(n, rule);
154 : : }
155 : : }
156 : 301 : break;
157 : 347 : case ProofRewriteRule::STR_INDEXOF_RE_EVAL:
158 : : {
159 : 347 : return rewriteViaStrIndexofReEval(n);
160 : : }
161 : : break;
162 : 274 : case ProofRewriteRule::STR_REPLACE_RE_EVAL:
163 : : {
164 : 274 : return rewriteViaStrReplaceReEval(n);
165 : : }
166 : : break;
167 : 288 : case ProofRewriteRule::STR_REPLACE_RE_ALL_EVAL:
168 : : {
169 : 288 : return rewriteViaStrReplaceReAllEval(n);
170 : : }
171 : : break;
172 : 125429 : case ProofRewriteRule::MACRO_STR_CONST_NCTN_CONCAT:
173 : : {
174 : 376287 : if (n.getKind() == Kind::STRING_CONTAINS
175 [ + + ][ + + ]: 125429 : && n[0].getKind() == Kind::CONST_STRING)
[ + + ][ + + ]
[ - - ]
176 : : {
177 : 43824 : NodeManager* nm = nodeManager();
178 : 43824 : RegExpEntail re(nm, nullptr);
179 : 43824 : Node re2 = re.getGeneralizedConstRegExp(n[1]);
180 [ + + ]: 43824 : if (!re2.isNull())
181 : : {
182 : : Node re2s =
183 : 10486 : nm->mkNode(Kind::REGEXP_CONCAT, d_sigmaStar, re2, d_sigmaStar);
184 : 5243 : String s = n[0].getConst<String>();
185 [ + + ]: 5243 : if (!RegExpEntail::testConstStringInRegExp(s, re2s))
186 : : {
187 : 5448 : return nm->mkConst(false);
188 : : }
189 [ + + ][ + + ]: 7967 : }
190 [ + + ][ + + ]: 46548 : }
191 : : }
192 : 122705 : break;
193 : 255 : case ProofRewriteRule::MACRO_STR_IN_RE_INCLUSION:
194 : 255 : return rewriteViaMacroStrInReInclusion(n);
195 : 162 : case ProofRewriteRule::MACRO_STR_SPLIT_CTN:
196 : 162 : return rewriteViaMacroStrSplitCtn(n);
197 : 210578 : case ProofRewriteRule::MACRO_STR_STRIP_ENDPOINTS:
198 : : {
199 : 210578 : std::vector<Node> nb, nrem, ne;
200 : 210578 : return rewriteViaMacroStrStripEndpoints(n, nb, nrem, ne);
201 : 210578 : }
202 : 162 : case ProofRewriteRule::MACRO_RE_INTER_UNION_CONST_ELIM:
203 : : {
204 : 162 : Node conflict;
205 : 162 : return rewriteViaMacroReInterUnionConstElim(n, conflict);
206 : 162 : }
207 : 217399 : case ProofRewriteRule::MACRO_STR_COMPONENT_CTN:
208 : : {
209 [ + + ]: 217399 : if (n.getKind() == Kind::STRING_CONTAINS)
210 : : {
211 : 217270 : std::vector<Node> nc1;
212 : 217270 : utils::getConcat(n[0], nc1);
213 : 217270 : std::vector<Node> nc2;
214 : 217270 : utils::getConcat(n[1], nc2);
215 : : // component-wise containment, note we do not use the extended version
216 : 217270 : std::vector<Node> nc1rb;
217 : 217270 : std::vector<Node> nc1re;
218 [ + + ]: 217270 : if (d_stringsEntail.componentContains(nc1, nc2, nc1rb, nc1re) != -1)
219 : : {
220 : 35594 : return nodeManager()->mkConst(true);
221 : : }
222 [ + + ][ + + ]: 270661 : }
[ + + ][ + + ]
223 : : }
224 : 199602 : break;
225 : 82409 : case ProofRewriteRule::SEQ_EVAL_OP:
226 : : {
227 : : // this is a catchall rule for evaluation of operations on constant
228 : : // sequences
229 : 82409 : TypeNode tn = utils::getOwnerStringType(n);
230 [ + + ]: 82409 : if (tn.isSequence())
231 : : {
232 [ + + ]: 4288 : for (const Node& nc : n)
233 : : {
234 [ + + ]: 3513 : if (!nc.isConst())
235 : : {
236 : 2019 : return Node::null();
237 : : }
238 [ + + ]: 3513 : }
239 : 775 : RewriteResponse response = postRewrite(n);
240 : 775 : Node ret = response.d_node;
241 [ + - ]: 775 : if (ret.isConst())
242 : : {
243 : 775 : return ret;
244 : : }
245 [ - + ][ - + ]: 1550 : }
246 [ + + ]: 82409 : }
247 : 79615 : break;
248 : 116 : case ProofRewriteRule::STR_OVERLAP_SPLIT_CTN:
249 : : case ProofRewriteRule::STR_OVERLAP_ENDPOINTS_CTN:
250 : : case ProofRewriteRule::STR_OVERLAP_ENDPOINTS_INDEXOF:
251 : : case ProofRewriteRule::STR_OVERLAP_ENDPOINTS_REPLACE:
252 : 116 : return rewriteViaOverlap(id, n);
253 : 0 : default: break;
254 : : }
255 : 484559 : return Node::null();
256 : : }
257 : :
258 : 2 : ArithEntail& SequencesRewriter::getArithEntail() { return d_arithEntail; }
259 : :
260 : 3 : StringsEntail& SequencesRewriter::getStringsEntail() { return d_stringsEntail; }
261 : :
262 : 631382 : Node SequencesRewriter::rewriteEquality(Node node)
263 : : {
264 [ - + ][ - + ]: 631382 : Assert(node.getKind() == Kind::EQUAL);
[ - - ]
265 [ + + ]: 631382 : if (node[0] == node[1])
266 : : {
267 : 34315 : return returnRewrite(node, d_true, Rewrite::EQ_REFL);
268 : : }
269 : 597067 : else if (node[0].isConst() && node[1].isConst())
270 : : {
271 : 5685 : return returnRewrite(node, d_false, Rewrite::EQ_CONST_FALSE);
272 : : }
273 : : // standard ordering
274 [ + + ]: 591382 : if (node[0] > node[1])
275 : : {
276 : 177292 : Node ret = nodeManager()->mkNode(Kind::EQUAL, node[1], node[0]);
277 : 88646 : return returnRewrite(node, ret, Rewrite::EQ_SYM);
278 : 88646 : }
279 : 502736 : return node;
280 : : }
281 : :
282 : 120837 : Node SequencesRewriter::rewriteEqualityExt(Node node)
283 : : {
284 [ - + ][ - + ]: 120837 : Assert(node.getKind() == Kind::EQUAL);
[ - - ]
285 : 120837 : TypeNode tn = node[0].getType();
286 [ + + ]: 120837 : if (tn.isInteger())
287 : : {
288 : 28076 : return rewriteArithEqualityExt(node);
289 : : }
290 [ + + ]: 92761 : if (tn.isStringLike())
291 : : {
292 : 92739 : return rewriteStrEqualityExt(node);
293 : : }
294 : 22 : return node;
295 : 120837 : }
296 : :
297 : 92739 : Node SequencesRewriter::rewriteStrEqualityExt(Node node)
298 : : {
299 : 92739 : Assert(node.getKind() == Kind::EQUAL && node[0].getType().isStringLike());
300 : 92739 : TypeNode stype = node[0].getType();
301 : :
302 : 92739 : bool hasStrTerm = false;
303 [ + + ]: 183871 : for (size_t r = 0; r < 2; r++)
304 : : {
305 [ + + ][ - - ]: 179095 : if (!node[r].isConst()
306 [ + + ][ + + ]: 179095 : && kindToTheoryId(node[r].getKind()) == THEORY_STRINGS)
[ + + ][ + - ]
[ - - ]
307 : : {
308 : 87963 : hasStrTerm = true;
309 : 87963 : break;
310 : : }
311 : : }
312 [ + + ]: 92739 : if (!hasStrTerm)
313 : : {
314 : : // equality between variables and constants, no rewrites apply
315 : 4776 : return node;
316 : : }
317 : :
318 : 87963 : NodeManager* nm = nodeManager();
319 : : // ( ~contains( s, t ) V ~contains( t, s ) ) => ( s == t ---> false )
320 [ + + ]: 257087 : for (unsigned r = 0; r < 2; r++)
321 : : {
322 : : // must call rewrite contains directly to avoid infinite loop
323 : 345634 : Node ctn = nm->mkNode(Kind::STRING_CONTAINS, node[r], node[1 - r]);
324 : 172817 : Node prev = ctn;
325 : 172817 : ctn = rewriteContains(ctn);
326 [ - + ][ - + ]: 172817 : Assert(!ctn.isNull());
[ - - ]
327 [ + + ][ + + ]: 172817 : if (ctn != prev && ctn.getKind() == Kind::STRING_CONTAINS)
[ + + ]
328 : : {
329 : 1345 : prev = ctn;
330 : 1345 : ctn = rewriteContains(ctn);
331 [ - + ][ - + ]: 1345 : Assert(!ctn.isNull());
[ - - ]
332 : : }
333 [ + + ]: 172817 : if (ctn.isConst())
334 : : {
335 [ + + ]: 54065 : if (!ctn.getConst<bool>())
336 : : {
337 : 3693 : return returnRewrite(node, ctn, Rewrite::EQ_NCTN);
338 : : }
339 : : else
340 : : {
341 : : // definitely contains but not syntactically equal
342 : : // We may be able to simplify, e.g.
343 : : // str.++( x, "a" ) == "a" ----> x = ""
344 : : }
345 : : }
346 [ + + ][ + + ]: 176510 : }
347 : :
348 [ + + ]: 505620 : std::vector<Node> c[2];
349 [ + + ]: 252810 : for (unsigned i = 0; i < 2; i++)
350 : : {
351 : 168540 : utils::getConcat(node[i], c[i]);
352 : : }
353 : :
354 : : // check if the prefix, suffix mismatches
355 : : // For example, str.++( x, "a", y ) == str.++( x, "bc", z ) ---> false
356 : 84270 : unsigned minsize = std::min(c[0].size(), c[1].size());
357 [ + + ]: 252561 : for (unsigned r = 0; r < 2; r++)
358 : : {
359 [ + + ]: 169442 : for (unsigned i = 0; i < minsize; i++)
360 : : {
361 [ + + ]: 169180 : unsigned index1 = r == 0 ? i : (c[0].size() - 1) - i;
362 [ + + ]: 169180 : unsigned index2 = r == 0 ? i : (c[1].size() - 1) - i;
363 : 169180 : Node s = c[0][index1];
364 : 169180 : Node t = c[1][index2];
365 [ + + ][ + + ]: 169180 : if (s.isConst() && t.isConst())
[ + + ]
366 : : {
367 : 1245 : size_t lenS = Word::getLength(s);
368 : 1245 : size_t lenT = Word::getLength(t);
369 [ + + ]: 1245 : size_t lenShort = lenS <= lenT ? lenS : lenT;
370 : 2490 : bool isSameFix = r == 1 ? Word::rstrncmp(s, t, lenShort)
371 : 1245 : : Word::strncmp(s, t, lenShort);
372 [ + + ]: 1245 : if (!isSameFix)
373 : : {
374 : 242 : Node ret = nodeManager()->mkConst(false);
375 : 242 : return returnRewrite(node, ret, Rewrite::EQ_NFIX);
376 : 242 : }
377 : : }
378 [ + + ]: 168938 : if (s != t)
379 : : {
380 : 168029 : break;
381 : : }
382 [ + + ][ + + ]: 337451 : }
[ + + ]
383 : : }
384 : :
385 : 84028 : Node new_ret;
386 : : // ------- equality unification
387 : 84028 : bool changed = false;
388 [ + + ]: 252084 : for (unsigned i = 0; i < 2; i++)
389 : : {
390 [ + + ][ + - ]: 168937 : while (!c[0].empty() && !c[1].empty() && c[0].back() == c[1].back())
[ + + ][ + + ]
391 : : {
392 : 881 : c[0].pop_back();
393 : 881 : c[1].pop_back();
394 : 881 : changed = true;
395 : : }
396 : : // splice constants
397 [ + - ][ + + ]: 335689 : if (!c[0].empty() && !c[1].empty() && c[0].back().isConst()
398 [ + + ][ + + ]: 335689 : && c[1].back().isConst())
[ + + ]
399 : : {
400 [ + + ]: 2580 : Node cs[2];
401 : : size_t csl[2];
402 [ + + ]: 1290 : for (unsigned j = 0; j < 2; j++)
403 : : {
404 : 860 : cs[j] = c[j].back();
405 : 860 : csl[j] = Word::getLength(cs[j]);
406 : : }
407 : 430 : size_t larger = csl[0] > csl[1] ? 0 : 1;
408 : 430 : size_t smallerSize = csl[1 - larger];
409 : 860 : if (cs[1 - larger]
410 : 675 : == (i == 0 ? Word::suffix(cs[larger], smallerSize)
411 : 245 : : Word::prefix(cs[larger], smallerSize)))
412 : : {
413 : 430 : size_t sizeDiff = csl[larger] - smallerSize;
414 : 430 : c[larger][c[larger].size() - 1] =
415 : 1105 : i == 0 ? Word::prefix(cs[larger], sizeDiff)
416 : 675 : : Word::suffix(cs[larger], sizeDiff);
417 : 430 : c[1 - larger].pop_back();
418 : 430 : changed = true;
419 : : }
420 [ + + ][ - - ]: 1290 : }
421 [ + + ]: 504168 : for (unsigned j = 0; j < 2; j++)
422 : : {
423 : 336112 : std::reverse(c[j].begin(), c[j].end());
424 : : }
425 : : }
426 [ + + ]: 84028 : if (changed)
427 : : {
428 : : // e.g. x++y = x++z ---> y = z, "AB" ++ x = "A" ++ y --> "B" ++ x = y
429 : 1060 : Node s1 = utils::mkConcat(c[0], stype);
430 : 1060 : Node s2 = utils::mkConcat(c[1], stype);
431 : 1060 : if (s1 != node[0] || s2 != node[1])
432 : : {
433 : 1060 : new_ret = s1.eqNode(s2);
434 : : // We generally don't apply the extended equality rewriter if the
435 : : // original node was an equality but we may be able to do additional
436 : : // rewriting here, e.g.,
437 : : // x++y = "" --> x = "" and y = ""
438 : 1060 : return returnRewrite(node, new_ret, Rewrite::STR_EQ_UNIFY);
439 : : }
440 [ - + ][ - + ]: 2120 : }
441 : :
442 : : // ------- rewrites for (= "" _)
443 : 82968 : Node empty = Word::mkEmptyWord(stype);
444 [ + + ]: 230245 : for (size_t i = 0; i < 2; i++)
445 : : {
446 [ + + ]: 156753 : if (node[i] == empty)
447 : : {
448 : 46944 : Node ne = node[1 - i];
449 [ + + ]: 46944 : if (ne.getKind() == Kind::STRING_REPLACE)
450 : : {
451 : : // (= "" (str.replace x y x)) ---> (= x "")
452 [ + + ]: 5620 : if (ne[0] == ne[2])
453 : : {
454 : 362 : Node ret = nm->mkNode(Kind::EQUAL, ne[0], empty);
455 : 181 : return returnRewrite(node, ret, Rewrite::STR_EMP_REPL_X_Y_X);
456 : 181 : }
457 : :
458 : : // (= "" (str.replace x y "A")) ---> (and (= x "") (not (= y "")))
459 [ + + ]: 5439 : if (d_stringsEntail.checkNonEmpty(ne[2]))
460 : : {
461 : 651 : Node ret = nm->mkNode(
462 : : Kind::AND,
463 : 434 : {nm->mkNode(Kind::EQUAL, ne[0], empty),
464 : 434 : nm->mkNode(Kind::NOT, nm->mkNode(Kind::EQUAL, ne[1], empty))});
465 : 217 : return returnRewrite(node, ret, Rewrite::STR_EMP_REPL_EMP);
466 : 217 : }
467 : :
468 : : // (= "" (str.replace x "A" "")) ---> (str.prefix x "A")
469 : 5222 : if (d_stringsEntail.checkLengthOne(ne[1], true) && ne[2] == empty)
470 : : {
471 : 1126 : Node ret = nm->mkNode(Kind::STRING_PREFIX, ne[0], ne[1]);
472 : 563 : return returnRewrite(node, ret, Rewrite::STR_EMP_REPL_EMP);
473 : 563 : }
474 : : }
475 [ + + ]: 41324 : else if (ne.getKind() == Kind::STRING_SUBSTR)
476 : : {
477 : 36806 : Node zero = nm->mkConstInt(Rational(0));
478 : :
479 [ + + ][ - - ]: 36806 : if (d_arithEntail.check(ne[1], false)
480 [ + + ][ + + ]: 36806 : && d_arithEntail.check(ne[2], true))
[ + + ][ + - ]
[ - - ]
481 : : {
482 : : // (= "" (str.substr x 0 m)) ---> (= "" x) if m > 0
483 [ + + ]: 1402 : if (ne[1] == zero)
484 : : {
485 : 1248 : Node ret = nm->mkNode(Kind::EQUAL, ne[0], empty);
486 : 624 : return returnRewrite(node, ret, Rewrite::STR_EMP_SUBSTR_LEQ_LEN);
487 : 624 : }
488 : :
489 : : // (= "" (str.substr x n m)) ---> (<= (str.len x) n)
490 : : // if n >= 0 and m > 0
491 : : Node ret = nm->mkNode(
492 : 1556 : Kind::LEQ, nm->mkNode(Kind::STRING_LENGTH, ne[0]), ne[1]);
493 : 778 : return returnRewrite(node, ret, Rewrite::STR_EMP_SUBSTR_LEQ_LEN);
494 : 778 : }
495 : :
496 : : // (= "" (str.substr "A" 0 z)) ---> (<= z 0)
497 : 35404 : if (d_stringsEntail.checkNonEmpty(ne[0]) && ne[1] == zero)
498 : : {
499 : 14226 : Node ret = nm->mkNode(Kind::LEQ, ne[2], zero);
500 : 7113 : return returnRewrite(node, ret, Rewrite::STR_EMP_SUBSTR_LEQ_Z);
501 : 7113 : }
502 [ + + ]: 36806 : }
503 [ + + ]: 46944 : }
504 : : }
505 : :
506 : : // ------- rewrites for (= (str.replace _ _ _) _)
507 [ + + ]: 220455 : for (size_t i = 0; i < 2; i++)
508 : : {
509 [ + + ]: 146984 : if (node[i].getKind() == Kind::STRING_REPLACE)
510 : : {
511 : 12451 : Node repl = node[i];
512 : 12451 : Node x = node[1 - i];
513 : :
514 : : // (= "A" (str.replace "" x y)) ---> (and (= x "") (= y "A"))
515 : 12451 : if (d_stringsEntail.checkNonEmpty(x) && repl[0] == empty)
516 : : {
517 : : Node ret =
518 : 32 : nm->mkNode(Kind::AND, {repl[1].eqNode(empty), repl[2].eqNode(x)});
519 : 8 : return returnRewrite(node, ret, Rewrite::STR_EQ_REPL_EMP);
520 : 8 : }
521 : :
522 : : // (= x (str.replace y x y)) ---> (= x y)
523 : 12443 : if (repl[0] == repl[2] && x == repl[1])
524 : : {
525 : 2 : Node ret = nm->mkNode(Kind::EQUAL, x, repl[0]);
526 : 1 : return returnRewrite(node, ret, Rewrite::STR_EQ_REPL_TO_EQ);
527 : 1 : }
528 : :
529 : : // (= x (str.replace x "A" "B")) ---> (not (str.contains x "A"))
530 [ + + ]: 12442 : if (x == repl[0])
531 : : {
532 : 8724 : Node eq = rewriteEquality(nm->mkNode(Kind::EQUAL, repl[1], repl[2]));
533 [ + + ][ + - ]: 4362 : if (eq.isConst() && !eq.getConst<bool>())
[ + + ]
534 : : {
535 : : Node ret = nm->mkNode(Kind::NOT,
536 : 20 : nm->mkNode(Kind::STRING_CONTAINS, x, repl[1]));
537 : 10 : return returnRewrite(node, ret, Rewrite::STR_EQ_REPL_NOT_CTN);
538 : 10 : }
539 [ + + ]: 4362 : }
540 : :
541 : : // (= (str.replace x y z) z) --> (or (= x y) (= x z))
542 : : // if (str.len y) = (str.len z)
543 [ + + ]: 12432 : if (repl[2] == x)
544 : : {
545 : 6038 : Node lenY = nm->mkNode(Kind::STRING_LENGTH, repl[1]);
546 : 6038 : Node lenZ = nm->mkNode(Kind::STRING_LENGTH, repl[2]);
547 [ + + ]: 3019 : if (d_arithEntail.checkEq(lenY, lenZ))
548 : : {
549 : 6 : Node ret = nm->mkNode(Kind::OR,
550 : 4 : {nm->mkNode(Kind::EQUAL, repl[0], repl[1]),
551 : 4 : nm->mkNode(Kind::EQUAL, repl[0], repl[2])});
552 : 2 : return returnRewrite(node, ret, Rewrite::STR_EQ_REPL_TO_DIS);
553 : 2 : }
554 [ + + ][ + + ]: 3021 : }
555 [ + + ][ + + ]: 12472 : }
556 : : }
557 : :
558 : : // Try to rewrite (= x y) into a conjunction of equalities based on length
559 : : // entailment.
560 : : //
561 : : // (<= (str.len x) (str.++ y1 ... yn)) AND (= x (str.++ y1 ... yn)) --->
562 : : // (and (= x (str.++ y1' ... ym')) (= y1'' "") ... (= yk'' ""))
563 : : //
564 : : // where yi' and yi'' correspond to some yj and
565 : : // (<= (str.len x) (str.++ y1' ... ym'))
566 : 73471 : new_ret = rewriteViaStrEqLenUnifyPrefix(node);
567 [ + + ]: 73471 : if (!new_ret.isNull())
568 : : {
569 : 166 : return returnRewrite(node, new_ret, Rewrite::STR_EQ_CONJ_LEN_ENTAIL);
570 : : }
571 : :
572 : : // (= (str.++ x_1 ... x_i x_{i + 1} ... x_n)
573 : : // (str.++ y_1 ... y_j y_{j + 1} ... y_m)) --->
574 : : // (and (= (str.++ x_1 ... x_i) (str.++ y_1 ... y_j))
575 : : // (= (str.++ x_{i + 1} ... x_n) (str.++ y_{j + 1} ... y_m)))
576 : : //
577 : : // if (str.len (str.++ x_1 ... x_i)) = (str.len (str.++ y_1 ... y_j))
578 : : //
579 : : // This rewrite performs length-based equality splitting: If we can show
580 : : // that two prefixes have the same length, we can split an equality into
581 : : // two equalities, one over the prefixes and another over the suffixes.
582 : : Rewrite rule;
583 : 73305 : new_ret = rewriteViaStrEqLenUnify(node, rule);
584 [ + + ]: 73305 : if (!new_ret.isNull())
585 : : {
586 : 49 : return returnRewrite(node, new_ret, rule);
587 : : }
588 : :
589 : 73256 : return node;
590 [ + + ][ - - ]: 429577 : }
591 : :
592 : 28076 : Node SequencesRewriter::rewriteArithEqualityExt(Node node)
593 : : {
594 : 28076 : Assert(node.getKind() == Kind::EQUAL && node[0].getType().isInteger());
595 : :
596 : : // cases where we can solve the equality
597 : :
598 : : // notice we cannot rewrite str.to.int(x)=n to x="n" due to leading zeroes.
599 : :
600 : 28076 : return node;
601 : : }
602 : :
603 : 198772 : Node SequencesRewriter::rewriteLength(Node node)
604 : : {
605 [ - + ][ - + ]: 198772 : Assert(node.getKind() == Kind::STRING_LENGTH);
[ - - ]
606 : 198772 : NodeManager* nm = nodeManager();
607 : 198772 : Kind nk0 = node[0].getKind();
608 [ + + ]: 198772 : if (node[0].isConst())
609 : : {
610 : 30838 : Node retNode = nm->mkConstInt(Rational(Word::getLength(node[0])));
611 : 15419 : return returnRewrite(node, retNode, Rewrite::LEN_EVAL);
612 : 15419 : }
613 [ + + ]: 183353 : else if (nk0 == Kind::STRING_CONCAT)
614 : : {
615 : 15664 : Node tmpNode = node[0];
616 [ + - ]: 15664 : if (tmpNode.getKind() == Kind::STRING_CONCAT)
617 : : {
618 : 15664 : std::vector<Node> node_vec;
619 [ + + ]: 59778 : for (unsigned int i = 0; i < tmpNode.getNumChildren(); ++i)
620 : : {
621 [ + + ]: 44114 : if (tmpNode[i].isConst())
622 : : {
623 : 10569 : node_vec.push_back(
624 : 21138 : nm->mkConstInt(Rational(Word::getLength(tmpNode[i]))));
625 : : }
626 : : else
627 : : {
628 : 33545 : node_vec.push_back(
629 : 33545 : nodeManager()->mkNode(Kind::STRING_LENGTH, tmpNode[i]));
630 : : }
631 : : }
632 : 15664 : Node retNode = nodeManager()->mkNode(Kind::ADD, node_vec);
633 : 15664 : return returnRewrite(node, retNode, Rewrite::LEN_CONCAT);
634 : 15664 : }
635 [ - + ]: 15664 : }
636 [ + + ][ + + ]: 167689 : else if (nk0 == Kind::STRING_REPLACE || nk0 == Kind::STRING_REPLACE_ALL)
637 : : {
638 : 7822 : Node len1 = nm->mkNode(Kind::STRING_LENGTH, node[0][1]);
639 : 7822 : Node len2 = nm->mkNode(Kind::STRING_LENGTH, node[0][2]);
640 [ + + ]: 3911 : if (d_arithEntail.checkEq(len1, len2))
641 : : {
642 : : // len( y ) == len( z ) => len( str.replace( x, y, z ) ) ---> len( x )
643 : 554 : Node retNode = nm->mkNode(Kind::STRING_LENGTH, node[0][0]);
644 : 277 : return returnRewrite(node, retNode, Rewrite::LEN_REPL_INV);
645 : 277 : }
646 [ + + ][ + + ]: 7822 : }
647 [ + + ][ + + ]: 163778 : else if (nk0 == Kind::STRING_TO_LOWER || nk0 == Kind::STRING_TO_UPPER
648 [ + + ][ + + ]: 163705 : || nk0 == Kind::STRING_REV || nk0 == Kind::STRING_UPDATE)
649 : : {
650 : : // len( f( x ) ) == len( x ) where f is to_lower, to_upper, or rev.
651 : : // len( update( x, n, y ) ) = len( x )
652 : 1238 : Node retNode = nm->mkNode(Kind::STRING_LENGTH, node[0][0]);
653 : 619 : return returnRewrite(node, retNode, Rewrite::LEN_CONV_INV);
654 : 619 : }
655 [ + + ][ - + ]: 163159 : else if (nk0 == Kind::SEQ_UNIT || nk0 == Kind::STRING_UNIT)
656 : : {
657 : 818 : Node retNode = nm->mkConstInt(Rational(1));
658 : 818 : return returnRewrite(node, retNode, Rewrite::LEN_SEQ_UNIT);
659 : 818 : }
660 : 165975 : return node;
661 : : }
662 : :
663 : : // TODO (#1180) add rewrite
664 : : // str.++( str.substr( x, n1, n2 ), str.substr( x, n1+n2, n3 ) ) --->
665 : : // str.substr( x, n1, n2+n3 )
666 : 253257 : Node SequencesRewriter::rewriteConcat(Node node)
667 : : {
668 [ - + ][ - + ]: 253257 : Assert(node.getKind() == Kind::STRING_CONCAT);
[ - - ]
669 [ + - ]: 506514 : Trace("strings-rewrite-debug")
670 : 253257 : << "Strings::rewriteConcat start " << node << std::endl;
671 : 253257 : std::vector<Node> node_vec;
672 : 253257 : Node preNode = Node::null();
673 [ + + ]: 1099399 : for (Node tmpNode : node)
674 : : {
675 [ + + ]: 846142 : if (tmpNode.getKind() == Kind::STRING_CONCAT)
676 : : {
677 : 11474 : unsigned j = 0;
678 : : // combine the first term with the previous constant if applicable
679 [ + + ]: 11474 : if (!preNode.isNull())
680 : : {
681 [ + + ]: 2767 : if (tmpNode[0].isConst())
682 : : {
683 : 607 : std::vector<Node> wvec;
684 : 607 : wvec.push_back(preNode);
685 : 607 : wvec.push_back(tmpNode[0]);
686 : 607 : preNode = Word::mkWordFlatten(wvec);
687 : 607 : node_vec.push_back(preNode);
688 : 607 : }
689 : : else
690 : : {
691 : 2160 : node_vec.push_back(preNode);
692 : 2160 : node_vec.push_back(tmpNode[0]);
693 : : }
694 : 2767 : preNode = Node::null();
695 : 2767 : ++j;
696 : : }
697 : : // insert the middle terms to node_vec
698 [ + - ]: 11474 : if (j <= tmpNode.getNumChildren() - 1)
699 : : {
700 : 11474 : node_vec.insert(node_vec.end(), tmpNode.begin() + j, tmpNode.end() - 1);
701 : : }
702 : : // take the last term as the current
703 : 11474 : tmpNode = tmpNode[tmpNode.getNumChildren() - 1];
704 : : }
705 [ + + ]: 846142 : if (!tmpNode.isConst())
706 : : {
707 [ + + ]: 536896 : if (!preNode.isNull())
708 : : {
709 [ + - ][ + + ]: 139683 : if (preNode.isConst() && !Word::isEmpty(preNode))
[ + - ][ + + ]
[ - - ]
710 : : {
711 : 134667 : node_vec.push_back(preNode);
712 : : }
713 : 139683 : preNode = Node::null();
714 : : }
715 : 536896 : node_vec.push_back(tmpNode);
716 : : }
717 : : else
718 : : {
719 [ + + ]: 309246 : if (preNode.isNull())
720 : : {
721 : 242584 : preNode = tmpNode;
722 : : }
723 : : else
724 : : {
725 : 66662 : std::vector<Node> vec;
726 : 66662 : vec.push_back(preNode);
727 : 66662 : vec.push_back(tmpNode);
728 : 66662 : preNode = Word::mkWordFlatten(vec);
729 : 66662 : }
730 : : }
731 : 846142 : }
732 [ + + ][ + - ]: 253257 : if (!preNode.isNull() && (!preNode.isConst() || !Word::isEmpty(preNode)))
[ + + ][ + + ]
[ + + ][ - - ]
733 : : {
734 : 95577 : node_vec.push_back(preNode);
735 : : }
736 : :
737 : 253257 : TypeNode tn = node.getType();
738 : 253257 : Node retNode = utils::mkConcat(node_vec, tn);
739 [ + - ]: 506514 : Trace("strings-rewrite-debug")
740 : 253257 : << "Strings::rewriteConcat end " << retNode << std::endl;
741 [ + + ]: 253257 : if (retNode != node)
742 : : {
743 : 41852 : return returnRewrite(node, retNode, Rewrite::CONCAT_NORM);
744 : : }
745 : 211405 : return node;
746 : 253257 : }
747 : :
748 : 116 : Node SequencesRewriter::rewriteAllRegExp(TNode node)
749 : : {
750 [ - + ][ - + ]: 116 : Assert(node.getKind() == Kind::REGEXP_ALL);
[ - - ]
751 : 116 : NodeManager* nm = nodeManager();
752 : : // re.all ----> (re.* re.allchar)
753 : 232 : Node ret = nm->mkNode(Kind::REGEXP_STAR, nm->mkNode(Kind::REGEXP_ALLCHAR));
754 : 232 : return returnRewrite(node, ret, Rewrite::RE_ALL_ELIM);
755 : 116 : }
756 : :
757 : 8981 : Node SequencesRewriter::rewriteConcatRegExp(TNode node)
758 : : {
759 [ - + ][ - + ]: 8981 : Assert(node.getKind() == Kind::REGEXP_CONCAT);
[ - - ]
760 : 8981 : NodeManager* nm = nodeManager();
761 [ + - ]: 17962 : Trace("strings-rewrite-debug")
762 : 8981 : << "Strings::rewriteConcatRegExp flatten " << node << std::endl;
763 : 8981 : Node retNode = node;
764 : 8981 : std::vector<Node> vec;
765 : 8981 : bool changed = false;
766 : 8981 : Node emptyRe;
767 : :
768 : : // get the string type that are members of this regular expression
769 : 8981 : TypeNode rtype = node.getType();
770 : 8981 : TypeNode stype;
771 [ + - ]: 8981 : if (rtype.isRegExp())
772 : : {
773 : : // standard regular expressions are for strings
774 : 8981 : stype = nm->stringType();
775 : : }
776 : : else
777 : : {
778 : 0 : Unimplemented();
779 : : }
780 : :
781 [ + + ]: 38160 : for (const Node& c : node)
782 : : {
783 [ + + ]: 29214 : if (c.getKind() == Kind::REGEXP_CONCAT)
784 : : {
785 : 428 : changed = true;
786 [ + + ]: 1584 : for (const Node& cc : c)
787 : : {
788 : 1156 : vec.push_back(cc);
789 : 1156 : }
790 : : }
791 [ + + ][ + + ]: 37600 : else if (c.getKind() == Kind::STRING_TO_REGEXP && c[0].isConst()
[ - - ]
792 : 37600 : && Word::isEmpty(c[0]))
793 : : {
794 : 104 : changed = true;
795 : 104 : emptyRe = c;
796 : : }
797 [ + + ]: 28682 : else if (c.getKind() == Kind::REGEXP_NONE)
798 : : {
799 : : // re.++( ..., empty, ... ) ---> empty
800 : 35 : Node ret = nm->mkNode(Kind::REGEXP_NONE);
801 : 35 : return returnRewrite(node, ret, Rewrite::RE_CONCAT_EMPTY);
802 : 35 : }
803 : : else
804 : : {
805 : 28647 : vec.push_back(c);
806 : : }
807 [ + + ]: 29214 : }
808 [ + + ]: 8946 : if (changed)
809 : : {
810 : : // flatten
811 : : // this handles nested re.++ and elimination or str.to.re(""), e.g.:
812 : : // re.++( re.++( R1, R2 ), str.to.re(""), R3 ) ---> re.++( R1, R2, R3 )
813 [ + + ]: 508 : if (vec.empty())
814 : : {
815 [ - + ][ - + ]: 4 : Assert(!emptyRe.isNull());
[ - - ]
816 : 4 : retNode = emptyRe;
817 : : }
818 : : else
819 : : {
820 [ + + ]: 504 : retNode = vec.size() == 1 ? vec[0] : nm->mkNode(Kind::REGEXP_CONCAT, vec);
821 : : }
822 : 508 : return returnRewrite(node, retNode, Rewrite::RE_CONCAT_FLATTEN);
823 : : }
824 [ + - ]: 16876 : Trace("strings-rewrite-debug")
825 : 8438 : << "Strings::rewriteConcatRegExp start " << node << std::endl;
826 : 8438 : std::vector<Node> cvec;
827 : : // the current accumulation of constant strings
828 : 8438 : std::vector<Node> preReStr;
829 : : // whether the last component was (_)*
830 : 8438 : bool lastAllStar = false;
831 : 8438 : String emptyStr = String("");
832 : : // this loop checks to see if components can be combined or dropped
833 [ + + ]: 44812 : for (unsigned i = 0, size = vec.size(); i <= size; i++)
834 : : {
835 : 36374 : Node curr;
836 [ + + ]: 36374 : if (i < size)
837 : : {
838 : 27936 : curr = vec[i];
839 [ - + ][ - + ]: 27936 : Assert(curr.getKind() != Kind::REGEXP_CONCAT);
[ - - ]
840 : : }
841 : : // update preReStr
842 [ + + ][ + + ]: 36374 : if (!curr.isNull() && curr.getKind() == Kind::STRING_TO_REGEXP)
[ + + ]
843 : : {
844 : 8415 : lastAllStar = false;
845 : 8415 : preReStr.push_back(curr[0]);
846 : 8415 : curr = Node::null();
847 : : }
848 [ + + ]: 27959 : else if (!preReStr.empty())
849 : : {
850 [ - + ][ - + ]: 7890 : Assert(!lastAllStar);
[ - - ]
851 : : // this groups consecutive strings a++b ---> ab
852 : : Node acc =
853 : 15780 : nm->mkNode(Kind::STRING_TO_REGEXP, utils::mkConcat(preReStr, stype));
854 : 7890 : cvec.push_back(acc);
855 : 7890 : preReStr.clear();
856 : 7890 : }
857 [ + + ][ + + ]: 20069 : else if (!curr.isNull() && lastAllStar)
[ + + ]
858 : : {
859 : : // if empty, drop it
860 : : // e.g. this ensures we rewrite (_)* ++ (a)* ---> (_)*
861 [ + + ][ - - ]: 401 : if (RegExpEntail::isConstRegExp(curr)
862 [ + + ][ + + ]: 401 : && RegExpEntail::testConstStringInRegExp(emptyStr, curr))
[ + + ][ + - ]
[ - - ]
863 : : {
864 : 194 : curr = Node::null();
865 : : }
866 : : }
867 [ + + ]: 36374 : if (!curr.isNull())
868 : : {
869 : 19327 : lastAllStar = false;
870 [ + + ]: 19327 : if (curr.getKind() == Kind::REGEXP_STAR)
871 : : {
872 : : // we can group stars (a)* ++ (a)* ---> (a)*
873 [ + + ][ + + ]: 8418 : if (!cvec.empty() && cvec.back() == curr)
[ + + ]
874 : : {
875 : 41 : curr = Node::null();
876 : : }
877 [ + + ]: 8377 : else if (curr[0].getKind() == Kind::REGEXP_ALLCHAR)
878 : : {
879 [ - + ][ - + ]: 3329 : Assert(!lastAllStar);
[ - - ]
880 : 3329 : lastAllStar = true;
881 : : // go back and remove empty ones from back of cvec
882 : : // e.g. this ensures we rewrite (a)* ++ (_)* ---> (_)*
883 : 3329 : while (
884 [ + + ][ - - ]: 5050 : !cvec.empty() && RegExpEntail::isConstRegExp(cvec.back())
885 [ + + ][ + + ]: 8441 : && RegExpEntail::testConstStringInRegExp(emptyStr, cvec.back()))
[ + + ][ + + ]
[ + + ][ - - ]
886 : : {
887 : 62 : cvec.pop_back();
888 : : }
889 : : }
890 : : }
891 : : }
892 [ + + ]: 36374 : if (!curr.isNull())
893 : : {
894 : 19286 : cvec.push_back(curr);
895 : : }
896 : 36374 : }
897 [ - + ][ - + ]: 8438 : Assert(!cvec.empty());
[ - - ]
898 : 8438 : retNode = utils::mkConcat(cvec, rtype);
899 [ + + ]: 8438 : if (retNode != node)
900 : : {
901 : : // handles all cases where consecutive re constants are combined or
902 : : // dropped as described in the loop above.
903 : 375 : return returnRewrite(node, retNode, Rewrite::RE_CONCAT);
904 : : }
905 : :
906 : : // flipping adjacent star arguments
907 : 8063 : changed = false;
908 [ + + ]: 26145 : for (size_t i = 0, size = cvec.size() - 1; i < size; i++)
909 : : {
910 [ + + ][ + + ]: 18082 : if (cvec[i].getKind() == Kind::REGEXP_STAR && cvec[i][0] == cvec[i + 1])
[ + + ][ + + ]
[ - - ]
911 : : {
912 : : // by convention, flip the order (a*)++a ---> a++(a*)
913 : 195 : std::swap(cvec[i], cvec[i + 1]);
914 : 195 : changed = true;
915 : : }
916 : : }
917 [ + + ]: 8063 : if (changed)
918 : : {
919 : 104 : retNode = utils::mkConcat(cvec, rtype);
920 : 104 : return returnRewrite(node, retNode, Rewrite::RE_CONCAT_OPT);
921 : : }
922 : 7959 : return node;
923 : 8981 : }
924 : :
925 : 4827 : Node SequencesRewriter::rewriteStarRegExp(TNode node)
926 : : {
927 [ - + ][ - + ]: 4827 : Assert(node.getKind() == Kind::REGEXP_STAR);
[ - - ]
928 : 4827 : NodeManager* nm = nodeManager();
929 : 4827 : Node retNode = node;
930 [ + + ]: 4827 : if (node[0].getKind() == Kind::REGEXP_STAR)
931 : : {
932 : : // ((R)*)* ---> R*
933 : 32 : return returnRewrite(node, node[0], Rewrite::RE_STAR_NESTED_STAR);
934 : : }
935 : 6385 : else if (node[0].getKind() == Kind::STRING_TO_REGEXP && node[0][0].isConst()
936 : 6385 : && Word::isEmpty(node[0][0]))
937 : : {
938 : : // ("")* ---> ""
939 : 18 : return returnRewrite(node, node[0], Rewrite::RE_STAR_EMPTY_STRING);
940 : : }
941 [ + + ]: 4777 : else if (node[0].getKind() == Kind::REGEXP_NONE)
942 : : {
943 : : // (empty)* ---> ""
944 : 28 : retNode = nm->mkNode(Kind::STRING_TO_REGEXP, nm->mkConst(String("")));
945 : 28 : return returnRewrite(node, retNode, Rewrite::RE_STAR_EMPTY);
946 : : }
947 [ + + ]: 4749 : else if (node[0].getKind() == Kind::REGEXP_UNION)
948 : : {
949 [ + + ]: 2304 : for (const Node& nc : node[0])
950 : : {
951 [ + + ]: 1628 : if (nc.getKind() == Kind::REGEXP_ALLCHAR)
952 : : {
953 : : // (re.* (re.union ... re.allchar ...)) ---> (re.* re.allchar)
954 : 12 : retNode = nm->mkNode(Kind::REGEXP_STAR, nc);
955 : 12 : return returnRewrite(node, retNode, Rewrite::RE_STAR_UNION_CHAR);
956 : : }
957 [ + + ][ + + ]: 2316 : }
958 : : // simplification of unions under star
959 [ + + ]: 676 : if (RegExpEntail::hasEpsilonNode(node[0]))
960 : : {
961 : 26 : bool changed = false;
962 : 26 : std::vector<Node> node_vec;
963 [ + + ]: 78 : for (const Node& nc : node[0])
964 : : {
965 : 103 : if (nc.getKind() == Kind::STRING_TO_REGEXP && nc[0].isConst()
966 : 103 : && Word::isEmpty(nc[0]))
967 : : {
968 : : // can be removed
969 : 26 : changed = true;
970 : : }
971 : : else
972 : : {
973 : 26 : node_vec.push_back(nc);
974 : : }
975 : 78 : }
976 [ + - ]: 26 : if (changed)
977 : : {
978 : 26 : retNode = node_vec.size() == 1
979 [ + - ]: 52 : ? node_vec[0]
980 : 26 : : nm->mkNode(Kind::REGEXP_UNION, node_vec);
981 : 26 : retNode = nm->mkNode(Kind::REGEXP_STAR, retNode);
982 : : // simplification of union beneath star based on loop above
983 : : // for example, ( "" | "a" )* ---> ("a")*
984 : 26 : return returnRewrite(node, retNode, Rewrite::RE_STAR_UNION);
985 : : }
986 [ - + ]: 26 : }
987 : : }
988 : 4711 : return node;
989 : 4827 : }
990 : :
991 : 23913 : Node SequencesRewriter::rewriteViaMacroReInterUnionInclusion(const Node& node)
992 : : {
993 : 23913 : Kind nk = node.getKind();
994 [ + + ][ + + ]: 23913 : if (nk != Kind::REGEXP_UNION && nk != Kind::REGEXP_INTER)
995 : : {
996 : 19644 : return Node::null();
997 : : }
998 [ + + ]: 25614 : std::vector<Node> polRegExp[2];
999 [ + + ]: 14550 : for (const Node& ni : node)
1000 : : {
1001 : 10281 : Kind nik = ni.getKind();
1002 [ + + ]: 10281 : uint32_t pindex = nik == Kind::REGEXP_COMPLEMENT ? 1 : 0;
1003 [ + + ]: 10281 : Node nia = pindex == 1 ? ni[0] : ni;
1004 : 10281 : polRegExp[pindex].push_back(nia);
1005 : 10281 : }
1006 [ + + ]: 5796 : for (const Node& negMem : polRegExp[1])
1007 : : {
1008 [ + + ]: 2956 : for (const Node& posMem : polRegExp[0])
1009 : : {
1010 [ + + ]: 1429 : Node m1 = nk == Kind::REGEXP_INTER ? negMem : posMem;
1011 [ + + ]: 1429 : Node m2 = nk == Kind::REGEXP_INTER ? posMem : negMem;
1012 : : // inclusion test for conflicting case m1 contains m2
1013 : : // (re.inter (re.comp R1) R2) --> re.none where R1 includes R2
1014 : : // (re.union R1 (re.comp R2)) --> (re.* re.allchar) where R1 includes R2
1015 [ + + ]: 1429 : if (RegExpEntail::regExpIncludes(m1, m2))
1016 : : {
1017 : 266 : NodeManager* nm = nodeManager();
1018 : : Node retNode = nk == Kind::REGEXP_INTER
1019 : : ? nm->mkNode(Kind::REGEXP_NONE)
1020 : : : nm->mkNode(Kind::REGEXP_STAR,
1021 : 317 : nm->mkNode(Kind::REGEXP_ALLCHAR));
1022 : 266 : std::vector<Node> newChildren;
1023 : 266 : newChildren.push_back(retNode);
1024 : : // Now go back and include all the remaining children that were
1025 : : // not involved. This simplifies proof checking, since we can isolate
1026 : : // which children led to the conflict.
1027 : : // In particular, if Ri includes Rj, then we rewrite
1028 : : // (re.inter R1 ... (re.comp Ri) ... Rj ... Rn)
1029 : : // to
1030 : : // (re.inter re.none R1...R{i-1} R{i+1} ... R{j-1} R{j+1} .. Rn)
1031 : : // where the latter will be rewritten to re.none.
1032 : 266 : bool foundPos = false;
1033 : 266 : bool foundNeg = false;
1034 [ + + ]: 849 : for (const Node& nc : node)
1035 : : {
1036 [ + + ][ + + ]: 583 : if (!foundPos && nc == posMem)
[ + + ]
1037 : : {
1038 : 266 : foundPos = true;
1039 : 266 : continue;
1040 : : }
1041 [ + + ]: 282 : if (!foundNeg && nc.getKind() == Kind::REGEXP_COMPLEMENT
1042 [ + + ][ + - ]: 599 : && nc[0] == negMem)
[ + + ][ + + ]
[ - - ]
1043 : : {
1044 : 266 : foundNeg = true;
1045 : 266 : continue;
1046 : : }
1047 : 51 : newChildren.push_back(nc);
1048 [ + + ]: 583 : }
1049 [ + + ]: 266 : if (newChildren.size() > 1)
1050 : : {
1051 : 51 : retNode = nm->mkNode(nk, newChildren);
1052 : : }
1053 : 266 : return retNode;
1054 : 266 : }
1055 [ + + ][ + + ]: 1695 : }
1056 : : }
1057 : 4003 : return Node::null();
1058 [ + + ][ - - ]: 12807 : }
1059 : :
1060 : 83 : Node SequencesRewriter::rewriteViaReInterUnionInclusion(ProofRewriteRule id,
1061 : : const Node& n)
1062 : : {
1063 [ + - ][ - + ]: 83 : if (n.getNumChildren() != 2 || n[1].getKind() != Kind::REGEXP_COMPLEMENT)
[ + - ][ - + ]
[ - - ]
1064 : : {
1065 : 0 : return Node::null();
1066 : : }
1067 : 83 : Kind k = n.getKind();
1068 [ + + ]: 83 : if (id == ProofRewriteRule::RE_INTER_INCLUSION)
1069 : : {
1070 : 71 : if (k == Kind::REGEXP_INTER && RegExpEntail::regExpIncludes(n[1][0], n[0]))
1071 : : {
1072 : 71 : return nodeManager()->mkNode(Kind::REGEXP_NONE);
1073 : : }
1074 : : }
1075 : : else
1076 : : {
1077 [ - + ][ - + ]: 12 : Assert(id == ProofRewriteRule::RE_UNION_INCLUSION);
[ - - ]
1078 : 12 : if (k == Kind::REGEXP_UNION && RegExpEntail::regExpIncludes(n[0], n[1][0]))
1079 : : {
1080 : 12 : NodeManager* nm = nodeManager();
1081 : 12 : return nm->mkNode(Kind::REGEXP_STAR, nm->mkNode(Kind::REGEXP_ALLCHAR));
1082 : : }
1083 : : }
1084 : 0 : return Node::null();
1085 : : }
1086 : :
1087 : 4515 : Node SequencesRewriter::rewriteAndOrRegExp(TNode node)
1088 : : {
1089 : 4515 : Kind nk = node.getKind();
1090 [ + + ][ + - ]: 4515 : Assert(nk == Kind::REGEXP_UNION || nk == Kind::REGEXP_INTER);
[ - + ][ - + ]
[ - - ]
1091 [ + - ]: 9030 : Trace("strings-rewrite-debug")
1092 : 4515 : << "Strings::rewriteAndOrRegExp start " << node << std::endl;
1093 : 4515 : NodeManager* nm = nodeManager();
1094 : 4515 : std::vector<Node> node_vec;
1095 : : // list of constant string regular expressions (str.to_re c)
1096 : 4515 : std::vector<Node> constStrRe;
1097 : 4515 : bool changed = false;
1098 [ + + ]: 15206 : for (const Node& ni : node)
1099 : : {
1100 : 10772 : Kind nik = ni.getKind();
1101 [ + + ]: 10772 : if (nik == nk)
1102 : : {
1103 [ + + ]: 232 : for (const Node& nic : ni)
1104 : : {
1105 [ + + ]: 162 : if (std::find(node_vec.begin(), node_vec.end(), nic) == node_vec.end())
1106 : : {
1107 : 160 : node_vec.push_back(nic);
1108 : : }
1109 : 162 : }
1110 : 70 : changed = true;
1111 : : }
1112 [ + + ]: 10702 : else if (nik == Kind::REGEXP_NONE)
1113 : : {
1114 [ + + ]: 52 : if (nk == Kind::REGEXP_INTER)
1115 : : {
1116 : 22 : return returnRewrite(node, ni, Rewrite::RE_AND_EMPTY);
1117 : : }
1118 : : // otherwise, can ignore
1119 : 30 : changed = true;
1120 : : }
1121 : 10650 : else if (nik == Kind::REGEXP_STAR
1122 [ + + ][ + + ]: 10650 : && ni[0].getKind() == Kind::REGEXP_ALLCHAR)
[ + + ][ + + ]
[ - - ]
1123 : : {
1124 [ + + ]: 68 : if (nk == Kind::REGEXP_UNION)
1125 : : {
1126 : 46 : return returnRewrite(node, ni, Rewrite::RE_OR_ALL);
1127 : : }
1128 : : // otherwise, can ignore
1129 : 22 : changed = true;
1130 : : }
1131 [ + + ]: 10582 : else if (std::find(node_vec.begin(), node_vec.end(), ni) == node_vec.end())
1132 : : {
1133 [ + + ][ + + ]: 10552 : if (nik == Kind::STRING_TO_REGEXP && ni[0].isConst())
[ + + ][ + + ]
[ - - ]
1134 : : {
1135 [ + + ]: 3744 : if (nk == Kind::REGEXP_INTER)
1136 : : {
1137 [ + + ]: 353 : if (!constStrRe.empty())
1138 : : {
1139 [ - + ][ - + ]: 13 : Assert(constStrRe[0][0] != ni[0]);
[ - - ]
1140 : : // (re.inter .. (str.to_re c1) .. (str.to_re c2) ..) ---> re.none
1141 : : // for distinct constant strings c1, c2.
1142 : 13 : Node ret = nm->mkNode(Kind::REGEXP_NONE);
1143 : : return returnRewrite(
1144 : 13 : node, ret, Rewrite::RE_INTER_CONST_CONST_CONFLICT);
1145 : 13 : }
1146 : : }
1147 : : else
1148 : : {
1149 [ - + ][ - + ]: 3391 : Assert(nk == Kind::REGEXP_UNION);
[ - - ]
1150 : : }
1151 : 3731 : constStrRe.push_back(ni);
1152 : : }
1153 : 10539 : node_vec.push_back(ni);
1154 : : }
1155 : : else
1156 : : {
1157 : 30 : changed = true;
1158 : : }
1159 [ + + ]: 10772 : }
1160 : : // if we already changed due to flattening, return already
1161 [ + + ]: 4434 : if (changed)
1162 : : {
1163 : 147 : Node retNode = node;
1164 [ - + ]: 147 : if (node_vec.empty())
1165 : : {
1166 [ - - ]: 0 : if (nk == Kind::REGEXP_INTER)
1167 : : {
1168 : : retNode =
1169 : 0 : nm->mkNode(Kind::REGEXP_STAR, nm->mkNode(Kind::REGEXP_ALLCHAR));
1170 : : }
1171 : : else
1172 : : {
1173 : 0 : retNode = nm->mkNode(Kind::REGEXP_NONE);
1174 : : }
1175 : : }
1176 : : else
1177 : : {
1178 [ + + ]: 147 : retNode = node_vec.size() == 1 ? node_vec[0] : nm->mkNode(nk, node_vec);
1179 : : }
1180 [ + - ]: 147 : if (retNode != node)
1181 : : {
1182 : : // flattening and removing children, based on loop above
1183 : 147 : return returnRewrite(node, retNode, Rewrite::RE_ANDOR_FLATTEN);
1184 : : }
1185 [ - + ]: 147 : }
1186 : : // try to eliminate components via constant membership tests
1187 : 4287 : Node conflict;
1188 : 4287 : Node retNode = rewriteViaMacroReInterUnionConstElim(node, conflict);
1189 [ + + ]: 4287 : if (!retNode.isNull())
1190 : : {
1191 : 231 : return returnRewrite(node, retNode, Rewrite::RE_ANDOR_CONST_REMOVE);
1192 : : }
1193 : :
1194 : : // use inclusion tests
1195 : 4056 : retNode = rewriteViaMacroReInterUnionInclusion(node);
1196 [ + + ]: 4056 : if (!retNode.isNull())
1197 : : {
1198 : 152 : return returnRewrite(node, retNode, Rewrite::RE_ANDOR_INC_CONFLICT);
1199 : : }
1200 : :
1201 : : // otherwise there is no change
1202 : 3904 : return node;
1203 : 4515 : }
1204 : :
1205 : 155 : Node SequencesRewriter::rewriteLoopRegExp(TNode node)
1206 : : {
1207 [ - + ][ - + ]: 155 : Assert(node.getKind() == Kind::REGEXP_LOOP);
[ - - ]
1208 : 155 : uint32_t l = utils::getLoopMinOccurrences(node);
1209 : 155 : uint32_t u = utils::getLoopMaxOccurrences(node);
1210 : 155 : Node r = node[0];
1211 : 155 : Node retNode = node;
1212 : :
1213 : 155 : NodeManager* nm = nodeManager();
1214 [ + + ]: 155 : if (u < l)
1215 : : {
1216 : : // ((_ re.loop l u) r) --> re.none if u < l
1217 : 23 : std::vector<Node> nvec;
1218 : 23 : retNode = nm->mkNode(Kind::REGEXP_NONE, nvec);
1219 : 23 : return returnRewrite(node, retNode, Rewrite::RE_LOOP_NONE);
1220 : 23 : }
1221 [ + + ]: 132 : else if (u == 0)
1222 : : {
1223 : 2 : retNode = nm->mkNode(Kind::STRING_TO_REGEXP, nm->mkConst(String("")));
1224 : 2 : return returnRewrite(node, retNode, Rewrite::RE_LOOP_ZERO);
1225 : : }
1226 [ + + ]: 130 : else if (r.getKind() == Kind::REGEXP_STAR)
1227 : : {
1228 : 10 : return returnRewrite(node, r, Rewrite::RE_LOOP_STAR);
1229 : : }
1230 : 120 : retNode = rewriteViaReLoopElim(node);
1231 [ + - ][ + - ]: 120 : Assert(!retNode.isNull() && retNode != node);
[ - + ][ - + ]
[ - - ]
1232 : 120 : return returnRewrite(node, retNode, Rewrite::RE_LOOP);
1233 : 155 : }
1234 : :
1235 : 73537 : Node SequencesRewriter::rewriteViaStrEqLenUnifyPrefix(const Node& node)
1236 : : {
1237 : 73537 : Node newRet;
1238 [ + + ]: 220233 : for (unsigned i = 0; i < 2; i++)
1239 : : {
1240 [ + + ]: 146910 : if (node[1 - i].getKind() == Kind::STRING_CONCAT)
1241 : : {
1242 : 2047 : newRet = d_stringsEntail.inferEqsFromContains(node[i], node[1 - i]);
1243 : : // don't rewrite if just returning a (flipped) equality
1244 [ + + ][ + + ]: 2047 : if (!newRet.isNull() && newRet.getKind() == Kind::AND)
[ + + ]
1245 : : {
1246 [ + + ]: 214 : if (i == 1)
1247 : : {
1248 : : // flip the first equality back
1249 : 50 : std::vector<Node> nc(newRet.begin(), newRet.end());
1250 : 50 : nc[0] = nc[0][1].eqNode(nc[0][0]);
1251 : 50 : newRet = nodeManager()->mkNode(Kind::AND, nc);
1252 : 50 : }
1253 : 214 : return newRet;
1254 : : }
1255 : : }
1256 : : }
1257 : 73323 : return Node::null();
1258 : 73537 : }
1259 : :
1260 : 73341 : Node SequencesRewriter::rewriteViaStrEqLenUnify(const Node& node, Rewrite& rule)
1261 : : {
1262 [ + + ][ - - ]: 73341 : if (node[0].getKind() == Kind::STRING_CONCAT
1263 [ + + ][ + + ]: 73341 : && node[1].getKind() == Kind::STRING_CONCAT)
[ + + ][ + - ]
[ - - ]
1264 : : {
1265 : 243 : std::vector<Node> v0, v1;
1266 : 243 : utils::getConcat(node[0], v0);
1267 : 243 : utils::getConcat(node[1], v1);
1268 : 243 : size_t startRhs = 0;
1269 : 243 : TypeNode stype = node[0].getType();
1270 [ + + ]: 1052 : for (size_t i = 0, size0 = v0.size(); i <= size0; i++)
1271 : : {
1272 : 894 : const std::vector<Node> pfxv0(v0.begin(), v0.begin() + i);
1273 : 894 : Node pfx0 = utils::mkConcat(pfxv0, stype);
1274 [ + + ]: 3613 : for (size_t j = startRhs, size1 = v1.size(); j <= size1; j++)
1275 : : {
1276 [ + + ][ + + ]: 3137 : if (!(i == 0 && j == 0) && !(i == v0.size() && j == v1.size()))
[ + + ][ + + ]
[ + + ]
1277 : : {
1278 : 2736 : std::vector<Node> pfxv1(v1.begin(), v1.begin() + j);
1279 : 2736 : Node pfx1 = utils::mkConcat(pfxv1, stype);
1280 : 2736 : Node lenPfx0 = d_nm->mkNode(Kind::STRING_LENGTH, pfx0);
1281 : 2736 : Node lenPfx1 = d_nm->mkNode(Kind::STRING_LENGTH, pfx1);
1282 : :
1283 [ + + ]: 2736 : if (d_arithEntail.checkEq(lenPfx0, lenPfx1))
1284 : : {
1285 : 83 : std::vector<Node> sfxv0(v0.begin() + i, v0.end());
1286 : 83 : std::vector<Node> sfxv1(v1.begin() + j, v1.end());
1287 : : Node ret =
1288 : 249 : d_nm->mkNode(Kind::AND,
1289 : 83 : {pfx0.eqNode(pfx1),
1290 : 166 : utils::mkConcat(sfxv0, stype)
1291 : 249 : .eqNode(utils::mkConcat(sfxv1, stype))});
1292 : 83 : rule = Rewrite::SPLIT_EQ;
1293 : 83 : return ret;
1294 : 83 : }
1295 [ + + ]: 2653 : else if (d_arithEntail.check(lenPfx1, lenPfx0, true))
1296 : : {
1297 : : // The prefix on the right-hand side is strictly longer than the
1298 : : // prefix on the left-hand side, so we try to strip the right-hand
1299 : : // prefix by the length of the left-hand prefix
1300 : : //
1301 : : // Example:
1302 : : // (= (str.++ "A" x y) (str.++ x "AB" z)) --->
1303 : : // (and (= (str.++ "A" x) (str.++ x "A")) (= y (str.++ "B" z)))
1304 : 333 : std::vector<Node> rpfxv1;
1305 [ - + ]: 333 : if (d_stringsEntail.stripSymbolicLength(
1306 : : pfxv1, rpfxv1, 1, lenPfx0, true))
1307 : : {
1308 : : // The rewrite requires the full left-hand prefix length to be
1309 : : // stripped (otherwise we would have to keep parts of the
1310 : : // left-hand prefix).
1311 : 0 : if (lenPfx0.isConst() && lenPfx0.getConst<Rational>().isZero())
1312 : : {
1313 : 0 : std::vector<Node> sfxv0(v0.begin() + i, v0.end());
1314 : 0 : pfxv1.insert(pfxv1.end(), v1.begin() + j, v1.end());
1315 : : Node ret =
1316 : 0 : d_nm->mkNode(Kind::AND,
1317 : 0 : {pfx0.eqNode(utils::mkConcat(rpfxv1, stype)),
1318 : 0 : utils::mkConcat(sfxv0, stype)
1319 : 0 : .eqNode(utils::mkConcat(pfxv1, stype))});
1320 : 0 : rule = Rewrite::SPLIT_EQ_STRIP_R;
1321 : 0 : return ret;
1322 : 0 : }
1323 : : }
1324 : :
1325 : : // If the prefix of the right-hand side is (strictly) longer than
1326 : : // the prefix of the left-hand side, we can advance the left-hand
1327 : : // side (since the length of the right-hand side is only increasing
1328 : : // in the inner loop)
1329 : 333 : break;
1330 [ - + ]: 333 : }
1331 [ + + ]: 2320 : else if (d_arithEntail.check(lenPfx0, lenPfx1, true))
1332 : : {
1333 : : // The prefix on the left-hand side is strictly longer than the
1334 : : // prefix on the right-hand side, so we try to strip the left-hand
1335 : : // prefix by the length of the right-hand prefix
1336 : : //
1337 : : // Example:
1338 : : // (= (str.++ x "AB" z) (str.++ "A" x y)) --->
1339 : : // (and (= (str.++ x "A") (str.++ "A" x)) (= (str.++ "B" z) y))
1340 : 311 : std::vector<Node> sfxv0 = pfxv0;
1341 : 311 : std::vector<Node> rpfxv0;
1342 [ + + ]: 311 : if (d_stringsEntail.stripSymbolicLength(
1343 : : sfxv0, rpfxv0, 1, lenPfx1, true))
1344 : : {
1345 : : // The rewrite requires the full right-hand prefix length to be
1346 : : // stripped (otherwise we would have to keep parts of the
1347 : : // right-hand prefix).
1348 [ + - ][ + - ]: 2 : if (lenPfx1.isConst() && lenPfx1.getConst<Rational>().isZero())
[ + - ]
1349 : : {
1350 : 2 : sfxv0.insert(sfxv0.end(), v0.begin() + i, v0.end());
1351 : 2 : std::vector<Node> sfxv1(v1.begin() + j, v1.end());
1352 : : Node ret =
1353 : 6 : d_nm->mkNode(Kind::AND,
1354 : 4 : {utils::mkConcat(rpfxv0, stype).eqNode(pfx1),
1355 : 4 : utils::mkConcat(sfxv0, stype)
1356 : 6 : .eqNode(utils::mkConcat(sfxv1, stype))});
1357 : 2 : rule = Rewrite::SPLIT_EQ_STRIP_L;
1358 : 2 : return ret;
1359 : 2 : }
1360 : : }
1361 : :
1362 : : // If the prefix of the left-hand side is (strictly) longer than
1363 : : // the prefix of the right-hand side, then we don't need to check
1364 : : // that right-hand prefix for future left-hand prefixes anymore
1365 : : // (since they are increasing in length)
1366 : 309 : startRhs = j + 1;
1367 [ + + ][ + + ]: 313 : }
1368 [ + + ][ + + ]: 3990 : }
[ + + ][ + + ]
[ + + ][ + + ]
1369 : : }
1370 [ + + ][ + + ]: 979 : }
1371 [ + + ][ + + ]: 413 : }
[ + + ]
1372 : 73256 : return Node::null();
1373 : : }
1374 : :
1375 : 19989 : Node SequencesRewriter::rewriteViaReLoopElim(const Node& node)
1376 : : {
1377 [ + + ]: 19989 : if (node.getKind() != Kind::REGEXP_LOOP)
1378 : : {
1379 : 19797 : return Node::null();
1380 : : }
1381 : 192 : uint32_t l = utils::getLoopMinOccurrences(node);
1382 : 192 : uint32_t u = utils::getLoopMaxOccurrences(node);
1383 [ + + ]: 192 : if (u < l)
1384 : : {
1385 : 6 : return Node::null();
1386 : : }
1387 : 186 : Node r = node[0];
1388 : 186 : std::vector<Node> vec_nodes;
1389 [ + + ]: 801 : for (unsigned i = 0; i < l; i++)
1390 : : {
1391 : 615 : vec_nodes.push_back(r);
1392 : : }
1393 : 186 : NodeManager* nm = nodeManager();
1394 : 186 : Node n = vec_nodes.size() == 0
1395 : 220 : ? nm->mkNode(Kind::STRING_TO_REGEXP, nm->mkConst(String("")))
1396 : 152 : : vec_nodes.size() == 1 ? r
1397 [ + + ][ + + ]: 406 : : nm->mkNode(Kind::REGEXP_CONCAT, vec_nodes);
[ + + ][ + + ]
[ - - ]
1398 : 186 : Node retNode;
1399 [ + + ]: 186 : if (u == l)
1400 : : {
1401 : 119 : retNode = n;
1402 : : }
1403 : : else
1404 : : {
1405 : 67 : std::vector<Node> vec2;
1406 : 67 : vec2.push_back(n);
1407 : 67 : TypeNode rtype = nm->regExpType();
1408 [ + + ]: 448 : for (uint32_t j = l; j < u; j++)
1409 : : {
1410 : 381 : vec_nodes.push_back(r);
1411 : 381 : n = utils::mkConcat(vec_nodes, rtype);
1412 : 381 : vec2.push_back(n);
1413 : : }
1414 : 67 : retNode = nm->mkNode(Kind::REGEXP_UNION, vec2);
1415 : 67 : }
1416 [ + - ]: 372 : Trace("strings-lp") << "Strings::lp " << node << " => " << retNode
1417 : 186 : << std::endl;
1418 [ - + ][ - + ]: 186 : Assert(retNode != node);
[ - - ]
1419 : 186 : return retNode;
1420 : 186 : }
1421 : :
1422 : 19820 : Node SequencesRewriter::rewriteViaReEqElim(const Node& n)
1423 : : {
1424 : 19820 : if (n.getKind() != Kind::EQUAL || !n[0].getType().isRegExp())
1425 : : {
1426 : 19802 : return Node::null();
1427 : : }
1428 : 18 : NodeManager* nm = nodeManager();
1429 : 18 : Node v = SkolemCache::mkRegExpEqVar(nm, n);
1430 : 36 : Node mem1 = nm->mkNode(Kind::STRING_IN_REGEXP, v, n[0]);
1431 : 36 : Node mem2 = nm->mkNode(Kind::STRING_IN_REGEXP, v, n[1]);
1432 : 54 : return nm->mkNode(Kind::FORALL,
1433 [ + + ][ - - ]: 72 : {nm->mkNode(Kind::BOUND_VAR_LIST, v), mem1.eqNode(mem2)});
1434 : 18 : }
1435 : :
1436 : 110236 : Node SequencesRewriter::rewriteViaStrInReEval(const Node& node)
1437 : : {
1438 [ + + ][ + + ]: 140522 : if (node.getKind() != Kind::STRING_IN_REGEXP || !node[0].isConst()
[ - - ]
1439 : 140522 : || !RegExpEntail::isConstRegExp(node[1]))
1440 : : {
1441 : 106928 : return Node::null();
1442 : : }
1443 : : // test whether x in node[1]
1444 : 3308 : String s = node[0].getConst<String>();
1445 : 3308 : bool test = RegExpEntail::testConstStringInRegExp(s, node[1]);
1446 : 3308 : return nodeManager()->mkConst(test);
1447 : 3308 : }
1448 : :
1449 : 19520 : Node SequencesRewriter::rewriteViaStrInReConcatStarChar(const Node& n)
1450 : : {
1451 : 58560 : if (n.getKind() != Kind::STRING_IN_REGEXP
1452 [ + + ][ + + ]: 20869 : || n[0].getKind() != Kind::STRING_CONCAT
[ - - ]
1453 [ + + ][ + + ]: 20869 : || n[1].getKind() != Kind::REGEXP_STAR)
[ + + ][ + + ]
[ - - ]
1454 : : {
1455 : 19401 : return Node::null();
1456 : : }
1457 : 238 : Node len = RegExpEntail::getFixedLengthForRegexp(n[1][0]);
1458 [ - + ]: 119 : if (len.isNull())
1459 : : {
1460 : 0 : return Node::null();
1461 : : }
1462 [ + - ][ - + ]: 119 : if (!len.isConst() || len.getConst<Rational>() != Rational(1))
[ + - ][ - + ]
[ - - ]
1463 : : {
1464 : 0 : return Node::null();
1465 : : }
1466 : 119 : NodeManager* nm = nodeManager();
1467 : 119 : std::vector<Node> cc;
1468 : 119 : utils::getConcat(n[0], cc);
1469 : 119 : std::vector<Node> conj;
1470 [ + + ]: 462 : for (const Node& c : cc)
1471 : : {
1472 : 343 : conj.push_back(nm->mkNode(Kind::STRING_IN_REGEXP, c, n[1]));
1473 : : }
1474 : 119 : return nm->mkAnd(conj);
1475 : 119 : }
1476 : :
1477 : 19409 : Node SequencesRewriter::rewriteViaStrInReSigma(const Node& n)
1478 : : {
1479 : 58227 : if (n.getKind() != Kind::STRING_IN_REGEXP
1480 [ + + ][ + + ]: 19409 : || n[1].getKind() != Kind::REGEXP_CONCAT)
[ + + ][ + + ]
[ - - ]
1481 : : {
1482 : 19283 : return Node::null();
1483 : : }
1484 : 126 : const Node& r = n[1];
1485 : 126 : bool allSigmaStrict = true;
1486 : 126 : size_t allSigmaMinSize = 0;
1487 [ + + ]: 217 : for (const Node& rc : r)
1488 : : {
1489 [ + + ]: 203 : if (rc.getKind() == Kind::REGEXP_ALLCHAR)
1490 : : {
1491 : 45 : allSigmaMinSize++;
1492 : : }
1493 : 474 : else if (rc.getKind() == Kind::REGEXP_STAR
1494 [ + + ][ + + ]: 158 : && rc[0].getKind() == Kind::REGEXP_ALLCHAR)
[ + + ][ + + ]
[ - - ]
1495 : : {
1496 : 46 : allSigmaStrict = false;
1497 : : }
1498 : : else
1499 : : {
1500 : 112 : return Node::null();
1501 : : }
1502 [ + + ]: 203 : }
1503 : : // x in re.++(_*, _, _) ---> str.len(x) >= 2
1504 : 14 : NodeManager* nm = nodeManager();
1505 : 14 : Node num = nm->mkConstInt(Rational(allSigmaMinSize));
1506 : 28 : Node lenx = nm->mkNode(Kind::STRING_LENGTH, n[0]);
1507 [ + + ]: 14 : return nm->mkNode(allSigmaStrict ? Kind::EQUAL : Kind::GEQ, lenx, num);
1508 : 126 : }
1509 : 19399 : Node SequencesRewriter::rewriteViaStrInReSigmaStar(const Node& n)
1510 : : {
1511 : 58197 : if (n.getKind() != Kind::STRING_IN_REGEXP
1512 [ + + ][ + + ]: 20627 : || n[1].getKind() != Kind::REGEXP_STAR
[ - - ]
1513 : 20627 : || n[1][0].getKind() != Kind::REGEXP_CONCAT)
1514 : : {
1515 : 19392 : return Node::null();
1516 : : }
1517 : 7 : const Node& r = n[1][0];
1518 [ + + ]: 28 : for (const Node& rc : r)
1519 : : {
1520 [ - + ]: 21 : if (rc.getKind() != Kind::REGEXP_ALLCHAR)
1521 : : {
1522 : 0 : return Node::null();
1523 : : }
1524 [ + - ]: 21 : }
1525 : 7 : NodeManager* nm = nodeManager();
1526 : 7 : Node zero = nm->mkConstInt(Rational(0));
1527 : 7 : Node num = nm->mkConstInt(Rational(r.getNumChildren()));
1528 : 14 : Node lenx = nm->mkNode(Kind::STRING_LENGTH, n[0]);
1529 : 14 : Node t = nm->mkNode(Kind::INTS_MODULUS, lenx, num);
1530 : 7 : return nm->mkNode(Kind::EQUAL, t, zero);
1531 : 7 : }
1532 : :
1533 : 112190 : Node SequencesRewriter::rewriteViaMacroSubstrStripSymLength(const Node& node,
1534 : : Rewrite& rule,
1535 : : StringsEntail& sent)
1536 : : {
1537 [ + + ]: 112190 : if (node.getKind() != Kind::STRING_SUBSTR)
1538 : : {
1539 : 331 : return Node::null();
1540 : : }
1541 : 111859 : std::vector<Node> ch1;
1542 : 111859 : std::vector<Node> ch2;
1543 : 111859 : return sent.rewriteViaMacroSubstrStripSymLength(node, rule, ch1, ch2);
1544 : 111859 : }
1545 : :
1546 : 15841 : Node SequencesRewriter::rewriteViaMacroStrInReInclusion(const Node& n)
1547 : : {
1548 [ + + ]: 15841 : if (n.getKind() != Kind::STRING_IN_REGEXP)
1549 : : {
1550 : 165 : return Node::null();
1551 : : }
1552 : : // check regular expression inclusion
1553 : : // This makes a regular expression that contains all possible model values
1554 : : // for x, and checks whether r includes this regular expression. If so,
1555 : : // the membership rewrites to true.
1556 : 15676 : RegExpEntail re(nodeManager(), nullptr);
1557 : 15676 : Node reForX = re.getGeneralizedConstRegExp(n[0]);
1558 : : // only chance of success is if there was at least one constant
1559 [ + + ]: 15676 : if (!reForX.isNull())
1560 : : {
1561 [ + + ]: 2848 : if (RegExpEntail::regExpIncludes(n[1], reForX))
1562 : : {
1563 : 152 : return d_true;
1564 : : }
1565 : : }
1566 : 15524 : return Node::null();
1567 : 15676 : }
1568 : :
1569 : 26142 : Node SequencesRewriter::rewriteViaMacroStrSplitCtn(const Node& node)
1570 : : {
1571 : 78426 : if (node.getKind() != Kind::STRING_CONTAINS
1572 : 52143 : || node[0].getKind() != Kind::STRING_CONCAT || !node[1].isConst()
1573 : 52143 : || Word::getLength(node[1]) == 0) // don't bother if empty string
1574 : : {
1575 : 21186 : return Node::null();
1576 : : }
1577 : 4956 : Node t = node[1];
1578 : : // Below, we are looking for a constant component of node[0]
1579 : : // has no overlap with node[1], which means we can split.
1580 : : // Notice that if the first or last components had no
1581 : : // overlap, these would have been removed by strip
1582 : : // constant endpoints. Hence, we consider only the inner children.
1583 [ + + ]: 8657 : for (size_t i = 1, iend = (node[0].getNumChildren() - 1); i < iend; i++)
1584 : : {
1585 : : // constant contains
1586 [ + + ]: 4564 : if (node[0][i].isConst())
1587 : : {
1588 : : // if no overlap, we can split into disjunction
1589 : 5541 : if (!Word::hasOverlap(node[0][i], node[1], false)
1590 : 5541 : && !Word::hasOverlap(node[1], node[0][i], false))
1591 : : {
1592 : 863 : std::vector<Node> nc0;
1593 : 863 : utils::getConcat(node[0], nc0);
1594 [ + + ]: 5178 : std::vector<Node> spl[2];
1595 : 863 : spl[0].insert(spl[0].end(), nc0.begin(), nc0.begin() + i);
1596 [ - + ][ - + ]: 863 : Assert(i < nc0.size() - 1);
[ - - ]
1597 : 863 : spl[1].insert(spl[1].end(), nc0.begin() + i + 1, nc0.end());
1598 : 863 : TypeNode stype = node[0].getType();
1599 : 3452 : Node ret = nodeManager()->mkNode(
1600 : : Kind::OR,
1601 : 863 : {nodeManager()->mkNode(Kind::STRING_CONTAINS,
1602 : 1726 : utils::mkConcat(spl[0], stype),
1603 : : node[1]),
1604 : 863 : nodeManager()->mkNode(Kind::STRING_CONTAINS,
1605 : 1726 : utils::mkConcat(spl[1], stype),
1606 : 6041 : node[1])});
1607 : 863 : return ret;
1608 [ + + ][ - - ]: 4315 : }
1609 : : }
1610 : : }
1611 : 4093 : return Node::null();
1612 : 4956 : }
1613 : :
1614 : 210659 : Node SequencesRewriter::rewriteViaMacroStrStripEndpoints(
1615 : : const Node& n,
1616 : : std::vector<Node>& nb,
1617 : : std::vector<Node>& nrem,
1618 : : std::vector<Node>& ne)
1619 : : {
1620 : 210659 : Kind k = n.getKind();
1621 : 210659 : std::vector<int> dirs;
1622 [ + + ]: 210659 : if (k == Kind::STRING_INDEXOF)
1623 : : {
1624 : : // must start at zero
1625 : 7854 : if (!n[2].isConst() || n[2].getConst<Rational>().sgn() != 0)
1626 : : {
1627 : 0 : return Node::null();
1628 : : }
1629 : : // only strip off the end
1630 : 7854 : dirs.push_back(-1);
1631 : : }
1632 [ + + ][ + + ]: 202805 : else if (k == Kind::STRING_CONTAINS || k == Kind::STRING_REPLACE)
1633 : : {
1634 [ + + ]: 202664 : if (n[1].isConst())
1635 : : {
1636 : : // if constant, we strip from one direction at a time, to ease proof
1637 : : // reconstruction
1638 : 67708 : dirs.push_back(-1);
1639 : 67708 : dirs.push_back(1);
1640 : : }
1641 : : else
1642 : : {
1643 : 134956 : dirs.push_back(0);
1644 : : }
1645 : : }
1646 : : else
1647 : : {
1648 : 141 : return Node::null();
1649 : : }
1650 : :
1651 : 210518 : std::vector<Node> nc2;
1652 : 210518 : utils::getConcat(n[1], nc2);
1653 [ - + ]: 210518 : if (nc2.empty())
1654 : : {
1655 : 0 : return Node::null();
1656 : : }
1657 : : // strip endpoints
1658 : 210518 : bool success = false;
1659 [ + + ]: 482816 : for (int dir : dirs)
1660 : : {
1661 : 276531 : nrem.clear();
1662 : 276531 : utils::getConcat(n[0], nrem);
1663 : 276531 : nb.clear();
1664 : 276531 : ne.clear();
1665 [ + + ]: 276531 : if (d_stringsEntail.stripConstantEndpoints(nrem, nc2, nb, ne, dir))
1666 : : {
1667 : 4233 : success = true;
1668 : 4233 : break;
1669 : : }
1670 : : }
1671 [ + + ]: 210518 : if (success)
1672 : : {
1673 : 4233 : NodeManager* nm = nodeManager();
1674 : 4233 : TypeNode stype = n[0].getType();
1675 : 4233 : Node rem = utils::mkConcat(nrem, stype);
1676 [ + + ][ + - ]: 4233 : switch (k)
1677 : : {
1678 : 3709 : case Kind::STRING_CONTAINS:
1679 : : {
1680 : 3709 : return nm->mkNode(Kind::STRING_CONTAINS, rem, n[1]);
1681 : : }
1682 : 424 : case Kind::STRING_REPLACE:
1683 : : {
1684 : 424 : std::vector<Node> cc;
1685 : 424 : cc.insert(cc.end(), nb.begin(), nb.end());
1686 : 424 : cc.push_back(nm->mkNode(Kind::STRING_REPLACE, rem, n[1], n[2]));
1687 : 424 : cc.insert(cc.end(), ne.begin(), ne.end());
1688 : 424 : return utils::mkConcat(cc, stype);
1689 : 424 : }
1690 : 100 : case Kind::STRING_INDEXOF:
1691 : : {
1692 : 100 : return nm->mkNode(Kind::STRING_INDEXOF, rem, n[1], n[2]);
1693 : : }
1694 : 0 : default: break;
1695 : : }
1696 [ - + ][ - + ]: 8466 : }
1697 : 206285 : return Node::null();
1698 : 210659 : }
1699 : :
1700 : 4455 : Node SequencesRewriter::rewriteViaMacroReInterUnionConstElim(const Node& n,
1701 : : Node& conflict)
1702 : : {
1703 : 4455 : Kind k = n.getKind();
1704 [ + + ][ + + ]: 4455 : if (k != Kind::REGEXP_INTER && k != Kind::REGEXP_UNION)
1705 : : {
1706 : 138 : return Node::null();
1707 : : }
1708 : 4317 : std::vector<Node> constStrRe;
1709 : 4317 : std::vector<Node> otherRe;
1710 [ + + ]: 14699 : for (const Node& nc : n)
1711 : : {
1712 [ + + ]: 10382 : if (!RegExpEntail::isConstRegExp(nc))
1713 : : {
1714 : 1042 : continue;
1715 : : }
1716 [ + + ]: 9340 : if (nc.getKind() == Kind::STRING_TO_REGEXP)
1717 : : {
1718 [ - + ][ - + ]: 3708 : Assert(nc[0].isConst());
[ - - ]
1719 : 3708 : constStrRe.push_back(nc);
1720 : : }
1721 : : else
1722 : : {
1723 : 5632 : otherRe.push_back(nc);
1724 : : }
1725 [ + + ]: 10382 : }
1726 : :
1727 [ + + ][ + + ]: 4317 : if (constStrRe.empty() || otherRe.empty())
[ + + ]
1728 : : {
1729 : 3308 : return Node::null();
1730 : : }
1731 : : // go back and process constant strings against the others
1732 : 1009 : std::unordered_set<Node> toRemove;
1733 [ + + ]: 2158 : for (const Node& c : constStrRe)
1734 : : {
1735 : 1171 : Assert(c.getKind() == Kind::STRING_TO_REGEXP && c[0].isConst());
1736 : 1171 : String s = c[0].getConst<String>();
1737 [ + + ]: 3158 : for (const Node& r : otherRe)
1738 : : {
1739 [ - + ][ - + ]: 2094 : Assert(RegExpEntail::isConstRegExp(r));
[ - - ]
1740 [ + - ]: 4188 : Trace("strings-rewrite-debug")
1741 : 2094 : << "Check " << c << " vs " << r << std::endl;
1742 : : // skip if already removing, or not constant
1743 [ - + ]: 2094 : if (toRemove.find(r) != toRemove.end())
1744 : : {
1745 [ - - ]: 0 : Trace("strings-rewrite-debug") << "...skip" << std::endl;
1746 : 0 : continue;
1747 : : }
1748 : : // test whether c from (str.to_re c) is in r
1749 [ + + ]: 2094 : if (RegExpEntail::testConstStringInRegExp(s, r))
1750 : : {
1751 [ + - ]: 286 : Trace("strings-rewrite-debug") << "...included" << std::endl;
1752 [ + + ]: 286 : if (k == Kind::REGEXP_INTER)
1753 : : {
1754 : : // (re.inter .. (str.to_re c) .. R ..) --->
1755 : : // (re.inter .. (str.to_re c) .. ..) when c in R
1756 : 201 : toRemove.insert(r);
1757 : : }
1758 : : else
1759 : : {
1760 : : // (re.union .. (str.to_re c) .. R ..) --->
1761 : : // (re.union .. .. R ..) when c in R
1762 : 85 : toRemove.insert(c);
1763 : 85 : break;
1764 : : }
1765 : : }
1766 : : else
1767 : : {
1768 [ + - ]: 1808 : Trace("strings-rewrite-debug") << "...not included" << std::endl;
1769 [ + + ]: 1808 : if (k == Kind::REGEXP_INTER)
1770 : : {
1771 : 22 : conflict = c;
1772 : : // (re.inter .. (str.to_re c) .. R ..) ---> re.none
1773 : : // if c is not a member of R.
1774 : 22 : return nodeManager()->mkNode(Kind::REGEXP_NONE);
1775 : : }
1776 : : }
1777 : : }
1778 [ + + ]: 1171 : }
1779 : :
1780 [ + + ]: 987 : if (!toRemove.empty())
1781 : : {
1782 : 239 : std::vector<Node> vec;
1783 [ + + ]: 764 : for (const Node& nc : n)
1784 : : {
1785 [ + + ]: 525 : if (toRemove.find(nc) == toRemove.end())
1786 : : {
1787 : 239 : vec.push_back(nc);
1788 : : }
1789 : 525 : }
1790 [ - + ][ - + ]: 239 : Assert(!vec.empty());
[ - - ]
1791 [ + - ]: 239 : return vec.size() == 1 ? vec[0] : nodeManager()->mkNode(k, vec);
1792 : 239 : }
1793 : :
1794 : 748 : return Node::null();
1795 : 4317 : }
1796 : :
1797 : 1396 : Node SequencesRewriter::rewriteViaStrIndexofReEval(const Node& n)
1798 : : {
1799 : 2524 : if (n.getKind() == Kind::STRING_INDEXOF_RE && n[0].isConst() && n[2].isConst()
1800 : 2524 : && RegExpEntail::isConstRegExp(n[1]))
1801 : : {
1802 : 336 : NodeManager* nm = nodeManager();
1803 : 336 : Rational nrat = n[2].getConst<Rational>();
1804 : 336 : String s = n[0].getConst<String>();
1805 : 336 : Rational rsize(s.size());
1806 [ + + ][ + + ]: 336 : if (nrat > rsize || nrat.sgn() < 0)
[ + + ]
1807 : : {
1808 : 21 : Node negone = nm->mkConstInt(Rational(-1));
1809 : 21 : return negone;
1810 : 21 : }
1811 : 315 : uint32_t start = nrat.getNumerator().toUnsignedInt();
1812 : 315 : Node rem = nm->mkConst(s.substr(start));
1813 : 315 : std::pair<size_t, size_t> match = firstMatch(rem, n[1]);
1814 : : Node ret = nm->mkConstInt(
1815 : 315 : Rational(match.first == string::npos
1816 : : ? -1
1817 [ + + ]: 630 : : static_cast<int64_t>(start + match.first)));
1818 : 315 : return ret;
1819 : 336 : }
1820 : 1060 : return Node::null();
1821 : : }
1822 : :
1823 : 883 : Node SequencesRewriter::rewriteViaStrReplaceReEval(const Node& n)
1824 : : {
1825 [ + + ][ + + ]: 1502 : if (n.getKind() == Kind::STRING_REPLACE_RE && n[0].isConst()
[ - - ]
1826 : 1502 : && RegExpEntail::isConstRegExp(n[1]))
1827 : : {
1828 : 369 : NodeManager* nm = nodeManager();
1829 : : // str.replace_re("ZABCZ", re.++("A", _*, "C"), y) ---> "Z" ++ y ++ "Z"
1830 : 369 : std::pair<size_t, size_t> match = firstMatch(n[0], n[1]);
1831 [ + + ]: 369 : if (match.first != string::npos)
1832 : : {
1833 : 225 : String s = n[0].getConst<String>();
1834 : 900 : Node ret = nm->mkNode(Kind::STRING_CONCAT,
1835 : 450 : {nm->mkConst(s.substr(0, match.first)),
1836 : : n[2],
1837 : 450 : nm->mkConst(s.substr(match.second))});
1838 : 225 : return ret;
1839 : 225 : }
1840 : 144 : return n[0];
1841 : : }
1842 : 514 : return Node::null();
1843 : : }
1844 : :
1845 : 924 : Node SequencesRewriter::rewriteViaStrReplaceReAllEval(const Node& n)
1846 : : {
1847 [ + + ][ + + ]: 1602 : if (n.getKind() == Kind::STRING_REPLACE_RE_ALL && n[0].isConst()
[ - - ]
1848 : 1602 : && RegExpEntail::isConstRegExp(n[1]))
1849 : : {
1850 : 482 : NodeManager* nm = nodeManager();
1851 : : // str.replace_re_all("ZABCZAB", re.++("A", _*, "C"), y) --->
1852 : : // "Z" ++ y ++ "Z" ++ y
1853 : 482 : TypeNode t = n[0].getType();
1854 [ - + ][ - + ]: 482 : Assert(t.isString());
[ - - ]
1855 : 482 : Node emp = Word::mkEmptyWord(t);
1856 : : Node yp = nm->mkNode(Kind::REGEXP_INTER,
1857 : : n[1],
1858 : 964 : nm->mkNode(Kind::REGEXP_COMPLEMENT,
1859 : 1928 : nm->mkNode(Kind::STRING_TO_REGEXP, emp)));
1860 : 482 : std::vector<Node> res;
1861 : 482 : String rem = n[0].getConst<String>();
1862 : 482 : std::pair<size_t, size_t> match(0, 0);
1863 [ + + ]: 871 : while (rem.size() != 0)
1864 : : {
1865 : 621 : match = firstMatch(nm->mkConst(rem), yp);
1866 [ + + ]: 621 : if (match.first == string::npos)
1867 : : {
1868 : 232 : break;
1869 : : }
1870 : 389 : res.push_back(nm->mkConst(rem.substr(0, match.first)));
1871 : 389 : res.push_back(n[2]);
1872 : 389 : rem = rem.substr(match.second);
1873 : : }
1874 : : // only concatenate remainder if non-empty
1875 [ + + ]: 482 : if (rem.size() != 0)
1876 : : {
1877 : 232 : res.push_back(nm->mkConst(rem));
1878 : : }
1879 : 482 : Node ret = utils::mkConcat(res, t);
1880 : 482 : return ret;
1881 : 482 : }
1882 : 442 : return Node::null();
1883 : : }
1884 : :
1885 : 116 : Node SequencesRewriter::rewriteViaOverlap(ProofRewriteRule id, const Node& n)
1886 : : {
1887 [ - + ]: 116 : if (n.getNumChildren() < 2)
1888 : : {
1889 : 0 : return Node::null();
1890 : : }
1891 : : // get the list of overlaps to check, based on the rule, which will be passed
1892 : : // to Word::hasOverlap below.
1893 : 116 : std::vector<std::tuple<Node, Node, int>> overlap;
1894 : 116 : Kind k = n.getKind();
1895 [ + + ][ + + ]: 116 : switch (id)
[ - ]
1896 : : {
1897 : 8 : case ProofRewriteRule::STR_OVERLAP_SPLIT_CTN:
1898 : : {
1899 [ + - ][ - + ]: 8 : if (k != Kind::STRING_CONTAINS || n[0].getNumChildren() != 3)
[ + - ][ - + ]
[ - - ]
1900 : : {
1901 : 0 : return Node::null();
1902 : : }
1903 : 8 : overlap.emplace_back(n[0][1], n[1], false);
1904 : 8 : overlap.emplace_back(n[1], n[0][1], false);
1905 : : }
1906 : 8 : break;
1907 : 64 : case ProofRewriteRule::STR_OVERLAP_ENDPOINTS_CTN:
1908 : : {
1909 [ + - ][ - + ]: 128 : if (k != Kind::STRING_CONTAINS || n[0].getNumChildren() != 3
[ - - ]
1910 [ + - ][ - + ]: 128 : || n[1].getNumChildren() != 3)
[ + - ][ + - ]
[ - - ]
1911 : : {
1912 : 0 : return Node::null();
1913 : : }
1914 : 64 : overlap.emplace_back(n[0][0], n[1][0], false);
1915 : 64 : overlap.emplace_back(n[0][2], n[1][2], true);
1916 : : }
1917 : 64 : break;
1918 : 12 : case ProofRewriteRule::STR_OVERLAP_ENDPOINTS_INDEXOF:
1919 : : {
1920 [ + - ][ - + ]: 24 : if (k != Kind::STRING_INDEXOF || n[0].getNumChildren() != 2
[ - - ]
1921 : 24 : || n[1].getNumChildren() != 2 || !n[2].isConst()
1922 [ + - ][ - + ]: 24 : || n[2].getConst<Rational>().sgn() != 0)
[ + - ][ + - ]
[ - - ]
1923 : : {
1924 : 0 : return Node::null();
1925 : : }
1926 : 12 : overlap.emplace_back(n[0][1], n[1][1], true);
1927 : : }
1928 : 12 : break;
1929 : 32 : case ProofRewriteRule::STR_OVERLAP_ENDPOINTS_REPLACE:
1930 : : {
1931 [ + - ][ - + ]: 64 : if (k != Kind::STRING_REPLACE || n[0].getNumChildren() != 3
[ - - ]
1932 [ + - ][ - + ]: 64 : || n[1].getNumChildren() != 3)
[ + - ][ + - ]
[ - - ]
1933 : : {
1934 : 0 : return Node::null();
1935 : : }
1936 : 32 : overlap.emplace_back(n[0][0], n[1][0], false);
1937 : 32 : overlap.emplace_back(n[0][2], n[1][2], true);
1938 : : }
1939 : 32 : break;
1940 : 0 : default: return Node::null();
1941 : : }
1942 [ + + ]: 336 : for (const std::tuple<Node, Node, int>& f : overlap)
1943 : : {
1944 : 220 : const Node& c1 = std::get<0>(f);
1945 : 220 : const Node& c2 = std::get<1>(f);
1946 : : // ensure it is a constant
1947 [ + - ][ - + ]: 220 : if (!c1.isConst() || !c2.isConst())
[ - + ]
1948 : : {
1949 : 0 : return Node::null();
1950 : : }
1951 : : // if it has an overlap
1952 [ - + ]: 220 : if (Word::hasOverlap(c1, c2, std::get<2>(f)))
1953 : : {
1954 : 0 : return Node::null();
1955 : : }
1956 : : }
1957 : :
1958 : : // checks succeeded, make the appropriate rewritten term
1959 : 116 : NodeManager* nm = nodeManager();
1960 [ + + ][ + + ]: 116 : switch (id)
[ - ]
1961 : : {
1962 : 8 : case ProofRewriteRule::STR_OVERLAP_SPLIT_CTN:
1963 : 24 : return nm->mkNode(
1964 : : Kind::OR,
1965 [ + + ][ - - ]: 32 : {nm->mkNode(k, n[0][0], n[1]), nm->mkNode(k, n[0][2], n[1])});
1966 : 64 : case ProofRewriteRule::STR_OVERLAP_ENDPOINTS_CTN:
1967 : 64 : return nm->mkNode(k, n[0][1], n[1]);
1968 : 12 : case ProofRewriteRule::STR_OVERLAP_ENDPOINTS_INDEXOF:
1969 : 12 : return nm->mkNode(k, n[0][0], n[1], n[2]);
1970 : 32 : case ProofRewriteRule::STR_OVERLAP_ENDPOINTS_REPLACE:
1971 : : return nm->mkNode(Kind::STRING_CONCAT,
1972 : : n[0][0],
1973 : 64 : nm->mkNode(k, n[0][1], n[1], n[2]),
1974 : 96 : n[0][2]);
1975 : 0 : default: break;
1976 : : }
1977 : 0 : return Node::null();
1978 : 116 : }
1979 : :
1980 : 28 : Node SequencesRewriter::rewriteRepeatRegExp(TNode node)
1981 : : {
1982 [ - + ][ - + ]: 28 : Assert(node.getKind() == Kind::REGEXP_REPEAT);
[ - - ]
1983 : 28 : NodeManager* nm = nodeManager();
1984 : : // ((_ re.^ n) R) --> ((_ re.loop n n) R)
1985 : 28 : unsigned r = utils::getRepeatAmount(node);
1986 : 28 : Node lop = nm->mkConst(RegExpLoop(r, r));
1987 : 56 : Node retNode = nm->mkNode(Kind::REGEXP_LOOP, lop, node[0]);
1988 : 56 : return returnRewrite(node, retNode, Rewrite::RE_REPEAT_ELIM);
1989 : 28 : }
1990 : :
1991 : 114 : Node SequencesRewriter::rewriteOptionRegExp(TNode node)
1992 : : {
1993 [ - + ][ - + ]: 114 : Assert(node.getKind() == Kind::REGEXP_OPT);
[ - - ]
1994 : 114 : NodeManager* nm = nodeManager();
1995 : : Node retNode =
1996 : : nm->mkNode(Kind::REGEXP_UNION,
1997 : 228 : nm->mkNode(Kind::STRING_TO_REGEXP, nm->mkConst(String(""))),
1998 : 342 : node[0]);
1999 : 228 : return returnRewrite(node, retNode, Rewrite::RE_OPT_ELIM);
2000 : 114 : }
2001 : :
2002 : 239 : Node SequencesRewriter::rewritePlusRegExp(TNode node)
2003 : : {
2004 [ - + ][ - + ]: 239 : Assert(node.getKind() == Kind::REGEXP_PLUS);
[ - - ]
2005 : 239 : NodeManager* nm = nodeManager();
2006 : : Node retNode = nm->mkNode(
2007 : 478 : Kind::REGEXP_CONCAT, node[0], nm->mkNode(Kind::REGEXP_STAR, node[0]));
2008 : 478 : return returnRewrite(node, retNode, Rewrite::RE_PLUS_ELIM);
2009 : 239 : }
2010 : :
2011 : 479 : Node SequencesRewriter::rewriteDifferenceRegExp(TNode node)
2012 : : {
2013 [ - + ][ - + ]: 479 : Assert(node.getKind() == Kind::REGEXP_DIFF);
[ - - ]
2014 : 479 : NodeManager* nm = nodeManager();
2015 : : Node retNode = nm->mkNode(Kind::REGEXP_INTER,
2016 : : node[0],
2017 : 958 : nm->mkNode(Kind::REGEXP_COMPLEMENT, node[1]));
2018 : 958 : return returnRewrite(node, retNode, Rewrite::RE_DIFF_ELIM);
2019 : 479 : }
2020 : :
2021 : 1340 : Node SequencesRewriter::rewriteRangeRegExp(TNode node)
2022 : : {
2023 [ - + ][ - + ]: 1340 : Assert(node.getKind() == Kind::REGEXP_RANGE);
[ - - ]
2024 : 1340 : NodeManager* nm = nodeManager();
2025 : : unsigned ch[2];
2026 : 1340 : bool hasNonConst = false;
2027 [ + + ]: 3950 : for (size_t i = 0; i < 2; ++i)
2028 : : {
2029 [ + + ]: 2650 : if (!node[i].isConst())
2030 : : {
2031 : 4 : hasNonConst = true;
2032 : 4 : continue;
2033 : : }
2034 [ + + ]: 2646 : else if (node[i].getConst<String>().size() != 1)
2035 : : {
2036 : : // non-singleton means empty
2037 : 40 : Node retNode = nm->mkNode(Kind::REGEXP_NONE);
2038 : 40 : return returnRewrite(node, retNode, Rewrite::RE_RANGE_NON_SINGLETON);
2039 : 40 : }
2040 : 2606 : ch[i] = node[i].getConst<String>().front();
2041 : : }
2042 [ + + ]: 1300 : if (hasNonConst)
2043 : : {
2044 : : // not applied to characters, it is not handled
2045 : 2 : return node;
2046 : : }
2047 : :
2048 [ + + ]: 1298 : if (node[0] == node[1])
2049 : : {
2050 : 10 : Node retNode = nm->mkNode(Kind::STRING_TO_REGEXP, node[0]);
2051 : : // re.range( "A", "A" ) ---> str.to_re( "A" )
2052 : 10 : return returnRewrite(node, retNode, Rewrite::RE_RANGE_SINGLE);
2053 : 10 : }
2054 : :
2055 [ + + ]: 1288 : if (ch[0] > ch[1])
2056 : : {
2057 : : // re.range( "B", "A" ) ---> re.none
2058 : 12 : Node retNode = nm->mkNode(Kind::REGEXP_NONE);
2059 : 12 : return returnRewrite(node, retNode, Rewrite::RE_RANGE_EMPTY);
2060 : 12 : }
2061 : 1276 : return node;
2062 : : }
2063 : :
2064 : 36696 : Node SequencesRewriter::rewriteViaStrInReConsume(const Node& node)
2065 : : {
2066 [ + + ]: 36696 : if (node.getKind() != Kind::STRING_IN_REGEXP)
2067 : : {
2068 : 18171 : return Node::null();
2069 : : }
2070 : : // if star, we consider the body of the star
2071 : 18525 : bool isStar = (node[1].getKind() == Kind::REGEXP_STAR);
2072 [ + + ]: 18525 : size_t numIter = isStar ? 2 : 1;
2073 [ + + ]: 43540 : for (size_t i = 0; i < numIter; i++)
2074 : : {
2075 [ + + ]: 26712 : int dir = isStar ? (i == 0 ? 0 : 1) : -1;
2076 [ + + ][ + + ]: 26712 : Node r = isStar ? node[1][0] : node[1];
[ - - ]
2077 : 26712 : std::vector<Node> children;
2078 : 26712 : utils::getConcat(r, children);
2079 : 26712 : std::vector<Node> mchildren;
2080 : 26712 : utils::getConcat(node[0], mchildren);
2081 : : Node scn =
2082 : 26712 : RegExpEntail::simpleRegexpConsume(d_nm, mchildren, children, dir);
2083 [ + + ]: 26712 : if (!scn.isNull())
2084 : : {
2085 : 495 : return scn;
2086 : : }
2087 [ + + ][ + + ]: 26217 : else if (!isStar || children.empty())
[ + + ]
2088 : : {
2089 : : // Given a membership (str.++ x1 ... xn) in (re.++ r1 ... rm),
2090 : : // above, we strip components to construct an equivalent membership:
2091 : : // (str.++ xi .. xj) in (re.++ rk ... rl).
2092 : 20352 : Node xn = utils::mkConcat(mchildren, node[0].getType());
2093 : : // if we considered the body of the star, we revert to the original RE
2094 : 20080 : Node rn = isStar ? node[1] : utils::mkConcat(children, node[1].getType());
2095 : : // construct the updated regular expression
2096 : 20352 : Node newMem = nodeManager()->mkNode(Kind::STRING_IN_REGEXP, xn, rn);
2097 [ + + ]: 10176 : if (newMem != node)
2098 : : {
2099 : 1202 : return newMem;
2100 : : }
2101 [ + + ][ + + ]: 12580 : }
[ + + ]
2102 [ + + ][ + + ]: 31803 : }
[ + + ][ + + ]
2103 : 16828 : return Node::null();
2104 : : }
2105 : :
2106 : 27196 : Node SequencesRewriter::rewriteMembership(TNode node)
2107 : : {
2108 [ - + ][ - + ]: 27196 : Assert(node.getKind() == Kind::STRING_IN_REGEXP);
[ - - ]
2109 : 27196 : NodeManager* nm = nodeManager();
2110 : 27196 : Node x = node[0];
2111 : 27196 : Node r = node[1];
2112 : :
2113 : 27196 : TypeNode stype = x.getType();
2114 : 27196 : TypeNode rtype = r.getType();
2115 : :
2116 [ + + ]: 27196 : if (r.getKind() == Kind::REGEXP_NONE)
2117 : : {
2118 : 292 : Node retNode = nodeManager()->mkConst(false);
2119 : 292 : return returnRewrite(node, retNode, Rewrite::RE_IN_EMPTY);
2120 : 292 : }
2121 : : // test for constant evaluation
2122 : 26904 : Node eval = rewriteViaStrInReEval(node);
2123 [ + + ]: 26904 : if (!eval.isNull())
2124 : : {
2125 : 2677 : return returnRewrite(node, eval, Rewrite::RE_IN_EVAL);
2126 : : }
2127 [ + + ]: 24227 : else if (r.getKind() == Kind::REGEXP_ALLCHAR)
2128 : : {
2129 : 140 : Node one = nm->mkConstInt(Rational(1));
2130 : 280 : Node retNode = one.eqNode(nm->mkNode(Kind::STRING_LENGTH, x));
2131 : 140 : return returnRewrite(node, retNode, Rewrite::RE_IN_SIGMA);
2132 : 140 : }
2133 [ + + ]: 24087 : else if (r.getKind() == Kind::REGEXP_STAR)
2134 : : {
2135 [ + + ]: 9211 : if (x.isConst())
2136 : : {
2137 : 76 : size_t xlen = Word::getLength(x);
2138 [ + + ]: 76 : if (xlen == 0)
2139 : : {
2140 : : // e.g. (str.in.re "" (re.* (str.to.re x))) ----> true
2141 : 28 : return returnRewrite(node, d_true, Rewrite::RE_EMPTY_IN_STR_STAR);
2142 : : }
2143 [ + + ]: 48 : else if (xlen == 1)
2144 : : {
2145 [ + + ]: 36 : if (r[0].getKind() == Kind::STRING_TO_REGEXP)
2146 : : {
2147 : 16 : Node retNode = r[0][0].eqNode(x);
2148 : : // e.g. (str.in.re "A" (re.* (str.to.re x))) ----> "A" = x
2149 : 8 : return returnRewrite(node, retNode, Rewrite::RE_CHAR_IN_STR_STAR);
2150 : 8 : }
2151 : : }
2152 : : }
2153 [ + + ]: 9135 : else if (x.getKind() == Kind::STRING_CONCAT)
2154 : : {
2155 : : // (str.in.re (str.++ x1 ... xn) (re.* R)) -->
2156 : : // (str.in.re x1 (re.* R)) AND ... AND (str.in.re xn (re.* R))
2157 : : // if the length of all strings in R is one.
2158 : 3644 : Node flr = RegExpEntail::getFixedLengthForRegexp(r[0]);
2159 [ + + ]: 1822 : if (!flr.isNull())
2160 : : {
2161 : 980 : Node one = nm->mkConstInt(Rational(1));
2162 [ + + ]: 980 : if (flr == one)
2163 : : {
2164 : 746 : NodeBuilder nb(nodeManager(), Kind::AND);
2165 [ + + ]: 2899 : for (const Node& xc : x)
2166 : : {
2167 : 2153 : nb << nm->mkNode(Kind::STRING_IN_REGEXP, xc, r);
2168 : 2153 : }
2169 : : return returnRewrite(
2170 : 746 : node, nb.constructNode(), Rewrite::RE_IN_DIST_CHAR_STAR);
2171 : 746 : }
2172 [ + + ]: 980 : }
2173 [ + + ]: 1822 : }
2174 [ + + ]: 8429 : if (r[0].getKind() == Kind::REGEXP_ALLCHAR)
2175 : : {
2176 : 446 : return returnRewrite(node, d_true, Rewrite::RE_IN_SIGMA_STAR);
2177 : : }
2178 [ + + ]: 7983 : else if (r[0].getKind() == Kind::REGEXP_CONCAT)
2179 : : {
2180 : 993 : bool isAllchar = true;
2181 [ + + ]: 1069 : for (const Node& rc : r[0])
2182 : : {
2183 [ + + ]: 1056 : if (rc.getKind() != Kind::REGEXP_ALLCHAR)
2184 : : {
2185 : 980 : isAllchar = false;
2186 : 980 : break;
2187 : : }
2188 [ + + ]: 2049 : }
2189 [ + + ]: 993 : if (isAllchar)
2190 : : {
2191 : : // For example:
2192 : : // (str.in_re x (re.* re.allchar re.allchar)) --->
2193 : : // (= (mod (str.len x) 2) 0)
2194 : 13 : Node zero = nm->mkConstInt(Rational(0));
2195 : 26 : Node factor = nm->mkConstInt(Rational(r[0].getNumChildren()));
2196 : : Node t = nm->mkNode(
2197 : 26 : Kind::INTS_MODULUS, nm->mkNode(Kind::STRING_LENGTH, x), factor);
2198 : 13 : Node retNode = t.eqNode(zero);
2199 : 13 : return returnRewrite(node, retNode, Rewrite::RE_IN_CHAR_MODULUS_STAR);
2200 : 13 : }
2201 : : }
2202 : : }
2203 [ + + ]: 14876 : else if (r.getKind() == Kind::REGEXP_CONCAT)
2204 : : {
2205 : 9123 : bool allSigma = true;
2206 : 9123 : bool allSigmaStrict = true;
2207 : 9123 : unsigned allSigmaMinSize = 0;
2208 : 9123 : Node constStr;
2209 : 9123 : size_t constIdx = 0;
2210 : 9123 : size_t nchildren = r.getNumChildren();
2211 [ + + ]: 17524 : for (size_t i = 0; i < nchildren; i++)
2212 : : {
2213 : 16448 : Node rc = r[i];
2214 [ - + ][ - + ]: 16448 : Assert(rc.getKind() != Kind::REGEXP_NONE);
[ - - ]
2215 [ + + ]: 16448 : if (rc.getKind() == Kind::REGEXP_ALLCHAR)
2216 : : {
2217 : 1181 : allSigmaMinSize++;
2218 : : }
2219 : 45801 : else if (rc.getKind() == Kind::REGEXP_STAR
2220 [ + + ][ + + ]: 15267 : && rc[0].getKind() == Kind::REGEXP_ALLCHAR)
[ + + ][ + + ]
[ - - ]
2221 : : {
2222 : 2694 : allSigmaStrict = false;
2223 : : }
2224 [ + + ]: 12573 : else if (rc.getKind() == Kind::STRING_TO_REGEXP)
2225 : : {
2226 [ + + ]: 5652 : if (constStr.isNull())
2227 : : {
2228 : 4526 : constStr = rc[0];
2229 : 4526 : constIdx = i;
2230 : : }
2231 : : else
2232 : : {
2233 : 1126 : allSigma = false;
2234 : 1126 : break;
2235 : : }
2236 : : }
2237 : : else
2238 : : {
2239 : 6921 : allSigma = false;
2240 : 6921 : break;
2241 : : }
2242 [ + + ]: 16448 : }
2243 [ + + ]: 9123 : if (allSigma)
2244 : : {
2245 [ + + ]: 1076 : if (constStr.isNull())
2246 : : {
2247 : : // x in re.++(_*, _, _) ---> str.len(x) >= 2
2248 : 26 : Node num = nm->mkConstInt(Rational(allSigmaMinSize));
2249 : 26 : Node lenx = nm->mkNode(Kind::STRING_LENGTH, x);
2250 : : Node retNode =
2251 [ + + ]: 52 : nm->mkNode(allSigmaStrict ? Kind::EQUAL : Kind::GEQ, lenx, num);
2252 : 26 : return returnRewrite(node, retNode, Rewrite::RE_CONCAT_PURE_ALLCHAR);
2253 : 26 : }
2254 [ + + ][ + + ]: 1050 : else if (allSigmaMinSize == 0 && nchildren >= 3 && constIdx != 0
[ + - ]
2255 [ + - ]: 148 : && constIdx != nchildren - 1)
2256 : : {
2257 : : // x in re.++(_*, "abc", _*) ---> str.contains(x, "abc")
2258 : 296 : Node retNode = nm->mkNode(Kind::STRING_CONTAINS, x, constStr);
2259 : 148 : return returnRewrite(node, retNode, Rewrite::RE_CONCAT_TO_CONTAINS);
2260 : 148 : }
2261 : : }
2262 [ + + ]: 9123 : }
2263 : 5753 : else if (r.getKind() == Kind::REGEXP_INTER
2264 [ + + ][ + + ]: 5753 : || r.getKind() == Kind::REGEXP_UNION)
[ + + ]
2265 : : {
2266 : 1372 : std::vector<Node> mvec;
2267 [ + + ]: 4275 : for (unsigned i = 0; i < r.getNumChildren(); i++)
2268 : : {
2269 : 2903 : mvec.push_back(nodeManager()->mkNode(Kind::STRING_IN_REGEXP, x, r[i]));
2270 : : }
2271 : : Node retNode = nodeManager()->mkNode(
2272 [ + + ]: 1372 : r.getKind() == Kind::REGEXP_INTER ? Kind::AND : Kind::OR, mvec);
2273 : 1372 : return returnRewrite(node, retNode, Rewrite::RE_IN_ANDOR);
2274 : 1372 : }
2275 [ + + ]: 4381 : else if (r.getKind() == Kind::STRING_TO_REGEXP)
2276 : : {
2277 : 2577 : Node retNode = x.eqNode(r[0]);
2278 : 2577 : return returnRewrite(node, retNode, Rewrite::RE_IN_CSTRING);
2279 : 2577 : }
2280 [ + + ]: 1804 : else if (r.getKind() == Kind::REGEXP_RANGE)
2281 : : {
2282 : : // x in re.range( char_i, char_j ) ---> i <= str.code(x) <= j
2283 : : // we do not do this if the arguments are not constant
2284 [ + - ]: 871 : if (RegExpEntail::isConstRegExp(r))
2285 : : {
2286 : 871 : Node xcode = nm->mkNode(Kind::STRING_TO_CODE, x);
2287 : 2613 : Node retNode = nm->mkNode(
2288 : : Kind::AND,
2289 : 1742 : {nm->mkNode(Kind::LEQ, nm->mkNode(Kind::STRING_TO_CODE, r[0]), xcode),
2290 : 1742 : nm->mkNode(
2291 : 3484 : Kind::LEQ, xcode, nm->mkNode(Kind::STRING_TO_CODE, r[1]))});
2292 : 871 : return returnRewrite(node, retNode, Rewrite::RE_IN_RANGE);
2293 : 871 : }
2294 : : }
2295 [ + + ]: 933 : else if (r.getKind() == Kind::REGEXP_COMPLEMENT)
2296 : : {
2297 : 1734 : Node retNode = nm->mkNode(Kind::STRING_IN_REGEXP, x, r[0]).negate();
2298 : 867 : return returnRewrite(node, retNode, Rewrite::RE_IN_COMPLEMENT);
2299 : 867 : }
2300 : :
2301 : : // do simple consumes
2302 : 16985 : Node retNode = rewriteViaStrInReConsume(node);
2303 [ + + ]: 16985 : if (!retNode.isNull())
2304 : : {
2305 [ + - ]: 2798 : Trace("regexp-ext-rewrite")
2306 : 1399 : << "Regexp : rewrite : " << node << " -> " << retNode << std::endl;
2307 : 1399 : return returnRewrite(node, retNode, Rewrite::RE_SIMPLE_CONSUME);
2308 : : }
2309 : : // check regular expression inclusion
2310 : : // This makes a regular expression that contains all possible model values
2311 : : // for x, and checks whether r includes this regular expression. If so,
2312 : : // the membership rewrites to true.
2313 : 15586 : Node ret = rewriteViaMacroStrInReInclusion(node);
2314 [ + + ]: 15586 : if (!ret.isNull())
2315 : : {
2316 : 134 : return returnRewrite(node, ret, Rewrite::RE_IN_INCLUSION);
2317 : : }
2318 : 15452 : return node;
2319 : 27196 : }
2320 : :
2321 : 1597271 : RewriteResponse SequencesRewriter::postRewrite(TNode node)
2322 : : {
2323 [ + - ]: 3194542 : Trace("sequences-postrewrite")
2324 : 1597271 : << "Strings::SequencesRewriter::postRewrite start " << node << std::endl;
2325 : 1597271 : Node retNode = node;
2326 : 1597271 : Kind nk = node.getKind();
2327 [ + + ]: 1597271 : if (nk == Kind::STRING_CONCAT)
2328 : : {
2329 : 253257 : retNode = rewriteConcat(node);
2330 : : }
2331 [ + + ]: 1344014 : else if (nk == Kind::EQUAL)
2332 : : {
2333 : 627020 : retNode = rewriteEquality(node);
2334 : : }
2335 [ + + ]: 716994 : else if (nk == Kind::STRING_LENGTH)
2336 : : {
2337 : 198772 : retNode = rewriteLength(node);
2338 : : }
2339 [ + + ]: 518222 : else if (nk == Kind::STRING_CHARAT)
2340 : : {
2341 : 401 : retNode = rewriteCharAt(node);
2342 : : }
2343 [ + + ]: 517821 : else if (nk == Kind::STRING_SUBSTR)
2344 : : {
2345 : 128632 : retNode = rewriteSubstr(node);
2346 : : }
2347 [ + + ]: 389189 : else if (nk == Kind::STRING_UPDATE)
2348 : : {
2349 : 2556 : retNode = rewriteUpdate(node);
2350 : : }
2351 [ + + ]: 386633 : else if (nk == Kind::STRING_CONTAINS)
2352 : : {
2353 : 131350 : retNode = rewriteContains(node);
2354 : : }
2355 [ + + ]: 255283 : else if (nk == Kind::STRING_INDEXOF)
2356 : : {
2357 : 13868 : retNode = rewriteIndexof(node);
2358 : : }
2359 [ + + ]: 241415 : else if (nk == Kind::STRING_INDEXOF_RE)
2360 : : {
2361 : 1610 : retNode = rewriteIndexofRe(node);
2362 : : }
2363 [ + + ]: 239805 : else if (nk == Kind::STRING_REPLACE)
2364 : : {
2365 : 17910 : retNode = rewriteReplace(node);
2366 : : }
2367 [ + + ]: 221895 : else if (nk == Kind::STRING_REPLACE_ALL)
2368 : : {
2369 : 3389 : retNode = rewriteReplaceAll(node);
2370 : : }
2371 [ + + ]: 218506 : else if (nk == Kind::STRING_REPLACE_RE)
2372 : : {
2373 : 785 : retNode = rewriteReplaceRe(node);
2374 : : }
2375 [ + + ]: 217721 : else if (nk == Kind::STRING_REPLACE_RE_ALL)
2376 : : {
2377 : 766 : retNode = rewriteReplaceReAll(node);
2378 : : }
2379 [ + + ]: 216955 : else if (nk == Kind::STRING_REV)
2380 : : {
2381 : 647 : retNode = rewriteStrReverse(node);
2382 : : }
2383 [ + + ][ + + ]: 216308 : else if (nk == Kind::STRING_PREFIX || nk == Kind::STRING_SUFFIX)
2384 : : {
2385 : 998 : retNode = rewritePrefixSuffix(node);
2386 : : }
2387 [ + + ]: 215310 : else if (nk == Kind::STRING_IN_REGEXP)
2388 : : {
2389 : 27196 : retNode = rewriteMembership(node);
2390 : : }
2391 [ + + ]: 188114 : else if (nk == Kind::REGEXP_ALL)
2392 : : {
2393 : 116 : retNode = rewriteAllRegExp(node);
2394 : : }
2395 [ + + ]: 187998 : else if (nk == Kind::REGEXP_CONCAT)
2396 : : {
2397 : 8981 : retNode = rewriteConcatRegExp(node);
2398 : : }
2399 [ + + ][ + + ]: 179017 : else if (nk == Kind::REGEXP_UNION || nk == Kind::REGEXP_INTER)
2400 : : {
2401 : 4515 : retNode = rewriteAndOrRegExp(node);
2402 : : }
2403 [ + + ]: 174502 : else if (nk == Kind::REGEXP_DIFF)
2404 : : {
2405 : 479 : retNode = rewriteDifferenceRegExp(node);
2406 : : }
2407 [ + + ]: 174023 : else if (nk == Kind::REGEXP_STAR)
2408 : : {
2409 : 4827 : retNode = rewriteStarRegExp(node);
2410 : : }
2411 [ + + ]: 169196 : else if (nk == Kind::REGEXP_PLUS)
2412 : : {
2413 : 239 : retNode = rewritePlusRegExp(node);
2414 : : }
2415 [ + + ]: 168957 : else if (nk == Kind::REGEXP_OPT)
2416 : : {
2417 : 114 : retNode = rewriteOptionRegExp(node);
2418 : : }
2419 [ + + ]: 168843 : else if (nk == Kind::REGEXP_RANGE)
2420 : : {
2421 : 1340 : retNode = rewriteRangeRegExp(node);
2422 : : }
2423 [ + + ]: 167503 : else if (nk == Kind::REGEXP_LOOP)
2424 : : {
2425 : 155 : retNode = rewriteLoopRegExp(node);
2426 : : }
2427 [ + + ]: 167348 : else if (nk == Kind::REGEXP_REPEAT)
2428 : : {
2429 : 28 : retNode = rewriteRepeatRegExp(node);
2430 : : }
2431 [ + + ]: 167320 : else if (nk == Kind::SEQ_UNIT)
2432 : : {
2433 : 3693 : retNode = rewriteSeqUnit(node);
2434 : : }
2435 [ + + ]: 163627 : else if (nk == Kind::SEQ_NTH)
2436 : : {
2437 : 9429 : retNode = rewriteSeqNth(node);
2438 : : }
2439 : :
2440 [ + - ]: 3194542 : Trace("sequences-postrewrite")
2441 : 0 : << "Strings::SequencesRewriter::postRewrite returning " << retNode
2442 : 1597271 : << std::endl;
2443 [ + + ]: 1597271 : if (node != retNode)
2444 : : {
2445 [ + - ]: 615094 : Trace("strings-rewrite-debug") << "Strings::SequencesRewriter::postRewrite "
2446 : 307547 : << node << " to " << retNode << std::endl;
2447 : 307547 : return RewriteResponse(REWRITE_AGAIN_FULL, retNode);
2448 : : }
2449 [ + - ]: 1289724 : Trace("strings-rewrite-nf") << "No rewrites for : " << node << std::endl;
2450 : 1289724 : return RewriteResponse(REWRITE_DONE, retNode);
2451 : 1597271 : }
2452 : :
2453 : 1560690 : RewriteResponse SequencesRewriter::preRewrite(TNode node)
2454 : : {
2455 : 1560690 : return RewriteResponse(REWRITE_DONE, node);
2456 : : }
2457 : :
2458 : 9429 : Node SequencesRewriter::rewriteSeqNth(Node node)
2459 : : {
2460 [ - + ][ - + ]: 9429 : Assert(node.getKind() == Kind::SEQ_NTH);
[ - - ]
2461 : 9429 : Node s = node[0];
2462 : 9429 : Node i = node[1];
2463 [ + + ][ + + ]: 9429 : if (s.isConst() && i.isConst())
[ + + ]
2464 : : {
2465 : 452 : size_t len = Word::getLength(s);
2466 [ + + ]: 452 : if (i.getConst<Rational>().sgn() != -1)
2467 : : {
2468 : 412 : Integer posInt = i.getConst<Rational>().getNumerator();
2469 [ + + ][ + + ]: 412 : if (posInt.fitsUnsignedInt() && posInt < Integer(len))
[ + + ][ + + ]
[ - - ]
2470 : : {
2471 : 259 : size_t pos = posInt.toUnsignedInt();
2472 : 259 : Node ret = Word::getNth(s, pos);
2473 : 259 : return returnRewrite(node, ret, Rewrite::SEQ_NTH_EVAL);
2474 : 259 : }
2475 [ + + ]: 412 : }
2476 : : }
2477 : :
2478 : 9170 : std::vector<Node> prefix, suffix;
2479 : 9170 : utils::getConcat(s, suffix);
2480 [ + + ]: 12374 : if ((i.isConst() && i.getConst<Rational>().isZero())
2481 [ + + ][ + + ]: 12374 : || d_stringsEntail.stripSymbolicLength(suffix, prefix, 1, i, true))
[ + + ]
2482 : : {
2483 [ + + ]: 1713 : if (suffix.size() > 0)
2484 : : {
2485 [ + + ]: 1677 : if (suffix[0].getKind() == Kind::SEQ_UNIT)
2486 : : {
2487 : : // (seq.nth (seq.++ prefix (seq.unit x) suffix) n) ---> x
2488 : : // if len(prefix) = n
2489 : 341 : Node ret = suffix[0][0];
2490 : 341 : return returnRewrite(node, ret, Rewrite::SEQ_NTH_EVAL_SYM);
2491 : 341 : }
2492 : : // TODO: STRING_UNIT?
2493 : : }
2494 : : }
2495 : :
2496 : 8829 : return node;
2497 : 9429 : }
2498 : :
2499 : 401 : Node SequencesRewriter::rewriteCharAt(Node node)
2500 : : {
2501 [ - + ][ - + ]: 401 : Assert(node.getKind() == Kind::STRING_CHARAT);
[ - - ]
2502 : 401 : NodeManager* nm = nodeManager();
2503 : 401 : Node one = nm->mkConstInt(Rational(1));
2504 : 802 : Node retNode = nm->mkNode(Kind::STRING_SUBSTR, node[0], node[1], one);
2505 : 802 : return returnRewrite(node, retNode, Rewrite::CHARAT_ELIM);
2506 : 401 : }
2507 : :
2508 : 128635 : Node SequencesRewriter::rewriteSubstr(Node node)
2509 : : {
2510 [ - + ][ - + ]: 128635 : Assert(node.getKind() == Kind::STRING_SUBSTR);
[ - - ]
2511 : :
2512 : 128635 : NodeManager* nm = nodeManager();
2513 [ + + ]: 128635 : if (node[0].isConst())
2514 : : {
2515 [ + + ]: 30965 : if (Word::isEmpty(node[0]))
2516 : : {
2517 : 2594 : Node ret = node[0];
2518 : 2594 : return returnRewrite(node, ret, Rewrite::SS_EMPTYSTR);
2519 : 2594 : }
2520 : : // rewriting for constant arguments
2521 : 28371 : if (node[1].isConst() && node[2].isConst())
2522 : : {
2523 : 10792 : Node s = node[0];
2524 : 10792 : cvc5::internal::Rational rMaxInt(String::maxSize());
2525 : : uint32_t start;
2526 [ + + ]: 10792 : if (node[1].getConst<Rational>() > rMaxInt)
2527 : : {
2528 : : // start beyond the maximum size of strings
2529 : : // thus, it must be beyond the end point of this string
2530 : 10 : Node ret = Word::mkEmptyWord(node.getType());
2531 : 10 : return returnRewrite(node, ret, Rewrite::SS_CONST_START_MAX_OOB);
2532 : 10 : }
2533 [ + + ]: 10782 : else if (node[1].getConst<Rational>().sgn() < 0)
2534 : : {
2535 : : // start before the beginning of the string
2536 : 930 : Node ret = Word::mkEmptyWord(node.getType());
2537 : 930 : return returnRewrite(node, ret, Rewrite::SS_CONST_START_NEG);
2538 : 930 : }
2539 : : else
2540 : : {
2541 : 9852 : start = node[1].getConst<Rational>().getNumerator().toUnsignedInt();
2542 [ + + ]: 9852 : if (start >= Word::getLength(node[0]))
2543 : : {
2544 : : // start beyond the end of the string
2545 : 511 : Node ret = Word::mkEmptyWord(node.getType());
2546 : 511 : return returnRewrite(node, ret, Rewrite::SS_CONST_START_OOB);
2547 : 511 : }
2548 : : }
2549 : 18682 : Rational endPt(node[1].getConst<Rational>()
2550 : 18682 : + node[2].getConst<Rational>());
2551 [ + + ]: 9341 : if (endPt > rMaxInt)
2552 : : {
2553 : : // take up to the end of the string
2554 : 2 : size_t lenS = Word::getLength(s);
2555 : 2 : Node ret = Word::suffix(s, lenS - start);
2556 : 2 : return returnRewrite(node, ret, Rewrite::SS_CONST_LEN_MAX_OOB);
2557 : 2 : }
2558 [ + + ]: 9339 : else if (node[2].getConst<Rational>().sgn() <= 0)
2559 : : {
2560 : 860 : Node ret = Word::mkEmptyWord(node.getType());
2561 : 860 : return returnRewrite(node, ret, Rewrite::SS_CONST_LEN_NON_POS);
2562 : 860 : }
2563 : : else
2564 : : {
2565 : : uint32_t len =
2566 : 8479 : node[2].getConst<Rational>().getNumerator().toUnsignedInt();
2567 : : // should not overflow due to checks above
2568 [ + + ][ + - ]: 8479 : Assert(start == 0 || start + len > len);
[ - + ][ - + ]
[ - - ]
2569 [ + + ]: 8479 : if (start + len > Word::getLength(node[0]))
2570 : : {
2571 : : // take up to the end of the string
2572 : 604 : size_t lenS = Word::getLength(s);
2573 : 604 : Node ret = Word::suffix(s, lenS - start);
2574 : 604 : return returnRewrite(node, ret, Rewrite::SS_CONST_END_OOB);
2575 : 604 : }
2576 : : else
2577 : : {
2578 : : // compute the substr using the constant string
2579 : 7875 : Node ret = Word::substr(s, start, len);
2580 : 7875 : return returnRewrite(node, ret, Rewrite::SS_CONST_SS);
2581 : 7875 : }
2582 : : }
2583 : 10792 : }
2584 : : }
2585 : 115249 : Node zero = nm->mkConstInt(cvc5::internal::Rational(0));
2586 : :
2587 : : // if entailed non-positive length or negative start point
2588 [ + + ]: 115249 : if (d_arithEntail.check(zero, node[1], true))
2589 : : {
2590 : 163 : Node ret = Word::mkEmptyWord(node.getType());
2591 : 163 : return returnRewrite(node, ret, Rewrite::SS_START_NEG);
2592 : 163 : }
2593 [ + + ]: 115086 : else if (d_arithEntail.check(zero, node[2]))
2594 : : {
2595 : 2928 : Node ret = Word::mkEmptyWord(node.getType());
2596 : 2928 : return returnRewrite(node, ret, Rewrite::SS_LEN_NON_POS);
2597 : 2928 : }
2598 : :
2599 [ + + ]: 112158 : if (node[0].getKind() == Kind::STRING_SUBSTR)
2600 : : {
2601 : : // (str.substr (str.substr x a b) c d) ---> "" if c >= b
2602 : : //
2603 : : // Note that this rewrite can be generalized to:
2604 : : //
2605 : : // (str.substr x a b) ---> "" if a >= (str.len x)
2606 : : //
2607 : : // This can be done when we generalize our entailment methods to
2608 : : // accept an optional context. Then we could conjecture that
2609 : : // (str.substr x a b) rewrites to "" and do a case analysis:
2610 : : //
2611 : : // - a < 0 or b < 0 (the result is trivially empty in these cases)
2612 : : // - a >= (str.len x) assuming that { a >= 0, b >= 0 }
2613 : : //
2614 : : // For example, for (str.substr (str.substr x a a) a a), we could
2615 : : // then deduce that under those assumptions, "a" is an
2616 : : // over-approximation of the length of (str.substr x a a), which
2617 : : // then allows us to reason that the result of the whole term must
2618 : : // be empty.
2619 [ + + ]: 11557 : if (d_arithEntail.check(node[1], node[0][2]))
2620 : : {
2621 : 68 : Node ret = Word::mkEmptyWord(node.getType());
2622 : 68 : return returnRewrite(node, ret, Rewrite::SS_START_GEQ_LEN);
2623 : 68 : }
2624 : : }
2625 [ + + ]: 100601 : else if (node[0].getKind() == Kind::STRING_REPLACE)
2626 : : {
2627 : : // (str.substr (str.replace x y z) 0 n)
2628 : : // ---> (str.replace (str.substr x 0 n) y z)
2629 : : // if (str.len y) = 1 and (str.len z) = 1
2630 [ + + ]: 3698 : if (node[1] == zero)
2631 : : {
2632 : 3180 : if (d_stringsEntail.checkLengthOne(node[0][1], true)
2633 : 3180 : && d_stringsEntail.checkLengthOne(node[0][2], true))
2634 : : {
2635 : : Node ret = nm->mkNode(
2636 : : Kind::STRING_REPLACE,
2637 : 122 : nm->mkNode(Kind::STRING_SUBSTR, node[0][0], node[1], node[2]),
2638 : : node[0][1],
2639 : 244 : node[0][2]);
2640 : 61 : return returnRewrite(node, ret, Rewrite::SUBSTR_REPL_SWAP);
2641 : 61 : }
2642 : : }
2643 : : }
2644 : :
2645 : 112029 : TypeNode stype = node.getType();
2646 : :
2647 : : // (str.substr s x x) ---> "" if (str.len s) <= 1
2648 : 112029 : if (node[1] == node[2] && d_stringsEntail.checkLengthOne(node[0]))
2649 : : {
2650 : 6 : Node ret = Word::mkEmptyWord(node.getType());
2651 : 6 : return returnRewrite(node, ret, Rewrite::SS_LEN_ONE_Z_Z);
2652 : 6 : }
2653 : :
2654 : 224046 : Node slenRew = nm->mkNode(Kind::STRING_LENGTH, node[0]);
2655 : : // make strict to avoid infinite loops
2656 [ + + ]: 112023 : if (d_arithEntail.check(node[2], slenRew, true))
2657 : : {
2658 : : // end point beyond end point of string, map to slenRew
2659 : 460 : Node ret = nm->mkNode(Kind::STRING_SUBSTR, node[0], node[1], slenRew);
2660 : 230 : return returnRewrite(node, ret, Rewrite::SS_END_PT_NORM);
2661 : 230 : }
2662 : :
2663 : : // Rewrite based on symbolic length analysis, using the strings entailment
2664 : : // utility that is owned by this rewriter. This handles three rewrite rules
2665 : : // that are also included as part of the macro proof rewrite rule
2666 : : // MACRO_SUBSTR_STRIP_SYM_LENGTH.
2667 : : Rewrite ruleSymLen;
2668 : : Node retSymLen =
2669 : 111793 : rewriteViaMacroSubstrStripSymLength(node, ruleSymLen, d_stringsEntail);
2670 [ + + ]: 111793 : if (!retSymLen.isNull())
2671 : : {
2672 : 4727 : return returnRewrite(node, retSymLen, ruleSymLen);
2673 : : }
2674 : : // combine substr
2675 [ + + ]: 107066 : if (node[0].getKind() == Kind::STRING_SUBSTR)
2676 : : {
2677 : 11167 : Node start_inner = node[0][1];
2678 : 11167 : Node start_outer = node[1];
2679 : 11167 : if (d_arithEntail.check(start_outer) && d_arithEntail.check(start_inner))
2680 : : {
2681 : : // both are positive
2682 : : // thus, start point is definitely start_inner+start_outer.
2683 : : // We can rewrite if it for certain what the length is
2684 : :
2685 : : // the length of a string from the inner substr subtracts the start point
2686 : : // of the outer substr
2687 : 15614 : Node len_from_inner = nm->mkNode(Kind::SUB, node[0][2], start_outer);
2688 : 7807 : Node len_from_outer = node[2];
2689 : 7807 : Node new_len;
2690 : 7807 : Rewrite rule = Rewrite::NONE;
2691 : : // take quantity that is for sure smaller than the other
2692 [ - + ]: 7807 : if (len_from_inner == len_from_outer)
2693 : : {
2694 : 0 : new_len = len_from_inner;
2695 : 0 : rule = Rewrite::SS_COMBINE_EQ;
2696 : : }
2697 [ + + ]: 7807 : else if (d_arithEntail.check(len_from_inner, len_from_outer))
2698 : : {
2699 : 590 : new_len = len_from_outer;
2700 : 590 : rule = Rewrite::SS_COMBINE_GEQ_INNER;
2701 : : }
2702 [ + + ]: 7217 : else if (d_arithEntail.check(len_from_outer, len_from_inner))
2703 : : {
2704 : 283 : new_len = len_from_inner;
2705 : 283 : rule = Rewrite::SS_COMBINE_GEQ_OUTER;
2706 : : }
2707 [ + + ]: 7807 : if (!new_len.isNull())
2708 : : {
2709 : 1746 : Node new_start = nm->mkNode(Kind::ADD, start_inner, start_outer);
2710 : : Node ret =
2711 : 1746 : nm->mkNode(Kind::STRING_SUBSTR, node[0][0], new_start, new_len);
2712 : 873 : return returnRewrite(node, ret, rule);
2713 : 873 : }
2714 [ + + ][ + + ]: 9553 : }
[ + + ]
2715 [ + + ][ + + ]: 12040 : }
2716 : 106193 : return node;
2717 : 115249 : }
2718 : :
2719 : 2556 : Node SequencesRewriter::rewriteUpdate(Node node)
2720 : : {
2721 [ - + ][ - + ]: 2556 : Assert(node.getKind() == Kind::STRING_UPDATE);
[ - - ]
2722 : 2556 : Node s = node[0];
2723 : 2556 : Node i = node[1];
2724 : 2556 : Node x = node[2];
2725 [ + + ]: 2556 : if (s.isConst())
2726 : : {
2727 [ + + ]: 383 : if (Word::isEmpty(s))
2728 : : {
2729 : 14 : return returnRewrite(node, s, Rewrite::UPD_EMPTYSTR);
2730 : : }
2731 : : // rewriting for constant arguments
2732 [ + + ]: 369 : if (node[1].isConst())
2733 : : {
2734 : 325 : cvc5::internal::Rational rMaxInt(String::maxSize());
2735 [ - + ]: 325 : if (node[1].getConst<Rational>() > rMaxInt)
2736 : : {
2737 : : // start beyond the maximum size of strings
2738 : : // thus, it must be beyond the end point of this string
2739 : 0 : return returnRewrite(node, s, Rewrite::UPD_CONST_INDEX_MAX_OOB);
2740 : : }
2741 [ + + ]: 325 : else if (node[1].getConst<Rational>().sgn() < 0)
2742 : : {
2743 : : // start before the beginning of the string
2744 : 16 : return returnRewrite(node, s, Rewrite::UPD_CONST_INDEX_NEG);
2745 : : }
2746 : : uint32_t start =
2747 : 309 : node[1].getConst<Rational>().getNumerator().toUnsignedInt();
2748 : 309 : size_t len = Word::getLength(s);
2749 [ + + ]: 309 : if (start >= len)
2750 : : {
2751 : : // start beyond the end of the string
2752 : 34 : return returnRewrite(node, s, Rewrite::UPD_CONST_INDEX_OOB);
2753 : : }
2754 [ + + ]: 275 : if (node[2].isConst())
2755 : : {
2756 : 394 : Node ret = Word::update(s, start, node[2]);
2757 : 197 : return returnRewrite(node, ret, Rewrite::UPD_EVAL);
2758 : 197 : }
2759 [ + + ]: 325 : }
2760 : : }
2761 : :
2762 : 2295 : NodeManager* nm = nodeManager();
2763 : 2295 : Node zero = nm->mkConstInt(0);
2764 : 2295 : Node sLen = nm->mkNode(Kind::STRING_LENGTH, s);
2765 : 2295 : if (d_arithEntail.check(zero, i, true) || d_arithEntail.check(i, sLen))
2766 : : {
2767 : : // (seq.update s i x) ---> s if x < 0 or x >= len(s)
2768 : 22 : Node ret = s;
2769 : 22 : return returnRewrite(node, ret, Rewrite::UPD_OOB);
2770 : 22 : }
2771 : :
2772 : 2273 : std::vector<Node> prefix, suffix;
2773 : 2273 : utils::getConcat(s, suffix);
2774 [ + + ]: 4052 : if ((i.isConst() && i.getConst<Rational>().isZero())
2775 [ + + ][ + + ]: 4052 : || d_stringsEntail.stripSymbolicLength(suffix, prefix, 1, i, true))
[ + + ]
2776 : : {
2777 : 1319 : Node updateLen = nm->mkNode(Kind::STRING_LENGTH, x);
2778 : 1319 : std::vector<Node> replaced;
2779 [ + + ]: 1319 : if (d_stringsEntail.stripSymbolicLength(
2780 : : suffix, replaced, 1, updateLen, true))
2781 : : {
2782 : : // (seq.update (seq.++ p r s) i x) ---> (seq.++ p x s)
2783 : : // if len(p) = i and len(r) = len(x)
2784 : 63 : prefix.emplace_back(x);
2785 : 63 : prefix.insert(prefix.end(), suffix.begin(), suffix.end());
2786 : 63 : Node ret = utils::mkConcat(prefix, node.getType());
2787 : 63 : return returnRewrite(node, ret, Rewrite::UPD_EVAL_SYM);
2788 : 63 : }
2789 [ + + ][ + + ]: 1382 : }
2790 : :
2791 [ + + ][ - + ]: 2210 : if (s.getKind() == Kind::STRING_REV && d_stringsEntail.checkLengthOne(x))
[ + + ][ - + ]
[ - - ]
2792 : : {
2793 : : // str.update(str.rev(s), n, t) --->
2794 : : // str.rev(str.update(s, len(s) - (n + 1), t))
2795 : : Node idx =
2796 : 0 : nm->mkNode(Kind::SUB,
2797 : 0 : {nm->mkNode(Kind::STRING_LENGTH, s),
2798 : 0 : nm->mkNode(Kind::ADD, i, nm->mkConstInt(Rational(1)))});
2799 : : Node ret = nm->mkNode(Kind::STRING_REV,
2800 : 0 : nm->mkNode(Kind::STRING_UPDATE, s[0], idx, x));
2801 : 0 : return returnRewrite(node, ret, Rewrite::UPD_REV);
2802 : 0 : }
2803 : :
2804 : 2210 : return node;
2805 : 2556 : }
2806 : :
2807 : 305512 : Node SequencesRewriter::rewriteContains(Node node)
2808 : : {
2809 [ - + ][ - + ]: 305512 : Assert(node.getKind() == Kind::STRING_CONTAINS);
[ - - ]
2810 : 305512 : NodeManager* nm = nodeManager();
2811 : :
2812 [ + + ]: 305512 : if (node[0] == node[1])
2813 : : {
2814 : 6726 : return returnRewrite(node, d_true, Rewrite::CTN_EQ);
2815 : : }
2816 [ + + ]: 298786 : if (node[0].isConst())
2817 : : {
2818 [ + + ]: 122617 : if (node[1].isConst())
2819 : : {
2820 : 10493 : Node ret = nm->mkConst(Word::find(node[0], node[1]) != std::string::npos);
2821 : 10493 : return returnRewrite(node, ret, Rewrite::CTN_CONST);
2822 : 10493 : }
2823 : : else
2824 : : {
2825 : 112124 : Node t = node[1];
2826 [ + + ]: 112124 : if (Word::isEmpty(node[0]))
2827 : : {
2828 : 106422 : Node len1 = nodeManager()->mkNode(Kind::STRING_LENGTH, node[1]);
2829 [ + + ]: 53211 : if (d_arithEntail.check(len1, true))
2830 : : {
2831 : : // we handle the false case here since the rewrite for equality
2832 : : // uses this function, hence we want to conclude false if possible.
2833 : : // len(x)>0 => contains( "", x ) ---> false
2834 : 1878 : Node ret = nodeManager()->mkConst(false);
2835 : 1878 : return returnRewrite(node, ret, Rewrite::CTN_LHS_EMPTYSTR);
2836 : 1878 : }
2837 [ + + ]: 53211 : }
2838 [ + + ]: 58913 : else if (d_stringsEntail.checkLengthOne(t))
2839 : : {
2840 : 31080 : std::vector<Node> vec = Word::getChars(node[0]);
2841 : 15540 : Node emp = Word::mkEmptyWord(t.getType());
2842 : 15540 : NodeBuilder nb(nodeManager(), Kind::OR);
2843 : 15540 : nb << emp.eqNode(t);
2844 [ + + ]: 33371 : for (const Node& c : vec)
2845 : : {
2846 [ - + ][ - + ]: 53493 : AssertEqual(c.getType(), t.getType());
[ - - ]
2847 : 17831 : nb << c.eqNode(t);
2848 : : }
2849 : :
2850 : : // str.contains("ABCabc", t) --->
2851 : : // t = "" v t = "A" v t = "B" v t = "C" v t = "a" v t = "b" v t = "c"
2852 : : // if len(t) <= 1
2853 : 15540 : Node ret = nb;
2854 : 15540 : return returnRewrite(node, ret, Rewrite::CTN_SPLIT);
2855 : 15540 : }
2856 : : else
2857 : : {
2858 : : Node ret =
2859 : 43373 : rewriteViaRule(ProofRewriteRule::MACRO_STR_CONST_NCTN_CONCAT, node);
2860 [ + + ]: 43373 : if (!ret.isNull())
2861 : : {
2862 : 2626 : return returnRewrite(node, ret, Rewrite::CTN_NCONST_CTN_CONCAT);
2863 : : }
2864 [ + + ]: 43373 : }
2865 [ + + ]: 112124 : }
2866 : : }
2867 : 268249 : Node maybeRew;
2868 : 268249 : Rewrite maybeRule = Rewrite::NONE;
2869 [ + + ]: 268249 : if (node[1].isConst())
2870 : : {
2871 : 121401 : size_t len = Word::getLength(node[1]);
2872 [ + + ]: 121401 : if (len == 0)
2873 : : {
2874 : : // contains( x, "" ) ---> true
2875 : 50719 : Node ret = nodeManager()->mkConst(true);
2876 : 50719 : return returnRewrite(node, ret, Rewrite::CTN_RHS_EMPTYSTR);
2877 : 50719 : }
2878 [ + + ]: 70682 : else if (len == 1)
2879 : : {
2880 : : // The following rewrites are specific to a single character second
2881 : : // argument of contains, where we can reason that this character is
2882 : : // not split over multiple components in the first argument.
2883 [ + + ]: 51757 : if (node[0].getKind() == Kind::STRING_CONCAT)
2884 : : {
2885 : 9973 : std::vector<Node> nc1;
2886 : 9973 : utils::getConcat(node[0], nc1);
2887 : 9973 : NodeBuilder nb(nodeManager(), Kind::OR);
2888 [ + + ]: 42819 : for (const Node& ncc : nc1)
2889 : : {
2890 : 32846 : nb << nm->mkNode(Kind::STRING_CONTAINS, ncc, node[1]);
2891 : : }
2892 : 9973 : Node ret = nb.constructNode();
2893 : : // str.contains( x ++ y, "A" ) --->
2894 : : // str.contains( x, "A" ) OR str.contains( y, "A" )
2895 : : // Remember the rewrite, we might find a better rule in following.
2896 : 9973 : maybeRew = ret;
2897 : 9973 : maybeRule = Rewrite::CTN_CONCAT_CHAR;
2898 : 9973 : }
2899 [ + + ]: 41784 : else if (node[0].getKind() == Kind::STRING_REPLACE)
2900 : : {
2901 : 14148 : Node rplDomain = d_stringsEntail.checkContains(node[0][1], node[1]);
2902 [ + + ][ + + ]: 7074 : if (!rplDomain.isNull() && !rplDomain.getConst<bool>())
[ + + ]
2903 : : {
2904 : 556 : Node d1 = nm->mkNode(Kind::STRING_CONTAINS, node[0][0], node[1]);
2905 : 834 : Node d2 = nm->mkNode(
2906 : : Kind::AND,
2907 : 556 : {nm->mkNode(Kind::STRING_CONTAINS, node[0][0], node[0][1]),
2908 : 556 : nm->mkNode(Kind::STRING_CONTAINS, node[0][2], node[1])});
2909 : 556 : Node ret = nm->mkNode(Kind::OR, d1, d2);
2910 : : // If str.contains( y, "A" ) ---> false, then:
2911 : : // str.contains( str.replace( x, y, z ), "A" ) --->
2912 : : // str.contains( x, "A" ) OR
2913 : : // ( str.contains( x, y ) AND str.contains( z, "A" ) )
2914 : 278 : return returnRewrite(node, ret, Rewrite::CTN_REPL_CHAR);
2915 : 278 : }
2916 [ + + ]: 7074 : }
2917 : : }
2918 : : }
2919 : 217252 : std::vector<Node> nc1;
2920 : 217252 : utils::getConcat(node[0], nc1);
2921 : 217252 : std::vector<Node> nc2;
2922 : 217252 : utils::getConcat(node[1], nc2);
2923 : :
2924 : : // component-wise containment
2925 : 217252 : Node cret = rewriteViaRule(ProofRewriteRule::MACRO_STR_COMPONENT_CTN, node);
2926 [ + + ]: 217252 : if (!cret.isNull())
2927 : : {
2928 : 17779 : return returnRewrite(node, cret, Rewrite::CTN_COMPONENT);
2929 : : }
2930 : 199473 : TypeNode stype = node[0].getType();
2931 : :
2932 : : // (str.contains (str.++ ... s ...) (str.substr s n m)) ---> true
2933 [ + + ]: 199473 : if (node[1].getKind() == Kind::STRING_SUBSTR)
2934 : : {
2935 [ + + ]: 64273 : if (std::find(nc1.begin(), nc1.end(), node[1][0]) != nc1.end())
2936 : : {
2937 : 2712 : Node res = nm->mkConst(true);
2938 : 2712 : return returnRewrite(node, res, Rewrite::CTN_CONCAT_CTN_SUBSTR);
2939 : 2712 : }
2940 : : }
2941 : :
2942 : : // strip endpoints
2943 : : Node retStr =
2944 : 196761 : rewriteViaRule(ProofRewriteRule::MACRO_STR_STRIP_ENDPOINTS, node);
2945 [ + + ]: 196761 : if (!retStr.isNull())
2946 : : {
2947 : 3565 : return returnRewrite(node, retStr, Rewrite::CTN_STRIP_ENDPT);
2948 : : }
2949 : :
2950 [ + + ]: 412966 : for (const Node& n : nc2)
2951 : : {
2952 [ + + ]: 220315 : if (nc2.size() > 1)
2953 : : {
2954 : 82628 : Node ctnConst = d_stringsEntail.checkContains(node[0], n);
2955 [ + + ][ + + ]: 41314 : if (!ctnConst.isNull() && !ctnConst.getConst<bool>())
[ + + ]
2956 : : {
2957 : 105 : Node res = nm->mkConst(false);
2958 : 105 : return returnRewrite(node, res, Rewrite::CTN_CONCAT_COM_NON_CTN);
2959 : 105 : }
2960 [ + + ]: 41314 : }
2961 [ + + ]: 220210 : if (n.getKind() == Kind::STRING_REPLACE)
2962 : : {
2963 : : // (str.contains x (str.replace y z w)) --> false
2964 : : // if (str.contains x y) = false and (str.contains x w) = false
2965 : : //
2966 : : // Reasoning: (str.contains x y) checks that x does not contain y if the
2967 : : // replacement does not change y. (str.contains x w) checks that if the
2968 : : // replacement changes anything in y, the w makes it impossible for it to
2969 : : // occur in x.
2970 : 36162 : Node ctnConst = d_stringsEntail.checkContains(node[0], n[0]);
2971 [ + + ][ + + ]: 18081 : if (!ctnConst.isNull() && !ctnConst.getConst<bool>())
[ + + ]
2972 : : {
2973 : 11764 : Node ctnConst2 = d_stringsEntail.checkContains(node[0], n[2]);
2974 [ + + ][ + + ]: 5882 : if (!ctnConst2.isNull() && !ctnConst2.getConst<bool>())
[ + + ]
2975 : : {
2976 : 440 : Node res = nm->mkConst(false);
2977 : 440 : return returnRewrite(node, res, Rewrite::CTN_RPL_NON_CTN);
2978 : 440 : }
2979 [ + + ]: 5882 : }
2980 [ + + ]: 18081 : }
2981 : : }
2982 : :
2983 : : // length entailment
2984 : 385302 : Node len_n1 = nodeManager()->mkNode(Kind::STRING_LENGTH, node[0]);
2985 : 385302 : Node len_n2 = nodeManager()->mkNode(Kind::STRING_LENGTH, node[1]);
2986 [ + + ]: 192651 : if (d_arithEntail.check(len_n2, len_n1, true))
2987 : : {
2988 : : // len( n2 ) > len( n1 ) => contains( n1, n2 ) ---> false
2989 : 1021 : Node ret = nodeManager()->mkConst(false);
2990 : 1021 : return returnRewrite(node, ret, Rewrite::CTN_LEN_INEQ);
2991 : 1021 : }
2992 : :
2993 : : // multi-set reasoning
2994 : : // For example, contains( str.++( x, "b" ), str.++( "a", x ) ) ---> false
2995 : : // since the number of a's in the second argument is greater than the number
2996 : : // of a's in the first argument
2997 [ + + ]: 191630 : if (d_stringsEntail.checkMultisetSubset(node[0], node[1]))
2998 : : {
2999 : 104 : Node ret = nm->mkConst(false);
3000 : 104 : return returnRewrite(node, ret, Rewrite::CTN_MSET_NSS);
3001 : 104 : }
3002 : :
3003 [ + + ]: 191526 : if (d_arithEntail.check(len_n2, len_n1, false))
3004 : : {
3005 : : // len( n2 ) >= len( n1 ) => contains( n1, n2 ) ---> n1 = n2
3006 : 137534 : Node ret = node[0].eqNode(node[1]);
3007 : 68767 : return returnRewrite(node, ret, Rewrite::CTN_LEN_INEQ_NSTRICT);
3008 : 68767 : }
3009 : :
3010 : : // splitting
3011 [ + + ]: 122759 : if (node[0].getKind() == Kind::STRING_CONCAT)
3012 : : {
3013 : : // e.g. (str.contains (str.++ x "AB" y) "C") -->
3014 : : // (or (str.contains x "C") (str.contains y "C")
3015 : 25980 : Node ret = rewriteViaMacroStrSplitCtn(node);
3016 [ + + ]: 25980 : if (!ret.isNull())
3017 : : {
3018 : 851 : return returnRewrite(node, ret, Rewrite::CTN_SPLIT);
3019 : : }
3020 [ + + ]: 25980 : }
3021 [ + + ]: 96779 : else if (node[0].getKind() == Kind::STRING_SUBSTR)
3022 : : {
3023 : : // (str.contains (str.substr x n (str.len y)) y) --->
3024 : : // (= (str.substr x n (str.len y)) y)
3025 : : //
3026 : : // TODO: Remove with under-/over-approximation
3027 [ + + ]: 17390 : if (node[0][2] == nm->mkNode(Kind::STRING_LENGTH, node[1]))
3028 : : {
3029 : 38 : Node ret = nm->mkNode(Kind::EQUAL, node[0], node[1]);
3030 : 19 : return returnRewrite(node, ret, Rewrite::CTN_SUBSTR);
3031 : 19 : }
3032 : : }
3033 [ + + ]: 79389 : else if (node[0].getKind() == Kind::STRING_REPLACE)
3034 : : {
3035 [ + + ]: 9562 : if (node[0][0] == node[0][2])
3036 : : {
3037 : : // (str.contains (str.replace x y x) y) ---> (str.contains x y)
3038 [ + + ]: 1216 : if (node[0][1] == node[1])
3039 : : {
3040 : 110 : Node ret = nm->mkNode(Kind::STRING_CONTAINS, node[0][0], node[1]);
3041 : 55 : return returnRewrite(node, ret, Rewrite::CTN_REPL_TO_CTN);
3042 : 55 : }
3043 : :
3044 : : // (str.contains (str.replace x y x) z) ---> (str.contains x z)
3045 : : // if (str.len z) <= 1
3046 [ + + ]: 1161 : if (d_stringsEntail.checkLengthOne(node[1]))
3047 : : {
3048 : 1664 : Node ret = nm->mkNode(Kind::STRING_CONTAINS, node[0][0], node[1]);
3049 : 832 : return returnRewrite(node, ret, Rewrite::CTN_REPL_LEN_ONE_TO_CTN);
3050 : 832 : }
3051 : : }
3052 : :
3053 : : // (str.contains (str.replace x y z) z) --->
3054 : : // (or (str.contains x y) (str.contains x z))
3055 [ + + ]: 8675 : if (node[0][2] == node[1])
3056 : : {
3057 : 4086 : Node ret = nm->mkNode(
3058 : : Kind::OR,
3059 : 2724 : {nm->mkNode(Kind::STRING_CONTAINS, node[0][0], node[0][1]),
3060 : 2724 : nm->mkNode(Kind::STRING_CONTAINS, node[0][0], node[0][2])});
3061 : 1362 : return returnRewrite(node, ret, Rewrite::CTN_REPL_TO_CTN_DISJ);
3062 : 1362 : }
3063 : : }
3064 : 69827 : else if (node[0].getKind() == Kind::STRING_ITOS && node[1].isConst())
3065 : : {
3066 : 726 : String s = node[1].getConst<String>();
3067 [ - + ]: 726 : if (!s.isNumber())
3068 : : {
3069 : 0 : Node ret = nm->mkConst(false);
3070 : 0 : return returnRewrite(node, ret, Rewrite::CTN_ITOS_NON_DIGIT);
3071 : 0 : }
3072 [ + - ]: 726 : }
3073 : :
3074 [ + + ]: 119640 : if (node[1].getKind() == Kind::STRING_REPLACE)
3075 : : {
3076 : : // (str.contains x (str.replace y x y)) --->
3077 : : // (str.contains x y)
3078 : 10667 : if (node[0] == node[1][1] && node[1][0] == node[1][2])
3079 : : {
3080 : 40 : Node ret = nm->mkNode(Kind::STRING_CONTAINS, node[0], node[1][0]);
3081 : 20 : return returnRewrite(node, ret, Rewrite::CTN_REPL);
3082 : 20 : }
3083 : :
3084 : : // (str.contains x (str.replace "" x y)) --->
3085 : : // (= "" (str.replace "" x y))
3086 : : //
3087 : : // Note: Length-based reasoning is not sufficient to get this rewrite. We
3088 : : // can neither show that str.len(str.replace("", x, y)) - str.len(x) >= 0
3089 : : // nor str.len(x) - str.len(str.replace("", x, y)) >= 0
3090 : 10647 : Node emp = Word::mkEmptyWord(stype);
3091 : 10647 : if (node[0] == node[1][1] && node[1][0] == emp)
3092 : : {
3093 : 2 : Node ret = nm->mkNode(Kind::EQUAL, emp, node[1]);
3094 : 1 : return returnRewrite(node, ret, Rewrite::CTN_REPL_EMPTY);
3095 : 1 : }
3096 [ + + ]: 10647 : }
3097 : : // If we marked a rewrite but did not yet return it.
3098 [ + + ]: 119619 : if (!maybeRew.isNull())
3099 : : {
3100 : 1523 : return returnRewrite(node, maybeRew, maybeRule);
3101 : : }
3102 : :
3103 : 118096 : return node;
3104 : 268249 : }
3105 : :
3106 : 13868 : Node SequencesRewriter::rewriteIndexof(Node node)
3107 : : {
3108 [ - + ][ - + ]: 13868 : Assert(node.getKind() == Kind::STRING_INDEXOF);
[ - - ]
3109 : 13868 : NodeManager* nm = nodeManager();
3110 : :
3111 : 13868 : if (node[2].isConst() && node[2].getConst<Rational>().sgn() < 0)
3112 : : {
3113 : : // z<0 implies str.indexof( x, y, z ) --> -1
3114 : 185 : Node negone = nm->mkConstInt(Rational(-1));
3115 : 185 : return returnRewrite(node, negone, Rewrite::IDOF_NEG);
3116 : 185 : }
3117 : :
3118 : : // the string type
3119 : 13683 : TypeNode stype = node[0].getType();
3120 : :
3121 : : // evaluation and simple cases
3122 : 13683 : std::vector<Node> children0;
3123 : 13683 : utils::getConcat(node[0], children0);
3124 : 13683 : if (children0[0].isConst() && node[1].isConst() && node[2].isConst())
3125 : : {
3126 : 1776 : cvc5::internal::Rational rMaxInt(cvc5::internal::String::maxSize());
3127 [ + + ]: 1776 : if (node[2].getConst<Rational>() > rMaxInt)
3128 : : {
3129 [ - + ]: 10 : if (node[0].isConst())
3130 : : {
3131 : : // We know that, due to limitations on the size of string constants
3132 : : // in our implementation, that accessing a position greater than
3133 : : // rMaxInt is guaranteed to be out of bounds.
3134 : 0 : Node negone = nm->mkConstInt(Rational(-1));
3135 : 0 : return returnRewrite(node, negone, Rewrite::IDOF_MAX);
3136 : 0 : }
3137 : : }
3138 : : else
3139 : : {
3140 [ - + ][ - + ]: 1766 : Assert(node[2].getConst<Rational>().sgn() >= 0);
[ - - ]
3141 : 1766 : Node s = children0[0];
3142 : 1766 : Node t = node[1];
3143 : : uint32_t start =
3144 : 1766 : node[2].getConst<Rational>().getNumerator().toUnsignedInt();
3145 : 1766 : std::size_t ret = Word::find(s, t, start);
3146 [ + + ]: 1766 : if (ret != std::string::npos)
3147 : : {
3148 : 719 : Node retv = nm->mkConstInt(Rational(static_cast<unsigned>(ret)));
3149 : 719 : return returnRewrite(node, retv, Rewrite::IDOF_FIND);
3150 : 719 : }
3151 [ + + ]: 1047 : else if (children0.size() == 1)
3152 : : {
3153 : 537 : Node negone = nm->mkConstInt(Rational(-1));
3154 : 537 : return returnRewrite(node, negone, Rewrite::IDOF_NFIND);
3155 : 537 : }
3156 [ + + ][ + + ]: 3022 : }
3157 [ + + ]: 1776 : }
3158 : :
3159 [ + + ]: 12427 : if (node[0] == node[1])
3160 : : {
3161 [ + + ]: 970 : if (node[2].isConst())
3162 : : {
3163 [ + - ]: 31 : if (node[2].getConst<Rational>().sgn() == 0)
3164 : : {
3165 : : // indexof( x, x, 0 ) --> 0
3166 : 31 : Node zero = nm->mkConstInt(Rational(0));
3167 : 31 : return returnRewrite(node, zero, Rewrite::IDOF_EQ_CST_START);
3168 : 31 : }
3169 : : }
3170 [ - + ]: 939 : if (d_arithEntail.check(node[2], true))
3171 : : {
3172 : : // y>0 implies indexof( x, x, y ) --> -1
3173 : 0 : Node negone = nm->mkConstInt(Rational(-1));
3174 : 0 : return returnRewrite(node, negone, Rewrite::IDOF_EQ_NSTART);
3175 : 0 : }
3176 : 939 : Node emp = Word::mkEmptyWord(stype);
3177 [ + + ]: 939 : if (node[0] != emp)
3178 : : {
3179 : : // indexof( x, x, z ) ---> indexof( "", "", z )
3180 : 266 : Node ret = nm->mkNode(Kind::STRING_INDEXOF, emp, emp, node[2]);
3181 : 133 : return returnRewrite(node, ret, Rewrite::IDOF_EQ_NORM);
3182 : 133 : }
3183 [ + + ]: 939 : }
3184 : :
3185 : 24526 : Node len0 = nm->mkNode(Kind::STRING_LENGTH, node[0]);
3186 : 24526 : Node len1 = nm->mkNode(Kind::STRING_LENGTH, node[1]);
3187 : 24526 : Node len0m2 = nm->mkNode(Kind::SUB, len0, node[2]);
3188 : :
3189 [ + + ]: 12263 : if (node[1].isConst())
3190 : : {
3191 [ + + ]: 8608 : if (Word::isEmpty(node[1]))
3192 : : {
3193 : 1060 : if (d_arithEntail.check(len0, node[2]) && d_arithEntail.check(node[2]))
3194 : : {
3195 : : // len(x)>=z ^ z >=0 implies indexof( x, "", z ) ---> z
3196 : 98 : return returnRewrite(node, node[2], Rewrite::IDOF_EMP_IDOF);
3197 : : }
3198 : : }
3199 : : }
3200 : :
3201 [ + + ]: 12165 : if (d_arithEntail.check(len1, len0m2, true))
3202 : : {
3203 : : // len(x)-z < len(y) implies indexof( x, y, z ) ----> -1
3204 : 15 : Node negone = nm->mkConstInt(Rational(-1));
3205 : 15 : return returnRewrite(node, negone, Rewrite::IDOF_LEN);
3206 : 15 : }
3207 : :
3208 : 12150 : Node fstr = node[0];
3209 : 12150 : if (!node[2].isConst() || node[2].getConst<Rational>().sgn() != 0)
3210 : : {
3211 : 4106 : fstr = nm->mkNode(Kind::STRING_SUBSTR, node[0], node[2], len0);
3212 : : }
3213 : :
3214 : 24300 : Node cmp_conr = d_stringsEntail.checkContains(fstr, node[1]);
3215 [ + - ]: 24300 : Trace("strings-rewrite-debug") << "For " << node << ", check contains("
3216 [ - + ][ - - ]: 12150 : << fstr << ", " << node[1] << ")" << std::endl;
3217 [ + - ]: 12150 : Trace("strings-rewrite-debug") << "...got " << cmp_conr << std::endl;
3218 : 12150 : std::vector<Node> children1;
3219 : 12150 : utils::getConcat(node[1], children1);
3220 [ + + ]: 12150 : if (!cmp_conr.isNull())
3221 : : {
3222 [ + + ]: 2145 : if (cmp_conr.getConst<bool>())
3223 : : {
3224 : 2103 : if (node[2].isConst() && node[2].getConst<Rational>().sgn() == 0)
3225 : : {
3226 : : // past the first position in node[0] that contains node[1], we can drop
3227 : 1103 : std::vector<Node> nb;
3228 : 1103 : std::vector<Node> ne;
3229 : 1103 : int cc = d_stringsEntail.componentContains(
3230 : : children0, children1, nb, ne, true, 1);
3231 [ + + ][ + + ]: 1103 : if (cc != -1 && !ne.empty())
[ + + ]
3232 : : {
3233 : : // For example:
3234 : : // str.indexof(str.++(x,y,z),y,0) ---> str.indexof(str.++(x,y),y,0)
3235 : 173 : Node nn = utils::mkConcat(children0, stype);
3236 : 346 : Node ret = nm->mkNode(Kind::STRING_INDEXOF, nn, node[1], node[2]);
3237 : 173 : return returnRewrite(node, ret, Rewrite::IDOF_DEF_CTN);
3238 : 173 : }
3239 : :
3240 : : // Strip components from the beginning that are guaranteed not to match
3241 [ + + ]: 930 : if (d_stringsEntail.stripConstantEndpoints(
3242 : : children0, children1, nb, ne, 1))
3243 : : {
3244 : : // str.indexof(str.++("AB", x, "C"), "C", 0) --->
3245 : : // 2 + str.indexof(str.++(x, "C"), "C", 0)
3246 : 66 : Node ret = nm->mkNode(
3247 : : Kind::ADD,
3248 : 44 : {nm->mkNode(Kind::STRING_LENGTH, utils::mkConcat(nb, stype)),
3249 : 88 : nm->mkNode(Kind::STRING_INDEXOF,
3250 : 44 : utils::mkConcat(children0, stype),
3251 : : node[1],
3252 : 66 : node[2])});
3253 : 22 : return returnRewrite(node, ret, Rewrite::IDOF_STRIP_CNST_ENDPTS);
3254 : 22 : }
3255 [ + + ][ + + ]: 1298 : }
3256 : : // To show that the first argument definitely contains the second, the
3257 : : // index must be a valid index in the first argument. This ensures that
3258 : : // (str.indexof t "" n) is not rewritten to something other than -1 when n
3259 : : // is beyond the length of t. This is not required for the above rewrites,
3260 : : // which only apply when n=0.
3261 : 1908 : if (d_arithEntail.check(node[2]) && d_arithEntail.check(len0, node[2]))
3262 : : {
3263 : : // strip symbolic length
3264 : 946 : Node new_len = node[2];
3265 : 946 : std::vector<Node> nr;
3266 [ + + ]: 946 : if (d_stringsEntail.stripSymbolicLength(children0, nr, 1, new_len))
3267 : : {
3268 : : // For example:
3269 : : // z>=0 and z>str.len( x1 ) and str.contains( x2, y )-->true
3270 : : // implies
3271 : : // str.indexof( str.++( x1, x2 ), y, z ) --->
3272 : : // str.len( x1 ) + str.indexof( x2, y, z-str.len(x1) )
3273 : 38 : Node nn = utils::mkConcat(children0, stype);
3274 : 114 : Node ret = nm->mkNode(
3275 : : Kind::ADD,
3276 : 76 : {nm->mkNode(Kind::SUB, node[2], new_len),
3277 : 76 : nm->mkNode(Kind::STRING_INDEXOF, nn, node[1], new_len)});
3278 : 38 : return returnRewrite(node, ret, Rewrite::IDOF_STRIP_SYM_LEN);
3279 : 38 : }
3280 [ + + ][ + + ]: 984 : }
3281 : : }
3282 : : else
3283 : : {
3284 : : // str.contains( x, y ) --> false implies str.indexof(x,y,z) --> -1
3285 : 42 : Node negone = nm->mkConstInt(Rational(-1));
3286 : 42 : return returnRewrite(node, negone, Rewrite::IDOF_NCTN);
3287 : 42 : }
3288 : : }
3289 : : else
3290 : : {
3291 : 10005 : Node new_len = node[2];
3292 : 10005 : std::vector<Node> nr;
3293 [ + + ]: 10005 : if (d_stringsEntail.stripSymbolicLength(children0, nr, 1, new_len))
3294 : : {
3295 : : // Normalize the string before the start index.
3296 : : //
3297 : : // For example:
3298 : : // str.indexof(str.++("ABCD", x), y, 3) --->
3299 : : // str.indexof(str.++("AAAD", x), y, 3)
3300 : 260 : Node nodeNr = utils::mkConcat(nr, stype);
3301 : 260 : Node normNr = lengthPreserveRewrite(nodeNr);
3302 [ + + ]: 260 : if (normNr != nodeNr)
3303 : : {
3304 : 43 : std::vector<Node> normNrChildren;
3305 : 43 : utils::getConcat(normNr, normNrChildren);
3306 : 43 : std::vector<Node> children(normNrChildren);
3307 : 43 : children.insert(children.end(), children0.begin(), children0.end());
3308 : 43 : Node nn = utils::mkConcat(children, stype);
3309 : 86 : Node res = nm->mkNode(Kind::STRING_INDEXOF, nn, node[1], node[2]);
3310 : 43 : return returnRewrite(node, res, Rewrite::IDOF_NORM_PREFIX);
3311 : 43 : }
3312 [ + + ][ + + ]: 303 : }
3313 [ + + ][ + + ]: 10048 : }
3314 : :
3315 : 11832 : if (node[2].isConst() && node[2].getConst<Rational>().sgn() == 0)
3316 : : {
3317 : : Node retStr =
3318 : 7827 : rewriteViaRule(ProofRewriteRule::MACRO_STR_STRIP_ENDPOINTS, node);
3319 [ + + ]: 7827 : if (!retStr.isNull())
3320 : : {
3321 : : // For example:
3322 : : // str.indexof( str.++( x, "A" ), "B", 0 ) ---> str.indexof( x, "B", 0 )
3323 : 73 : return returnRewrite(node, retStr, Rewrite::RPL_PULL_ENDPT);
3324 : : }
3325 [ + + ]: 7827 : }
3326 : :
3327 : 11759 : return node;
3328 : 13683 : }
3329 : :
3330 : 1610 : Node SequencesRewriter::rewriteIndexofRe(Node node)
3331 : : {
3332 [ - + ][ - + ]: 1610 : Assert(node.getKind() == Kind::STRING_INDEXOF_RE);
[ - - ]
3333 : 1610 : NodeManager* nm = nodeManager();
3334 : 1610 : Node s = node[0];
3335 : 1610 : Node r = node[1];
3336 : 1610 : Node n = node[2];
3337 : 1610 : Node zero = nm->mkConstInt(Rational(0));
3338 : 1610 : Node slen = nm->mkNode(Kind::STRING_LENGTH, s);
3339 : :
3340 : 1610 : if (d_arithEntail.check(zero, n, true) || d_arithEntail.check(n, slen, true))
3341 : : {
3342 : 55 : Node ret = nm->mkConstInt(Rational(-1));
3343 : 55 : return returnRewrite(node, ret, Rewrite::INDEXOF_RE_INVALID_INDEX);
3344 : 55 : }
3345 : :
3346 [ + + ]: 1555 : if (RegExpEntail::isConstRegExp(r))
3347 : : {
3348 : 1049 : Node neval = rewriteViaStrIndexofReEval(node);
3349 [ + + ]: 1049 : if (!neval.isNull())
3350 : : {
3351 : 257 : return returnRewrite(node, neval, Rewrite::INDEXOF_RE_EVAL);
3352 : : }
3353 : 792 : if (d_arithEntail.check(n, zero) && d_arithEntail.check(slen, n))
3354 : : {
3355 : 516 : String emptyStr("");
3356 [ + + ]: 516 : if (RegExpEntail::testConstStringInRegExp(emptyStr, r))
3357 : : {
3358 : 14 : return returnRewrite(node, n, Rewrite::INDEXOF_RE_EMP_RE);
3359 : : }
3360 [ + + ]: 516 : }
3361 [ + + ]: 778 : if (r.getKind() == Kind::REGEXP_NONE)
3362 : : {
3363 : 12 : Node ret = nm->mkConstInt(Rational(-1));
3364 : 12 : return returnRewrite(node, ret, Rewrite::INDEXOF_RE_NONE);
3365 : 12 : }
3366 [ + + ]: 1049 : }
3367 : 1272 : return node;
3368 : 1610 : }
3369 : :
3370 : 17910 : Node SequencesRewriter::rewriteReplace(Node node)
3371 : : {
3372 [ - + ][ - + ]: 17910 : Assert(node.getKind() == Kind::STRING_REPLACE);
[ - - ]
3373 : 17910 : NodeManager* nm = nodeManager();
3374 : :
3375 : : // the string type
3376 : 17910 : TypeNode stype = node.getType();
3377 : :
3378 : 17910 : std::vector<Node> children0;
3379 : 17910 : utils::getConcat(node[0], children0);
3380 : :
3381 [ + + ][ + + ]: 17910 : if (node[1].isConst() && children0[0].isConst())
[ + - ][ + + ]
[ - - ]
3382 : : {
3383 : 4728 : Node s = children0[0];
3384 : 4728 : Node t = node[1];
3385 : 4728 : std::size_t p = Word::find(s, t);
3386 [ + + ]: 4728 : if (p == std::string::npos)
3387 : : {
3388 [ + + ]: 1344 : if (children0.size() == 1)
3389 : : {
3390 : 966 : return returnRewrite(node, node[0], Rewrite::RPL_CONST_NFIND);
3391 : : }
3392 : : }
3393 : : else
3394 : : {
3395 : 3384 : Node s1 = Word::substr(s, 0, p);
3396 : 6768 : Node s3 = Word::substr(s, p + Word::getLength(t));
3397 : 3384 : std::vector<Node> children;
3398 [ + + ]: 3384 : if (!Word::isEmpty(s1))
3399 : : {
3400 : 229 : children.push_back(s1);
3401 : : }
3402 : 3384 : children.push_back(node[2]);
3403 [ + + ]: 3384 : if (!Word::isEmpty(s3))
3404 : : {
3405 : 1431 : children.push_back(s3);
3406 : : }
3407 : 3384 : children.insert(children.end(), children0.begin() + 1, children0.end());
3408 : 3384 : Node ret;
3409 [ + + ][ + + ]: 3384 : if (children0.size() == 1 && node[2].isConst())
[ + + ][ + + ]
[ - - ]
3410 : : {
3411 : : // evaluate the constant, this ensures that we always immediately
3412 : : // evaluate constants immediately, which is important for proof
3413 : : // reconstruction.
3414 : 1621 : ret = Word::mkWordFlatten(children);
3415 : : }
3416 : : else
3417 : : {
3418 : 1763 : ret = utils::mkConcat(children, stype);
3419 : : }
3420 : 3384 : return returnRewrite(node, ret, Rewrite::RPL_CONST_FIND);
3421 : 3384 : }
3422 [ + + ][ + + ]: 9078 : }
3423 : :
3424 : 13560 : if (node[1].isConst() && Word::isEmpty(node[1]))
3425 : : {
3426 : 548 : Node ret = nm->mkNode(Kind::STRING_CONCAT, node[2], node[0]);
3427 : 274 : return returnRewrite(node, ret, Rewrite::RPL_RPL_EMPTY);
3428 : 274 : }
3429 : :
3430 : : // rewrites that apply to both replace and replaceall
3431 : 13286 : Node rri = rewriteReplaceInternal(node);
3432 [ + + ]: 13286 : if (!rri.isNull())
3433 : : {
3434 : : // printing of the rewrite managed by the call above
3435 : 759 : return rri;
3436 : : }
3437 : :
3438 [ + + ]: 12527 : if (node[0] == node[2])
3439 : : {
3440 : : // ( len( y )>=len(x) ) => str.replace( x, y, x ) ---> x
3441 : 4580 : Node l0 = nodeManager()->mkNode(Kind::STRING_LENGTH, node[0]);
3442 : 4580 : Node l1 = nodeManager()->mkNode(Kind::STRING_LENGTH, node[1]);
3443 [ + + ]: 2290 : if (d_arithEntail.check(l1, l0))
3444 : : {
3445 : 872 : return returnRewrite(node, node[0], Rewrite::RPL_RPL_LEN_ID);
3446 : : }
3447 [ + + ][ + + ]: 3162 : }
3448 : :
3449 : 11655 : std::vector<Node> children1;
3450 : 11655 : utils::getConcat(node[1], children1);
3451 : :
3452 : : // check if contains definitely does (or does not) hold
3453 : 23310 : Node cmp_conr = d_stringsEntail.checkContains(node[0], node[1]);
3454 [ + + ]: 11655 : if (!cmp_conr.isNull())
3455 : : {
3456 [ - + ][ - + ]: 4660 : Assert(cmp_conr.isConst());
[ - - ]
3457 [ + + ]: 4660 : if (cmp_conr.getConst<bool>())
3458 : : {
3459 : : // component-wise containment
3460 : 3838 : std::vector<Node> cb;
3461 : 3838 : std::vector<Node> ce;
3462 : 3838 : int cc = d_stringsEntail.componentContains(
3463 : : children0, children1, cb, ce, true, 1);
3464 [ + + ]: 3838 : if (cc != -1)
3465 : : {
3466 [ + + ][ + + ]: 3647 : if (cc == 0 && children0[0] == children1[0])
[ + + ]
3467 : : {
3468 : : // definitely a prefix, can do the replace
3469 : : // for example,
3470 : : // str.replace( str.++( x, "ab" ), str.++( x, "a" ), y ) --->
3471 : : // str.++( y, "b" )
3472 : 178 : std::vector<Node> cres;
3473 : 178 : cres.push_back(node[2]);
3474 : 178 : cres.insert(cres.end(), ce.begin(), ce.end());
3475 : 178 : Node ret = utils::mkConcat(cres, stype);
3476 : 178 : return returnRewrite(node, ret, Rewrite::RPL_CCTN_RPL);
3477 : 178 : }
3478 [ + + ]: 3469 : else if (!ce.empty())
3479 : : {
3480 : : // we can pull remainder past first definite containment
3481 : : // for example,
3482 : : // str.replace( str.++( x, "ab" ), "a", y ) --->
3483 : : // str.++( str.replace( str.++( x, "a" ), "a", y ), "b" )
3484 : : // this is independent of whether the second argument may be empty
3485 : 971 : std::vector<Node> scc;
3486 : 2913 : scc.push_back(nodeManager()->mkNode(Kind::STRING_REPLACE,
3487 : 1942 : utils::mkConcat(children0, stype),
3488 : : node[1],
3489 : : node[2]));
3490 : 971 : scc.insert(scc.end(), ce.begin(), ce.end());
3491 : 971 : Node ret = utils::mkConcat(scc, stype);
3492 : 971 : return returnRewrite(node, ret, Rewrite::RPL_CCTN);
3493 : 971 : }
3494 : : }
3495 [ + + ][ + + ]: 4987 : }
3496 : : else
3497 : : {
3498 : : // ~contains( t, s ) => ( replace( t, s, r ) ----> t )
3499 : 822 : return returnRewrite(node, node[0], Rewrite::RPL_NCTN);
3500 : : }
3501 : : }
3502 : :
3503 [ + + ]: 9684 : if (d_stringsEntail.checkNonEmpty(node[1]))
3504 : : {
3505 : : // pull endpoints that can be stripped
3506 : : // for example,
3507 : : // str.replace( str.++( "b", x, "b" ), "a", y ) --->
3508 : : // str.++( "b", str.replace( x, "a", y ), "b" )
3509 : : Node retStr =
3510 : 5672 : rewriteViaRule(ProofRewriteRule::MACRO_STR_STRIP_ENDPOINTS, node);
3511 [ + + ]: 5672 : if (!retStr.isNull())
3512 : : {
3513 : 352 : return returnRewrite(node, retStr, Rewrite::RPL_PULL_ENDPT);
3514 : : }
3515 [ + + ]: 5672 : }
3516 : :
3517 : 9332 : children1.clear();
3518 : 9332 : utils::getConcat(node[1], children1);
3519 : 9332 : Node lastChild1 = children1[children1.size() - 1];
3520 [ + + ]: 9332 : if (lastChild1.getKind() == Kind::STRING_SUBSTR)
3521 : : {
3522 : : // (str.replace x (str.++ t (str.substr y i j)) z) --->
3523 : : // (str.replace x (str.++ t
3524 : : // (str.substr y i (+ (str.len x) 1 (- (str.len t))))) z)
3525 : : // if j > len(x)
3526 : : //
3527 : : // Reasoning: If the string to be replaced is longer than x, then it does
3528 : : // not matter how much longer it is, the result is always x. Thus, it is
3529 : : // fine to only look at the prefix of length len(x) + 1 - len(t).
3530 : :
3531 : 269 : children1.pop_back();
3532 : : // Length of the non-substr components in the second argument
3533 : : Node partLen1 =
3534 : 538 : nm->mkNode(Kind::STRING_LENGTH, utils::mkConcat(children1, stype));
3535 : 538 : Node maxLen1 = nm->mkNode(Kind::ADD, partLen1, lastChild1[2]);
3536 : :
3537 : 269 : Node zero = nm->mkConstInt(Rational(0));
3538 : 269 : Node one = nm->mkConstInt(Rational(1));
3539 : 538 : Node len0 = nm->mkNode(Kind::STRING_LENGTH, node[0]);
3540 : 538 : Node len0_1 = nm->mkNode(Kind::ADD, len0, one);
3541 : : // Check len(t) + j > len(x) + 1
3542 [ + + ]: 269 : if (d_arithEntail.check(maxLen1, len0_1, true))
3543 : : {
3544 : 4 : children1.push_back(nm->mkNode(
3545 : : Kind::STRING_SUBSTR,
3546 : : lastChild1[0],
3547 : : lastChild1[1],
3548 : 8 : nm->mkNode(Kind::ADD, len0, one, nm->mkNode(Kind::NEG, partLen1))));
3549 : : Node res = nm->mkNode(Kind::STRING_REPLACE,
3550 : : node[0],
3551 : 8 : utils::mkConcat(children1, stype),
3552 : 16 : node[2]);
3553 : 4 : return returnRewrite(node, res, Rewrite::REPL_SUBST_IDX);
3554 : 4 : }
3555 [ + + ][ + + ]: 289 : }
[ + + ][ + + ]
[ + + ][ + + ]
3556 : :
3557 [ + + ]: 9328 : if (node[0].getKind() == Kind::STRING_REPLACE)
3558 : : {
3559 : 882 : Node x = node[0];
3560 : 882 : Node y = node[1];
3561 : 882 : Node z = node[2];
3562 : 882 : if (x[0] == x[2] && x[0] == y)
3563 : : {
3564 : : // (str.replace (str.replace y w y) y z) -->
3565 : : // (str.replace (str.replace y w z) y z)
3566 : : // if (str.len w) >= (str.len z) and w != z
3567 : : //
3568 : : // Reasoning: There are two cases: (1) w does not appear in y and (2) w
3569 : : // does appear in y.
3570 : : //
3571 : : // Case (1): In this case, the reasoning is trivial. The
3572 : : // inner replace does not do anything, so we can just replace its third
3573 : : // argument with any string.
3574 : : //
3575 : : // Case (2): After the inner replace, we are guaranteed to have a string
3576 : : // that contains y at the index of w in the original string y. The outer
3577 : : // replace then replaces that y with z, so we can short-circuit that
3578 : : // replace by directly replacing w with z in the inner replace. We can
3579 : : // only do that if the result of the new inner replace does not contain
3580 : : // y, otherwise we end up doing two replaces that are different from the
3581 : : // original expression. We enforce that by requiring that the length of w
3582 : : // has to be greater or equal to the length of z and that w and z have to
3583 : : // be different. This makes sure that an inner replace changes a string
3584 : : // to a string that is shorter than y, making it impossible for the outer
3585 : : // replace to match.
3586 : 71 : Node w = x[1];
3587 : :
3588 : : // (str.len w) >= (str.len z)
3589 : 71 : Node wlen = nm->mkNode(Kind::STRING_LENGTH, w);
3590 : 71 : Node zlen = nm->mkNode(Kind::STRING_LENGTH, z);
3591 [ + + ]: 71 : if (d_arithEntail.check(wlen, zlen))
3592 : : {
3593 : : // w != z
3594 [ + + ][ + + ]: 39 : if (w != z && w.isConst() && z.isConst())
[ + - ][ + + ]
3595 : : {
3596 : : Node ret = nm->mkNode(Kind::STRING_REPLACE,
3597 : 22 : nm->mkNode(Kind::STRING_REPLACE, y, w, z),
3598 : : y,
3599 : 44 : z);
3600 : 11 : return returnRewrite(node, ret, Rewrite::REPL_REPL_SHORT_CIRCUIT);
3601 : 11 : }
3602 : : }
3603 [ + + ][ + + ]: 93 : }
[ + + ]
3604 [ + + ][ + + ]: 904 : }
[ + + ]
3605 : :
3606 [ + + ]: 9317 : if (node[1].getKind() == Kind::STRING_REPLACE)
3607 : : {
3608 [ + + ]: 1046 : if (node[1][0] == node[0])
3609 : : {
3610 : 304 : if (node[1][0] == node[1][2] && node[1][0] == node[2])
3611 : : {
3612 : : // str.replace( x, str.replace( x, y, x ), x ) ---> x
3613 : 10 : return returnRewrite(node, node[0], Rewrite::REPL_REPL2_INV_ID);
3614 : : }
3615 : 294 : bool dualReplIteSuccess = false;
3616 : 588 : Node cmp_con2 = d_stringsEntail.checkContains(node[1][0], node[1][2]);
3617 [ + + ][ - + ]: 294 : if (!cmp_con2.isNull() && !cmp_con2.getConst<bool>())
[ - + ]
3618 : : {
3619 : : // str.contains( x, z ) ---> false
3620 : : // implies
3621 : : // str.replace( x, str.replace( x, y, z ), w ) --->
3622 : : // ite( str.contains( x, y ), x, w )
3623 : 0 : dualReplIteSuccess = true;
3624 : : }
3625 : : else
3626 : : {
3627 : : // str.contains( y, z ) ---> false and str.contains( z, y ) ---> false
3628 : : // implies
3629 : : // str.replace( x, str.replace( x, y, z ), w ) --->
3630 : : // ite( str.contains( x, y ), x, w )
3631 : 294 : cmp_con2 = d_stringsEntail.checkContains(node[1][1], node[1][2]);
3632 [ + + ][ + + ]: 294 : if (!cmp_con2.isNull() && !cmp_con2.getConst<bool>())
[ + + ]
3633 : : {
3634 : 96 : cmp_con2 = d_stringsEntail.checkContains(node[1][2], node[1][1]);
3635 [ + - ][ + + ]: 96 : if (!cmp_con2.isNull() && !cmp_con2.getConst<bool>())
[ + + ]
3636 : : {
3637 : 40 : dualReplIteSuccess = true;
3638 : : }
3639 : : }
3640 : : }
3641 [ + + ]: 294 : if (dualReplIteSuccess)
3642 : : {
3643 : : Node res =
3644 : : nm->mkNode(Kind::ITE,
3645 : 80 : nm->mkNode(Kind::STRING_CONTAINS, node[0], node[1][1]),
3646 : : node[0],
3647 : 160 : node[2]);
3648 : 40 : return returnRewrite(node, res, Rewrite::REPL_DUAL_REPL_ITE);
3649 : 40 : }
3650 [ + + ]: 294 : }
3651 : :
3652 : 996 : bool invSuccess = false;
3653 [ + + ]: 996 : if (node[1][1] == node[0])
3654 : : {
3655 [ + + ]: 122 : if (node[1][0] == node[1][2])
3656 : : {
3657 : : // str.replace(x, str.replace(y, x, y), w) ---> str.replace(x, y, w)
3658 : 6 : invSuccess = true;
3659 : : }
3660 : 116 : else if (node[1][1] == node[2] || node[1][0] == node[2])
3661 : : {
3662 : : // str.contains(y, z) ----> false and ( y == w or x == w ) implies
3663 : : // implies
3664 : : // str.replace(x, str.replace(y, x, z), w) ---> str.replace(x, y, w)
3665 : 112 : Node cmp_con2 = d_stringsEntail.checkContains(node[1][0], node[1][2]);
3666 [ + + ][ - + ]: 56 : invSuccess = !cmp_con2.isNull() && !cmp_con2.getConst<bool>();
3667 : 56 : }
3668 : : }
3669 : : else
3670 : : {
3671 : : // str.contains(x, z) ----> false and str.contains(x, w) ----> false
3672 : : // implies
3673 : : // str.replace(x, str.replace(y, z, w), u) ---> str.replace(x, y, u)
3674 : 1748 : Node cmp_con2 = d_stringsEntail.checkContains(node[0], node[1][1]);
3675 [ + + ][ + + ]: 874 : if (!cmp_con2.isNull() && !cmp_con2.getConst<bool>())
[ + + ]
3676 : : {
3677 : 80 : cmp_con2 = d_stringsEntail.checkContains(node[0], node[1][2]);
3678 [ + + ][ - + ]: 80 : invSuccess = !cmp_con2.isNull() && !cmp_con2.getConst<bool>();
3679 : : }
3680 : 874 : }
3681 [ + + ]: 996 : if (invSuccess)
3682 : : {
3683 : 12 : Node res = nm->mkNode(Kind::STRING_REPLACE, node[0], node[1][0], node[2]);
3684 : 6 : return returnRewrite(node, res, Rewrite::REPL_REPL2_INV);
3685 : 6 : }
3686 : : }
3687 [ + + ]: 9261 : if (node[2].getKind() == Kind::STRING_REPLACE)
3688 : : {
3689 [ + + ]: 548 : if (node[2][1] == node[0])
3690 : : {
3691 : : // str.contains( z, w ) ----> false implies
3692 : : // str.replace( x, w, str.replace( z, x, y ) ) ---> str.replace( x, w, z )
3693 : 48 : Node cmp_con2 = d_stringsEntail.checkContains(node[2][0], node[1]);
3694 [ + + ][ - + ]: 24 : if (!cmp_con2.isNull() && !cmp_con2.getConst<bool>())
[ - + ]
3695 : : {
3696 : : Node res =
3697 : 0 : nm->mkNode(Kind::STRING_REPLACE, node[0], node[1], node[2][0]);
3698 : 0 : return returnRewrite(node, res, Rewrite::REPL_REPL3_INV);
3699 : 0 : }
3700 [ + - ]: 24 : }
3701 [ + + ]: 548 : if (node[2][0] == node[1])
3702 : : {
3703 : 4 : bool success = false;
3704 : 4 : if (node[2][0] == node[2][2] && node[2][1] == node[0])
3705 : : {
3706 : : // str.replace( x, y, str.replace( y, x, y ) ) ---> x
3707 : 0 : success = true;
3708 : : }
3709 : : else
3710 : : {
3711 : : // str.contains( x, z ) ----> false implies
3712 : : // str.replace( x, y, str.replace( y, z, w ) ) ---> x
3713 : 4 : cmp_conr = d_stringsEntail.checkContains(node[0], node[2][1]);
3714 [ - + ][ - - ]: 4 : success = !cmp_conr.isNull() && !cmp_conr.getConst<bool>();
3715 : : }
3716 [ - + ]: 4 : if (success)
3717 : : {
3718 : 0 : return returnRewrite(node, node[0], Rewrite::REPL_REPL3_INV_ID);
3719 : : }
3720 : : }
3721 : : }
3722 : : // miniscope based on components that do not contribute to contains
3723 : : // for example,
3724 : : // str.replace( x ++ y ++ x ++ y, "A", z ) -->
3725 : : // str.replace( x ++ y, "A", z ) ++ x ++ y
3726 : : // since if "A" occurs in x ++ y ++ x ++ y, then it must occur in x ++ y.
3727 [ + + ]: 9261 : if (d_stringsEntail.checkLengthOne(node[1]))
3728 : : {
3729 : 4667 : Node lastLhs;
3730 : 4667 : unsigned lastCheckIndex = 0;
3731 [ + + ]: 4721 : for (unsigned i = 1, iend = children0.size(); i < iend; i++)
3732 : : {
3733 : 1963 : unsigned checkIndex = children0.size() - i;
3734 : 1963 : std::vector<Node> checkLhs;
3735 : 3926 : checkLhs.insert(
3736 : 3926 : checkLhs.end(), children0.begin(), children0.begin() + checkIndex);
3737 : 1963 : Node lhs = utils::mkConcat(checkLhs, stype);
3738 : 1963 : Node rhs = children0[checkIndex];
3739 : 3926 : Node ctn = d_stringsEntail.checkContains(lhs, rhs);
3740 [ + + ][ + - ]: 1963 : if (!ctn.isNull() && ctn.getConst<bool>())
[ + + ]
3741 : : {
3742 : 54 : lastLhs = lhs;
3743 : 54 : lastCheckIndex = checkIndex;
3744 : : }
3745 : : else
3746 : : {
3747 : 1909 : break;
3748 : : }
3749 [ + + ][ + + ]: 7690 : }
[ + + ][ + + ]
3750 [ + + ]: 4667 : if (!lastLhs.isNull())
3751 : : {
3752 : 44 : std::vector<Node> remc(children0.begin() + lastCheckIndex,
3753 : 44 : children0.end());
3754 : 44 : Node rem = utils::mkConcat(remc, stype);
3755 : 44 : std::vector<Node> rchildren;
3756 : 44 : rchildren.push_back(
3757 : 88 : nm->mkNode(Kind::STRING_REPLACE, lastLhs, node[1], node[2]));
3758 : : // "inline" the components of concatenation, which makes RARE
3759 : : // reconstruction easier.
3760 : 44 : utils::getConcat(rem, rchildren);
3761 : 44 : Node ret = utils::mkConcat(rchildren, lastLhs.getType());
3762 : : // for example:
3763 : : // str.replace( x ++ x, "A", y ) ---> str.replace( x, "A", y ) ++ x
3764 : : // Since we know that the first occurrence of "A" cannot be in the
3765 : : // second occurrence of x. Notice this is specific to single characters
3766 : : // due to complications with finds that span multiple components for
3767 : : // non-characters.
3768 : 44 : return returnRewrite(node, ret, Rewrite::REPL_CHAR_NCONTRIB_FIND);
3769 : 44 : }
3770 [ + + ]: 4667 : }
3771 : :
3772 : : // TODO (#1180) incorporate these?
3773 : : // contains( t, s ) =>
3774 : : // replace( replace( x, t, s ), s, r ) ----> replace( x, t, r )
3775 : : // contains( t, s ) =>
3776 : : // contains( replace( t, s, r ), r ) ----> true
3777 : :
3778 : 9217 : return node;
3779 : 17910 : }
3780 : :
3781 : 3389 : Node SequencesRewriter::rewriteReplaceAll(Node node)
3782 : : {
3783 [ - + ][ - + ]: 3389 : Assert(node.getKind() == Kind::STRING_REPLACE_ALL);
[ - - ]
3784 : :
3785 : 3389 : TypeNode stype = node.getType();
3786 : :
3787 : 3389 : if (node[0].isConst() && node[1].isConst())
3788 : : {
3789 : 793 : std::vector<Node> children;
3790 : 793 : Node s = node[0];
3791 : 793 : Node t = node[1];
3792 : 793 : if (Word::isEmpty(s) || Word::isEmpty(t))
3793 : : {
3794 : 471 : return returnRewrite(node, node[0], Rewrite::REPLALL_EMPTY_FIND);
3795 : : }
3796 : 322 : std::size_t sizeS = Word::getLength(s);
3797 : 322 : std::size_t sizeT = Word::getLength(t);
3798 : 322 : std::size_t index = 0;
3799 : 322 : std::size_t curr = 0;
3800 : : do
3801 : : {
3802 : 563 : curr = Word::find(s, t, index);
3803 [ + + ]: 563 : if (curr != std::string::npos)
3804 : : {
3805 [ + + ]: 241 : if (curr > index)
3806 : : {
3807 : 44 : children.push_back(Word::substr(s, index, curr - index));
3808 : : }
3809 : 241 : children.push_back(node[2]);
3810 : 241 : index = curr + sizeT;
3811 : : }
3812 : : else
3813 : : {
3814 : 322 : children.push_back(Word::substr(s, index, sizeS - index));
3815 : : }
3816 [ + + ][ + - ]: 563 : } while (curr != std::string::npos && curr < sizeS);
3817 [ - + ][ - + ]: 322 : Assert(!children.empty());
[ - - ]
3818 : : // constant evaluation, construct the concatenation and flatten it.
3819 : 322 : Node res;
3820 [ + + ]: 322 : if (node[2].isConst())
3821 : : {
3822 : 319 : res = Word::mkWordFlatten(children);
3823 : : }
3824 : : else
3825 : : {
3826 : 3 : res = utils::mkConcat(children, stype);
3827 : : }
3828 : 322 : return returnRewrite(node, res, Rewrite::REPLALL_CONST);
3829 : 793 : }
3830 : :
3831 : : // rewrites that apply to both replace and replaceall
3832 : 2596 : Node rri = rewriteReplaceInternal(node);
3833 [ + + ]: 2596 : if (!rri.isNull())
3834 : : {
3835 : : // printing of the rewrite managed by the call above
3836 : 272 : return rri;
3837 : : }
3838 : :
3839 : 4648 : Node cmp_conr = d_stringsEntail.checkContains(node[0], node[1]);
3840 [ + + ][ + + ]: 2324 : if (!cmp_conr.isNull() && !cmp_conr.getConst<bool>())
[ + + ]
3841 : : {
3842 : : // ~contains( t, s ) => ( replace_all( t, s, r ) ----> t )
3843 : 160 : return returnRewrite(node, node[0], Rewrite::RPL_NCTN);
3844 : : }
3845 : :
3846 : 2164 : return node;
3847 : 3389 : }
3848 : :
3849 : 15882 : Node SequencesRewriter::rewriteReplaceInternal(Node node)
3850 : : {
3851 : 15882 : Kind nk = node.getKind();
3852 [ + + ][ + - ]: 15882 : Assert(nk == Kind::STRING_REPLACE || nk == Kind::STRING_REPLACE_ALL);
[ - + ][ - + ]
[ - - ]
3853 : :
3854 [ + + ]: 15882 : if (node[1] == node[2])
3855 : : {
3856 : 574 : return returnRewrite(node, node[0], Rewrite::RPL_ID);
3857 : : }
3858 : :
3859 [ + + ]: 15308 : if (node[0] == node[1])
3860 : : {
3861 : : // only holds for replaceall if non-empty
3862 [ + + ][ + + ]: 789 : if (nk == Kind::STRING_REPLACE || d_stringsEntail.checkNonEmpty(node[1]))
[ + + ][ + + ]
[ - - ]
3863 : : {
3864 : 457 : return returnRewrite(node, node[2], Rewrite::RPL_REPLACE);
3865 : : }
3866 : : }
3867 : :
3868 : 14851 : return Node::null();
3869 : : }
3870 : :
3871 : 785 : Node SequencesRewriter::rewriteReplaceRe(Node node)
3872 : : {
3873 [ - + ][ - + ]: 785 : Assert(node.getKind() == Kind::STRING_REPLACE_RE);
[ - - ]
3874 : 785 : NodeManager* nm = nodeManager();
3875 : 785 : Node x = node[0];
3876 : 785 : Node y = node[1];
3877 : 785 : Node z = node[2];
3878 : :
3879 [ + + ]: 785 : if (RegExpEntail::isConstRegExp(y))
3880 : : {
3881 : 609 : Node neval = rewriteViaStrReplaceReEval(node);
3882 [ + + ]: 609 : if (!neval.isNull())
3883 : : {
3884 : 359 : return returnRewrite(node, neval, Rewrite::REPLACE_RE_EVAL);
3885 : : }
3886 : : // str.replace_re( x, y, z ) ---> z ++ x if "" in y ---> true
3887 : 250 : String emptyStr("");
3888 [ + + ]: 250 : if (RegExpEntail::testConstStringInRegExp(emptyStr, y))
3889 : : {
3890 : 8 : Node ret = nm->mkNode(Kind::STRING_CONCAT, z, x);
3891 : 4 : return returnRewrite(node, ret, Rewrite::REPLACE_RE_EMP_RE);
3892 : 4 : }
3893 [ + + ]: 246 : if (y.getKind() == Kind::REGEXP_NONE)
3894 : : {
3895 : 27 : return returnRewrite(node, x, Rewrite::REPLACE_RE_NONE);
3896 : : }
3897 [ + + ][ + + ]: 640 : }
3898 : 395 : return node;
3899 : 785 : }
3900 : :
3901 : 766 : Node SequencesRewriter::rewriteReplaceReAll(Node node)
3902 : : {
3903 [ - + ][ - + ]: 766 : Assert(node.getKind() == Kind::STRING_REPLACE_RE_ALL);
[ - - ]
3904 : 766 : Node x = node[0];
3905 : 766 : Node y = node[1];
3906 : 766 : Node z = node[2];
3907 : :
3908 [ + + ]: 766 : if (RegExpEntail::isConstRegExp(y))
3909 : : {
3910 : 636 : Node neval = rewriteViaStrReplaceReAllEval(node);
3911 [ + + ]: 636 : if (!neval.isNull())
3912 : : {
3913 : 440 : return returnRewrite(node, neval, Rewrite::REPLACE_RE_ALL_EVAL);
3914 : : }
3915 [ + + ]: 196 : if (y.getKind() == Kind::REGEXP_NONE)
3916 : : {
3917 : 10 : return returnRewrite(node, x, Rewrite::REPLACE_RE_ALL_NONE);
3918 : : }
3919 [ + + ]: 636 : }
3920 : :
3921 : 316 : return node;
3922 : 766 : }
3923 : :
3924 : 1305 : std::pair<size_t, size_t> SequencesRewriter::firstMatch(Node n, Node r)
3925 : : {
3926 : 1305 : Assert(n.isConst() && n.getType().isStringLike());
3927 [ - + ][ - + ]: 1305 : Assert(r.getType().isRegExp());
[ - - ]
3928 : 1305 : NodeManager* nm = nodeManager();
3929 : :
3930 : 2610 : Node re = nm->mkNode(Kind::REGEXP_CONCAT, r, d_sigmaStar);
3931 : 1305 : String s = n.getConst<String>();
3932 : :
3933 [ + + ]: 1305 : if (s.size() == 0)
3934 : : {
3935 [ + + ]: 154 : if (RegExpEntail::testConstStringInRegExp(s, r))
3936 : : {
3937 : 39 : return std::make_pair(0, 0);
3938 : : }
3939 : : else
3940 : : {
3941 : 115 : return std::make_pair(string::npos, string::npos);
3942 : : }
3943 : : }
3944 : :
3945 [ + + ]: 2269 : for (size_t i = 0, size = s.size(); i < size; i++)
3946 : : {
3947 : 1912 : String ss = s.substr(i);
3948 [ + + ]: 1912 : if (RegExpEntail::testConstStringInRegExp(ss, re))
3949 : : {
3950 [ + - ]: 1766 : for (size_t j = i; j <= size; j++)
3951 : : {
3952 : 1766 : String substr = s.substr(i, j - i);
3953 [ + + ]: 1766 : if (RegExpEntail::testConstStringInRegExp(substr, r))
3954 : : {
3955 : 794 : return std::make_pair(i, j);
3956 : : }
3957 [ + + ]: 1766 : }
3958 : : }
3959 [ + + ]: 1912 : }
3960 : :
3961 : 357 : return std::make_pair(string::npos, string::npos);
3962 : 1305 : }
3963 : :
3964 : 647 : Node SequencesRewriter::rewriteStrReverse(Node node)
3965 : : {
3966 [ - + ][ - + ]: 647 : Assert(node.getKind() == Kind::STRING_REV);
[ - - ]
3967 : 647 : NodeManager* nm = nodeManager();
3968 : 647 : Node x = node[0];
3969 [ + + ]: 647 : if (x.isConst())
3970 : : {
3971 : : // reverse the characters in the constant
3972 : 159 : Node retNode = Word::reverse(x);
3973 : 159 : return returnRewrite(node, retNode, Rewrite::STR_CONV_CONST);
3974 : 159 : }
3975 [ + + ]: 488 : else if (x.getKind() == Kind::STRING_CONCAT)
3976 : : {
3977 : 92 : std::vector<Node> children;
3978 [ + + ]: 278 : for (const Node& nc : x)
3979 : : {
3980 : 186 : children.push_back(nm->mkNode(Kind::STRING_REV, nc));
3981 : 186 : }
3982 : 92 : std::reverse(children.begin(), children.end());
3983 : : // rev( x1 ++ x2 ) --> rev( x2 ) ++ rev( x1 )
3984 : 92 : Node retNode = nm->mkNode(Kind::STRING_CONCAT, children);
3985 : 92 : return returnRewrite(node, retNode, Rewrite::STR_REV_MINSCOPE_CONCAT);
3986 : 92 : }
3987 [ + + ]: 396 : else if (x.getKind() == Kind::STRING_REV)
3988 : : {
3989 : : // rev( rev( x ) ) --> x
3990 : 12 : Node retNode = x[0];
3991 : 12 : return returnRewrite(node, retNode, Rewrite::STR_REV_IDEM);
3992 : 12 : }
3993 [ + - ][ + + ]: 384 : else if (x.getKind() == Kind::STRING_UNIT || x.getKind() == Kind::SEQ_UNIT)
[ + + ]
3994 : : {
3995 : : // rev( str.unit( x ) ) --> str.unit( x )
3996 : 14 : return returnRewrite(node, x, Rewrite::STR_REV_UNIT);
3997 : : }
3998 : 370 : return node;
3999 : 647 : }
4000 : :
4001 : 998 : Node SequencesRewriter::rewritePrefixSuffix(Node n)
4002 : : {
4003 [ + + ][ + - ]: 998 : Assert(n.getKind() == Kind::STRING_PREFIX
[ - + ][ - + ]
[ - - ]
4004 : : || n.getKind() == Kind::STRING_SUFFIX);
4005 : 998 : bool isPrefix = n.getKind() == Kind::STRING_PREFIX;
4006 [ + + ]: 998 : if (n[0] == n[1])
4007 : : {
4008 : 33 : Node ret = nodeManager()->mkConst(true);
4009 : 33 : return returnRewrite(n, ret, Rewrite::SUF_PREFIX_EQ);
4010 : 33 : }
4011 [ + + ]: 965 : if (n[0].isConst())
4012 : : {
4013 [ + + ]: 565 : if (Word::isEmpty(n[0]))
4014 : : {
4015 : 29 : Node ret = nodeManager()->mkConst(true);
4016 : 29 : return returnRewrite(n, ret, Rewrite::SUF_PREFIX_EMPTY_CONST);
4017 : 29 : }
4018 : : }
4019 [ + + ]: 936 : if (n[1].isConst())
4020 : : {
4021 : 331 : Node s = n[1];
4022 : 331 : size_t lenS = Word::getLength(s);
4023 [ + + ]: 331 : if (n[0].isConst())
4024 : : {
4025 : 109 : Node ret = nodeManager()->mkConst(false);
4026 : 109 : Node t = n[0];
4027 : 109 : size_t lenT = Word::getLength(t);
4028 [ + + ]: 109 : if (lenS >= lenT)
4029 : : {
4030 : 68 : if ((isPrefix && t == Word::prefix(s, lenT))
4031 : 68 : || (!isPrefix && t == Word::suffix(s, lenT)))
4032 : : {
4033 : 32 : ret = nodeManager()->mkConst(true);
4034 : : }
4035 : : }
4036 : 109 : return returnRewrite(n, ret, Rewrite::SUF_PREFIX_CONST);
4037 : 109 : }
4038 [ + + ]: 222 : else if (lenS == 0)
4039 : : {
4040 : 8 : Node ret = n[0].eqNode(n[1]);
4041 : 4 : return returnRewrite(n, ret, Rewrite::SUF_PREFIX_EMPTY);
4042 : 4 : }
4043 [ + - ]: 218 : else if (lenS == 1)
4044 : : {
4045 : : // (str.prefix x "A") and (str.suffix x "A") are equivalent to
4046 : : // (str.contains "A" x )
4047 : 436 : Node ret = nodeManager()->mkNode(Kind::STRING_CONTAINS, n[1], n[0]);
4048 : 218 : return returnRewrite(n, ret, Rewrite::SUF_PREFIX_CTN);
4049 : 218 : }
4050 [ - + ]: 331 : }
4051 : 1210 : Node lens = nodeManager()->mkNode(Kind::STRING_LENGTH, n[0]);
4052 : 1210 : Node lent = nodeManager()->mkNode(Kind::STRING_LENGTH, n[1]);
4053 : :
4054 : : // Check if we can turn the prefix/suffix into an equality by showing that the
4055 : : // prefix/suffix is at least as long as the string
4056 [ + + ]: 605 : if (d_arithEntail.check(lens, lent))
4057 : : {
4058 : 94 : Node retNode = n[0].eqNode(n[1]);
4059 : 47 : return returnRewrite(n, retNode, Rewrite::SUF_PREFIX_TO_EQS);
4060 : 47 : }
4061 : :
4062 : 558 : Node val;
4063 [ + + ]: 558 : if (isPrefix)
4064 : : {
4065 : 343 : val = nodeManager()->mkConstInt(cvc5::internal::Rational(0));
4066 : : }
4067 : : else
4068 : : {
4069 : 215 : val = nodeManager()->mkNode(Kind::SUB, lent, lens);
4070 : : }
4071 : :
4072 : : // general reduction to equality + substr
4073 : : Node retNode =
4074 : 1116 : n[0].eqNode(nodeManager()->mkNode(Kind::STRING_SUBSTR, n[1], val, lens));
4075 : :
4076 : 558 : return returnRewrite(n, retNode, Rewrite::SUF_PREFIX_ELIM);
4077 : 605 : }
4078 : :
4079 : 262 : Node SequencesRewriter::lengthPreserveRewrite(Node n)
4080 : : {
4081 : 262 : NodeManager* nm = nodeManager();
4082 : : Node len =
4083 : 524 : d_arithEntail.rewriteLengthIntro(nm->mkNode(Kind::STRING_LENGTH, n));
4084 : 262 : len = d_arithEntail.rewriteArith(len);
4085 : 524 : Node res = canonicalStrForSymbolicLength(len, n.getType());
4086 [ - + ]: 524 : return res.isNull() ? n : res;
4087 : 262 : }
4088 : :
4089 : 268 : Node SequencesRewriter::canonicalStrForSymbolicLength(Node len,
4090 : : TypeNode stype) const
4091 : : {
4092 : 268 : NodeManager* nm = nodeManager();
4093 : :
4094 : 268 : Node res;
4095 [ + + ]: 268 : if (len.isConst())
4096 : : {
4097 : : // c -> "A" repeated c times
4098 : 238 : Rational ratLen = len.getConst<Rational>();
4099 [ - + ][ - + ]: 238 : Assert(ratLen.getDenominator() == 1);
[ - - ]
4100 : 238 : Integer intLen = ratLen.getNumerator();
4101 : 238 : uint32_t u = intLen.getUnsignedInt();
4102 [ + - ]: 238 : if (stype.isString()) // string-only
4103 : : {
4104 : 238 : res = nm->mkConst(String(std::string(u, 'A')));
4105 : : }
4106 : : // we could do this for sequences, but we need to be careful: some
4107 : : // sorts do not permit values that the solver can handle (e.g. uninterpreted
4108 : : // sorts and arrays).
4109 : 238 : }
4110 [ + + ]: 30 : else if (len.getKind() == Kind::ADD)
4111 : : {
4112 : : // x + y -> norm(x) + norm(y)
4113 : 2 : NodeBuilder concatBuilder(nodeManager(), Kind::STRING_CONCAT);
4114 [ + + ]: 6 : for (const auto& n : len)
4115 : : {
4116 : 8 : Node sn = canonicalStrForSymbolicLength(n, stype);
4117 [ - + ]: 4 : if (sn.isNull())
4118 : : {
4119 : 0 : return Node::null();
4120 : : }
4121 : 4 : std::vector<Node> snChildren;
4122 : 4 : utils::getConcat(sn, snChildren);
4123 : 4 : concatBuilder.append(snChildren);
4124 [ + - ][ + - ]: 4 : }
4125 : 2 : res = concatBuilder.constructNode();
4126 [ + - ]: 2 : }
4127 [ + - ]: 2 : else if (len.getKind() == Kind::MULT && len.getNumChildren() == 2
4128 [ + + ][ + - ]: 30 : && len[0].isConst())
[ + + ][ + + ]
[ - - ]
4129 : : {
4130 : : // c * x -> norm(x) repeated c times
4131 : 2 : Rational ratReps = len[0].getConst<Rational>();
4132 [ - + ][ - + ]: 2 : Assert(ratReps.getDenominator() == 1);
[ - - ]
4133 : 2 : Integer intReps = ratReps.getNumerator();
4134 : :
4135 : 4 : Node nRep = canonicalStrForSymbolicLength(len[1], stype);
4136 [ - + ]: 2 : if (nRep.isNull())
4137 : : {
4138 : 0 : return Node::null();
4139 : : }
4140 : 2 : std::vector<Node> nRepChildren;
4141 : 2 : utils::getConcat(nRep, nRepChildren);
4142 : 2 : NodeBuilder concatBuilder(nodeManager(), Kind::STRING_CONCAT);
4143 [ + + ]: 6 : for (size_t i = 0, reps = intReps.getUnsignedInt(); i < reps; i++)
4144 : : {
4145 : 4 : concatBuilder.append(nRepChildren);
4146 : : }
4147 : 2 : res = concatBuilder.constructNode();
4148 [ + - ][ + - ]: 2 : }
[ + - ]
4149 [ + - ]: 26 : else if (len.getKind() == Kind::STRING_LENGTH)
4150 : : {
4151 : : // len(x) -> x
4152 : 26 : res = len[0];
4153 : : }
4154 : 268 : return res;
4155 : 268 : }
4156 : :
4157 : 3693 : Node SequencesRewriter::rewriteSeqUnit(Node node)
4158 : : {
4159 [ - + ][ - + ]: 3693 : Assert(node.getKind() == Kind::SEQ_UNIT);
[ - - ]
4160 : 3693 : NodeManager* nm = nodeManager();
4161 [ + + ]: 3693 : if (node[0].isConst())
4162 : : {
4163 : 1145 : std::vector<Node> seq;
4164 : 1145 : seq.push_back(node[0]);
4165 : : // important to take the type according to the operator here, not the
4166 : : // type of the argument
4167 : 1145 : TypeNode stype = node.getType().getSequenceElementType();
4168 : 1145 : Node ret = nm->mkConst(Sequence(stype, seq));
4169 : 1145 : return returnRewrite(node, ret, Rewrite::SEQ_UNIT_EVAL);
4170 : 1145 : }
4171 : 2548 : return node;
4172 : : }
4173 : :
4174 : 463071 : Node SequencesRewriter::returnRewrite(Node node, Node ret, Rewrite r)
4175 : : {
4176 [ + - ]: 926142 : Trace("strings-rewrite") << "Rewrite " << node << " to " << ret << " by " << r
4177 : 463071 : << "." << std::endl;
4178 [ + + ]: 463071 : if (d_statistics != nullptr)
4179 : : {
4180 : 458544 : (*d_statistics) << r;
4181 : : }
4182 : 463071 : return ret;
4183 : : }
4184 : :
4185 : : } // namespace strings
4186 : : } // namespace theory
4187 : : } // namespace cvc5::internal
|
