GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/strings/strings_rewriter.cpp Lines: 161 161 100.0 %
Date: 2021-08-16 Branches: 422 874 48.3 %

Line Exec Source
1
/******************************************************************************
2
 * Top contributors (to current version):
3
 *   Andrew Reynolds, Andres Noetzli, Gereon Kremer
4
 *
5
 * This file is part of the cvc5 project.
6
 *
7
 * Copyright (c) 2009-2021 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::kind;
25
26
namespace cvc5 {
27
namespace theory {
28
namespace strings {
29
30
9865
StringsRewriter::StringsRewriter(HistogramStat<Rewrite>* statistics)
31
9865
    : SequencesRewriter(statistics)
32
{
33
9865
}
34
35
544743
RewriteResponse StringsRewriter::postRewrite(TNode node)
36
{
37
1089486
  Trace("strings-postrewrite")
38
544743
      << "Strings::StringsRewriter::postRewrite start " << node << std::endl;
39
40
1089486
  Node retNode = node;
41
544743
  Kind nk = node.getKind();
42
544743
  if (nk == kind::STRING_LT)
43
  {
44
17
    retNode = rewriteStringLt(node);
45
  }
46
544726
  else if (nk == kind::STRING_LEQ)
47
  {
48
355
    retNode = rewriteStringLeq(node);
49
  }
50
544371
  else if (nk == STRING_TOLOWER || nk == STRING_TOUPPER)
51
  {
52
212
    retNode = rewriteStrConvert(node);
53
  }
54
544159
  else if (nk == STRING_IS_DIGIT)
55
  {
56
8
    retNode = rewriteStringIsDigit(node);
57
  }
58
544151
  else if (nk == kind::STRING_ITOS)
59
  {
60
571
    retNode = rewriteIntToStr(node);
61
  }
62
543580
  else if (nk == kind::STRING_STOI)
63
  {
64
458
    retNode = rewriteStrToInt(node);
65
  }
66
543122
  else if (nk == STRING_TO_CODE)
67
  {
68
4645
    retNode = rewriteStringToCode(node);
69
  }
70
538477
  else if (nk == STRING_FROM_CODE)
71
  {
72
100
    retNode = rewriteStringFromCode(node);
73
  }
74
  else
75
  {
76
538377
    return SequencesRewriter::postRewrite(node);
77
  }
78
79
12732
  Trace("strings-postrewrite")
80
6366
      << "Strings::StringsRewriter::postRewrite returning " << retNode
81
6366
      << std::endl;
82
6366
  if (node != retNode)
83
  {
84
3940
    Trace("strings-rewrite-debug") << "Strings::StringsRewriter::postRewrite "
85
1970
                                   << node << " to " << retNode << std::endl;
86
1970
    return RewriteResponse(REWRITE_AGAIN_FULL, retNode);
87
  }
88
4396
  return RewriteResponse(REWRITE_DONE, retNode);
89
}
90
91
458
Node StringsRewriter::rewriteStrToInt(Node node)
92
{
93
458
  Assert(node.getKind() == STRING_STOI);
94
458
  NodeManager* nm = NodeManager::currentNM();
95
458
  if (node[0].isConst())
96
  {
97
368
    Node ret;
98
368
    String s = node[0].getConst<String>();
99
184
    if (s.isNumber())
100
    {
101
85
      ret = nm->mkConst(s.toNumber());
102
    }
103
    else
104
    {
105
99
      ret = nm->mkConst(Rational(-1));
106
    }
107
184
    return returnRewrite(node, ret, Rewrite::STOI_EVAL);
108
  }
109
274
  else if (node[0].getKind() == STRING_CONCAT)
110
  {
111
716
    for (TNode nc : node[0])
112
    {
113
592
      if (nc.isConst())
114
      {
115
36
        String t = nc.getConst<String>();
116
20
        if (!t.isNumber())
117
        {
118
8
          Node ret = nm->mkConst(Rational(-1));
119
4
          return returnRewrite(node, ret, Rewrite::STOI_CONCAT_NONNUM);
120
        }
121
      }
122
    }
123
  }
124
270
  return node;
125
}
126
127
571
Node StringsRewriter::rewriteIntToStr(Node node)
128
{
129
571
  Assert(node.getKind() == STRING_ITOS);
130
571
  NodeManager* nm = NodeManager::currentNM();
131
571
  if (node[0].isConst())
132
  {
133
526
    Node ret;
134
263
    if (node[0].getConst<Rational>().sgn() == -1)
135
    {
136
129
      ret = nm->mkConst(String(""));
137
    }
138
    else
139
    {
140
268
      std::string stmp = node[0].getConst<Rational>().getNumerator().toString();
141
134
      Assert(stmp[0] != '-');
142
134
      ret = nm->mkConst(String(stmp));
143
    }
144
263
    return returnRewrite(node, ret, Rewrite::ITOS_EVAL);
145
  }
146
308
  return node;
147
}
148
149
212
Node StringsRewriter::rewriteStrConvert(Node node)
150
{
151
212
  Kind nk = node.getKind();
152
212
  Assert(nk == STRING_TOLOWER || nk == STRING_TOUPPER);
153
212
  NodeManager* nm = NodeManager::currentNM();
154
212
  if (node[0].isConst())
155
  {
156
52
    std::vector<unsigned> nvec = node[0].getConst<String>().getVec();
157
96
    for (unsigned i = 0, nvsize = nvec.size(); i < nvsize; i++)
158
    {
159
70
      unsigned newChar = nvec[i];
160
      // transform it
161
      // upper 65 ... 90
162
      // lower 97 ... 122
163
70
      if (nk == STRING_TOUPPER)
164
      {
165
36
        if (newChar >= 97 && newChar <= 122)
166
        {
167
22
          newChar = newChar - 32;
168
        }
169
      }
170
34
      else if (nk == STRING_TOLOWER)
171
      {
172
34
        if (newChar >= 65 && newChar <= 90)
173
        {
174
25
          newChar = newChar + 32;
175
        }
176
      }
177
70
      nvec[i] = newChar;
178
    }
179
52
    Node retNode = nm->mkConst(String(nvec));
180
26
    return returnRewrite(node, retNode, Rewrite::STR_CONV_CONST);
181
  }
182
186
  else if (node[0].getKind() == STRING_CONCAT)
183
  {
184
100
    NodeBuilder concatBuilder(STRING_CONCAT);
185
222
    for (const Node& nc : node[0])
186
    {
187
172
      concatBuilder << nm->mkNode(nk, nc);
188
    }
189
    // tolower( x1 ++ x2 ) --> tolower( x1 ) ++ tolower( x2 )
190
100
    Node retNode = concatBuilder.constructNode();
191
50
    return returnRewrite(node, retNode, Rewrite::STR_CONV_MINSCOPE_CONCAT);
192
  }
193
408
  else if (node[0].getKind() == STRING_TOLOWER
194
408
           || node[0].getKind() == STRING_TOUPPER)
195
  {
196
    // tolower( tolower( x ) ) --> tolower( x )
197
    // tolower( toupper( x ) ) --> tolower( x )
198
16
    Node retNode = nm->mkNode(nk, node[0][0]);
199
8
    return returnRewrite(node, retNode, Rewrite::STR_CONV_IDEM);
200
  }
201
128
  else if (node[0].getKind() == STRING_ITOS)
202
  {
203
    // tolower( str.from.int( x ) ) --> str.from.int( x )
204
4
    return returnRewrite(node, node[0], Rewrite::STR_CONV_ITOS);
205
  }
206
124
  return node;
207
}
208
209
17
Node StringsRewriter::rewriteStringLt(Node n)
210
{
211
17
  Assert(n.getKind() == kind::STRING_LT);
212
17
  NodeManager* nm = NodeManager::currentNM();
213
  // eliminate s < t ---> s != t AND s <= t
214
  Node retNode = nm->mkNode(
215
34
      AND, n[0].eqNode(n[1]).negate(), nm->mkNode(STRING_LEQ, n[0], n[1]));
216
34
  return returnRewrite(n, retNode, Rewrite::STR_LT_ELIM);
217
}
218
219
355
Node StringsRewriter::rewriteStringLeq(Node n)
220
{
221
355
  Assert(n.getKind() == kind::STRING_LEQ);
222
355
  NodeManager* nm = NodeManager::currentNM();
223
355
  if (n[0] == n[1])
224
  {
225
42
    Node ret = nm->mkConst(true);
226
21
    return returnRewrite(n, ret, Rewrite::STR_LEQ_ID);
227
  }
228
334
  if (n[0].isConst() && n[1].isConst())
229
  {
230
88
    String s = n[0].getConst<String>();
231
88
    String t = n[1].getConst<String>();
232
88
    Node ret = nm->mkConst(s.isLeq(t));
233
44
    return returnRewrite(n, ret, Rewrite::STR_LEQ_EVAL);
234
  }
235
  // empty strings
236
850
  for (unsigned i = 0; i < 2; i++)
237
  {
238
575
    if (n[i].isConst() && n[i].getConst<String>().empty())
239
    {
240
30
      Node ret = i == 0 ? nm->mkConst(true) : n[0].eqNode(n[1]);
241
15
      return returnRewrite(n, ret, Rewrite::STR_LEQ_EMPTY);
242
    }
243
  }
244
245
550
  std::vector<Node> n1;
246
275
  utils::getConcat(n[0], n1);
247
550
  std::vector<Node> n2;
248
275
  utils::getConcat(n[1], n2);
249
275
  Assert(!n1.empty() && !n2.empty());
250
251
  // constant prefixes
252
275
  if (n1[0].isConst() && n2[0].isConst() && n1[0] != n2[0])
253
  {
254
97
    String s = n1[0].getConst<String>();
255
97
    String t = n2[0].getConst<String>();
256
65
    size_t prefixLen = std::min(s.size(), t.size());
257
65
    s = s.prefix(prefixLen);
258
65
    t = t.prefix(prefixLen);
259
    // if the prefixes are not the same, then we can already decide the outcome
260
65
    if (s != t)
261
    {
262
66
      Node ret = nm->mkConst(s.isLeq(t));
263
33
      return returnRewrite(n, ret, Rewrite::STR_LEQ_CPREFIX);
264
    }
265
  }
266
242
  return n;
267
}
268
269
100
Node StringsRewriter::rewriteStringFromCode(Node n)
270
{
271
100
  Assert(n.getKind() == kind::STRING_FROM_CODE);
272
100
  NodeManager* nm = NodeManager::currentNM();
273
274
100
  if (n[0].isConst())
275
  {
276
44
    Integer i = n[0].getConst<Rational>().getNumerator();
277
44
    Node ret;
278
22
    if (i >= 0 && i < strings::utils::getAlphabetCardinality())
279
    {
280
18
      std::vector<unsigned> svec = {i.toUnsignedInt()};
281
9
      ret = nm->mkConst(String(svec));
282
    }
283
    else
284
    {
285
13
      ret = nm->mkConst(String(""));
286
    }
287
22
    return returnRewrite(n, ret, Rewrite::FROM_CODE_EVAL);
288
  }
289
78
  return n;
290
}
291
292
4645
Node StringsRewriter::rewriteStringToCode(Node n)
293
{
294
4645
  Assert(n.getKind() == kind::STRING_TO_CODE);
295
4645
  if (n[0].isConst())
296
  {
297
1271
    NodeManager* nm = NodeManager::currentNM();
298
2542
    String s = n[0].getConst<String>();
299
2542
    Node ret;
300
1271
    if (s.size() == 1)
301
    {
302
1200
      std::vector<unsigned> vec = s.getVec();
303
600
      Assert(vec.size() == 1);
304
600
      ret = nm->mkConst(Rational(vec[0]));
305
    }
306
    else
307
    {
308
671
      ret = nm->mkConst(Rational(-1));
309
    }
310
1271
    return returnRewrite(n, ret, Rewrite::TO_CODE_EVAL);
311
  }
312
3374
  return n;
313
}
314
315
8
Node StringsRewriter::rewriteStringIsDigit(Node n)
316
{
317
8
  Assert(n.getKind() == kind::STRING_IS_DIGIT);
318
8
  NodeManager* nm = NodeManager::currentNM();
319
  // eliminate str.is_digit(s) ----> 48 <= str.to_code(s) <= 57
320
16
  Node t = nm->mkNode(STRING_TO_CODE, n[0]);
321
  Node retNode = nm->mkNode(AND,
322
16
                            nm->mkNode(LEQ, nm->mkConst(Rational(48)), t),
323
32
                            nm->mkNode(LEQ, t, nm->mkConst(Rational(57))));
324
16
  return returnRewrite(n, retNode, Rewrite::IS_DIGIT_ELIM);
325
}
326
327
}  // namespace strings
328
}  // namespace theory
329
29340
}  // namespace cvc5