Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Andres Noetzli, Aina Niemetz
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
8 : : * in the top-level source directory and their institutional affiliations.
9 : : * All rights reserved. See the file COPYING in the top-level source
10 : : * directory for licensing information.
11 : : * ****************************************************************************
12 : : *
13 : : * Implementation of rewrite rules for string-specific operators in
14 : : * theory of strings.
15 : : */
16 : :
17 : : #include "theory/strings/strings_rewriter.h"
18 : :
19 : : #include "expr/node_builder.h"
20 : : #include "theory/strings/theory_strings_utils.h"
21 : : #include "util/rational.h"
22 : : #include "util/string.h"
23 : :
24 : : using namespace cvc5::internal::kind;
25 : :
26 : : namespace cvc5::internal {
27 : : namespace theory {
28 : : namespace strings {
29 : :
30 : 49274 : StringsRewriter::StringsRewriter(NodeManager* nm,
31 : : Rewriter* r,
32 : : HistogramStat<Rewrite>* statistics,
33 : 49274 : uint32_t alphaCard)
34 : 49274 : : SequencesRewriter(nm, r, statistics), d_alphaCard(alphaCard)
35 : : {
36 : 49274 : }
37 : :
38 : 993929 : RewriteResponse StringsRewriter::postRewrite(TNode node)
39 : : {
40 [ + - ]: 1987860 : Trace("strings-postrewrite")
41 : 993929 : << "Strings::StringsRewriter::postRewrite start " << node << std::endl;
42 : :
43 : 1987860 : Node retNode = node;
44 : 993929 : Kind nk = node.getKind();
45 [ + + ]: 993929 : if (nk == Kind::STRING_LT)
46 : : {
47 : 114 : retNode = rewriteStringLt(node);
48 : : }
49 [ + + ]: 993815 : else if (nk == Kind::STRING_LEQ)
50 : : {
51 : 1401 : retNode = rewriteStringLeq(node);
52 : : }
53 [ + + ][ + + ]: 992414 : else if (nk == Kind::STRING_TO_LOWER || nk == Kind::STRING_TO_UPPER)
54 : : {
55 : 913 : retNode = rewriteStrConvert(node);
56 : : }
57 [ + + ]: 991501 : else if (nk == Kind::STRING_IS_DIGIT)
58 : : {
59 : 24 : retNode = rewriteStringIsDigit(node);
60 : : }
61 [ + + ]: 991477 : else if (nk == Kind::STRING_ITOS)
62 : : {
63 : 1160 : retNode = rewriteIntToStr(node);
64 : : }
65 [ + + ]: 990317 : else if (nk == Kind::STRING_STOI)
66 : : {
67 : 1449 : retNode = rewriteStrToInt(node);
68 : : }
69 [ + + ]: 988868 : else if (nk == Kind::STRING_TO_CODE)
70 : : {
71 : 9208 : retNode = rewriteStringToCode(node);
72 : : }
73 [ + + ]: 979660 : else if (nk == Kind::STRING_FROM_CODE)
74 : : {
75 : 273 : retNode = rewriteStringFromCode(node);
76 : : }
77 [ - + ]: 979387 : else if (nk == Kind::STRING_UNIT)
78 : : {
79 : 0 : retNode = rewriteStringUnit(node);
80 : : }
81 : : else
82 : : {
83 : 979387 : return SequencesRewriter::postRewrite(node);
84 : : }
85 : :
86 [ + - ]: 29084 : Trace("strings-postrewrite")
87 : 0 : << "Strings::StringsRewriter::postRewrite returning " << retNode
88 : 14542 : << std::endl;
89 [ + + ]: 14542 : if (node != retNode)
90 : : {
91 [ + - ]: 7756 : Trace("strings-rewrite-debug") << "Strings::StringsRewriter::postRewrite "
92 : 3878 : << node << " to " << retNode << std::endl;
93 : 3878 : return RewriteResponse(REWRITE_AGAIN_FULL, retNode);
94 : : }
95 : 10664 : return RewriteResponse(REWRITE_DONE, retNode);
96 : : }
97 : :
98 : 1449 : Node StringsRewriter::rewriteStrToInt(Node node)
99 : : {
100 [ - + ][ - + ]: 1449 : Assert(node.getKind() == Kind::STRING_STOI);
[ - - ]
101 : 1449 : NodeManager* nm = nodeManager();
102 [ + + ]: 1449 : if (node[0].isConst())
103 : : {
104 : 1042 : Node ret;
105 : 521 : String s = node[0].getConst<String>();
106 [ + + ]: 521 : if (s.isNumber())
107 : : {
108 : 240 : ret = nm->mkConstInt(s.toNumber());
109 : : }
110 : : else
111 : : {
112 : 281 : ret = nm->mkConstInt(Rational(-1));
113 : : }
114 : 521 : return returnRewrite(node, ret, Rewrite::STOI_EVAL);
115 : : }
116 [ + + ]: 928 : else if (node[0].getKind() == Kind::STRING_CONCAT)
117 : : {
118 [ + + ]: 730 : for (TNode nc : node[0])
119 : : {
120 [ + + ]: 546 : if (nc.isConst())
121 : : {
122 : 104 : String t = nc.getConst<String>();
123 [ + + ]: 104 : if (!t.isNumber())
124 : : {
125 : 14 : Node ret = nm->mkConstInt(Rational(-1));
126 : 14 : return returnRewrite(node, ret, Rewrite::STOI_CONCAT_NONNUM);
127 : : }
128 : : }
129 : : }
130 : : }
131 : 914 : return node;
132 : : }
133 : :
134 : 1160 : Node StringsRewriter::rewriteIntToStr(Node node)
135 : : {
136 [ - + ][ - + ]: 1160 : Assert(node.getKind() == Kind::STRING_ITOS);
[ - - ]
137 : 1160 : NodeManager* nm = nodeManager();
138 [ + + ]: 1160 : if (node[0].isConst())
139 : : {
140 : 584 : Node ret;
141 [ + + ]: 584 : if (node[0].getConst<Rational>().sgn() == -1)
142 : : {
143 : 245 : ret = nm->mkConst(String(""));
144 : : }
145 : : else
146 : : {
147 : 678 : std::string stmp = node[0].getConst<Rational>().getNumerator().toString();
148 [ - + ][ - + ]: 339 : Assert(stmp[0] != '-');
[ - - ]
149 : 339 : ret = nm->mkConst(String(stmp));
150 : : }
151 : 584 : return returnRewrite(node, ret, Rewrite::ITOS_EVAL);
152 : : }
153 : 576 : return node;
154 : : }
155 : :
156 : 913 : Node StringsRewriter::rewriteStrConvert(Node node)
157 : : {
158 : 913 : Kind nk = node.getKind();
159 [ + + ][ - + ]: 913 : Assert(nk == Kind::STRING_TO_LOWER || nk == Kind::STRING_TO_UPPER);
[ - + ][ - - ]
160 : 913 : NodeManager* nm = nodeManager();
161 [ + + ]: 913 : if (node[0].isConst())
162 : : {
163 : 460 : std::vector<unsigned> nvec = node[0].getConst<String>().getVec();
164 [ + + ]: 1362 : for (unsigned i = 0, nvsize = nvec.size(); i < nvsize; i++)
165 : : {
166 : 1132 : unsigned newChar = nvec[i];
167 : : // transform it
168 : : // upper 65 ... 90
169 : : // lower 97 ... 122
170 [ + + ]: 1132 : if (nk == Kind::STRING_TO_UPPER)
171 : : {
172 [ + + ][ + + ]: 398 : if (newChar >= 97 && newChar <= 122)
173 : : {
174 : 34 : newChar = newChar - 32;
175 : : }
176 : : }
177 [ + - ]: 734 : else if (nk == Kind::STRING_TO_LOWER)
178 : : {
179 [ + + ][ + + ]: 734 : if (newChar >= 65 && newChar <= 90)
180 : : {
181 : 344 : newChar = newChar + 32;
182 : : }
183 : : }
184 : 1132 : nvec[i] = newChar;
185 : : }
186 : 230 : Node retNode = nm->mkConst(String(nvec));
187 : 230 : return returnRewrite(node, retNode, Rewrite::STR_CONV_CONST);
188 : : }
189 [ + + ]: 683 : else if (node[0].getKind() == Kind::STRING_CONCAT)
190 : : {
191 : 234 : NodeBuilder concatBuilder(Kind::STRING_CONCAT);
192 [ + + ]: 667 : for (const Node& nc : node[0])
193 : : {
194 : 550 : concatBuilder << nm->mkNode(nk, nc);
195 : : }
196 : : // to_lower( x1 ++ x2 ) --> to_lower( x1 ) ++ to_lower( x2 )
197 : 117 : Node retNode = concatBuilder.constructNode();
198 : 117 : return returnRewrite(node, retNode, Rewrite::STR_CONV_MINSCOPE_CONCAT);
199 : : }
200 [ + + ][ - - ]: 566 : else if (node[0].getKind() == Kind::STRING_TO_LOWER
201 [ + + ][ + + ]: 566 : || node[0].getKind() == Kind::STRING_TO_UPPER)
[ + + ][ + - ]
[ - - ]
202 : : {
203 : : // to_lower( to_lower( x ) ) --> to_lower( x )
204 : : // to_lower( toupper( x ) ) --> to_lower( x )
205 : 76 : Node retNode = nm->mkNode(nk, node[0][0]);
206 : 38 : return returnRewrite(node, retNode, Rewrite::STR_CONV_IDEM);
207 : : }
208 [ + + ]: 528 : else if (node[0].getKind() == Kind::STRING_ITOS)
209 : : {
210 : : // to_lower( str.from.int( x ) ) --> str.from.int( x )
211 : 12 : return returnRewrite(node, node[0], Rewrite::STR_CONV_ITOS);
212 : : }
213 : 516 : return node;
214 : : }
215 : :
216 : 114 : Node StringsRewriter::rewriteStringLt(Node n)
217 : : {
218 [ - + ][ - + ]: 114 : Assert(n.getKind() == Kind::STRING_LT);
[ - - ]
219 : 114 : NodeManager* nm = nodeManager();
220 : : // eliminate s < t ---> s != t AND s <= t
221 : : Node retNode = nm->mkNode(Kind::AND,
222 : 228 : n[0].eqNode(n[1]).negate(),
223 : 456 : nm->mkNode(Kind::STRING_LEQ, n[0], n[1]));
224 : 228 : return returnRewrite(n, retNode, Rewrite::STR_LT_ELIM);
225 : : }
226 : :
227 : 1401 : Node StringsRewriter::rewriteStringLeq(Node n)
228 : : {
229 [ - + ][ - + ]: 1401 : Assert(n.getKind() == Kind::STRING_LEQ);
[ - - ]
230 : 1401 : NodeManager* nm = nodeManager();
231 [ + + ]: 1401 : if (n[0] == n[1])
232 : : {
233 : 136 : Node ret = nm->mkConst(true);
234 : 136 : return returnRewrite(n, ret, Rewrite::STR_LEQ_ID);
235 : : }
236 : 1265 : if (n[0].isConst() && n[1].isConst())
237 : : {
238 : 384 : String s = n[0].getConst<String>();
239 : 384 : String t = n[1].getConst<String>();
240 : 192 : Node ret = nm->mkConst(s.isLeq(t));
241 : 192 : return returnRewrite(n, ret, Rewrite::STR_LEQ_EVAL);
242 : : }
243 : : // empty strings
244 [ + + ]: 3077 : for (unsigned i = 0; i < 2; i++)
245 : : {
246 : 2094 : if (n[i].isConst() && n[i].getConst<String>().empty())
247 : : {
248 : 166 : Node ret = i == 0 ? nm->mkConst(true) : n[0].eqNode(n[1]);
249 : 90 : return returnRewrite(n, ret, Rewrite::STR_LEQ_EMPTY);
250 : : }
251 : : }
252 : :
253 : 1966 : std::vector<Node> n1;
254 : 983 : utils::getConcat(n[0], n1);
255 : 1966 : std::vector<Node> n2;
256 : 983 : utils::getConcat(n[1], n2);
257 [ + - ][ + - ]: 1966 : Assert(!n1.empty() && !n2.empty());
[ - + ][ - - ]
258 : :
259 : : // constant prefixes
260 [ + + ][ + + ]: 983 : if (n1[0].isConst() && n2[0].isConst() && n1[0] != n2[0])
[ + + ][ + + ]
261 : : {
262 : 145 : String s = n1[0].getConst<String>();
263 : 145 : String t = n2[0].getConst<String>();
264 : 145 : size_t prefixLen = std::min(s.size(), t.size());
265 : 145 : s = s.prefix(prefixLen);
266 : 145 : t = t.prefix(prefixLen);
267 : : // if the prefixes are not the same, then we can already decide the outcome
268 [ + + ]: 145 : if (s != t)
269 : : {
270 : 89 : Node ret = nm->mkConst(s.isLeq(t));
271 : 89 : return returnRewrite(n, ret, Rewrite::STR_LEQ_CPREFIX);
272 : : }
273 : : }
274 : 894 : return n;
275 : : }
276 : :
277 : 273 : Node StringsRewriter::rewriteStringFromCode(Node n)
278 : : {
279 [ - + ][ - + ]: 273 : Assert(n.getKind() == Kind::STRING_FROM_CODE);
[ - - ]
280 : 273 : NodeManager* nm = nodeManager();
281 : :
282 [ + + ]: 273 : if (n[0].isConst())
283 : : {
284 : 106 : Integer i = n[0].getConst<Rational>().getNumerator();
285 : 53 : Node ret;
286 : 53 : if (i >= 0 && i < d_alphaCard)
287 : : {
288 : 35 : std::vector<unsigned> svec = {i.toUnsignedInt()};
289 : 35 : ret = nm->mkConst(String(svec));
290 : : }
291 : : else
292 : : {
293 : 18 : ret = nm->mkConst(String(""));
294 : : }
295 : 53 : return returnRewrite(n, ret, Rewrite::FROM_CODE_EVAL);
296 : : }
297 : 220 : return n;
298 : : }
299 : :
300 : 9208 : Node StringsRewriter::rewriteStringToCode(Node n)
301 : : {
302 [ - + ][ - + ]: 9208 : Assert(n.getKind() == Kind::STRING_TO_CODE);
[ - - ]
303 [ + + ]: 9208 : if (n[0].isConst())
304 : : {
305 : 1664 : NodeManager* nm = nodeManager();
306 : 3328 : String s = n[0].getConst<String>();
307 : 1664 : Node ret;
308 [ + + ]: 1664 : if (s.size() == 1)
309 : : {
310 : 1229 : std::vector<unsigned> vec = s.getVec();
311 [ - + ][ - + ]: 1229 : Assert(vec.size() == 1);
[ - - ]
312 : 1229 : ret = nm->mkConstInt(Rational(vec[0]));
313 : : }
314 : : else
315 : : {
316 : 435 : ret = nm->mkConstInt(Rational(-1));
317 : : }
318 : 1664 : return returnRewrite(n, ret, Rewrite::TO_CODE_EVAL);
319 : : }
320 : 7544 : return n;
321 : : }
322 : :
323 : 24 : Node StringsRewriter::rewriteStringIsDigit(Node n)
324 : : {
325 [ - + ][ - + ]: 24 : Assert(n.getKind() == Kind::STRING_IS_DIGIT);
[ - - ]
326 : 24 : NodeManager* nm = nodeManager();
327 : : // eliminate str.is_digit(s) ----> 48 <= str.to_code(s) <= 57
328 : 72 : Node t = nm->mkNode(Kind::STRING_TO_CODE, n[0]);
329 : : Node retNode =
330 : : nm->mkNode(Kind::AND,
331 : 48 : nm->mkNode(Kind::LEQ, nm->mkConstInt(Rational(48)), t),
332 : 96 : nm->mkNode(Kind::LEQ, t, nm->mkConstInt(Rational(57))));
333 : 48 : return returnRewrite(n, retNode, Rewrite::IS_DIGIT_ELIM);
334 : : }
335 : :
336 : 0 : Node StringsRewriter::rewriteStringUnit(Node n)
337 : : {
338 : 0 : Assert(n.getKind() == Kind::STRING_UNIT);
339 : 0 : NodeManager* nm = nodeManager();
340 [ - - ]: 0 : if (n[0].isConst())
341 : : {
342 : 0 : Integer i = n[0].getConst<Rational>().getNumerator();
343 : 0 : Node ret;
344 : 0 : if (i >= 0 && i < d_alphaCard)
345 : : {
346 : 0 : std::vector<unsigned> svec = {i.toUnsignedInt()};
347 : 0 : ret = nm->mkConst(String(svec));
348 : 0 : return returnRewrite(n, ret, Rewrite::SEQ_UNIT_EVAL);
349 : : }
350 : : }
351 : 0 : return n;
352 : : }
353 : :
354 : : } // namespace strings
355 : : } // namespace theory
356 : : } // namespace cvc5::internal
|
