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