Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/expr/sequence.cpp	Lines:	103	191	53.9 %
Date:	2021-09-29	Branches:	111	562	19.8 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Andres Noetzli
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Implementation of the sequence data type.
 */

#include "expr/sequence.h"

#include <limits>
#include <sstream>
#include <vector>

#include "expr/node.h"
#include "expr/type_node.h"

using namespace std;

namespace cvc5 {

Sequence::Sequence(const TypeNode& t, const std::vector<Node>& s)
    : d_type(new TypeNode(t)), d_seq(s)
{
}

Sequence::Sequence(const Sequence& seq)
    : d_type(new TypeNode(seq.getType())), d_seq(seq.getVec())
{
}

Sequence::~Sequence() {}

Sequence& Sequence::operator=(const Sequence& y)
{
  if (this != &y)
  {
    d_type.reset(new TypeNode(y.getType()));
    d_seq = y.getVec();
  }
  return *this;
}

int Sequence::cmp(const Sequence& y) const
{
  if (getType() != y.getType())
  {
    return getType() < y.getType() ? -1 : 1;
  }
  if (size() != y.size())
  {
    return size() < y.size() ? -1 : 1;
  }
  for (size_t i = 0, sz = size(); i < sz; ++i)
  {
    if (nth(i) != y.nth(i))
    {
      return nth(i) < y.nth(i) ? -1 : 1;
    }
  }
  return 0;
}

Sequence Sequence::concat(const Sequence& other) const
{
  Assert(getType() == other.getType());
  std::vector<Node> ret_vec(d_seq);
  ret_vec.insert(ret_vec.end(), other.d_seq.begin(), other.d_seq.end());
  return Sequence(getType(), ret_vec);
}

bool Sequence::strncmp(const Sequence& y, size_t n) const
{
  Assert(getType() == y.getType());
  size_t b = (size() >= y.size()) ? size() : y.size();
  size_t s = (size() <= y.size()) ? size() : y.size();
  if (n > s)
  {
    if (b != s)
    {
      return false;
    }
    n = s;
  }
  for (size_t i = 0; i < n; ++i)
  {
    if (nth(i) != y.nth(i))
    {
      return false;
    }
  }
  return true;
}

bool Sequence::rstrncmp(const Sequence& y, size_t n) const
{
  Assert(getType() == y.getType());
  size_t b = (size() >= y.size()) ? size() : y.size();
  size_t s = (size() <= y.size()) ? size() : y.size();
  if (n > s)
  {
    if (b != s)
    {
      return false;
    }
    n = s;
  }
  for (size_t i = 0; i < n; ++i)
  {
    if (nth(size() - i - 1) != y.nth(y.size() - i - 1))
    {
      return false;
    }
  }
  return true;
}

bool Sequence::empty() const { return d_seq.empty(); }

size_t Sequence::size() const { return d_seq.size(); }

const Node& Sequence::front() const
{
  Assert(!d_seq.empty());
  return d_seq.front();
}

const Node& Sequence::back() const
{
  Assert(!d_seq.empty());
  return d_seq.back();
}

const Node& Sequence::nth(size_t i) const
{
  Assert(i < size());
  return d_seq[i];
}

size_t Sequence::overlap(const Sequence& y) const
{
  Assert(getType() == y.getType());
  size_t i = size() < y.size() ? size() : y.size();
  for (; i > 0; i--)
  {
    Sequence s = suffix(i);
    Sequence p = y.prefix(i);
    if (s == p)
    {
      return i;
    }
  }
  return i;
}

size_t Sequence::roverlap(const Sequence& y) const
{
  Assert(getType() == y.getType());
  size_t i = size() < y.size() ? size() : y.size();
  for (; i > 0; i--)
  {
    Sequence s = prefix(i);
    Sequence p = y.suffix(i);
    if (s == p)
    {
      return i;
    }
  }
  return i;
}

const TypeNode& Sequence::getType() const { return *d_type; }

const std::vector<Node>& Sequence::getVec() const { return d_seq; }

bool Sequence::isRepeated() const
{
  if (size() > 1)
  {
    Node f = nth(0);
    for (unsigned i = 1, sz = size(); i < sz; ++i)
    {
      if (f != nth(i))
      {
        return false;
      }
    }
  }
  return true;
}

size_t Sequence::find(const Sequence& y, size_t start) const
{
  Assert(getType() == y.getType());
  if (size() < y.size() + start)
  {
    return std::string::npos;
  }
  if (y.empty())
  {
    return start;
  }
  if (empty())
  {
    return std::string::npos;
  }
  std::vector<Node>::const_iterator itr = std::search(
      d_seq.begin() + start, d_seq.end(), y.d_seq.begin(), y.d_seq.end());
  if (itr != d_seq.end())
  {
    return itr - d_seq.begin();
  }
  return std::string::npos;
}

size_t Sequence::rfind(const Sequence& y, size_t start) const
{
  Assert(getType() == y.getType());
  if (size() < y.size() + start)
  {
    return std::string::npos;
  }
  if (y.empty())
  {
    return start;
  }
  if (empty())
  {
    return std::string::npos;
  }
  std::vector<Node>::const_reverse_iterator itr = std::search(
      d_seq.rbegin() + start, d_seq.rend(), y.d_seq.rbegin(), y.d_seq.rend());
  if (itr != d_seq.rend())
  {
    return itr - d_seq.rbegin();
  }
  return std::string::npos;
}

bool Sequence::hasPrefix(const Sequence& y) const
{
  Assert(getType() == y.getType());
  size_t s = size();
  size_t ys = y.size();
  if (ys > s)
  {
    return false;
  }
  for (size_t i = 0; i < ys; i++)
  {
    if (nth(i) != y.nth(i))
    {
      return false;
    }
  }
  return true;
}

bool Sequence::hasSuffix(const Sequence& y) const
{
  Assert(getType() == y.getType());
  size_t s = size();
  size_t ys = y.size();
  if (ys > s)
  {
    return false;
  }
  size_t idiff = s - ys;
  for (size_t i = 0; i < ys; i++)
  {
    if (nth(i + idiff) != y.nth(i))
    {
      return false;
    }
  }
  return true;
}

Sequence Sequence::update(size_t i, const Sequence& t) const
{
  Assert(getType() == t.getType());
  if (i < size())
  {
    std::vector<Node> vec(d_seq.begin(), d_seq.begin() + i);
    size_t remNum = size() - i;
    size_t tnum = t.d_seq.size();
    if (tnum >= remNum)
    {
      vec.insert(vec.end(), t.d_seq.begin(), t.d_seq.begin() + remNum);
    }
    else
    {
      vec.insert(vec.end(), t.d_seq.begin(), t.d_seq.end());
      vec.insert(vec.end(), d_seq.begin() + i + tnum, d_seq.end());
    }
    return Sequence(getType(), vec);
  }
  return *this;
}

Sequence Sequence::replace(const Sequence& s, const Sequence& t) const
{
  Assert(getType() == s.getType());
  Assert(getType() == t.getType());
  size_t ret = find(s);
  if (ret != std::string::npos)
  {
    std::vector<Node> vec;
    vec.insert(vec.begin(), d_seq.begin(), d_seq.begin() + ret);
    vec.insert(vec.end(), t.d_seq.begin(), t.d_seq.end());
    vec.insert(vec.end(), d_seq.begin() + ret + s.size(), d_seq.end());
    return Sequence(getType(), vec);
  }
  return *this;
}

Sequence Sequence::substr(size_t i) const
{
  Assert(i >= 0);
  Assert(i <= size());
  std::vector<Node> retVec(d_seq.begin() + i, d_seq.end());
  return Sequence(getType(), retVec);
}

Sequence Sequence::substr(size_t i, size_t j) const
{
  Assert(i >= 0);
  Assert(j >= 0);
  Assert(i + j <= size());
  std::vector<Node>::const_iterator itr = d_seq.begin() + i;
  std::vector<Node> retVec(itr, itr + j);
  return Sequence(getType(), retVec);
}

bool Sequence::noOverlapWith(const Sequence& y) const
{
  Assert(getType() == y.getType());
  return y.find(*this) == std::string::npos
         && this->find(y) == std::string::npos && this->overlap(y) == 0
         && y.overlap(*this) == 0;
}

size_t Sequence::maxSize() { return std::numeric_limits<uint32_t>::max(); }

std::ostream& operator<<(std::ostream& os, const Sequence& s)
{
  const std::vector<Node>& vec = s.getVec();
  std::stringstream ss;
  if (vec.empty())
  {
    ss << "(as seq.empty " << s.getType() << ")";
  }
  else
  {
    ss << "(seq.++";
    for (const Node& n : vec)
    {
      ss << " " << n;
    }
    ss << ")";
  }
  return os << ss.str();
}

size_t SequenceHashFunction::operator()(const Sequence& s) const
{
  size_t ret = 0;
  const std::vector<Node>& vec = s.getVec();
  for (const Node& n : vec)
  {
    ret = fnv1a::fnv1a_64(ret, std::hash<Node>()(n));
  }
  return ret;
}

}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

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