Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/strings/type_enumerator.cpp	Lines:	125	149	83.9 %
Date:	2021-11-07	Branches:	85	266	32.0 %


/******************************************************************************
 * 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,
                          d_tep ? d_tep->getStringsAlphabetCard()
                                : utils::getDefaultAlphabetCardinality()));
  }
  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,
              tep ? tep->getStringsAlphabetCard()
                  : utils::getDefaultAlphabetCardinality())
{
  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	3160	Node makeStandardModelConstant(const std::vector<unsigned>& vec,
27		uint32_t cardinality)
28		{
29	6320	std::vector<unsigned> mvec;
30		// if we contain all of the printable characters
31	3160	if (cardinality >= 255)
32		{
33	7223	for (unsigned i = 0, vsize = vec.size(); i < vsize; i++)
34		{
35	4063	unsigned curr = vec[i];
36		// convert
37	4063	Assert(vec[i] < cardinality);
38	4063	if (vec[i] <= 61)
39		{
40		// first 62 printable characters [\u{65}-\u{126}]: 'A', 'B', 'C', ...
41	4063	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	4063	mvec.push_back(curr);
55		}
56		}
57		else
58		{
59		mvec = vec;
60		}
61	6320	return NodeManager::currentNM()->mkConst(String(mvec));
62		}
63
64	702	WordIter::WordIter(uint32_t startLength) : d_hasEndLength(false), d_endLength(0)
65		{
66	702	for (uint32_t i = 0; i < startLength; i++)
67		{
68		d_data.push_back(0);
69		}
70	702	}
71	712	WordIter::WordIter(uint32_t startLength, uint32_t endLength)
72	712	: d_hasEndLength(true), d_endLength(endLength)
73		{
74	2219	for (uint32_t i = 0; i < startLength; i++)
75		{
76	1507	d_data.push_back(0);
77		}
78	712	}
79
80	153	WordIter::WordIter(const WordIter& witer)
81	153	: d_hasEndLength(witer.d_hasEndLength),
82	153	d_endLength(witer.d_endLength),
83	306	d_data(witer.d_data)
84		{
85	153	}
86
87	3218	const std::vector<unsigned>& WordIter::getData() const { return d_data; }
88
89	1804	bool WordIter::increment(uint32_t card)
90		{
91	1804	for (unsigned i = 0, dsize = d_data.size(); i < dsize; ++i)
92		{
93	1684	if (d_data[i] + 1 < card)
94		{
95	1684	++d_data[i];
96	1684	return true;
97		}
98		else
99		{
100		d_data[i] = 0;
101		}
102		}
103	120	if (d_hasEndLength && d_data.size() == d_endLength)
104		{
105		return false;
106		}
107		// otherwise increase length
108	120	d_data.push_back(0);
109	120	return true;
110		}
111
112	702	SEnumLen::SEnumLen(TypeNode tn, uint32_t startLength)
113	702	: d_type(tn), d_witer(new WordIter(startLength))
114		{
115	702	}
116	712	SEnumLen::SEnumLen(TypeNode tn, uint32_t startLength, uint32_t endLength)
117	712	: d_type(tn), d_witer(new WordIter(startLength, endLength))
118		{
119	712	}
120
121	153	SEnumLen::SEnumLen(const SEnumLen& e)
122	153	: d_type(e.d_type), d_witer(new WordIter(*e.d_witer)), d_curr(e.d_curr)
123		{
124	153	}
125
126	3519	Node SEnumLen::getCurrent() const { return d_curr; }
127
128	3766	bool SEnumLen::isFinished() const { return d_curr.isNull(); }
129
130	691	StringEnumLen::StringEnumLen(uint32_t startLength,
131		uint32_t endLength,
132	691	uint32_t card)
133	1382	: SEnumLen(NodeManager::currentNM()->stringType(), startLength, endLength),
134	2073	d_cardinality(card)
135		{
136	691	mkCurr();
137	691	}
138
139	693	StringEnumLen::StringEnumLen(uint32_t startLength, uint32_t card)
140	1386	: SEnumLen(NodeManager::currentNM()->stringType(), startLength),
141	2079	d_cardinality(card)
142		{
143	693	mkCurr();
144	693	}
145
146	1776	bool StringEnumLen::increment()
147		{
148		// always use the same cardinality
149	1776	if (!d_witer->increment(d_cardinality))
150		{
151		d_curr = Node::null();
152		return false;
153		}
154	1776	mkCurr();
155	1776	return true;
156		}
157
158	3160	void StringEnumLen::mkCurr()
159		{
160	3160	d_curr = makeStandardModelConstant(d_witer->getData(), d_cardinality);
161	3160	}
162
163	9	SeqEnumLen::SeqEnumLen(TypeNode tn,
164		TypeEnumeratorProperties* tep,
165	9	uint32_t startLength)
166	9	: SEnumLen(tn, startLength)
167		{
168	27	d_elementEnumerator.reset(
169	27	new TypeEnumerator(d_type.getSequenceElementType(), tep));
170	9	mkCurr();
171	9	}
172
173	21	SeqEnumLen::SeqEnumLen(TypeNode tn,
174		TypeEnumeratorProperties* tep,
175		uint32_t startLength,
176	21	uint32_t endLength)
177	21	: SEnumLen(tn, startLength, endLength)
178		{
179	63	d_elementEnumerator.reset(
180	63	new TypeEnumerator(d_type.getSequenceElementType(), tep));
181		// ensure non-empty element domain
182	21	d_elementDomain.push_back((**d_elementEnumerator));
183	21	++(*d_elementEnumerator);
184	21	mkCurr();
185	21	}
186
187	4	SeqEnumLen::SeqEnumLen(const SeqEnumLen& wenum)
188		: SEnumLen(wenum),
189	8	d_elementEnumerator(new TypeEnumerator(*wenum.d_elementEnumerator)),
190	12	d_elementDomain(wenum.d_elementDomain)
191		{
192	4	}
193
194	28	bool SeqEnumLen::increment()
195		{
196	28	if (!d_elementEnumerator->isFinished())
197		{
198		// yet to establish domain
199	28	Assert(d_elementEnumerator != nullptr);
200	28	d_elementDomain.push_back((**d_elementEnumerator));
201	28	++(*d_elementEnumerator);
202		}
203		// the current cardinality is the domain size of the element
204	28	if (!d_witer->increment(d_elementDomain.size()))
205		{
206		Assert(d_elementEnumerator->isFinished());
207		d_curr = Node::null();
208		return false;
209		}
210	28	mkCurr();
211	28	return true;
212		}
213
214	58	void SeqEnumLen::mkCurr()
215		{
216	116	std::vector<Node> seq;
217	58	const std::vector<unsigned>& data = d_witer->getData();
218	137	for (unsigned i : data)
219		{
220	79	Assert(i < d_elementDomain.size());
221	79	seq.push_back(d_elementDomain[i]);
222		}
223		// make sequence from seq
224	174	d_curr = NodeManager::currentNM()->mkConst(
225	174	Sequence(d_type.getSequenceElementType(), seq));
226	58	}
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,
243		len,
244		d_tep ? d_tep->getStringsAlphabetCard()
245		: utils::getDefaultAlphabetCardinality()));
246		}
247		else
248		{
249		d_sels[key].reset(new SeqEnumLen(tn, d_tep, len, len));
250		}
251		return d_sels[key].get();
252		}
253
254	693	StringEnumerator::StringEnumerator(TypeNode type, TypeEnumeratorProperties* tep)
255		: TypeEnumeratorBase<StringEnumerator>(type),
256		d_wenum(0,
257		tep ? tep->getStringsAlphabetCard()
258	693	: utils::getDefaultAlphabetCardinality())
259		{
260	693	Assert(type.getKind() == kind::TYPE_CONSTANT
261		&& type.getConst<TypeConstant>() == STRING_TYPE);
262	693	}
263
264	149	StringEnumerator::StringEnumerator(const StringEnumerator& enumerator)
265	298	: TypeEnumeratorBase<StringEnumerator>(enumerator.getType()),
266	447	d_wenum(enumerator.d_wenum)
267		{
268	149	}
269
270	1963	Node StringEnumerator::operator*() { return d_wenum.getCurrent(); }
271
272	275	StringEnumerator& StringEnumerator::operator++()
273		{
274	275	d_wenum.increment();
275	275	return *this;
276		}
277
278	2198	bool StringEnumerator::isFinished() { return d_wenum.isFinished(); }
279
280	9	SequenceEnumerator::SequenceEnumerator(TypeNode type,
281	9	TypeEnumeratorProperties* tep)
282	9	: TypeEnumeratorBase<SequenceEnumerator>(type), d_wenum(type, tep, 0)
283		{
284	9	}
285
286	4	SequenceEnumerator::SequenceEnumerator(const SequenceEnumerator& enumerator)
287	8	: TypeEnumeratorBase<SequenceEnumerator>(enumerator.getType()),
288	12	d_wenum(enumerator.d_wenum)
289		{
290	4	}
291
292	42	Node SequenceEnumerator::operator*() { return d_wenum.getCurrent(); }
293
294	15	SequenceEnumerator& SequenceEnumerator::operator++()
295		{
296	15	d_wenum.increment();
297	15	return *this;
298		}
299
300	54	bool SequenceEnumerator::isFinished() { return d_wenum.isFinished(); }
301
302		} // namespace strings
303		} // namespace theory
304	31137	} // namespace cvc5