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