Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Aina Niemetz, Mathias Preiner
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
8 : : * in the top-level source directory and their institutional affiliations.
9 : : * All rights reserved. See the file COPYING in the top-level source
10 : : * directory for licensing information.
11 : : * ****************************************************************************
12 : : *
13 : : * Implementation of techniques for eliminating regular expressions.
14 : : */
15 : :
16 : : #include "theory/strings/regexp_elim.h"
17 : :
18 : : #include "expr/bound_var_manager.h"
19 : : #include "options/strings_options.h"
20 : : #include "proof/proof_node_manager.h"
21 : : #include "smt/env.h"
22 : : #include "theory/rewriter.h"
23 : : #include "theory/strings/regexp_entail.h"
24 : : #include "theory/strings/theory_strings_utils.h"
25 : : #include "theory/strings/word.h"
26 : : #include "util/rational.h"
27 : : #include "util/string.h"
28 : :
29 : : using namespace cvc5::internal::kind;
30 : :
31 : : namespace cvc5::internal {
32 : : namespace theory {
33 : : namespace strings {
34 : :
35 : : /**
36 : : * Attributes used for constructing unique bound variables. The following
37 : : * attributes are used to construct (deterministic) bound variables for
38 : : * eliminations within eliminateConcat and eliminateStar respectively.
39 : : */
40 : : struct ReElimConcatIndexAttributeId
41 : : {
42 : : };
43 : : typedef expr::Attribute<ReElimConcatIndexAttributeId, Node>
44 : : ReElimConcatIndexAttribute;
45 : : struct ReElimStarIndexAttributeId
46 : : {
47 : : };
48 : : typedef expr::Attribute<ReElimStarIndexAttributeId, Node>
49 : : ReElimStarIndexAttribute;
50 : :
51 : 49172 : RegExpElimination::RegExpElimination(Env& env, bool isAgg, context::Context* c)
52 : : : EnvObj(env),
53 : : d_isAggressive(isAgg),
54 : 98344 : d_epg(!env.isTheoryProofProducing()
55 : : ? nullptr
56 : 49172 : : new EagerProofGenerator(env, c, "RegExpElimination::epg"))
57 : : {
58 : 49172 : }
59 : :
60 : 310 : Node RegExpElimination::eliminate(Node atom, bool isAgg)
61 : : {
62 [ - + ][ - + ]: 310 : Assert(atom.getKind() == Kind::STRING_IN_REGEXP);
[ - - ]
63 [ + + ]: 310 : if (atom[1].getKind() == Kind::REGEXP_CONCAT)
64 : : {
65 : 192 : return eliminateConcat(atom, isAgg);
66 : : }
67 [ + - ]: 118 : else if (atom[1].getKind() == Kind::REGEXP_STAR)
68 : : {
69 : 118 : return eliminateStar(atom, isAgg);
70 : : }
71 : 0 : return Node::null();
72 : : }
73 : :
74 : 294 : TrustNode RegExpElimination::eliminateTrusted(Node atom)
75 : : {
76 : 588 : Node eatom = eliminate(atom, d_isAggressive);
77 [ + + ]: 294 : if (!eatom.isNull())
78 : : {
79 : : // Currently aggressive doesnt work due to fresh bound variables
80 [ + + ][ + + ]: 218 : if (isProofEnabled() && !d_isAggressive)
[ + + ]
81 : : {
82 : 20 : ProofNodeManager* pnm = d_env.getProofNodeManager();
83 : 40 : Node eq = atom.eqNode(eatom);
84 : 40 : Node aggn = NodeManager::currentNM()->mkConst(d_isAggressive);
85 : : std::shared_ptr<ProofNode> pn =
86 : 100 : pnm->mkNode(ProofRule::MACRO_RE_ELIM, {}, {atom, aggn}, eq);
87 : 20 : d_epg->setProofFor(eq, pn);
88 [ + - ]: 20 : return TrustNode::mkTrustRewrite(atom, eatom, d_epg.get());
89 : : }
90 : 198 : return TrustNode::mkTrustRewrite(atom, eatom, nullptr);
91 : : }
92 : 76 : return TrustNode::null();
93 : : }
94 : :
95 : 192 : Node RegExpElimination::eliminateConcat(Node atom, bool isAgg)
96 : : {
97 : 192 : NodeManager* nm = NodeManager::currentNM();
98 : 192 : BoundVarManager* bvm = nm->getBoundVarManager();
99 : 384 : Node x = atom[0];
100 : 384 : Node lenx = nm->mkNode(Kind::STRING_LENGTH, x);
101 : 384 : Node re = atom[1];
102 : 384 : Node zero = nm->mkConstInt(Rational(0));
103 : 384 : std::vector<Node> children;
104 : 192 : utils::getConcat(re, children);
105 : :
106 : : // If it can be reduced to memberships in fixed length regular expressions.
107 : : // This includes concatenations where at most one child is of the form
108 : : // (re.* re.allchar), which we abbreviate _* below, and all other children
109 : : // have a fixed length.
110 : : // The intuition why this is a "non-aggressive" rewrite is that membership
111 : : // into fixed length regular expressions are easy to handle.
112 : : // the index of _* in re
113 : 192 : unsigned pivotIndex = 0;
114 : 192 : bool hasPivotIndex = false;
115 : 192 : bool hasFixedLength = true;
116 : 384 : std::vector<Node> childLengths;
117 : 384 : std::vector<Node> childLengthsPostPivot;
118 [ + + ]: 872 : for (unsigned i = 0, size = children.size(); i < size; i++)
119 : : {
120 : 1360 : Node c = children[i];
121 : 1360 : Node fl = RegExpEntail::getFixedLengthForRegexp(c);
122 [ + + ]: 680 : if (fl.isNull())
123 : : {
124 [ + + ]: 208 : if (!hasPivotIndex && c.getKind() == Kind::REGEXP_STAR
125 [ + + ][ + + ]: 464 : && c[0].getKind() == Kind::REGEXP_ALLCHAR)
[ + + ][ + + ]
[ - - ]
126 : : {
127 : 40 : hasPivotIndex = true;
128 : 40 : pivotIndex = i;
129 : : // zero is used in sum below and is used for concat-fixed-len
130 : 40 : fl = zero;
131 : : }
132 : : else
133 : : {
134 : 216 : hasFixedLength = false;
135 : : }
136 : : }
137 [ + + ]: 680 : if (!fl.isNull())
138 : : {
139 : 464 : childLengths.push_back(fl);
140 [ + + ]: 464 : if (hasPivotIndex)
141 : : {
142 : 190 : childLengthsPostPivot.push_back(fl);
143 : : }
144 : : }
145 : : }
146 : 192 : Node lenSum = childLengths.size() > 1
147 : : ? nm->mkNode(Kind::ADD, childLengths)
148 [ + + ][ + + ]: 384 : : (childLengths.empty() ? zero : childLengths[0]);
149 : : // if we have a fixed length
150 [ + + ]: 192 : if (hasFixedLength)
151 : : {
152 [ - + ][ - + ]: 34 : Assert(re.getNumChildren() == children.size());
[ - - ]
153 : 68 : std::vector<Node> conc;
154 : 34 : conc.push_back(
155 [ + + ]: 68 : nm->mkNode(hasPivotIndex ? Kind::GEQ : Kind::EQUAL, lenx, lenSum));
156 : 68 : Node currEnd = zero;
157 [ + + ]: 222 : for (unsigned i = 0, size = childLengths.size(); i < size; i++)
158 : : {
159 [ + + ][ + + ]: 188 : if (hasPivotIndex && i == pivotIndex)
160 : : {
161 : 4 : Node ppSum = childLengthsPostPivot.size() == 1
162 : 0 : ? childLengthsPostPivot[0]
163 [ - + ]: 4 : : nm->mkNode(Kind::ADD, childLengthsPostPivot);
164 : 4 : currEnd = nm->mkNode(Kind::SUB, lenx, ppSum);
165 : : }
166 : : else
167 : : {
168 : : Node curr =
169 : 368 : nm->mkNode(Kind::STRING_SUBSTR, x, currEnd, childLengths[i]);
170 : : // We do not need to include memberships of the form
171 : : // (str.substr x n 1) in re.allchar
172 : : // since we know that by construction, n < len( x ).
173 [ + + ]: 184 : if (re[i].getKind() != Kind::REGEXP_ALLCHAR)
174 : : {
175 : 306 : Node currMem = nm->mkNode(Kind::STRING_IN_REGEXP, curr, re[i]);
176 : 102 : conc.push_back(currMem);
177 : : }
178 : 184 : currEnd = nm->mkNode(Kind::ADD, currEnd, childLengths[i]);
179 : : }
180 : : }
181 : 34 : Node res = nm->mkNode(Kind::AND, conc);
182 : : // For example:
183 : : // x in re.++(re.union(re.range("A", "J"), re.range("N", "Z")), "AB") -->
184 : : // len( x ) = 3 ^
185 : : // substr(x,0,1) in re.union(re.range("A", "J"), re.range("N", "Z")) ^
186 : : // substr(x,1,2) in "AB"
187 : : // An example with a pivot index:
188 : : // x in re.++( "AB" ++ _* ++ "C" ) -->
189 : : // len( x ) >= 3 ^
190 : : // substr( x, 0, 2 ) in "AB" ^
191 : : // substr( x, len( x ) - 1, 1 ) in "C"
192 : 34 : return returnElim(atom, res, "concat-fixed-len");
193 : : }
194 : :
195 : : // memberships of the form x in re.++ * s1 * ... * sn *, where * are
196 : : // any number of repetitions (exact or indefinite) of re.allchar.
197 [ + - ]: 158 : Trace("re-elim-debug") << "Try re concat with gaps " << atom << std::endl;
198 : 158 : bool onlySigmasAndConsts = true;
199 : 316 : std::vector<Node> sep_children;
200 : 316 : std::vector<unsigned> gap_minsize;
201 : 316 : std::vector<bool> gap_exact;
202 : : // the first gap is initially strict zero
203 : 158 : gap_minsize.push_back(0);
204 : 158 : gap_exact.push_back(true);
205 [ + + ]: 432 : for (const Node& c : children)
206 : : {
207 [ + - ]: 396 : Trace("re-elim-debug") << " " << c << std::endl;
208 : 396 : onlySigmasAndConsts = false;
209 [ + + ]: 396 : if (c.getKind() == Kind::STRING_TO_REGEXP)
210 : : {
211 : 178 : onlySigmasAndConsts = true;
212 : 178 : sep_children.push_back(c[0]);
213 : : // the next gap is initially strict zero
214 : 178 : gap_minsize.push_back(0);
215 : 178 : gap_exact.push_back(true);
216 : : }
217 : 654 : else if (c.getKind() == Kind::REGEXP_STAR
218 [ + + ][ + + ]: 218 : && c[0].getKind() == Kind::REGEXP_ALLCHAR)
[ + + ][ + + ]
[ - - ]
219 : : {
220 : : // found a gap of any size
221 : 84 : onlySigmasAndConsts = true;
222 : 84 : gap_exact[gap_exact.size() - 1] = false;
223 : : }
224 [ + + ]: 134 : else if (c.getKind() == Kind::REGEXP_ALLCHAR)
225 : : {
226 : : // add one to the minimum size of the gap
227 : 12 : onlySigmasAndConsts = true;
228 : 12 : gap_minsize[gap_minsize.size() - 1]++;
229 : : }
230 [ + + ]: 396 : if (!onlySigmasAndConsts)
231 : : {
232 [ + - ]: 122 : Trace("re-elim-debug") << "...cannot handle " << c << std::endl;
233 : 122 : break;
234 : : }
235 : : }
236 : : // we should always rewrite concatenations that are purely re.allchar
237 : : // and re.*( re.allchar ).
238 [ + + ][ - + ]: 158 : Assert(!onlySigmasAndConsts || !sep_children.empty());
[ - + ][ - - ]
239 [ + + ][ + - ]: 158 : if (onlySigmasAndConsts && !sep_children.empty())
[ + + ]
240 : : {
241 : 36 : bool canProcess = true;
242 : 36 : std::vector<Node> conj;
243 : : // The following constructs a set of constraints that encodes that a
244 : : // set of string terms are found, in order, in string x.
245 : : // prev_end stores the current (symbolic) index in x that we are
246 : : // searching.
247 : 36 : Node prev_end = zero;
248 : : // the symbolic index we start searching, for each child in sep_children.
249 : 36 : std::vector<Node> prev_ends;
250 : 36 : unsigned gap_minsize_end = gap_minsize.back();
251 : 36 : bool gap_exact_end = gap_exact.back();
252 : 36 : std::vector<Node> non_greedy_find_vars;
253 [ + + ]: 144 : for (unsigned i = 0, size = sep_children.size(); i < size; i++)
254 : : {
255 [ + + ]: 108 : if (gap_minsize[i] > 0)
256 : : {
257 : : // the gap to this child is at least gap_minsize[i]
258 : 24 : prev_end = nm->mkNode(
259 : 36 : Kind::ADD, prev_end, nm->mkConstInt(Rational(gap_minsize[i])));
260 : : }
261 : 108 : prev_ends.push_back(prev_end);
262 : 108 : Node sc = sep_children[i];
263 : 108 : Node lensc = nm->mkNode(Kind::STRING_LENGTH, sc);
264 [ + + ]: 108 : if (gap_exact[i])
265 : : {
266 : : // if the gap is exact, it is a substring constraint
267 : 72 : Node curr = prev_end;
268 : 72 : Node ss = nm->mkNode(Kind::STRING_SUBSTR, x, curr, lensc);
269 : 36 : conj.push_back(ss.eqNode(sc));
270 : 36 : prev_end = nm->mkNode(Kind::ADD, curr, lensc);
271 : : }
272 : : else
273 : : {
274 : : // otherwise, we can use indexof to represent some next occurrence
275 [ + + ][ - + ]: 72 : if (gap_exact[i + 1] && i + 1 != size)
[ - + ]
276 : : {
277 [ - - ]: 0 : if (!isAgg)
278 : : {
279 : 0 : canProcess = false;
280 : 0 : break;
281 : : }
282 : : // if the gap after this one is strict, we need a non-greedy find
283 : : // thus, we add a symbolic constant
284 : : Node cacheVal =
285 : 0 : BoundVarManager::getCacheValue(atom, nm->mkConstInt(Rational(i)));
286 : 0 : TypeNode intType = nm->integerType();
287 : : Node k =
288 : 0 : bvm->mkBoundVar<ReElimConcatIndexAttribute>(cacheVal, intType);
289 : 0 : non_greedy_find_vars.push_back(k);
290 : 0 : prev_end = nm->mkNode(Kind::ADD, prev_end, k);
291 : : }
292 : 216 : Node curr = nm->mkNode(Kind::STRING_INDEXOF, x, sc, prev_end);
293 : 144 : Node idofFind = curr.eqNode(nm->mkConstInt(Rational(-1))).negate();
294 : 72 : conj.push_back(idofFind);
295 : 72 : prev_end = nm->mkNode(Kind::ADD, curr, lensc);
296 : : }
297 : : }
298 : :
299 [ + - ]: 36 : if (canProcess)
300 : : {
301 : : // since sep_children is non-empty, conj is non-empty
302 [ - + ][ - + ]: 36 : Assert(!conj.empty());
[ - - ]
303 : : // Process the last gap, if necessary.
304 : : // Notice that if the last gap is not exact and its minsize is zero,
305 : : // then the last indexof/substr constraint entails the following
306 : : // constraint, so it is not necessary to add.
307 : : // Below, we may write "A" for (str.to.re "A") and _ for re.allchar:
308 : 72 : Node cEnd = nm->mkConstInt(Rational(gap_minsize_end));
309 [ + + ]: 36 : if (gap_exact_end)
310 : : {
311 [ - + ][ - + ]: 24 : Assert(!sep_children.empty());
[ - - ]
312 : : // if it is strict, it corresponds to a substr case.
313 : : // For example:
314 : : // x in (re.++ "A" (re.* _) "B" _ _) --->
315 : : // ... ^ "B" = substr( x, len( x ) - 3, 1 ) ^ ...
316 : 48 : Node sc = sep_children.back();
317 : 48 : Node lenSc = nm->mkNode(Kind::STRING_LENGTH, sc);
318 : : Node loc =
319 : 72 : nm->mkNode(Kind::SUB, lenx, nm->mkNode(Kind::ADD, lenSc, cEnd));
320 : 72 : Node scc = sc.eqNode(nm->mkNode(Kind::STRING_SUBSTR, x, loc, lenSc));
321 : : // We also must ensure that we fit. This constraint is necessary in
322 : : // addition to the constraint above. Take this example:
323 : : // x in (re.++ "A" _ (re.* _) "B" _) --->
324 : : // substr( x, 0, 1 ) = "A" ^ // find "A"
325 : : // indexof( x, "B", 2 ) != -1 ^ // find "B" >=1 after "A"
326 : : // substr( x, len(x)-2, 1 ) = "B" ^ // "B" is at end - 2.
327 : : // indexof( x, "B", 2 ) <= len( x ) - 2
328 : : // The last constaint ensures that the second and third constraints
329 : : // may refer to the same "B". If it were not for the last constraint, it
330 : : // would have been the case than "ABB" would be a model for x, where
331 : : // the second constraint refers to the third position, and the third
332 : : // constraint refers to the second position.
333 : : //
334 : : // With respect to the above example, the following is an optimization.
335 : : // For that example, we instead produce:
336 : : // x in (re.++ "A" _ (re.* _) "B" _) --->
337 : : // substr( x, 0, 1 ) = "A" ^ // find "A"
338 : : // substr( x, len(x)-2, 1 ) = "B" ^ // "B" is at end - 2
339 : : // 2 <= len( x ) - 2
340 : : // The intuition is that above, there are two constraints that insist
341 : : // that "B" is found, whereas we only need one. The last constraint
342 : : // above says that the "B" we find at end-2 can be found >=1 after
343 : : // the "A".
344 : 24 : conj.pop_back();
345 : : Node fit = nm->mkNode(
346 : 48 : gap_exact[sep_children.size() - 1] ? Kind::EQUAL : Kind::LEQ,
347 : 24 : prev_ends.back(),
348 [ - + ]: 120 : loc);
349 : :
350 : 24 : conj.push_back(scc);
351 : 24 : conj.push_back(fit);
352 : : }
353 [ - + ]: 12 : else if (gap_minsize_end > 0)
354 : : {
355 : : // if it is non-strict, we are in a "greedy find" situtation where
356 : : // we just need to ensure that the next occurrence fits.
357 : : // For example:
358 : : // x in (re.++ "A" (re.* _) "B" _ _ (re.* _)) --->
359 : : // ... ^ indexof( x, "B", 1 ) + 2 <= len( x )
360 : : Node fit =
361 : 0 : nm->mkNode(Kind::LEQ, nm->mkNode(Kind::ADD, prev_end, cEnd), lenx);
362 : 0 : conj.push_back(fit);
363 : : }
364 : 36 : Node res = nm->mkAnd(conj);
365 : : // process the non-greedy find variables
366 [ - + ]: 36 : if (!non_greedy_find_vars.empty())
367 : : {
368 : 0 : std::vector<Node> children2;
369 [ - - ]: 0 : for (const Node& v : non_greedy_find_vars)
370 : : {
371 : : Node bound = nm->mkNode(Kind::AND,
372 : 0 : nm->mkNode(Kind::LEQ, zero, v),
373 : 0 : nm->mkNode(Kind::LT, v, lenx));
374 : 0 : children2.push_back(bound);
375 : : }
376 : 0 : children2.push_back(res);
377 : 0 : Node body = nm->mkNode(Kind::AND, children2);
378 : 0 : Node bvl = nm->mkNode(Kind::BOUND_VAR_LIST, non_greedy_find_vars);
379 : 0 : res = utils::mkForallInternal(bvl, body.negate()).negate();
380 : : }
381 : : // must also give a minimum length requirement
382 : 36 : res = nm->mkNode(Kind::AND, res, nm->mkNode(Kind::GEQ, lenx, lenSum));
383 : : // Examples of this elimination:
384 : : // x in (re.++ "A" (re.* _) "B" (re.* _)) --->
385 : : // substr(x,0,1)="A" ^ indexof(x,"B",1)!=-1
386 : : // x in (re.++ (re.* _) "A" _ _ _ (re.* _) "B" _ _ (re.* _)) --->
387 : : // indexof(x,"A",0)!=-1 ^
388 : : // indexof( x, "B", indexof( x, "A", 0 ) + 1 + 3 ) != -1 ^
389 : : // indexof( x, "B", indexof( x, "A", 0 ) + 1 + 3 )+1+2 <= len(x) ^
390 : : // len(x) >= 7
391 : :
392 : : // An example of a non-greedy find:
393 : : // x in re.++( re.*( _ ), "A", _, "B", re.*( _ ) ) --->
394 : : // (exists k. 0 <= k < len( x ) ^
395 : : // indexof( x, "A", k ) != -1 ^
396 : : // substr( x, indexof( x, "A", k )+2, 1 ) = "B") ^
397 : : // len(x) >= 3
398 : 36 : return returnElim(atom, res, "concat-with-gaps");
399 : : }
400 : : }
401 : :
402 [ + + ]: 122 : if (!isAgg)
403 : : {
404 : 40 : return Node::null();
405 : : }
406 : : // only aggressive rewrites below here
407 : :
408 : : // if the first or last child is constant string, we can split the membership
409 : : // into a conjunction of two memberships.
410 : 164 : Node sStartIndex = zero;
411 : 164 : Node sLength = lenx;
412 : 164 : std::vector<Node> sConstraints;
413 : 164 : std::vector<Node> rexpElimChildren;
414 : 82 : unsigned nchildren = children.size();
415 [ - + ][ - + ]: 82 : Assert(nchildren > 1);
[ - - ]
416 [ + + ]: 246 : for (unsigned r = 0; r < 2; r++)
417 : : {
418 [ + + ]: 164 : unsigned index = r == 0 ? 0 : nchildren - 1;
419 : 328 : Node c = children[index];
420 [ + + ]: 164 : if (c.getKind() == Kind::STRING_TO_REGEXP)
421 : : {
422 [ + + ][ - + ]: 74 : Assert(children[index + (r == 0 ? 1 : -1)].getKind()
[ - + ][ - - ]
423 : : != Kind::STRING_TO_REGEXP);
424 : 148 : Node s = c[0];
425 : 148 : Node lens = nm->mkNode(Kind::STRING_LENGTH, s);
426 : 160 : Node sss = r == 0 ? zero : nm->mkNode(Kind::SUB, lenx, lens);
427 : 148 : Node ss = nm->mkNode(Kind::STRING_SUBSTR, x, sss, lens);
428 : 74 : sConstraints.push_back(ss.eqNode(s));
429 [ + + ]: 74 : if (r == 0)
430 : : {
431 : 62 : sStartIndex = lens;
432 : : }
433 [ + - ][ + + ]: 12 : else if (r == 1 && sConstraints.size() == 2)
[ + + ]
434 : : {
435 : : // first and last children cannot overlap
436 : 6 : Node bound = nm->mkNode(Kind::GEQ, sss, sStartIndex);
437 : 2 : sConstraints.push_back(bound);
438 : : }
439 : 74 : sLength = nm->mkNode(Kind::SUB, sLength, lens);
440 : : }
441 [ + + ][ + + ]: 164 : if (r == 1 && !sConstraints.empty())
[ + + ]
442 : : {
443 : : // add the middle children
444 [ + + ]: 74 : for (unsigned i = 1; i < (nchildren - 1); i++)
445 : : {
446 : 2 : rexpElimChildren.push_back(children[i]);
447 : : }
448 : : }
449 [ + + ]: 164 : if (c.getKind() != Kind::STRING_TO_REGEXP)
450 : : {
451 : 90 : rexpElimChildren.push_back(c);
452 : : }
453 : : }
454 [ + + ]: 82 : if (!sConstraints.empty())
455 : : {
456 : 216 : Node ss = nm->mkNode(Kind::STRING_SUBSTR, x, sStartIndex, sLength);
457 [ - + ][ - + ]: 72 : Assert(!rexpElimChildren.empty());
[ - - ]
458 : 144 : Node regElim = utils::mkConcat(rexpElimChildren, nm->regExpType());
459 : 72 : sConstraints.push_back(nm->mkNode(Kind::STRING_IN_REGEXP, ss, regElim));
460 : 72 : Node ret = nm->mkNode(Kind::AND, sConstraints);
461 : : // e.g.
462 : : // x in re.++( "A", R ) ---> substr(x,0,1)="A" ^ substr(x,1,len(x)-1) in R
463 : 72 : return returnElim(atom, ret, "concat-splice");
464 : : }
465 [ - + ][ - + ]: 10 : Assert(nchildren > 1);
[ - - ]
466 [ + - ]: 20 : for (unsigned i = 0; i < nchildren; i++)
467 : : {
468 [ + + ]: 20 : if (children[i].getKind() == Kind::STRING_TO_REGEXP)
469 : : {
470 : 20 : Node s = children[i][0];
471 : 20 : Node lens = nm->mkNode(Kind::STRING_LENGTH, s);
472 : : // there exists an index in this string such that the substring is this
473 : 20 : Node k;
474 : 20 : std::vector<Node> echildren;
475 [ - + ]: 10 : if (i == 0)
476 : : {
477 : 0 : k = zero;
478 : : }
479 [ - + ]: 10 : else if (i + 1 == nchildren)
480 : : {
481 : 0 : k = nm->mkNode(Kind::SUB, lenx, lens);
482 : : }
483 : : else
484 : : {
485 : : Node cacheVal =
486 : 30 : BoundVarManager::getCacheValue(atom, nm->mkConstInt(Rational(i)));
487 : 20 : TypeNode intType = nm->integerType();
488 : 10 : k = bvm->mkBoundVar<ReElimConcatIndexAttribute>(cacheVal, intType);
489 : : Node bound = nm->mkNode(
490 : : Kind::AND,
491 : 20 : nm->mkNode(Kind::LEQ, zero, k),
492 : 50 : nm->mkNode(Kind::LEQ, k, nm->mkNode(Kind::SUB, lenx, lens)));
493 : 10 : echildren.push_back(bound);
494 : : }
495 : 30 : Node substrEq = nm->mkNode(Kind::STRING_SUBSTR, x, k, lens).eqNode(s);
496 : 10 : echildren.push_back(substrEq);
497 [ + - ]: 10 : if (i > 0)
498 : : {
499 : 20 : std::vector<Node> rprefix;
500 : 10 : rprefix.insert(rprefix.end(), children.begin(), children.begin() + i);
501 : 20 : Node rpn = utils::mkConcat(rprefix, nm->regExpType());
502 : : Node substrPrefix =
503 : : nm->mkNode(Kind::STRING_IN_REGEXP,
504 : 20 : nm->mkNode(Kind::STRING_SUBSTR, x, zero, k),
505 : 40 : rpn);
506 : 10 : echildren.push_back(substrPrefix);
507 : : }
508 [ + - ]: 10 : if (i + 1 < nchildren)
509 : : {
510 : 20 : std::vector<Node> rsuffix;
511 : 10 : rsuffix.insert(rsuffix.end(), children.begin() + i + 1, children.end());
512 : 20 : Node rps = utils::mkConcat(rsuffix, nm->regExpType());
513 : 30 : Node ks = nm->mkNode(Kind::ADD, k, lens);
514 : : Node substrSuffix = nm->mkNode(
515 : : Kind::STRING_IN_REGEXP,
516 : 20 : nm->mkNode(
517 : 20 : Kind::STRING_SUBSTR, x, ks, nm->mkNode(Kind::SUB, lenx, ks)),
518 : 40 : rps);
519 : 10 : echildren.push_back(substrSuffix);
520 : : }
521 : 10 : Node body = nm->mkNode(Kind::AND, echildren);
522 [ + - ]: 10 : if (k.getKind() == Kind::BOUND_VARIABLE)
523 : : {
524 : 10 : Node bvl = nm->mkNode(Kind::BOUND_VAR_LIST, k);
525 : 10 : body = utils::mkForallInternal(bvl, body.negate()).negate();
526 : : }
527 : : // e.g. x in re.++( R1, "AB", R2 ) --->
528 : : // exists k.
529 : : // 0 <= k <= (len(x)-2) ^
530 : : // substr( x, k, 2 ) = "AB" ^
531 : : // substr( x, 0, k ) in R1 ^
532 : : // substr( x, k+2, len(x)-(k+2) ) in R2
533 : 10 : return returnElim(atom, body, "concat-find");
534 : : }
535 : : }
536 : 0 : return Node::null();
537 : : }
538 : :
539 : 118 : Node RegExpElimination::eliminateStar(Node atom, bool isAgg)
540 : : {
541 [ + + ]: 118 : if (!isAgg)
542 : : {
543 : 22 : return Node::null();
544 : : }
545 : : // only aggressive rewrites below here
546 : :
547 : 96 : NodeManager* nm = NodeManager::currentNM();
548 : 96 : BoundVarManager* bvm = nm->getBoundVarManager();
549 : 192 : Node x = atom[0];
550 : 192 : Node lenx = nm->mkNode(Kind::STRING_LENGTH, x);
551 : 192 : Node re = atom[1];
552 : 192 : Node zero = nm->mkConstInt(Rational(0));
553 : : // for regular expression star,
554 : : // if the period is a fixed constant, we can turn it into a bounded
555 : : // quantifier
556 : 192 : std::vector<Node> disj;
557 [ + + ]: 96 : if (re[0].getKind() == Kind::REGEXP_UNION)
558 : : {
559 [ + + ]: 30 : for (const Node& r : re[0])
560 : : {
561 : 20 : disj.push_back(r);
562 : : }
563 : : }
564 : : else
565 : : {
566 : 86 : disj.push_back(re[0]);
567 : : }
568 : 96 : bool lenOnePeriod = true;
569 : 192 : std::vector<Node> char_constraints;
570 : 192 : TypeNode intType = nm->integerType();
571 : 288 : Node index = bvm->mkBoundVar<ReElimStarIndexAttribute>(atom, intType);
572 : : Node substr_ch =
573 : 288 : nm->mkNode(Kind::STRING_SUBSTR, x, index, nm->mkConstInt(Rational(1)));
574 : : // handle the case where it is purely characters
575 [ + + ]: 148 : for (const Node& r : disj)
576 : : {
577 [ - + ][ - + ]: 106 : Assert(r.getKind() != Kind::REGEXP_UNION);
[ - - ]
578 [ - + ][ - + ]: 106 : Assert(r.getKind() != Kind::REGEXP_ALLCHAR);
[ - - ]
579 : 106 : lenOnePeriod = false;
580 : : // lenOnePeriod is true if this regular expression is a single character
581 : : // regular expression
582 [ + + ]: 106 : if (r.getKind() == Kind::STRING_TO_REGEXP)
583 : : {
584 : 172 : Node s = r[0];
585 [ + + ][ + + ]: 86 : if (s.isConst() && s.getConst<String>().size() == 1)
[ + + ]
586 : : {
587 : 42 : lenOnePeriod = true;
588 : : }
589 : : }
590 [ + + ]: 20 : else if (r.getKind() == Kind::REGEXP_RANGE)
591 : : {
592 : 10 : lenOnePeriod = true;
593 : : }
594 [ + + ]: 106 : if (!lenOnePeriod)
595 : : {
596 : 54 : break;
597 : : }
598 : : else
599 : : {
600 : 156 : Node regexp_ch = nm->mkNode(Kind::STRING_IN_REGEXP, substr_ch, r);
601 : 52 : char_constraints.push_back(regexp_ch);
602 : : }
603 : : }
604 [ + + ]: 96 : if (lenOnePeriod)
605 : : {
606 [ - + ][ - + ]: 42 : Assert(!char_constraints.empty());
[ - - ]
607 : : Node bound = nm->mkNode(Kind::AND,
608 : 84 : nm->mkNode(Kind::LEQ, zero, index),
609 : 210 : nm->mkNode(Kind::LT, index, lenx));
610 : 42 : Node conc = char_constraints.size() == 1
611 : 42 : ? char_constraints[0]
612 [ + - ]: 126 : : nm->mkNode(Kind::OR, char_constraints);
613 : 126 : Node body = nm->mkNode(Kind::OR, bound.negate(), conc);
614 : 84 : Node bvl = nm->mkNode(Kind::BOUND_VAR_LIST, index);
615 : 84 : Node res = utils::mkForallInternal(bvl, body);
616 : : // e.g.
617 : : // x in (re.* (re.union "A" "B" )) --->
618 : : // forall k. 0<=k<len(x) => (substr(x,k,1) in "A" OR substr(x,k,1) in "B")
619 : 42 : return returnElim(atom, res, "star-char");
620 : : }
621 : : // otherwise, for stars of constant length these are periodic
622 [ + + ]: 54 : if (disj.size() == 1)
623 : : {
624 : 44 : Node r = disj[0];
625 [ + - ]: 44 : if (r.getKind() == Kind::STRING_TO_REGEXP)
626 : : {
627 : 44 : Node s = r[0];
628 [ + + ]: 44 : if (s.isConst())
629 : : {
630 : 120 : Node lens = nm->mkConstInt(Word::getLength(s));
631 [ - + ][ - + ]: 40 : Assert(lens.getConst<Rational>().sgn() > 0);
[ - - ]
632 : 80 : std::vector<Node> conj;
633 : : // lens is a positive constant, so it is safe to use total div/mod here.
634 : : Node bound = nm->mkNode(
635 : : Kind::AND,
636 : 80 : nm->mkNode(Kind::LEQ, zero, index),
637 : 80 : nm->mkNode(Kind::LT,
638 : : index,
639 : 280 : nm->mkNode(Kind::INTS_DIVISION_TOTAL, lenx, lens)));
640 : 120 : Node conc = nm->mkNode(Kind::STRING_SUBSTR,
641 : : x,
642 : 80 : nm->mkNode(Kind::MULT, index, lens),
643 : : lens)
644 : 80 : .eqNode(s);
645 : 120 : Node body = nm->mkNode(Kind::OR, bound.negate(), conc);
646 : 80 : Node bvl = nm->mkNode(Kind::BOUND_VAR_LIST, index);
647 : 80 : Node res = utils::mkForallInternal(bvl, body);
648 : 120 : res = nm->mkNode(
649 : : Kind::AND,
650 : 80 : nm->mkNode(Kind::INTS_MODULUS_TOTAL, lenx, lens).eqNode(zero),
651 : 40 : res);
652 : : // e.g.
653 : : // x in ("abc")* --->
654 : : // forall k. 0 <= k < (len( x ) div 3) => substr(x,3*k,3) = "abc" ^
655 : : // len(x) mod 3 = 0
656 : 40 : return returnElim(atom, res, "star-constant");
657 : : }
658 : : }
659 : : }
660 : 14 : return Node::null();
661 : : }
662 : :
663 : 234 : Node RegExpElimination::returnElim(Node atom, Node atomElim, const char* id)
664 : : {
665 [ + - ]: 468 : Trace("re-elim") << "re-elim: " << atom << " to " << atomElim << " by " << id
666 : 234 : << "." << std::endl;
667 : 234 : return atomElim;
668 : : }
669 : 218 : bool RegExpElimination::isProofEnabled() const
670 : : {
671 : 218 : return d_env.isTheoryProofProducing();
672 : : }
673 : :
674 : : } // namespace strings
675 : : } // namespace theory
676 : : } // namespace cvc5::internal
|
