GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/strings/type_enumerator.h Lines: 7 7 100.0 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file type_enumerator.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Tianyi Liang, Mathias Preiner
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 Enumerators for strings
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__STRINGS__TYPE_ENUMERATOR_H
18
#define CVC4__THEORY__STRINGS__TYPE_ENUMERATOR_H
19
20
#include <vector>
21
22
#include "expr/node.h"
23
#include "expr/type_node.h"
24
#include "theory/type_enumerator.h"
25
26
namespace CVC4 {
27
namespace theory {
28
namespace strings {
29
30
/**
31
 * Make standard model constant
32
 *
33
 * In our string representation, we represent characters using vectors
34
 * of unsigned integers indicating code points for the characters of that
35
 * string.
36
 *
37
 * To make models user-friendly, we make unsigned integer 0 correspond to the
38
 * 65th character ("A") in the ASCII alphabet to make models intuitive. In
39
 * particular, say if we have a set of string variables that are distinct but
40
 * otherwise unconstrained, then the model may assign them "A", "B", "C", ...
41
 *
42
 * @param vec The code points of the string in a given model,
43
 * @param cardinality The cardinality of the alphabet,
44
 * @return A string whose characters have the code points corresponding
45
 * to vec in the standard model construction described above.
46
 */
47
Node makeStandardModelConstant(const std::vector<unsigned>& vec,
48
                               uint32_t cardinality);
49
50
/**
51
 * Generic iteration over vectors of indices of a given start/end length.
52
 */
53
1458
class WordIter
54
{
55
 public:
56
  /**
57
   * This iterator will start with words at length startLength and continue
58
   * indefinitely.
59
   */
60
  WordIter(uint32_t startLength);
61
  /**
62
   * This iterator will start with words at length startLength and continue
63
   * until length endLength.
64
   */
65
  WordIter(uint32_t startLength, uint32_t endLength);
66
  /** copy constructor */
67
  WordIter(const WordIter& witer);
68
  /** Get the current data */
69
  const std::vector<unsigned>& getData() const;
70
  /**
71
   * Increment assuming the cardinality of the alphabet is card. Notice that
72
   * the value of card may be different for multiple calls; the caller is
73
   * responsible for using this function to achieve the required result. This
74
   * is required for enumerating sequences where the cardinality of the
75
   * alphabet is not known upfront, but a lower bound can be determined.
76
   *
77
   * This method returns true if the increment was successful, otherwise we
78
   * are finished with this iterator.
79
   */
80
  bool increment(uint32_t card);
81
82
 private:
83
  /** Whether we have an end length */
84
  bool d_hasEndLength;
85
  /** The end length */
86
  uint32_t d_endLength;
87
  /** The data. */
88
  std::vector<unsigned> d_data;
89
};
90
91
/**
92
 * A virtual class for enumerating string-like terms, with a similar
93
 * interface to the one above.
94
 */
95
class SEnumLen
96
{
97
 public:
98
  SEnumLen(TypeNode tn, uint32_t startLength);
99
  SEnumLen(TypeNode tn, uint32_t startLength, uint32_t endLength);
100
  SEnumLen(const SEnumLen& e);
101
1458
  virtual ~SEnumLen() {}
102
  /** Get current term */
103
  Node getCurrent() const;
104
  /** Is this enumerator finished? */
105
  bool isFinished() const;
106
  /** increment, returns true if the increment was successful. */
107
  virtual bool increment() = 0;
108
109
 protected:
110
  /** The type we are enumerating */
111
  TypeNode d_type;
112
  /** The word iterator utility */
113
  std::unique_ptr<WordIter> d_witer;
114
  /** The current term */
115
  Node d_curr;
116
};
117
118
/**
119
 * Enumerates string values for a given length.
120
 */
121
182
class StringEnumLen : public SEnumLen
122
{
123
 public:
124
  /** For strings */
125
  StringEnumLen(uint32_t startLength, uint32_t card);
126
  StringEnumLen(uint32_t startLength, uint32_t endLength, uint32_t card);
127
  /** destructor */
128
1985
  ~StringEnumLen() {}
129
  /** increment */
130
  bool increment() override;
131
132
 private:
133
  /** The cardinality of the alphabet */
134
  uint32_t d_cardinality;
135
  /** Make the current term from d_data */
136
  void mkCurr();
137
};
138
139
/**
140
 * Enumerates sequence values for a given length.
141
 */
142
class SeqEnumLen : public SEnumLen
143
{
144
 public:
145
  /** For sequences */
146
  SeqEnumLen(TypeNode tn, TypeEnumeratorProperties* tep, uint32_t startLength);
147
  SeqEnumLen(TypeNode tn,
148
             TypeEnumeratorProperties* tep,
149
             uint32_t startLength,
150
             uint32_t endLength);
151
  /** copy constructor */
152
  SeqEnumLen(const SeqEnumLen& wenum);
153
  /** destructor */
154
29
  ~SeqEnumLen() {}
155
  /** increment */
156
  bool increment() override;
157
158
 private:
159
  /** an enumerator for the elements' type */
160
  std::unique_ptr<TypeEnumerator> d_elementEnumerator;
161
  /** The domain */
162
  std::vector<Node> d_elementDomain;
163
  /** Make the current term from d_data */
164
  void mkCurr();
165
};
166
167
class StringEnumerator : public TypeEnumeratorBase<StringEnumerator>
168
{
169
 public:
170
  StringEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr);
171
  StringEnumerator(const StringEnumerator& enumerator);
172
1788
  ~StringEnumerator() {}
173
  /** get the current term */
174
  Node operator*() override;
175
  /** increment */
176
  StringEnumerator& operator++() override;
177
  /** is this enumerator finished? */
178
  bool isFinished() override;
179
180
 private:
181
  /** underlying string enumerator */
182
  StringEnumLen d_wenum;
183
}; /* class StringEnumerator */
184
185
class SequenceEnumerator : public TypeEnumeratorBase<SequenceEnumerator>
186
{
187
 public:
188
  SequenceEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr);
189
  SequenceEnumerator(const SequenceEnumerator& enumerator);
190
2
  ~SequenceEnumerator() {}
191
  Node operator*() override;
192
  SequenceEnumerator& operator++() override;
193
  bool isFinished() override;
194
195
 private:
196
  /** underlying sequence enumerator */
197
  SeqEnumLen d_wenum;
198
}; /* class SequenceEnumerator */
199
200
}/* CVC4::theory::strings namespace */
201
}/* CVC4::theory namespace */
202
}/* CVC4 namespace */
203
204
#endif /* CVC4__THEORY__STRINGS__TYPE_ENUMERATOR_H */