1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Aina Niemetz, Yoni Zohar |
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 |
|
* Typing rules for the theory of strings and regexps. |
14 |
|
*/ |
15 |
|
#include "theory/strings/theory_strings_type_rules.h" |
16 |
|
|
17 |
|
#include <sstream> |
18 |
|
|
19 |
|
#include "expr/node_manager.h" |
20 |
|
#include "expr/sequence.h" |
21 |
|
#include "options/strings_options.h" |
22 |
|
#include "util/cardinality.h" |
23 |
|
|
24 |
|
namespace cvc5 { |
25 |
|
namespace theory { |
26 |
|
namespace strings { |
27 |
|
|
28 |
48025 |
TypeNode StringConcatTypeRule::computeType(NodeManager* nodeManager, |
29 |
|
TNode n, |
30 |
|
bool check) |
31 |
|
{ |
32 |
48025 |
TypeNode tret; |
33 |
213662 |
for (const Node& nc : n) |
34 |
|
{ |
35 |
331274 |
TypeNode t = nc.getType(check); |
36 |
165637 |
if (tret.isNull()) |
37 |
|
{ |
38 |
48025 |
tret = t; |
39 |
48025 |
if (check) |
40 |
|
{ |
41 |
48025 |
if (!t.isStringLike()) |
42 |
|
{ |
43 |
|
throw TypeCheckingExceptionPrivate( |
44 |
|
n, "expecting string-like terms in concat"); |
45 |
|
} |
46 |
|
} |
47 |
|
else |
48 |
|
{ |
49 |
|
break; |
50 |
|
} |
51 |
|
} |
52 |
117612 |
else if (t != tret) |
53 |
|
{ |
54 |
|
throw TypeCheckingExceptionPrivate( |
55 |
|
n, "expecting all children to have the same type in concat"); |
56 |
|
} |
57 |
|
} |
58 |
48025 |
return tret; |
59 |
|
} |
60 |
|
|
61 |
45844 |
TypeNode StringSubstrTypeRule::computeType(NodeManager* nodeManager, |
62 |
|
TNode n, |
63 |
|
bool check) |
64 |
|
{ |
65 |
45844 |
TypeNode t = n[0].getType(check); |
66 |
45844 |
if (check) |
67 |
|
{ |
68 |
45844 |
if (!t.isStringLike()) |
69 |
|
{ |
70 |
|
throw TypeCheckingExceptionPrivate( |
71 |
|
n, "expecting a string-like term in substr"); |
72 |
|
} |
73 |
91688 |
TypeNode t2 = n[1].getType(check); |
74 |
45844 |
if (!t2.isInteger()) |
75 |
|
{ |
76 |
|
throw TypeCheckingExceptionPrivate( |
77 |
|
n, "expecting an integer start term in substr"); |
78 |
|
} |
79 |
45844 |
t2 = n[2].getType(check); |
80 |
45844 |
if (!t2.isInteger()) |
81 |
|
{ |
82 |
|
throw TypeCheckingExceptionPrivate( |
83 |
|
n, "expecting an integer length term in substr"); |
84 |
|
} |
85 |
|
} |
86 |
45844 |
return t; |
87 |
|
} |
88 |
|
|
89 |
142 |
TypeNode StringUpdateTypeRule::computeType(NodeManager* nodeManager, |
90 |
|
TNode n, |
91 |
|
bool check) |
92 |
|
{ |
93 |
142 |
TypeNode t = n[0].getType(check); |
94 |
142 |
if (check) |
95 |
|
{ |
96 |
142 |
if (!t.isStringLike()) |
97 |
|
{ |
98 |
|
throw TypeCheckingExceptionPrivate( |
99 |
|
n, "expecting a string-like term in update"); |
100 |
|
} |
101 |
284 |
TypeNode t2 = n[1].getType(check); |
102 |
142 |
if (!t2.isInteger()) |
103 |
|
{ |
104 |
|
throw TypeCheckingExceptionPrivate( |
105 |
|
n, "expecting an integer start term in update"); |
106 |
|
} |
107 |
142 |
t2 = n[2].getType(check); |
108 |
142 |
if (!t2.isStringLike()) |
109 |
|
{ |
110 |
|
throw TypeCheckingExceptionPrivate( |
111 |
|
n, "expecting an string-like replace term in update"); |
112 |
|
} |
113 |
|
} |
114 |
142 |
return t; |
115 |
|
} |
116 |
|
|
117 |
153 |
TypeNode StringAtTypeRule::computeType(NodeManager* nodeManager, |
118 |
|
TNode n, |
119 |
|
bool check) |
120 |
|
{ |
121 |
153 |
TypeNode t = n[0].getType(check); |
122 |
153 |
if (check) |
123 |
|
{ |
124 |
153 |
if (!t.isStringLike()) |
125 |
|
{ |
126 |
|
throw TypeCheckingExceptionPrivate( |
127 |
|
n, "expecting a string-like term in str.at"); |
128 |
|
} |
129 |
306 |
TypeNode t2 = n[1].getType(check); |
130 |
153 |
if (!t2.isInteger()) |
131 |
|
{ |
132 |
|
throw TypeCheckingExceptionPrivate( |
133 |
|
n, "expecting an integer start term in str.at"); |
134 |
|
} |
135 |
|
} |
136 |
153 |
return t; |
137 |
|
} |
138 |
|
|
139 |
2188 |
TypeNode StringIndexOfTypeRule::computeType(NodeManager* nodeManager, |
140 |
|
TNode n, |
141 |
|
bool check) |
142 |
|
{ |
143 |
2188 |
if (check) |
144 |
|
{ |
145 |
4376 |
TypeNode t = n[0].getType(check); |
146 |
2188 |
if (!t.isStringLike()) |
147 |
|
{ |
148 |
|
throw TypeCheckingExceptionPrivate( |
149 |
|
n, "expecting a string-like term in indexof"); |
150 |
|
} |
151 |
4376 |
TypeNode t2 = n[1].getType(check); |
152 |
2188 |
if (t != t2) |
153 |
|
{ |
154 |
|
throw TypeCheckingExceptionPrivate( |
155 |
|
n, |
156 |
|
"expecting a term in second argument of indexof that is the same " |
157 |
|
"type as the first argument"); |
158 |
|
} |
159 |
2188 |
t = n[2].getType(check); |
160 |
2188 |
if (!t.isInteger()) |
161 |
|
{ |
162 |
|
throw TypeCheckingExceptionPrivate( |
163 |
|
n, "expecting an integer term in third argument of indexof"); |
164 |
|
} |
165 |
|
} |
166 |
2188 |
return nodeManager->integerType(); |
167 |
|
} |
168 |
|
|
169 |
3162 |
TypeNode StringReplaceTypeRule::computeType(NodeManager* nodeManager, |
170 |
|
TNode n, |
171 |
|
bool check) |
172 |
|
{ |
173 |
3162 |
TypeNode t = n[0].getType(check); |
174 |
3162 |
if (check) |
175 |
|
{ |
176 |
3162 |
if (!t.isStringLike()) |
177 |
|
{ |
178 |
|
throw TypeCheckingExceptionPrivate( |
179 |
|
n, "expecting a string-like term in replace"); |
180 |
|
} |
181 |
6324 |
TypeNode t2 = n[1].getType(check); |
182 |
3162 |
if (t != t2) |
183 |
|
{ |
184 |
|
throw TypeCheckingExceptionPrivate( |
185 |
|
n, |
186 |
|
"expecting a term in second argument of replace that is the same " |
187 |
|
"type as the first argument"); |
188 |
|
} |
189 |
3162 |
t2 = n[2].getType(check); |
190 |
3162 |
if (t != t2) |
191 |
|
{ |
192 |
|
throw TypeCheckingExceptionPrivate( |
193 |
|
n, |
194 |
|
"expecting a term in third argument of replace that is the same " |
195 |
|
"type as the first argument"); |
196 |
|
} |
197 |
|
} |
198 |
3162 |
return t; |
199 |
|
} |
200 |
|
|
201 |
240 |
TypeNode StringStrToBoolTypeRule::computeType(NodeManager* nodeManager, |
202 |
|
TNode n, |
203 |
|
bool check) |
204 |
|
{ |
205 |
240 |
if (check) |
206 |
|
{ |
207 |
480 |
TypeNode t = n[0].getType(check); |
208 |
240 |
if (!t.isStringLike()) |
209 |
|
{ |
210 |
|
std::stringstream ss; |
211 |
|
ss << "expecting a string-like term in argument of " << n.getKind(); |
212 |
|
throw TypeCheckingExceptionPrivate(n, ss.str()); |
213 |
|
} |
214 |
|
} |
215 |
240 |
return nodeManager->booleanType(); |
216 |
|
} |
217 |
|
|
218 |
43512 |
TypeNode StringStrToIntTypeRule::computeType(NodeManager* nodeManager, |
219 |
|
TNode n, |
220 |
|
bool check) |
221 |
|
{ |
222 |
43512 |
if (check) |
223 |
|
{ |
224 |
87024 |
TypeNode t = n[0].getType(check); |
225 |
43512 |
if (!t.isStringLike()) |
226 |
|
{ |
227 |
|
std::stringstream ss; |
228 |
|
ss << "expecting a string-like term in argument of " << n.getKind(); |
229 |
|
throw TypeCheckingExceptionPrivate(n, ss.str()); |
230 |
|
} |
231 |
|
} |
232 |
43512 |
return nodeManager->integerType(); |
233 |
|
} |
234 |
|
|
235 |
165 |
TypeNode StringStrToStrTypeRule::computeType(NodeManager* nodeManager, |
236 |
|
TNode n, |
237 |
|
bool check) |
238 |
|
{ |
239 |
165 |
TypeNode t = n[0].getType(check); |
240 |
165 |
if (check) |
241 |
|
{ |
242 |
165 |
if (!t.isStringLike()) |
243 |
|
{ |
244 |
|
std::stringstream ss; |
245 |
|
ss << "expecting a string term in argument of " << n.getKind(); |
246 |
|
throw TypeCheckingExceptionPrivate(n, ss.str()); |
247 |
|
} |
248 |
|
} |
249 |
165 |
return t; |
250 |
|
} |
251 |
|
|
252 |
41773 |
TypeNode StringRelationTypeRule::computeType(NodeManager* nodeManager, |
253 |
|
TNode n, |
254 |
|
bool check) |
255 |
|
{ |
256 |
41773 |
if (check) |
257 |
|
{ |
258 |
83546 |
TypeNode t = n[0].getType(check); |
259 |
41773 |
if (!t.isStringLike()) |
260 |
|
{ |
261 |
|
throw TypeCheckingExceptionPrivate( |
262 |
|
n, "expecting a string-like term in relation"); |
263 |
|
} |
264 |
83546 |
TypeNode t2 = n[1].getType(check); |
265 |
41773 |
if (t != t2) |
266 |
|
{ |
267 |
|
throw TypeCheckingExceptionPrivate( |
268 |
|
n, "expecting two terms of the same string-like type in relation"); |
269 |
|
} |
270 |
|
} |
271 |
41773 |
return nodeManager->booleanType(); |
272 |
|
} |
273 |
|
|
274 |
194 |
TypeNode RegExpRangeTypeRule::computeType(NodeManager* nodeManager, |
275 |
|
TNode n, |
276 |
|
bool check) |
277 |
|
{ |
278 |
194 |
if (check) |
279 |
|
{ |
280 |
194 |
TNode::iterator it = n.begin(); |
281 |
582 |
for (int i = 0; i < 2; ++i) |
282 |
|
{ |
283 |
776 |
TypeNode t = (*it).getType(check); |
284 |
388 |
if (!t.isString()) // string-only |
285 |
|
{ |
286 |
|
throw TypeCheckingExceptionPrivate( |
287 |
|
n, "expecting a string term in regexp range"); |
288 |
|
} |
289 |
388 |
++it; |
290 |
|
} |
291 |
|
} |
292 |
194 |
return nodeManager->regExpType(); |
293 |
|
} |
294 |
|
|
295 |
449 |
TypeNode ConstSequenceTypeRule::computeType(NodeManager* nodeManager, |
296 |
|
TNode n, |
297 |
|
bool check) |
298 |
|
{ |
299 |
449 |
Assert(n.getKind() == kind::CONST_SEQUENCE); |
300 |
449 |
return nodeManager->mkSequenceType(n.getConst<Sequence>().getType()); |
301 |
|
} |
302 |
|
|
303 |
276 |
TypeNode SeqUnitTypeRule::computeType(NodeManager* nodeManager, |
304 |
|
TNode n, |
305 |
|
bool check) |
306 |
|
{ |
307 |
276 |
return nodeManager->mkSequenceType(n[0].getType(check)); |
308 |
|
} |
309 |
|
|
310 |
237 |
TypeNode SeqNthTypeRule::computeType(NodeManager* nodeManager, |
311 |
|
TNode n, |
312 |
|
bool check) |
313 |
|
{ |
314 |
474 |
TypeNode t = n[0].getType(check); |
315 |
237 |
TypeNode t1 = t.getSequenceElementType(); |
316 |
237 |
if (check) |
317 |
|
{ |
318 |
237 |
if (!t.isSequence()) |
319 |
|
{ |
320 |
|
throw TypeCheckingExceptionPrivate(n, "expecting a sequence in nth"); |
321 |
|
} |
322 |
474 |
TypeNode t2 = n[1].getType(check); |
323 |
237 |
if (!t2.isInteger()) |
324 |
|
{ |
325 |
|
throw TypeCheckingExceptionPrivate( |
326 |
|
n, "expecting an integer start term in nth"); |
327 |
|
} |
328 |
|
} |
329 |
474 |
return t1; |
330 |
|
} |
331 |
|
|
332 |
|
Cardinality SequenceProperties::computeCardinality(TypeNode type) |
333 |
|
{ |
334 |
|
Assert(type.getKind() == kind::SEQUENCE_TYPE); |
335 |
|
return Cardinality::INTEGERS; |
336 |
|
} |
337 |
|
/** A sequence is well-founded if its element type is */ |
338 |
|
bool SequenceProperties::isWellFounded(TypeNode type) |
339 |
|
{ |
340 |
|
return type[0].isWellFounded(); |
341 |
|
} |
342 |
|
/** Make ground term for sequence type (return the empty sequence) */ |
343 |
|
Node SequenceProperties::mkGroundTerm(TypeNode type) |
344 |
|
{ |
345 |
|
Assert(type.isSequence()); |
346 |
|
// empty sequence |
347 |
|
std::vector<Node> seq; |
348 |
|
return NodeManager::currentNM()->mkConst( |
349 |
|
Sequence(type.getSequenceElementType(), seq)); |
350 |
|
} |
351 |
|
} // namespace strings |
352 |
|
} // namespace theory |
353 |
31125 |
} // namespace cvc5 |