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 rewrite rules for string-specific operators in
11 : : * theory of strings.
12 : : */
13 : :
14 : : #include "theory/strings/strings_rewriter.h"
15 : :
16 : : #include "expr/node_builder.h"
17 : : #include "theory/strings/theory_strings_utils.h"
18 : : #include "util/rational.h"
19 : : #include "util/string.h"
20 : :
21 : : using namespace cvc5::internal::kind;
22 : :
23 : : namespace cvc5::internal {
24 : : namespace theory {
25 : : namespace strings {
26 : :
27 : 51052 : StringsRewriter::StringsRewriter(NodeManager* nm,
28 : : ArithEntail& ae,
29 : : StringsEntail& se,
30 : : HistogramStat<Rewrite>* statistics,
31 : 51052 : uint32_t alphaCard)
32 : 51052 : : SequencesRewriter(nm, ae, se, statistics), d_alphaCard(alphaCard)
33 : : {
34 : 51052 : }
35 : :
36 : 1582198 : RewriteResponse StringsRewriter::postRewrite(TNode node)
37 : : {
38 [ + - ]: 3164396 : Trace("strings-postrewrite")
39 : 1582198 : << "Strings::StringsRewriter::postRewrite start " << node << std::endl;
40 : :
41 : 1582198 : Node retNode = node;
42 : 1582198 : Kind nk = node.getKind();
43 [ + + ]: 1582198 : if (nk == Kind::STRING_LT)
44 : : {
45 : 114 : retNode = rewriteStringLt(node);
46 : : }
47 [ + + ]: 1582084 : else if (nk == Kind::STRING_LEQ)
48 : : {
49 : 1399 : retNode = rewriteStringLeq(node);
50 : : }
51 [ + + ][ + + ]: 1580685 : else if (nk == Kind::STRING_TO_LOWER || nk == Kind::STRING_TO_UPPER)
52 : : {
53 : 1070 : retNode = rewriteStrConvert(node);
54 : : }
55 [ + + ]: 1579615 : else if (nk == Kind::STRING_IS_DIGIT)
56 : : {
57 : 34 : retNode = rewriteStringIsDigit(node);
58 : : }
59 [ + + ]: 1579581 : else if (nk == Kind::STRING_ITOS)
60 : : {
61 : 1518 : retNode = rewriteIntToStr(node);
62 : : }
63 [ + + ]: 1578063 : else if (nk == Kind::STRING_STOI)
64 : : {
65 : 1298 : retNode = rewriteStrToInt(node);
66 : : }
67 [ + + ]: 1576765 : else if (nk == Kind::STRING_TO_CODE)
68 : : {
69 : 9084 : retNode = rewriteStringToCode(node);
70 : : }
71 [ + + ]: 1567681 : else if (nk == Kind::STRING_FROM_CODE)
72 : : {
73 : 259 : retNode = rewriteStringFromCode(node);
74 : : }
75 [ - + ]: 1567422 : else if (nk == Kind::STRING_UNIT)
76 : : {
77 : 0 : retNode = rewriteStringUnit(node);
78 : : }
79 : : else
80 : : {
81 : 1567422 : return SequencesRewriter::postRewrite(node);
82 : : }
83 : :
84 [ + - ]: 29552 : Trace("strings-postrewrite")
85 : 0 : << "Strings::StringsRewriter::postRewrite returning " << retNode
86 : 14776 : << std::endl;
87 [ + + ]: 14776 : if (node != retNode)
88 : : {
89 [ + - ]: 7028 : Trace("strings-rewrite-debug") << "Strings::StringsRewriter::postRewrite "
90 : 3514 : << node << " to " << retNode << std::endl;
91 : 3514 : return RewriteResponse(REWRITE_AGAIN_FULL, retNode);
92 : : }
93 : 11262 : return RewriteResponse(REWRITE_DONE, retNode);
94 : 1582198 : }
95 : :
96 : 1298 : Node StringsRewriter::rewriteStrToInt(Node node)
97 : : {
98 [ - + ][ - + ]: 1298 : Assert(node.getKind() == Kind::STRING_STOI);
[ - - ]
99 : 1298 : NodeManager* nm = nodeManager();
100 [ + + ]: 1298 : if (node[0].isConst())
101 : : {
102 : 409 : Node ret;
103 : 409 : String s = node[0].getConst<String>();
104 [ + + ]: 409 : if (s.isNumber())
105 : : {
106 : 209 : ret = nm->mkConstInt(s.toNumber());
107 : : }
108 : : else
109 : : {
110 : 200 : ret = nm->mkConstInt(Rational(-1));
111 : : }
112 : 409 : return returnRewrite(node, ret, Rewrite::STOI_EVAL);
113 : 409 : }
114 [ + + ]: 889 : else if (node[0].getKind() == Kind::STRING_CONCAT)
115 : : {
116 [ + + ]: 644 : for (TNode nc : node[0])
117 : : {
118 [ + + ]: 490 : if (nc.isConst())
119 : : {
120 : 79 : String t = nc.getConst<String>();
121 [ + + ]: 79 : if (!t.isNumber())
122 : : {
123 : 15 : Node ret = nm->mkConstInt(Rational(-1));
124 : 15 : return returnRewrite(node, ret, Rewrite::STOI_CONCAT_NONNUM);
125 : 15 : }
126 [ + + ]: 79 : }
127 [ + + ][ + + ]: 659 : }
128 : : }
129 : 874 : return node;
130 : : }
131 : :
132 : 1518 : Node StringsRewriter::rewriteIntToStr(Node node)
133 : : {
134 [ - + ][ - + ]: 1518 : Assert(node.getKind() == Kind::STRING_ITOS);
[ - - ]
135 : 1518 : NodeManager* nm = nodeManager();
136 [ + + ]: 1518 : if (node[0].isConst())
137 : : {
138 : 350 : Node ret;
139 [ + + ]: 350 : if (node[0].getConst<Rational>().sgn() == -1)
140 : : {
141 : 82 : ret = nm->mkConst(String(""));
142 : : }
143 : : else
144 : : {
145 : 536 : std::string stmp = node[0].getConst<Rational>().getNumerator().toString();
146 [ - + ][ - + ]: 268 : Assert(stmp[0] != '-');
[ - - ]
147 : 268 : ret = nm->mkConst(String(stmp));
148 : 268 : }
149 : 350 : return returnRewrite(node, ret, Rewrite::ITOS_EVAL);
150 : 350 : }
151 : 1168 : return node;
152 : : }
153 : :
154 : 1070 : Node StringsRewriter::rewriteStrConvert(Node node)
155 : : {
156 : 1070 : Kind nk = node.getKind();
157 [ + + ][ + - ]: 1070 : Assert(nk == Kind::STRING_TO_LOWER || nk == Kind::STRING_TO_UPPER);
[ - + ][ - + ]
[ - - ]
158 : 1070 : NodeManager* nm = nodeManager();
159 [ + + ]: 1070 : if (node[0].isConst())
160 : : {
161 : 259 : std::vector<unsigned> nvec = node[0].getConst<String>().getVec();
162 [ + + ]: 1426 : for (unsigned i = 0, nvsize = nvec.size(); i < nvsize; i++)
163 : : {
164 : 1167 : unsigned newChar = nvec[i];
165 : : // transform it
166 : : // upper 65 ... 90
167 : : // lower 97 ... 122
168 [ + + ]: 1167 : if (nk == Kind::STRING_TO_UPPER)
169 : : {
170 [ + + ][ + + ]: 394 : if (newChar >= 97 && newChar <= 122)
171 : : {
172 : 32 : newChar = newChar - 32;
173 : : }
174 : : }
175 [ + - ]: 773 : else if (nk == Kind::STRING_TO_LOWER)
176 : : {
177 [ + + ][ + + ]: 773 : if (newChar >= 65 && newChar <= 90)
178 : : {
179 : 359 : newChar = newChar + 32;
180 : : }
181 : : }
182 : 1167 : nvec[i] = newChar;
183 : : }
184 : 259 : Node retNode = nm->mkConst(String(nvec));
185 : 259 : return returnRewrite(node, retNode, Rewrite::STR_CONV_CONST);
186 : 259 : }
187 [ + + ]: 811 : else if (node[0].getKind() == Kind::STRING_CONCAT)
188 : : {
189 : 128 : NodeBuilder concatBuilder(nm, Kind::STRING_CONCAT);
190 [ + + ]: 732 : for (const Node& nc : node[0])
191 : : {
192 : 604 : concatBuilder << nm->mkNode(nk, nc);
193 : 732 : }
194 : : // to_lower( x1 ++ x2 ) --> to_lower( x1 ) ++ to_lower( x2 )
195 : 128 : Node retNode = concatBuilder.constructNode();
196 : 128 : return returnRewrite(node, retNode, Rewrite::STR_CONV_MINSCOPE_CONCAT);
197 : 128 : }
198 [ + + ][ - - ]: 683 : else if (node[0].getKind() == Kind::STRING_TO_LOWER
199 [ + + ][ + + ]: 683 : || node[0].getKind() == Kind::STRING_TO_UPPER)
[ + + ][ + - ]
[ - - ]
200 : : {
201 : : // to_lower( to_lower( x ) ) --> to_lower( x )
202 : : // to_lower( toupper( x ) ) --> to_lower( x )
203 : 66 : Node retNode = nm->mkNode(nk, node[0][0]);
204 : 33 : return returnRewrite(node, retNode, Rewrite::STR_CONV_IDEM);
205 : 33 : }
206 [ + + ]: 650 : else if (node[0].getKind() == Kind::STRING_ITOS)
207 : : {
208 : : // to_lower( str.from.int( x ) ) --> str.from.int( x )
209 : 20 : return returnRewrite(node, node[0], Rewrite::STR_CONV_ITOS);
210 : : }
211 : 630 : return node;
212 : : }
213 : :
214 : 114 : Node StringsRewriter::rewriteStringLt(Node n)
215 : : {
216 [ - + ][ - + ]: 114 : Assert(n.getKind() == Kind::STRING_LT);
[ - - ]
217 : 114 : NodeManager* nm = nodeManager();
218 : : // eliminate s < t ---> s != t AND s <= t
219 : 342 : Node retNode = nm->mkNode(
220 : : Kind::AND,
221 : 228 : {n[0].eqNode(n[1]).negate(), nm->mkNode(Kind::STRING_LEQ, n[0], n[1])});
222 : 228 : return returnRewrite(n, retNode, Rewrite::STR_LT_ELIM);
223 : 114 : }
224 : :
225 : 1399 : Node StringsRewriter::rewriteStringLeq(Node n)
226 : : {
227 [ - + ][ - + ]: 1399 : Assert(n.getKind() == Kind::STRING_LEQ);
[ - - ]
228 : 1399 : NodeManager* nm = nodeManager();
229 [ + + ]: 1399 : if (n[0] == n[1])
230 : : {
231 : 115 : Node ret = nm->mkConst(true);
232 : 115 : return returnRewrite(n, ret, Rewrite::STR_LEQ_ID);
233 : 115 : }
234 : 1284 : if (n[0].isConst() && n[1].isConst())
235 : : {
236 : 254 : String s = n[0].getConst<String>();
237 : 254 : String t = n[1].getConst<String>();
238 : 254 : Node ret = nm->mkConst(s.isLeq(t));
239 : 254 : return returnRewrite(n, ret, Rewrite::STR_LEQ_EVAL);
240 : 254 : }
241 : : // empty strings
242 [ + + ]: 2992 : for (unsigned i = 0; i < 2; i++)
243 : : {
244 : 2028 : if (n[i].isConst() && n[i].getConst<String>().empty())
245 : : {
246 : 134 : Node ret = i == 0 ? nm->mkConst(true) : n[0].eqNode(n[1]);
247 : 66 : return returnRewrite(n, ret, Rewrite::STR_LEQ_EMPTY);
248 : 66 : }
249 : : }
250 : :
251 : 964 : std::vector<Node> n1;
252 : 964 : utils::getConcat(n[0], n1);
253 : 964 : std::vector<Node> n2;
254 : 964 : utils::getConcat(n[1], n2);
255 [ + - ][ + - ]: 964 : Assert(!n1.empty() && !n2.empty());
[ - + ][ - + ]
[ - - ]
256 : :
257 : : // constant prefixes
258 [ + + ][ + + ]: 964 : if (n1[0].isConst() && n2[0].isConst() && n1[0] != n2[0])
[ + + ][ + + ]
259 : : {
260 : 154 : String s = n1[0].getConst<String>();
261 : 154 : String t = n2[0].getConst<String>();
262 : 154 : size_t prefixLen = std::min(s.size(), t.size());
263 : 154 : s = s.prefix(prefixLen);
264 : 154 : t = t.prefix(prefixLen);
265 : : // if the prefixes are not the same, then we can already decide the outcome
266 [ + + ]: 154 : if (s != t)
267 : : {
268 : 90 : Node ret = nm->mkConst(s.isLeq(t));
269 : 90 : return returnRewrite(n, ret, Rewrite::STR_LEQ_CPREFIX);
270 : 90 : }
271 [ + + ][ + + ]: 244 : }
272 : 874 : return n;
273 : 964 : }
274 : :
275 : 259 : Node StringsRewriter::rewriteStringFromCode(Node n)
276 : : {
277 [ - + ][ - + ]: 259 : Assert(n.getKind() == Kind::STRING_FROM_CODE);
[ - - ]
278 : 259 : NodeManager* nm = nodeManager();
279 : :
280 [ + + ]: 259 : if (n[0].isConst())
281 : : {
282 : 65 : Integer i = n[0].getConst<Rational>().getNumerator();
283 : 65 : Node ret;
284 : 65 : if (i >= 0 && i < d_alphaCard)
285 : : {
286 : 51 : std::vector<unsigned> svec = {i.toUnsignedInt()};
287 : 51 : ret = nm->mkConst(String(svec));
288 : 51 : }
289 : : else
290 : : {
291 : 14 : ret = nm->mkConst(String(""));
292 : : }
293 : 65 : return returnRewrite(n, ret, Rewrite::FROM_CODE_EVAL);
294 : 65 : }
295 : 194 : return n;
296 : : }
297 : :
298 : 9084 : Node StringsRewriter::rewriteStringToCode(Node n)
299 : : {
300 [ - + ][ - + ]: 9084 : Assert(n.getKind() == Kind::STRING_TO_CODE);
[ - - ]
301 [ + + ]: 9084 : if (n[0].isConst())
302 : : {
303 : 1562 : NodeManager* nm = nodeManager();
304 : 1562 : String s = n[0].getConst<String>();
305 : 1562 : Node ret;
306 [ + + ]: 1562 : if (s.size() == 1)
307 : : {
308 : 1123 : std::vector<unsigned> vec = s.getVec();
309 [ - + ][ - + ]: 1123 : Assert(vec.size() == 1);
[ - - ]
310 : 1123 : ret = nm->mkConstInt(Rational(vec[0]));
311 : 1123 : }
312 : : else
313 : : {
314 : 439 : ret = nm->mkConstInt(Rational(-1));
315 : : }
316 : 1562 : return returnRewrite(n, ret, Rewrite::TO_CODE_EVAL);
317 : 1562 : }
318 : 7522 : return n;
319 : : }
320 : :
321 : 34 : Node StringsRewriter::rewriteStringIsDigit(Node n)
322 : : {
323 [ - + ][ - + ]: 34 : Assert(n.getKind() == Kind::STRING_IS_DIGIT);
[ - - ]
324 : 34 : NodeManager* nm = nodeManager();
325 : : // eliminate str.is_digit(s) ----> 48 <= str.to_code(s) <= 57
326 : 68 : Node t = nm->mkNode(Kind::STRING_TO_CODE, n[0]);
327 : : Node retNode =
328 : 102 : nm->mkNode(Kind::AND,
329 : 68 : {nm->mkNode(Kind::LEQ, nm->mkConstInt(Rational(48)), t),
330 : 68 : nm->mkNode(Kind::LEQ, t, nm->mkConstInt(Rational(57)))});
331 : 68 : return returnRewrite(n, retNode, Rewrite::IS_DIGIT_ELIM);
332 : 34 : }
333 : :
334 : 0 : Node StringsRewriter::rewriteStringUnit(Node n)
335 : : {
336 : 0 : Assert(n.getKind() == Kind::STRING_UNIT);
337 : 0 : NodeManager* nm = nodeManager();
338 [ - - ]: 0 : if (n[0].isConst())
339 : : {
340 : 0 : Integer i = n[0].getConst<Rational>().getNumerator();
341 : 0 : Node ret;
342 : 0 : if (i >= 0 && i < d_alphaCard)
343 : : {
344 : 0 : std::vector<unsigned> svec = {i.toUnsignedInt()};
345 : 0 : ret = nm->mkConst(String(svec));
346 : 0 : return returnRewrite(n, ret, Rewrite::SEQ_UNIT_EVAL);
347 : 0 : }
348 [ - - ][ - - ]: 0 : }
349 : 0 : return n;
350 : : }
351 : :
352 : : } // namespace strings
353 : : } // namespace theory
354 : : } // namespace cvc5::internal
|
