GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/strings/word.cpp Lines: 233 282 82.6 %
Date: 2021-03-23 Branches: 305 1028 29.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file word.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 utility functions for words.
13
 **/
14
15
#include "theory/strings/word.h"
16
17
#include "expr/sequence.h"
18
#include "util/string.h"
19
20
using namespace CVC4::kind;
21
22
namespace CVC4 {
23
namespace theory {
24
namespace strings {
25
26
1411900
Node Word::mkEmptyWord(TypeNode tn)
27
{
28
1411900
  if (tn.isString())
29
  {
30
2805256
    std::vector<unsigned> vec;
31
1402628
    return NodeManager::currentNM()->mkConst(String(vec));
32
  }
33
9272
  else if (tn.isSequence())
34
  {
35
18544
    std::vector<Node> seq;
36
    return NodeManager::currentNM()->mkConst(
37
9272
        Sequence(tn.getSequenceElementType(), seq));
38
  }
39
  Unimplemented();
40
  return Node::null();
41
}
42
43
47144
Node Word::mkWordFlatten(const std::vector<Node>& xs)
44
{
45
47144
  Assert(!xs.empty());
46
47144
  NodeManager* nm = NodeManager::currentNM();
47
47144
  Kind k = xs[0].getKind();
48
47144
  if (k == CONST_STRING)
49
  {
50
93312
    std::vector<unsigned> vec;
51
119425
    for (TNode x : xs)
52
    {
53
72769
      Assert(x.getKind() == CONST_STRING);
54
145538
      String sx = x.getConst<String>();
55
72769
      const std::vector<unsigned>& vecc = sx.getVec();
56
72769
      vec.insert(vec.end(), vecc.begin(), vecc.end());
57
    }
58
46656
    return nm->mkConst(String(vec));
59
  }
60
488
  else if (k == CONST_SEQUENCE)
61
  {
62
976
    std::vector<Node> seq;
63
976
    TypeNode tn = xs[0].getType();
64
1130
    for (TNode x : xs)
65
    {
66
642
      Assert(x.getType() == tn);
67
642
      const Sequence& sx = x.getConst<Sequence>();
68
642
      const std::vector<Node>& vecc = sx.getVec();
69
642
      seq.insert(seq.end(), vecc.begin(), vecc.end());
70
    }
71
    return NodeManager::currentNM()->mkConst(
72
488
        Sequence(tn.getSequenceElementType(), seq));
73
  }
74
  Unimplemented();
75
  return Node::null();
76
}
77
78
1195707
size_t Word::getLength(TNode x)
79
{
80
1195707
  Kind k = x.getKind();
81
1195707
  if (k == CONST_STRING)
82
  {
83
1184037
    return x.getConst<String>().size();
84
  }
85
11670
  else if (k == CONST_SEQUENCE)
86
  {
87
11670
    return x.getConst<Sequence>().size();
88
  }
89
  Unimplemented() << "Word::getLength on " << x;
90
  return 0;
91
}
92
93
193165
std::vector<Node> Word::getChars(TNode x)
94
{
95
193165
  Kind k = x.getKind();
96
193165
  std::vector<Node> ret;
97
193165
  NodeManager* nm = NodeManager::currentNM();
98
193165
  if (k == CONST_STRING)
99
  {
100
378240
    std::vector<unsigned> ccVec;
101
189120
    const std::vector<unsigned>& cvec = x.getConst<String>().getVec();
102
600990
    for (unsigned chVal : cvec)
103
    {
104
411870
      ccVec.clear();
105
411870
      ccVec.push_back(chVal);
106
823740
      Node ch = nm->mkConst(String(ccVec));
107
411870
      ret.push_back(ch);
108
    }
109
189120
    return ret;
110
  }
111
4045
  else if (k == CONST_SEQUENCE)
112
  {
113
8090
    TypeNode t = x.getConst<Sequence>().getType();
114
4045
    const Sequence& sx = x.getConst<Sequence>();
115
4045
    const std::vector<Node>& vec = sx.getVec();
116
6125
    for (const Node& v : vec)
117
    {
118
2080
      ret.push_back(nm->mkConst(Sequence(t, {v})));
119
    }
120
4045
    return ret;
121
  }
122
  Unimplemented();
123
  return ret;
124
}
125
126
325516
bool Word::isEmpty(TNode x) { return x.isConst() && getLength(x) == 0; }
127
128
35574
bool Word::strncmp(TNode x, TNode y, std::size_t n)
129
{
130
35574
  Kind k = x.getKind();
131
35574
  if (k == CONST_STRING)
132
  {
133
35570
    Assert(y.getKind() == CONST_STRING);
134
71140
    String sx = x.getConst<String>();
135
71140
    String sy = y.getConst<String>();
136
35570
    return sx.strncmp(sy, n);
137
  }
138
4
  else if (k == CONST_SEQUENCE)
139
  {
140
4
    Assert(y.getKind() == CONST_SEQUENCE);
141
4
    const Sequence& sx = x.getConst<Sequence>();
142
4
    const Sequence& sy = y.getConst<Sequence>();
143
4
    return sx.strncmp(sy, n);
144
  }
145
  Unimplemented();
146
  return false;
147
}
148
149
35497
bool Word::rstrncmp(TNode x, TNode y, std::size_t n)
150
{
151
35497
  Kind k = x.getKind();
152
35497
  if (k == CONST_STRING)
153
  {
154
35430
    Assert(y.getKind() == CONST_STRING);
155
70860
    String sx = x.getConst<String>();
156
70860
    String sy = y.getConst<String>();
157
35430
    return sx.rstrncmp(sy, n);
158
  }
159
67
  else if (k == CONST_SEQUENCE)
160
  {
161
67
    Assert(y.getKind() == CONST_SEQUENCE);
162
67
    const Sequence& sx = x.getConst<Sequence>();
163
67
    const Sequence& sy = y.getConst<Sequence>();
164
67
    return sx.rstrncmp(sy, n);
165
  }
166
  Unimplemented();
167
  return false;
168
}
169
170
90939
std::size_t Word::find(TNode x, TNode y, std::size_t start)
171
{
172
90939
  Kind k = x.getKind();
173
90939
  if (k == CONST_STRING)
174
  {
175
90678
    Assert(y.getKind() == CONST_STRING);
176
181356
    String sx = x.getConst<String>();
177
181356
    String sy = y.getConst<String>();
178
90678
    return sx.find(sy, start);
179
  }
180
261
  else if (k == CONST_SEQUENCE)
181
  {
182
261
    Assert(y.getKind() == CONST_SEQUENCE);
183
261
    const Sequence& sx = x.getConst<Sequence>();
184
261
    const Sequence& sy = y.getConst<Sequence>();
185
261
    return sx.find(sy, start);
186
  }
187
  Unimplemented();
188
  return 0;
189
}
190
191
10577
std::size_t Word::rfind(TNode x, TNode y, std::size_t start)
192
{
193
10577
  Kind k = x.getKind();
194
10577
  if (k == CONST_STRING)
195
  {
196
10483
    Assert(y.getKind() == CONST_STRING);
197
20966
    String sx = x.getConst<String>();
198
20966
    String sy = y.getConst<String>();
199
10483
    return sx.rfind(sy, start);
200
  }
201
94
  else if (k == CONST_SEQUENCE)
202
  {
203
94
    Assert(y.getKind() == CONST_SEQUENCE);
204
94
    const Sequence& sx = x.getConst<Sequence>();
205
94
    const Sequence& sy = y.getConst<Sequence>();
206
94
    return sx.rfind(sy, start);
207
  }
208
  Unimplemented();
209
  return 0;
210
}
211
212
5581
bool Word::hasPrefix(TNode x, TNode y)
213
{
214
5581
  Kind k = x.getKind();
215
5581
  if (k == CONST_STRING)
216
  {
217
5581
    Assert(y.getKind() == CONST_STRING);
218
11162
    String sx = x.getConst<String>();
219
11162
    String sy = y.getConst<String>();
220
5581
    return sx.hasPrefix(sy);
221
  }
222
  else if (k == CONST_SEQUENCE)
223
  {
224
    Assert(y.getKind() == CONST_SEQUENCE);
225
    const Sequence& sx = x.getConst<Sequence>();
226
    const Sequence& sy = y.getConst<Sequence>();
227
    return sx.hasPrefix(sy);
228
  }
229
  Unimplemented();
230
  return false;
231
}
232
233
9401
bool Word::hasSuffix(TNode x, TNode y)
234
{
235
9401
  Kind k = x.getKind();
236
9401
  if (k == CONST_STRING)
237
  {
238
9371
    Assert(y.getKind() == CONST_STRING);
239
18742
    String sx = x.getConst<String>();
240
18742
    String sy = y.getConst<String>();
241
9371
    return sx.hasSuffix(sy);
242
  }
243
30
  else if (k == CONST_SEQUENCE)
244
  {
245
30
    Assert(y.getKind() == CONST_SEQUENCE);
246
30
    const Sequence& sx = x.getConst<Sequence>();
247
30
    const Sequence& sy = y.getConst<Sequence>();
248
30
    return sx.hasSuffix(sy);
249
  }
250
  Unimplemented();
251
  return false;
252
}
253
254
103
Node Word::update(TNode x, std::size_t i, TNode t)
255
{
256
103
  NodeManager* nm = NodeManager::currentNM();
257
103
  Kind k = x.getKind();
258
103
  if (k == CONST_STRING)
259
  {
260
93
    Assert(t.getKind() == CONST_STRING);
261
186
    String sx = x.getConst<String>();
262
186
    String st = t.getConst<String>();
263
93
    return nm->mkConst(String(sx.update(i, st)));
264
  }
265
10
  else if (k == CONST_SEQUENCE)
266
  {
267
10
    Assert(t.getKind() == CONST_SEQUENCE);
268
10
    const Sequence& sx = x.getConst<Sequence>();
269
10
    const Sequence& st = t.getConst<Sequence>();
270
20
    Sequence res = sx.update(i, st);
271
10
    return nm->mkConst(res);
272
  }
273
  Unimplemented();
274
  return Node::null();
275
}
276
6
Node Word::replace(TNode x, TNode y, TNode t)
277
{
278
6
  NodeManager* nm = NodeManager::currentNM();
279
6
  Kind k = x.getKind();
280
6
  if (k == CONST_STRING)
281
  {
282
6
    Assert(y.getKind() == CONST_STRING);
283
6
    Assert(t.getKind() == CONST_STRING);
284
12
    String sx = x.getConst<String>();
285
12
    String sy = y.getConst<String>();
286
12
    String st = t.getConst<String>();
287
6
    return nm->mkConst(String(sx.replace(sy, st)));
288
  }
289
  else if (k == CONST_SEQUENCE)
290
  {
291
    Assert(y.getKind() == CONST_SEQUENCE);
292
    Assert(t.getKind() == CONST_SEQUENCE);
293
    const Sequence& sx = x.getConst<Sequence>();
294
    const Sequence& sy = y.getConst<Sequence>();
295
    const Sequence& st = t.getConst<Sequence>();
296
    Sequence res = sx.replace(sy, st);
297
    return nm->mkConst(res);
298
  }
299
  Unimplemented();
300
  return Node::null();
301
}
302
16181
Node Word::substr(TNode x, std::size_t i)
303
{
304
16181
  NodeManager* nm = NodeManager::currentNM();
305
16181
  Kind k = x.getKind();
306
16181
  if (k == CONST_STRING)
307
  {
308
32360
    String sx = x.getConst<String>();
309
16180
    return nm->mkConst(String(sx.substr(i)));
310
  }
311
1
  else if (k == CONST_SEQUENCE)
312
  {
313
1
    const Sequence& sx = x.getConst<Sequence>();
314
2
    Sequence res = sx.substr(i);
315
1
    return nm->mkConst(res);
316
  }
317
  Unimplemented();
318
  return Node::null();
319
}
320
45517
Node Word::substr(TNode x, std::size_t i, std::size_t j)
321
{
322
45517
  NodeManager* nm = NodeManager::currentNM();
323
45517
  Kind k = x.getKind();
324
45517
  if (k == CONST_STRING)
325
  {
326
90928
    String sx = x.getConst<String>();
327
45464
    return nm->mkConst(String(sx.substr(i, j)));
328
  }
329
53
  else if (k == CONST_SEQUENCE)
330
  {
331
53
    const Sequence& sx = x.getConst<Sequence>();
332
106
    Sequence res = sx.substr(i, j);
333
53
    return nm->mkConst(res);
334
  }
335
  Unimplemented();
336
  return Node::null();
337
}
338
339
19280
Node Word::prefix(TNode x, std::size_t i) { return substr(x, 0, i); }
340
341
27718
Node Word::suffix(TNode x, std::size_t i)
342
{
343
27718
  NodeManager* nm = NodeManager::currentNM();
344
27718
  Kind k = x.getKind();
345
27718
  if (k == CONST_STRING)
346
  {
347
55406
    String sx = x.getConst<String>();
348
27703
    return nm->mkConst(String(sx.suffix(i)));
349
  }
350
15
  else if (k == CONST_SEQUENCE)
351
  {
352
15
    const Sequence& sx = x.getConst<Sequence>();
353
30
    Sequence res = sx.suffix(i);
354
15
    return nm->mkConst(res);
355
  }
356
  Unimplemented();
357
  return Node::null();
358
}
359
360
363
bool Word::noOverlapWith(TNode x, TNode y)
361
{
362
363
  Kind k = x.getKind();
363
363
  if (k == CONST_STRING)
364
  {
365
363
    Assert(y.getKind() == CONST_STRING);
366
726
    String sx = x.getConst<String>();
367
726
    String sy = y.getConst<String>();
368
363
    return sx.noOverlapWith(sy);
369
  }
370
  else if (k == CONST_SEQUENCE)
371
  {
372
    Assert(y.getKind() == CONST_SEQUENCE);
373
    const Sequence& sx = x.getConst<Sequence>();
374
    const Sequence& sy = y.getConst<Sequence>();
375
    return sx.noOverlapWith(sy);
376
  }
377
  Unimplemented();
378
  return false;
379
}
380
381
4503
std::size_t Word::overlap(TNode x, TNode y)
382
{
383
4503
  Kind k = x.getKind();
384
4503
  if (k == CONST_STRING)
385
  {
386
4461
    Assert(y.getKind() == CONST_STRING);
387
8922
    String sx = x.getConst<String>();
388
8922
    String sy = y.getConst<String>();
389
4461
    return sx.overlap(sy);
390
  }
391
42
  else if (k == CONST_SEQUENCE)
392
  {
393
42
    Assert(y.getKind() == CONST_SEQUENCE);
394
42
    const Sequence& sx = x.getConst<Sequence>();
395
42
    const Sequence& sy = y.getConst<Sequence>();
396
42
    return sx.overlap(sy);
397
  }
398
  Unimplemented();
399
  return 0;
400
}
401
402
1979
std::size_t Word::roverlap(TNode x, TNode y)
403
{
404
1979
  Kind k = x.getKind();
405
1979
  if (k == CONST_STRING)
406
  {
407
1979
    Assert(y.getKind() == CONST_STRING);
408
3958
    String sx = x.getConst<String>();
409
3958
    String sy = y.getConst<String>();
410
1979
    return sx.roverlap(sy);
411
  }
412
  else if (k == CONST_SEQUENCE)
413
  {
414
    Assert(y.getKind() == CONST_SEQUENCE);
415
    const Sequence& sx = x.getConst<Sequence>();
416
    const Sequence& sy = y.getConst<Sequence>();
417
    return sx.roverlap(sy);
418
  }
419
  Unimplemented();
420
  return 0;
421
}
422
423
bool Word::isRepeated(TNode x)
424
{
425
  Kind k = x.getKind();
426
  if (k == CONST_STRING)
427
  {
428
    return x.getConst<String>().isRepeated();
429
  }
430
  else if (k == CONST_SEQUENCE)
431
  {
432
    return x.getConst<Sequence>().isRepeated();
433
  }
434
  Unimplemented();
435
  return false;
436
}
437
438
28879
Node Word::splitConstant(TNode x, TNode y, size_t& index, bool isRev)
439
{
440
28879
  Assert(x.isConst() && y.isConst());
441
28879
  size_t lenA = getLength(x);
442
28879
  size_t lenB = getLength(y);
443
28879
  index = lenA <= lenB ? 1 : 0;
444
28879
  size_t lenShort = index == 1 ? lenA : lenB;
445
28879
  bool cmp = isRev ? rstrncmp(x, y, lenShort) : strncmp(x, y, lenShort);
446
28879
  if (cmp)
447
  {
448
56188
    Node l = index == 0 ? x : y;
449
28094
    if (isRev)
450
    {
451
15203
      size_t new_len = getLength(l) - lenShort;
452
15203
      return substr(l, 0, new_len);
453
    }
454
    else
455
    {
456
12891
      return substr(l, lenShort);
457
    }
458
  }
459
  // not the same prefix/suffix
460
785
  return Node::null();
461
}
462
463
64
Node Word::reverse(TNode x)
464
{
465
64
  NodeManager* nm = NodeManager::currentNM();
466
64
  Kind k = x.getKind();
467
64
  if (k == CONST_STRING)
468
  {
469
120
    String sx = x.getConst<String>();
470
120
    std::vector<unsigned> nvec = sx.getVec();
471
60
    std::reverse(nvec.begin(), nvec.end());
472
60
    return nm->mkConst(String(nvec));
473
  }
474
4
  else if (k == CONST_SEQUENCE)
475
  {
476
4
    const Sequence& sx = x.getConst<Sequence>();
477
4
    const std::vector<Node>& vecc = sx.getVec();
478
8
    std::vector<Node> vecr(vecc.begin(), vecc.end());
479
4
    std::reverse(vecr.begin(), vecr.end());
480
8
    Sequence res(sx.getType(), vecr);
481
4
    return nm->mkConst(res);
482
  }
483
  Unimplemented();
484
  return Node::null();
485
}
486
487
}  // namespace strings
488
}  // namespace theory
489
26685
}  // namespace CVC4