GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/strings/strings_rewriter.cpp Lines: 161 161 100.0 %
Date: 2021-03-23 Branches: 422 876 48.2 %

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