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