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