Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/expr/sequence.cpp	Lines:	105	191	55.0 %
Date:	2021-05-22	Branches:	117	564	20.7 %


/******************************************************************************
 * 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 <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 <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	14136	Sequence::Sequence(const TypeNode& t, const std::vector<Node>& s)
29	14136	: d_type(new TypeNode(t)), d_seq(s)
30		{
31	14136	}
32
33	2036	Sequence::Sequence(const Sequence& seq)
34	2036	: d_type(new TypeNode(seq.getType())), d_seq(seq.getVec())
35		{
36	2036	}
37
38	16172	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	21373	int Sequence::cmp(const Sequence& y) const
51		{
52	21373	if (getType() != y.getType())
53		{
54	5243	return getType() < y.getType() ? -1 : 1;
55		}
56	16130	if (size() != y.size())
57		{
58		return size() < y.size() ? -1 : 1;
59		}
60	19731	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	16126	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	69593	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	60953	const TypeNode& Sequence::getType() const { return *d_type; }
179
180	29202	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	22196	size_t SequenceHashFunction::operator()(const Sequence& s) const
372		{
373	22196	size_t ret = 0;
374	22196	const std::vector<Node>& vec = s.getVec();
375	26694	for (const Node& n : vec)
376		{
377	4498	ret = fnv1a::fnv1a_64(ret, std::hash<Node>()(n));
378		}
379	22196	return ret;
380		}
381
382	28194	} // namespace cvc5