Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/strings/type_enumerator.cpp	Lines:	117	137	85.4 %
Date:	2021-09-18	Branches:	78	234	33.3 %


/******************************************************************************
 * 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));
}

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	2807	Node makeStandardModelConstant(const std::vector<unsigned>& vec,
27		uint32_t cardinality)
28		{
29	5614	std::vector<unsigned> mvec;
30		// if we contain all of the printable characters
31	2807	if (cardinality >= 255)
32		{
33	6742	for (unsigned i = 0, vsize = vec.size(); i < vsize; i++)
34		{
35	3935	unsigned curr = vec[i];
36		// convert
37	3935	Assert(vec[i] < cardinality);
38	3935	if (vec[i] <= 61)
39		{
40		// first 62 printable characters [\u{65}-\u{126}]: 'A', 'B', 'C', ...
41	3935	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	3935	mvec.push_back(curr);
55		}
56		}
57		else
58		{
59		mvec = vec;
60		}
61	5614	return NodeManager::currentNM()->mkConst(String(mvec));
62		}
63
64	453	WordIter::WordIter(uint32_t startLength) : d_hasEndLength(false), d_endLength(0)
65		{
66	453	for (uint32_t i = 0; i < startLength; i++)
67		{
68		d_data.push_back(0);
69		}
70	453	}
71	703	WordIter::WordIter(uint32_t startLength, uint32_t endLength)
72	703	: d_hasEndLength(true), d_endLength(endLength)
73		{
74	2191	for (uint32_t i = 0; i < startLength; i++)
75		{
76	1488	d_data.push_back(0);
77		}
78	703	}
79
80	147	WordIter::WordIter(const WordIter& witer)
81	147	: d_hasEndLength(witer.d_hasEndLength),
82	147	d_endLength(witer.d_endLength),
83	294	d_data(witer.d_data)
84		{
85	147	}
86
87	2855	const std::vector<unsigned>& WordIter::getData() const { return d_data; }
88
89	1699	bool WordIter::increment(uint32_t card)
90		{
91	1699	for (unsigned i = 0, dsize = d_data.size(); i < dsize; ++i)
92		{
93	1596	if (d_data[i] + 1 < card)
94		{
95	1596	++d_data[i];
96	1596	return true;
97		}
98		else
99		{
100		d_data[i] = 0;
101		}
102		}
103	103	if (d_hasEndLength && d_data.size() == d_endLength)
104		{
105		return false;
106		}
107		// otherwise increase length
108	103	d_data.push_back(0);
109	103	return true;
110		}
111
112	453	SEnumLen::SEnumLen(TypeNode tn, uint32_t startLength)
113	453	: d_type(tn), d_witer(new WordIter(startLength))
114		{
115	453	}
116	703	SEnumLen::SEnumLen(TypeNode tn, uint32_t startLength, uint32_t endLength)
117	703	: d_type(tn), d_witer(new WordIter(startLength, endLength))
118		{
119	703	}
120
121	147	SEnumLen::SEnumLen(const SEnumLen& e)
122	147	: d_type(e.d_type), d_witer(new WordIter(*e.d_witer)), d_curr(e.d_curr)
123		{
124	147	}
125
126	2872	Node SEnumLen::getCurrent() const { return d_curr; }
127
128	3080	bool SEnumLen::isFinished() const { return d_curr.isNull(); }
129
130	683	StringEnumLen::StringEnumLen(uint32_t startLength,
131		uint32_t endLength,
132	683	uint32_t card)
133	1366	: SEnumLen(NodeManager::currentNM()->stringType(), startLength, endLength),
134	2049	d_cardinality(card)
135		{
136	683	mkCurr();
137	683	}
138
139	448	StringEnumLen::StringEnumLen(uint32_t startLength, uint32_t card)
140	896	: SEnumLen(NodeManager::currentNM()->stringType(), startLength),
141	1344	d_cardinality(card)
142		{
143	448	mkCurr();
144	448	}
145
146	1676	bool StringEnumLen::increment()
147		{
148		// always use the same cardinality
149	1676	if (!d_witer->increment(d_cardinality))
150		{
151		d_curr = Node::null();
152		return false;
153		}
154	1676	mkCurr();
155	1676	return true;
156		}
157
158	2807	void StringEnumLen::mkCurr()
159		{
160	2807	d_curr = makeStandardModelConstant(d_witer->getData(), d_cardinality);
161	2807	}
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	448	StringEnumerator::StringEnumerator(TypeNode type, TypeEnumeratorProperties* tep)
229		: TypeEnumeratorBase<StringEnumerator>(type),
230	448	d_wenum(0, utils::getAlphabetCardinality())
231		{
232	448	Assert(type.getKind() == kind::TYPE_CONSTANT
233		&& type.getConst<TypeConstant>() == STRING_TYPE);
234	448	}
235
236	147	StringEnumerator::StringEnumerator(const StringEnumerator& enumerator)
237	294	: TypeEnumeratorBase<StringEnumerator>(enumerator.getType()),
238	441	d_wenum(enumerator.d_wenum)
239		{
240	147	}
241
242	1394	Node StringEnumerator::operator*() { return d_wenum.getCurrent(); }
243
244	240	StringEnumerator& StringEnumerator::operator++()
245		{
246	240	d_wenum.increment();
247	240	return *this;
248		}
249
250	1594	bool StringEnumerator::isFinished() { return d_wenum.isFinished(); }
251
252	5	SequenceEnumerator::SequenceEnumerator(TypeNode type,
253	5	TypeEnumeratorProperties* tep)
254	5	: TypeEnumeratorBase<SequenceEnumerator>(type), d_wenum(type, tep, 0)
255		{
256	5	}
257
258		SequenceEnumerator::SequenceEnumerator(const SequenceEnumerator& enumerator)
259		: TypeEnumeratorBase<SequenceEnumerator>(enumerator.getType()),
260		d_wenum(enumerator.d_wenum)
261		{
262		}
263
264	30	Node SequenceEnumerator::operator*() { return d_wenum.getCurrent(); }
265
266	11	SequenceEnumerator& SequenceEnumerator::operator++()
267		{
268	11	d_wenum.increment();
269	11	return *this;
270		}
271
272	38	bool SequenceEnumerator::isFinished() { return d_wenum.isFinished(); }
273
274		} // namespace strings
275		} // namespace theory
276	29574	} // namespace cvc5