Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/strings/type_enumerator.cpp	Lines:	117	148	79.1 %
Date:	2021-09-29	Branches:	78	262	29.8 %


/******************************************************************************
 * 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 "expr/sequence.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));
}

SEnumLenSet::SEnumLenSet(TypeEnumeratorProperties* tep) : d_tep(tep) {}

SEnumLen* SEnumLenSet::getEnumerator(size_t len, TypeNode tn)
{
  std::pair<size_t, TypeNode> key(len, tn);
  std::map<std::pair<size_t, TypeNode>, std::unique_ptr<SEnumLen> >::iterator
      it = d_sels.find(key);
  if (it != d_sels.end())
  {
    return it->second.get();
  }
  if (tn.isString())  // string-only
  {
    d_sels[key].reset(
        new StringEnumLen(len, len, utils::getAlphabetCardinality()));
  }
  else
  {
    d_sels[key].reset(new SeqEnumLen(tn, d_tep, len, len));
  }
  return d_sels[key].get();
}

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 "expr/sequence.h"
19		#include "theory/strings/theory_strings_utils.h"
20		#include "util/string.h"
21
22		namespace cvc5 {
23		namespace theory {
24		namespace strings {
25
26	2489	Node makeStandardModelConstant(const std::vector<unsigned>& vec,
27		uint32_t cardinality)
28		{
29	4978	std::vector<unsigned> mvec;
30		// if we contain all of the printable characters
31	2489	if (cardinality >= 255)
32		{
33	6066	for (unsigned i = 0, vsize = vec.size(); i < vsize; i++)
34		{
35	3577	unsigned curr = vec[i];
36		// convert
37	3577	Assert(vec[i] < cardinality);
38	3577	if (vec[i] <= 61)
39		{
40		// first 62 printable characters [\u{65}-\u{126}]: 'A', 'B', 'C', ...
41	3577	curr = vec[i] + 65;
42		}
43		else if (vec[i] <= 94)
44		{
45		// remaining 33 printable characters [\u{32}-\u{64}]: ' ', '!', '"', ...
46		curr = vec[i] - 30;
47		}
48		else
49		{
50		// the remaining characters, starting with \u{127} and wrapping around
51		// the first 32 non-printable characters.
52		curr = (vec[i] + 32) % cardinality;
53		}
54	3577	mvec.push_back(curr);
55		}
56		}
57		else
58		{
59		mvec = vec;
60		}
61	4978	return NodeManager::currentNM()->mkConst(String(mvec));
62		}
63
64	441	WordIter::WordIter(uint32_t startLength) : d_hasEndLength(false), d_endLength(0)
65		{
66	441	for (uint32_t i = 0; i < startLength; i++)
67		{
68		d_data.push_back(0);
69		}
70	441	}
71	614	WordIter::WordIter(uint32_t startLength, uint32_t endLength)
72	614	: d_hasEndLength(true), d_endLength(endLength)
73		{
74	1987	for (uint32_t i = 0; i < startLength; i++)
75		{
76	1373	d_data.push_back(0);
77		}
78	614	}
79
80	135	WordIter::WordIter(const WordIter& witer)
81	135	: d_hasEndLength(witer.d_hasEndLength),
82	135	d_endLength(witer.d_endLength),
83	270	d_data(witer.d_data)
84		{
85	135	}
86
87	2537	const std::vector<unsigned>& WordIter::getData() const { return d_data; }
88
89	1482	bool WordIter::increment(uint32_t card)
90		{
91	1482	for (unsigned i = 0, dsize = d_data.size(); i < dsize; ++i)
92		{
93	1391	if (d_data[i] + 1 < card)
94		{
95	1391	++d_data[i];
96	1391	return true;
97		}
98		else
99		{
100		d_data[i] = 0;
101		}
102		}
103	91	if (d_hasEndLength && d_data.size() == d_endLength)
104		{
105		return false;
106		}
107		// otherwise increase length
108	91	d_data.push_back(0);
109	91	return true;
110		}
111
112	441	SEnumLen::SEnumLen(TypeNode tn, uint32_t startLength)
113	441	: d_type(tn), d_witer(new WordIter(startLength))
114		{
115	441	}
116	614	SEnumLen::SEnumLen(TypeNode tn, uint32_t startLength, uint32_t endLength)
117	614	: d_type(tn), d_witer(new WordIter(startLength, endLength))
118		{
119	614	}
120
121	135	SEnumLen::SEnumLen(const SEnumLen& e)
122	135	: d_type(e.d_type), d_witer(new WordIter(*e.d_witer)), d_curr(e.d_curr)
123		{
124	135	}
125
126	2631	Node SEnumLen::getCurrent() const { return d_curr; }
127
128	2827	bool SEnumLen::isFinished() const { return d_curr.isNull(); }
129
130	594	StringEnumLen::StringEnumLen(uint32_t startLength,
131		uint32_t endLength,
132	594	uint32_t card)
133	1188	: SEnumLen(NodeManager::currentNM()->stringType(), startLength, endLength),
134	1782	d_cardinality(card)
135		{
136	594	mkCurr();
137	594	}
138
139	436	StringEnumLen::StringEnumLen(uint32_t startLength, uint32_t card)
140	872	: SEnumLen(NodeManager::currentNM()->stringType(), startLength),
141	1308	d_cardinality(card)
142		{
143	436	mkCurr();
144	436	}
145
146	1459	bool StringEnumLen::increment()
147		{
148		// always use the same cardinality
149	1459	if (!d_witer->increment(d_cardinality))
150		{
151		d_curr = Node::null();
152		return false;
153		}
154	1459	mkCurr();
155	1459	return true;
156		}
157
158	2489	void StringEnumLen::mkCurr()
159		{
160	2489	d_curr = makeStandardModelConstant(d_witer->getData(), d_cardinality);
161	2489	}
162
163	5	SeqEnumLen::SeqEnumLen(TypeNode tn,
164		TypeEnumeratorProperties* tep,
165	5	uint32_t startLength)
166	5	: SEnumLen(tn, startLength)
167		{
168	15	d_elementEnumerator.reset(
169	15	new TypeEnumerator(d_type.getSequenceElementType(), tep));
170	5	mkCurr();
171	5	}
172
173	20	SeqEnumLen::SeqEnumLen(TypeNode tn,
174		TypeEnumeratorProperties* tep,
175		uint32_t startLength,
176	20	uint32_t endLength)
177	20	: SEnumLen(tn, startLength, endLength)
178		{
179	60	d_elementEnumerator.reset(
180	60	new TypeEnumerator(d_type.getSequenceElementType(), tep));
181		// ensure non-empty element domain
182	20	d_elementDomain.push_back((**d_elementEnumerator));
183	20	++(*d_elementEnumerator);
184	20	mkCurr();
185	20	}
186
187		SeqEnumLen::SeqEnumLen(const SeqEnumLen& wenum)
188		: SEnumLen(wenum),
189		d_elementEnumerator(new TypeEnumerator(*wenum.d_elementEnumerator)),
190		d_elementDomain(wenum.d_elementDomain)
191		{
192		}
193
194	23	bool SeqEnumLen::increment()
195		{
196	23	if (!d_elementEnumerator->isFinished())
197		{
198		// yet to establish domain
199	23	Assert(d_elementEnumerator != nullptr);
200	23	d_elementDomain.push_back((**d_elementEnumerator));
201	23	++(*d_elementEnumerator);
202		}
203		// the current cardinality is the domain size of the element
204	23	if (!d_witer->increment(d_elementDomain.size()))
205		{
206		Assert(d_elementEnumerator->isFinished());
207		d_curr = Node::null();
208		return false;
209		}
210	23	mkCurr();
211	23	return true;
212		}
213
214	48	void SeqEnumLen::mkCurr()
215		{
216	96	std::vector<Node> seq;
217	48	const std::vector<unsigned>& data = d_witer->getData();
218	121	for (unsigned i : data)
219		{
220	73	Assert(i < d_elementDomain.size());
221	73	seq.push_back(d_elementDomain[i]);
222		}
223		// make sequence from seq
224	144	d_curr = NodeManager::currentNM()->mkConst(
225	144	Sequence(d_type.getSequenceElementType(), seq));
226	48	}
227
228		SEnumLenSet::SEnumLenSet(TypeEnumeratorProperties* tep) : d_tep(tep) {}
229
230		SEnumLen* SEnumLenSet::getEnumerator(size_t len, TypeNode tn)
231		{
232		std::pair<size_t, TypeNode> key(len, tn);
233		std::map<std::pair<size_t, TypeNode>, std::unique_ptr<SEnumLen> >::iterator
234		it = d_sels.find(key);
235		if (it != d_sels.end())
236		{
237		return it->second.get();
238		}
239		if (tn.isString()) // string-only
240		{
241		d_sels[key].reset(
242		new StringEnumLen(len, len, utils::getAlphabetCardinality()));
243		}
244		else
245		{
246		d_sels[key].reset(new SeqEnumLen(tn, d_tep, len, len));
247		}
248		return d_sels[key].get();
249		}
250
251	436	StringEnumerator::StringEnumerator(TypeNode type, TypeEnumeratorProperties* tep)
252		: TypeEnumeratorBase<StringEnumerator>(type),
253	436	d_wenum(0, utils::getAlphabetCardinality())
254		{
255	436	Assert(type.getKind() == kind::TYPE_CONSTANT
256		&& type.getConst<TypeConstant>() == STRING_TYPE);
257	436	}
258
259	135	StringEnumerator::StringEnumerator(const StringEnumerator& enumerator)
260	270	: TypeEnumeratorBase<StringEnumerator>(enumerator.getType()),
261	405	d_wenum(enumerator.d_wenum)
262		{
263	135	}
264
265	1358	Node StringEnumerator::operator*() { return d_wenum.getCurrent(); }
266
267	228	StringEnumerator& StringEnumerator::operator++()
268		{
269	228	d_wenum.increment();
270	228	return *this;
271		}
272
273	1546	bool StringEnumerator::isFinished() { return d_wenum.isFinished(); }
274
275	5	SequenceEnumerator::SequenceEnumerator(TypeNode type,
276	5	TypeEnumeratorProperties* tep)
277	5	: TypeEnumeratorBase<SequenceEnumerator>(type), d_wenum(type, tep, 0)
278		{
279	5	}
280
281		SequenceEnumerator::SequenceEnumerator(const SequenceEnumerator& enumerator)
282		: TypeEnumeratorBase<SequenceEnumerator>(enumerator.getType()),
283		d_wenum(enumerator.d_wenum)
284		{
285		}
286
287	30	Node SequenceEnumerator::operator*() { return d_wenum.getCurrent(); }
288
289	11	SequenceEnumerator& SequenceEnumerator::operator++()
290		{
291	11	d_wenum.increment();
292	11	return *this;
293		}
294
295	38	bool SequenceEnumerator::isFinished() { return d_wenum.isFinished(); }
296
297		} // namespace strings
298		} // namespace theory
299	22746	} // namespace cvc5