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

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