Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/strings/type_enumerator.cpp	Lines:	117	137	85.4 %
Date:	2021-05-22	Branches:	78	236	33.1 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Mathias Preiner, 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 enumerators for strings.
 */

#include "theory/strings/type_enumerator.h"

#include "theory/strings/theory_strings_utils.h"
#include "util/string.h"

namespace cvc5 {
namespace theory {
namespace strings {

Node makeStandardModelConstant(const std::vector<unsigned>& vec,
                               uint32_t cardinality)
{
  std::vector<unsigned> mvec;
  // if we contain all of the printable characters
  if (cardinality >= 255)
  {
    for (unsigned i = 0, vsize = vec.size(); i < vsize; i++)
    {
      unsigned curr = vec[i];
      // convert
      Assert(vec[i] < cardinality);
      if (vec[i] <= 61)
      {
        // first 62 printable characters [\u{65}-\u{126}]: 'A', 'B', 'C', ...
        curr = vec[i] + 65;
      }
      else if (vec[i] <= 94)
      {
        // remaining 33 printable characters [\u{32}-\u{64}]: ' ', '!', '"', ...
        curr = vec[i] - 30;
      }
      else
      {
        // the remaining characters, starting with \u{127} and wrapping around
        // the first 32 non-printable characters.
        curr = (vec[i] + 32) % cardinality;
      }
      mvec.push_back(curr);
    }
  }
  else
  {
    mvec = vec;
  }
  return NodeManager::currentNM()->mkConst(String(mvec));
}

WordIter::WordIter(uint32_t startLength) : d_hasEndLength(false), d_endLength(0)
{
  for (uint32_t i = 0; i < startLength; i++)
  {
    d_data.push_back(0);
  }
}
WordIter::WordIter(uint32_t startLength, uint32_t endLength)
    : d_hasEndLength(true), d_endLength(endLength)
{
  for (uint32_t i = 0; i < startLength; i++)
  {
    d_data.push_back(0);
  }
}

WordIter::WordIter(const WordIter& witer)
    : d_hasEndLength(witer.d_hasEndLength),
      d_endLength(witer.d_endLength),
      d_data(witer.d_data)
{
}

const std::vector<unsigned>& WordIter::getData() const { return d_data; }

bool WordIter::increment(uint32_t card)
{
  for (unsigned i = 0, dsize = d_data.size(); i < dsize; ++i)
  {
    if (d_data[i] + 1 < card)
    {
      ++d_data[i];
      return true;
    }
    else
    {
      d_data[i] = 0;
    }
  }
  if (d_hasEndLength && d_data.size() == d_endLength)
  {
    return false;
  }
  // otherwise increase length
  d_data.push_back(0);
  return true;
}

SEnumLen::SEnumLen(TypeNode tn, uint32_t startLength)
    : d_type(tn), d_witer(new WordIter(startLength))
{
}
SEnumLen::SEnumLen(TypeNode tn, uint32_t startLength, uint32_t endLength)
    : d_type(tn), d_witer(new WordIter(startLength, endLength))
{
}

SEnumLen::SEnumLen(const SEnumLen& e)
    : d_type(e.d_type), d_witer(new WordIter(*e.d_witer)), d_curr(e.d_curr)
{
}

Node SEnumLen::getCurrent() const { return d_curr; }

bool SEnumLen::isFinished() const { return d_curr.isNull(); }

StringEnumLen::StringEnumLen(uint32_t startLength,
                             uint32_t endLength,
                             uint32_t card)
    : SEnumLen(NodeManager::currentNM()->stringType(), startLength, endLength),
      d_cardinality(card)
{
  mkCurr();
}

StringEnumLen::StringEnumLen(uint32_t startLength, uint32_t card)
    : SEnumLen(NodeManager::currentNM()->stringType(), startLength),
      d_cardinality(card)
{
  mkCurr();
}

bool StringEnumLen::increment()
{
  // always use the same cardinality
  if (!d_witer->increment(d_cardinality))
  {
    d_curr = Node::null();
    return false;
  }
  mkCurr();
  return true;
}

void StringEnumLen::mkCurr()
{
  d_curr = makeStandardModelConstant(d_witer->getData(), d_cardinality);
}

SeqEnumLen::SeqEnumLen(TypeNode tn,
                       TypeEnumeratorProperties* tep,
                       uint32_t startLength)
    : SEnumLen(tn, startLength)
{
  d_elementEnumerator.reset(
      new TypeEnumerator(d_type.getSequenceElementType(), tep));
  mkCurr();
}

SeqEnumLen::SeqEnumLen(TypeNode tn,
                       TypeEnumeratorProperties* tep,
                       uint32_t startLength,
                       uint32_t endLength)
    : SEnumLen(tn, startLength, endLength)
{
  d_elementEnumerator.reset(
      new TypeEnumerator(d_type.getSequenceElementType(), tep));
  // ensure non-empty element domain
  d_elementDomain.push_back((**d_elementEnumerator));
  ++(*d_elementEnumerator);
  mkCurr();
}

SeqEnumLen::SeqEnumLen(const SeqEnumLen& wenum)
    : SEnumLen(wenum),
      d_elementEnumerator(new TypeEnumerator(*wenum.d_elementEnumerator)),
      d_elementDomain(wenum.d_elementDomain)
{
}

bool SeqEnumLen::increment()
{
  if (!d_elementEnumerator->isFinished())
  {
    // yet to establish domain
    Assert(d_elementEnumerator != nullptr);
    d_elementDomain.push_back((**d_elementEnumerator));
    ++(*d_elementEnumerator);
  }
  // the current cardinality is the domain size of the element
  if (!d_witer->increment(d_elementDomain.size()))
  {
    Assert(d_elementEnumerator->isFinished());
    d_curr = Node::null();
    return false;
  }
  mkCurr();
  return true;
}

void SeqEnumLen::mkCurr()
{
  std::vector<Node> seq;
  const std::vector<unsigned>& data = d_witer->getData();
  for (unsigned i : data)
  {
    Assert(i < d_elementDomain.size());
    seq.push_back(d_elementDomain[i]);
  }
  // make sequence from seq
  d_curr = NodeManager::currentNM()->mkConst(
      Sequence(d_type.getSequenceElementType(), seq));
}

StringEnumerator::StringEnumerator(TypeNode type, TypeEnumeratorProperties* tep)
    : TypeEnumeratorBase<StringEnumerator>(type),
      d_wenum(0, utils::getAlphabetCardinality())
{
  Assert(type.getKind() == kind::TYPE_CONSTANT
         && type.getConst<TypeConstant>() == STRING_TYPE);
}

StringEnumerator::StringEnumerator(const StringEnumerator& enumerator)
    : TypeEnumeratorBase<StringEnumerator>(enumerator.getType()),
      d_wenum(enumerator.d_wenum)
{
}

Node StringEnumerator::operator*() { return d_wenum.getCurrent(); }

StringEnumerator& StringEnumerator::operator++()
{
  d_wenum.increment();
  return *this;
}

bool StringEnumerator::isFinished() { return d_wenum.isFinished(); }

SequenceEnumerator::SequenceEnumerator(TypeNode type,
                                       TypeEnumeratorProperties* tep)
    : TypeEnumeratorBase<SequenceEnumerator>(type), d_wenum(type, tep, 0)
{
}

SequenceEnumerator::SequenceEnumerator(const SequenceEnumerator& enumerator)
    : TypeEnumeratorBase<SequenceEnumerator>(enumerator.getType()),
      d_wenum(enumerator.d_wenum)
{
}

Node SequenceEnumerator::operator*() { return d_wenum.getCurrent(); }

SequenceEnumerator& SequenceEnumerator::operator++()
{
  d_wenum.increment();
  return *this;
}

bool SequenceEnumerator::isFinished() { return d_wenum.isFinished(); }

}  // namespace strings
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Mathias Preiner, 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 enumerators for strings.
14		*/
15
16		#include "theory/strings/type_enumerator.h"
17
18		#include "theory/strings/theory_strings_utils.h"
19		#include "util/string.h"
20
21		namespace cvc5 {
22		namespace theory {
23		namespace strings {
24
25	2482	Node makeStandardModelConstant(const std::vector<unsigned>& vec,
26		uint32_t cardinality)
27		{
28	4964	std::vector<unsigned> mvec;
29		// if we contain all of the printable characters
30	2482	if (cardinality >= 255)
31		{
32	6319	for (unsigned i = 0, vsize = vec.size(); i < vsize; i++)
33		{
34	3837	unsigned curr = vec[i];
35		// convert
36	3837	Assert(vec[i] < cardinality);
37	3837	if (vec[i] <= 61)
38		{
39		// first 62 printable characters [\u{65}-\u{126}]: 'A', 'B', 'C', ...
40	3837	curr = vec[i] + 65;
41		}
42		else if (vec[i] <= 94)
43		{
44		// remaining 33 printable characters [\u{32}-\u{64}]: ' ', '!', '"', ...
45		curr = vec[i] - 30;
46		}
47		else
48		{
49		// the remaining characters, starting with \u{127} and wrapping around
50		// the first 32 non-printable characters.
51		curr = (vec[i] + 32) % cardinality;
52		}
53	3837	mvec.push_back(curr);
54		}
55		}
56		else
57		{
58		mvec = vec;
59		}
60	4964	return NodeManager::currentNM()->mkConst(String(mvec));
61		}
62
63	427	WordIter::WordIter(uint32_t startLength) : d_hasEndLength(false), d_endLength(0)
64		{
65	427	for (uint32_t i = 0; i < startLength; i++)
66		{
67		d_data.push_back(0);
68		}
69	427	}
70	568	WordIter::WordIter(uint32_t startLength, uint32_t endLength)
71	568	: d_hasEndLength(true), d_endLength(endLength)
72		{
73	2025	for (uint32_t i = 0; i < startLength; i++)
74		{
75	1457	d_data.push_back(0);
76		}
77	568	}
78
79	129	WordIter::WordIter(const WordIter& witer)
80	129	: d_hasEndLength(witer.d_hasEndLength),
81	129	d_endLength(witer.d_endLength),
82	258	d_data(witer.d_data)
83		{
84	129	}
85
86	2507	const std::vector<unsigned>& WordIter::getData() const { return d_data; }
87
88	1512	bool WordIter::increment(uint32_t card)
89		{
90	1512	for (unsigned i = 0, dsize = d_data.size(); i < dsize; ++i)
91		{
92	1402	if (d_data[i] + 1 < card)
93		{
94	1402	++d_data[i];
95	1402	return true;
96		}
97		else
98		{
99		d_data[i] = 0;
100		}
101		}
102	110	if (d_hasEndLength && d_data.size() == d_endLength)
103		{
104		return false;
105		}
106		// otherwise increase length
107	110	d_data.push_back(0);
108	110	return true;
109		}
110
111	427	SEnumLen::SEnumLen(TypeNode tn, uint32_t startLength)
112	427	: d_type(tn), d_witer(new WordIter(startLength))
113		{
114	427	}
115	568	SEnumLen::SEnumLen(TypeNode tn, uint32_t startLength, uint32_t endLength)
116	568	: d_type(tn), d_witer(new WordIter(startLength, endLength))
117		{
118	568	}
119
120	129	SEnumLen::SEnumLen(const SEnumLen& e)
121	129	: d_type(e.d_type), d_witer(new WordIter(*e.d_witer)), d_curr(e.d_curr)
122		{
123	129	}
124
125	2717	Node SEnumLen::getCurrent() const { return d_curr; }
126
127	2943	bool SEnumLen::isFinished() const { return d_curr.isNull(); }
128
129	554	StringEnumLen::StringEnumLen(uint32_t startLength,
130		uint32_t endLength,
131	554	uint32_t card)
132	1108	: SEnumLen(NodeManager::currentNM()->stringType(), startLength, endLength),
133	1662	d_cardinality(card)
134		{
135	554	mkCurr();
136	554	}
137
138	426	StringEnumLen::StringEnumLen(uint32_t startLength, uint32_t card)
139	852	: SEnumLen(NodeManager::currentNM()->stringType(), startLength),
140	1278	d_cardinality(card)
141		{
142	426	mkCurr();
143	426	}
144
145	1502	bool StringEnumLen::increment()
146		{
147		// always use the same cardinality
148	1502	if (!d_witer->increment(d_cardinality))
149		{
150		d_curr = Node::null();
151		return false;
152		}
153	1502	mkCurr();
154	1502	return true;
155		}
156
157	2482	void StringEnumLen::mkCurr()
158		{
159	2482	d_curr = makeStandardModelConstant(d_witer->getData(), d_cardinality);
160	2482	}
161
162	1	SeqEnumLen::SeqEnumLen(TypeNode tn,
163		TypeEnumeratorProperties* tep,
164	1	uint32_t startLength)
165	1	: SEnumLen(tn, startLength)
166		{
167	3	d_elementEnumerator.reset(
168	3	new TypeEnumerator(d_type.getSequenceElementType(), tep));
169	1	mkCurr();
170	1	}
171
172	14	SeqEnumLen::SeqEnumLen(TypeNode tn,
173		TypeEnumeratorProperties* tep,
174		uint32_t startLength,
175	14	uint32_t endLength)
176	14	: SEnumLen(tn, startLength, endLength)
177		{
178	42	d_elementEnumerator.reset(
179	42	new TypeEnumerator(d_type.getSequenceElementType(), tep));
180		// ensure non-empty element domain
181	14	d_elementDomain.push_back((**d_elementEnumerator));
182	14	++(*d_elementEnumerator);
183	14	mkCurr();
184	14	}
185
186		SeqEnumLen::SeqEnumLen(const SeqEnumLen& wenum)
187		: SEnumLen(wenum),
188		d_elementEnumerator(new TypeEnumerator(*wenum.d_elementEnumerator)),
189		d_elementDomain(wenum.d_elementDomain)
190		{
191		}
192
193	10	bool SeqEnumLen::increment()
194		{
195	10	if (!d_elementEnumerator->isFinished())
196		{
197		// yet to establish domain
198	10	Assert(d_elementEnumerator != nullptr);
199	10	d_elementDomain.push_back((**d_elementEnumerator));
200	10	++(*d_elementEnumerator);
201		}
202		// the current cardinality is the domain size of the element
203	10	if (!d_witer->increment(d_elementDomain.size()))
204		{
205		Assert(d_elementEnumerator->isFinished());
206		d_curr = Node::null();
207		return false;
208		}
209	10	mkCurr();
210	10	return true;
211		}
212
213	25	void SeqEnumLen::mkCurr()
214		{
215	50	std::vector<Node> seq;
216	25	const std::vector<unsigned>& data = d_witer->getData();
217	79	for (unsigned i : data)
218		{
219	54	Assert(i < d_elementDomain.size());
220	54	seq.push_back(d_elementDomain[i]);
221		}
222		// make sequence from seq
223	75	d_curr = NodeManager::currentNM()->mkConst(
224	75	Sequence(d_type.getSequenceElementType(), seq));
225	25	}
226
227	426	StringEnumerator::StringEnumerator(TypeNode type, TypeEnumeratorProperties* tep)
228		: TypeEnumeratorBase<StringEnumerator>(type),
229	426	d_wenum(0, utils::getAlphabetCardinality())
230		{
231	426	Assert(type.getKind() == kind::TYPE_CONSTANT
232		&& type.getConst<TypeConstant>() == STRING_TYPE);
233	426	}
234
235	129	StringEnumerator::StringEnumerator(const StringEnumerator& enumerator)
236	258	: TypeEnumeratorBase<StringEnumerator>(enumerator.getType()),
237	387	d_wenum(enumerator.d_wenum)
238		{
239	129	}
240
241	1466	Node StringEnumerator::operator*() { return d_wenum.getCurrent(); }
242
243	262	StringEnumerator& StringEnumerator::operator++()
244		{
245	262	d_wenum.increment();
246	262	return *this;
247		}
248
249	1692	bool StringEnumerator::isFinished() { return d_wenum.isFinished(); }
250
251	1	SequenceEnumerator::SequenceEnumerator(TypeNode type,
252	1	TypeEnumeratorProperties* tep)
253	1	: TypeEnumeratorBase<SequenceEnumerator>(type), d_wenum(type, tep, 0)
254		{
255	1	}
256
257		SequenceEnumerator::SequenceEnumerator(const SequenceEnumerator& enumerator)
258		: TypeEnumeratorBase<SequenceEnumerator>(enumerator.getType()),
259		d_wenum(enumerator.d_wenum)
260		{
261		}
262
263	2	Node SequenceEnumerator::operator*() { return d_wenum.getCurrent(); }
264
265	1	SequenceEnumerator& SequenceEnumerator::operator++()
266		{
267	1	d_wenum.increment();
268	1	return *this;
269		}
270
271	2	bool SequenceEnumerator::isFinished() { return d_wenum.isFinished(); }
272
273		} // namespace strings
274		} // namespace theory
275	28194	} // namespace cvc5