GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/sequence.cpp Lines: 105 191 55.0 %
Date: 2021-03-22 Branches: 118 566 20.8 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sequence.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 the sequence data type.
13
 **/
14
15
#include "expr/sequence.h"
16
17
#include <sstream>
18
#include <vector>
19
20
#include "expr/node.h"
21
#include "expr/type_node.h"
22
23
using namespace std;
24
25
namespace CVC4 {
26
27
13873
Sequence::Sequence(const TypeNode& t, const std::vector<Node>& s)
28
13873
    : d_type(new TypeNode(t)), d_seq(s)
29
{
30
13873
}
31
32
1926
Sequence::Sequence(const Sequence& seq)
33
1926
    : d_type(new TypeNode(seq.getType())), d_seq(seq.getVec())
34
{
35
1926
}
36
37
15793
Sequence::~Sequence() {}
38
39
Sequence& Sequence::operator=(const Sequence& y)
40
{
41
  if (this != &y)
42
  {
43
    d_type.reset(new TypeNode(y.getType()));
44
    d_seq = y.getVec();
45
  }
46
  return *this;
47
}
48
49
20908
int Sequence::cmp(const Sequence& y) const
50
{
51
20908
  if (getType() != y.getType())
52
  {
53
5163
    return getType() < y.getType() ? -1 : 1;
54
  }
55
15745
  if (size() != y.size())
56
  {
57
    return size() < y.size() ? -1 : 1;
58
  }
59
19285
  for (size_t i = 0, sz = size(); i < sz; ++i)
60
  {
61
3544
    if (nth(i) != y.nth(i))
62
    {
63
4
      return nth(i) < y.nth(i) ? -1 : 1;
64
    }
65
  }
66
15741
  return 0;
67
}
68
69
Sequence Sequence::concat(const Sequence& other) const
70
{
71
  Assert(getType() == other.getType());
72
  std::vector<Node> ret_vec(d_seq);
73
  ret_vec.insert(ret_vec.end(), other.d_seq.begin(), other.d_seq.end());
74
  return Sequence(getType(), ret_vec);
75
}
76
77
4
bool Sequence::strncmp(const Sequence& y, size_t n) const
78
{
79
4
  Assert(getType() == y.getType());
80
4
  size_t b = (size() >= y.size()) ? size() : y.size();
81
4
  size_t s = (size() <= y.size()) ? size() : y.size();
82
4
  if (n > s)
83
  {
84
    if (b != s)
85
    {
86
      return false;
87
    }
88
    n = s;
89
  }
90
4
  for (size_t i = 0; i < n; ++i)
91
  {
92
4
    if (nth(i) != y.nth(i))
93
    {
94
4
      return false;
95
    }
96
  }
97
  return true;
98
}
99
100
67
bool Sequence::rstrncmp(const Sequence& y, size_t n) const
101
{
102
67
  Assert(getType() == y.getType());
103
67
  size_t b = (size() >= y.size()) ? size() : y.size();
104
67
  size_t s = (size() <= y.size()) ? size() : y.size();
105
67
  if (n > s)
106
  {
107
    if (b != s)
108
    {
109
      return false;
110
    }
111
    n = s;
112
  }
113
162
  for (size_t i = 0; i < n; ++i)
114
  {
115
95
    if (nth(size() - i - 1) != y.nth(y.size() - i - 1))
116
    {
117
      return false;
118
    }
119
  }
120
67
  return true;
121
}
122
123
632
bool Sequence::empty() const { return d_seq.empty(); }
124
125
68001
size_t Sequence::size() const { return d_seq.size(); }
126
127
const Node& Sequence::front() const
128
{
129
  Assert(!d_seq.empty());
130
  return d_seq.front();
131
}
132
133
const Node& Sequence::back() const
134
{
135
  Assert(!d_seq.empty());
136
  return d_seq.back();
137
}
138
139
7354
const Node& Sequence::nth(size_t i) const
140
{
141
7354
  Assert(i < size());
142
7354
  return d_seq[i];
143
}
144
145
42
size_t Sequence::overlap(const Sequence& y) const
146
{
147
42
  Assert(getType() == y.getType());
148
42
  size_t i = size() < y.size() ? size() : y.size();
149
50
  for (; i > 0; i--)
150
  {
151
46
    Sequence s = suffix(i);
152
46
    Sequence p = y.prefix(i);
153
42
    if (s == p)
154
    {
155
38
      return i;
156
    }
157
  }
158
4
  return i;
159
}
160
161
size_t Sequence::roverlap(const Sequence& y) const
162
{
163
  Assert(getType() == y.getType());
164
  size_t i = size() < y.size() ? size() : y.size();
165
  for (; i > 0; i--)
166
  {
167
    Sequence s = prefix(i);
168
    Sequence p = y.suffix(i);
169
    if (s == p)
170
    {
171
      return i;
172
    }
173
  }
174
  return i;
175
}
176
177
59631
const TypeNode& Sequence::getType() const { return *d_type; }
178
179
28264
const std::vector<Node>& Sequence::getVec() const { return d_seq; }
180
181
bool Sequence::isRepeated() const
182
{
183
  if (size() > 1)
184
  {
185
    Node f = nth(0);
186
    for (unsigned i = 1, sz = size(); i < sz; ++i)
187
    {
188
      if (f != nth(i))
189
      {
190
        return false;
191
      }
192
    }
193
  }
194
  return true;
195
}
196
197
261
size_t Sequence::find(const Sequence& y, size_t start) const
198
{
199
261
  Assert(getType() == y.getType());
200
261
  if (size() < y.size() + start)
201
  {
202
1
    return std::string::npos;
203
  }
204
260
  if (y.empty())
205
  {
206
    return start;
207
  }
208
260
  if (empty())
209
  {
210
    return std::string::npos;
211
  }
212
  std::vector<Node>::const_iterator itr = std::search(
213
260
      d_seq.begin() + start, d_seq.end(), y.d_seq.begin(), y.d_seq.end());
214
260
  if (itr != d_seq.end())
215
  {
216
249
    return itr - d_seq.begin();
217
  }
218
11
  return std::string::npos;
219
}
220
221
94
size_t Sequence::rfind(const Sequence& y, size_t start) const
222
{
223
94
  Assert(getType() == y.getType());
224
94
  if (size() < y.size() + start)
225
  {
226
38
    return std::string::npos;
227
  }
228
56
  if (y.empty())
229
  {
230
    return start;
231
  }
232
56
  if (empty())
233
  {
234
    return std::string::npos;
235
  }
236
  std::vector<Node>::const_reverse_iterator itr = std::search(
237
56
      d_seq.rbegin() + start, d_seq.rend(), y.d_seq.rbegin(), y.d_seq.rend());
238
56
  if (itr != d_seq.rend())
239
  {
240
56
    return itr - d_seq.rbegin();
241
  }
242
  return std::string::npos;
243
}
244
245
bool Sequence::hasPrefix(const Sequence& y) const
246
{
247
  Assert(getType() == y.getType());
248
  size_t s = size();
249
  size_t ys = y.size();
250
  if (ys > s)
251
  {
252
    return false;
253
  }
254
  for (size_t i = 0; i < ys; i++)
255
  {
256
    if (nth(i) != y.nth(i))
257
    {
258
      return false;
259
    }
260
  }
261
  return true;
262
}
263
264
30
bool Sequence::hasSuffix(const Sequence& y) const
265
{
266
30
  Assert(getType() == y.getType());
267
30
  size_t s = size();
268
30
  size_t ys = y.size();
269
30
  if (ys > s)
270
  {
271
    return false;
272
  }
273
30
  size_t idiff = s - ys;
274
60
  for (size_t i = 0; i < ys; i++)
275
  {
276
30
    if (nth(i + idiff) != y.nth(i))
277
    {
278
      return false;
279
    }
280
  }
281
30
  return true;
282
}
283
284
10
Sequence Sequence::update(size_t i, const Sequence& t) const
285
{
286
10
  Assert(getType() == t.getType());
287
10
  if (i < size())
288
  {
289
20
    std::vector<Node> vec(d_seq.begin(), d_seq.begin() + i);
290
10
    size_t remNum = size() - i;
291
10
    size_t tnum = t.d_seq.size();
292
10
    if (tnum >= remNum)
293
    {
294
2
      vec.insert(vec.end(), t.d_seq.begin(), t.d_seq.begin() + remNum);
295
    }
296
    else
297
    {
298
8
      vec.insert(vec.end(), t.d_seq.begin(), t.d_seq.end());
299
8
      vec.insert(vec.end(), d_seq.begin() + i + tnum, d_seq.end());
300
    }
301
10
    return Sequence(getType(), vec);
302
  }
303
  return *this;
304
}
305
306
Sequence Sequence::replace(const Sequence& s, const Sequence& t) const
307
{
308
  Assert(getType() == s.getType());
309
  Assert(getType() == t.getType());
310
  size_t ret = find(s);
311
  if (ret != std::string::npos)
312
  {
313
    std::vector<Node> vec;
314
    vec.insert(vec.begin(), d_seq.begin(), d_seq.begin() + ret);
315
    vec.insert(vec.end(), t.d_seq.begin(), t.d_seq.end());
316
    vec.insert(vec.end(), d_seq.begin() + ret + s.size(), d_seq.end());
317
    return Sequence(getType(), vec);
318
  }
319
  return *this;
320
}
321
322
1
Sequence Sequence::substr(size_t i) const
323
{
324
1
  Assert(i >= 0);
325
1
  Assert(i <= size());
326
2
  std::vector<Node> retVec(d_seq.begin() + i, d_seq.end());
327
2
  return Sequence(getType(), retVec);
328
}
329
330
152
Sequence Sequence::substr(size_t i, size_t j) const
331
{
332
152
  Assert(i >= 0);
333
152
  Assert(j >= 0);
334
152
  Assert(i + j <= size());
335
152
  std::vector<Node>::const_iterator itr = d_seq.begin() + i;
336
304
  std::vector<Node> retVec(itr, itr + j);
337
304
  return Sequence(getType(), retVec);
338
}
339
340
bool Sequence::noOverlapWith(const Sequence& y) const
341
{
342
  Assert(getType() == y.getType());
343
  return y.find(*this) == std::string::npos
344
         && this->find(y) == std::string::npos && this->overlap(y) == 0
345
         && y.overlap(*this) == 0;
346
}
347
348
size_t Sequence::maxSize() { return std::numeric_limits<uint32_t>::max(); }
349
350
std::ostream& operator<<(std::ostream& os, const Sequence& s)
351
{
352
  const std::vector<Node>& vec = s.getVec();
353
  std::stringstream ss;
354
  if (vec.empty())
355
  {
356
    ss << "(as seq.empty " << s.getType() << ")";
357
  }
358
  else
359
  {
360
    ss << "(seq.++";
361
    for (const Node& n : vec)
362
    {
363
      ss << " " << n;
364
    }
365
    ss << ")";
366
  }
367
  return os << ss.str();
368
}
369
370
21481
size_t SequenceHashFunction::operator()(const Sequence& s) const
371
{
372
21481
  size_t ret = 0;
373
21481
  const std::vector<Node>& vec = s.getVec();
374
25861
  for (const Node& n : vec)
375
  {
376
4380
    ret = fnv1a::fnv1a_64(ret, NodeHashFunction()(n));
377
  }
378
21481
  return ret;
379
}
380
381
26676
}  // namespace CVC4