1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Kshitij Bansal, Mudathir Mohamed |
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 |
|
* Sets theory type rules. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/sets/theory_sets_type_rules.h" |
17 |
|
|
18 |
|
#include <climits> |
19 |
|
#include <sstream> |
20 |
|
|
21 |
|
#include "theory/sets/normal_form.h" |
22 |
|
#include "theory/sets/singleton_op.h" |
23 |
|
#include "util/cardinality.h" |
24 |
|
|
25 |
|
namespace cvc5 { |
26 |
|
namespace theory { |
27 |
|
namespace sets { |
28 |
|
|
29 |
7391 |
TypeNode SetsBinaryOperatorTypeRule::computeType(NodeManager* nodeManager, |
30 |
|
TNode n, |
31 |
|
bool check) |
32 |
|
{ |
33 |
7391 |
Assert(n.getKind() == kind::UNION || n.getKind() == kind::INTERSECTION |
34 |
|
|| n.getKind() == kind::SETMINUS); |
35 |
7391 |
TypeNode setType = n[0].getType(check); |
36 |
7391 |
if (check) |
37 |
|
{ |
38 |
7391 |
if (!setType.isSet()) |
39 |
|
{ |
40 |
|
throw TypeCheckingExceptionPrivate( |
41 |
|
n, "operator expects a set, first argument is not"); |
42 |
|
} |
43 |
14782 |
TypeNode secondSetType = n[1].getType(check); |
44 |
7391 |
if (secondSetType != setType) |
45 |
|
{ |
46 |
4 |
std::stringstream ss; |
47 |
2 |
ss << "Operator " << n.getKind() |
48 |
2 |
<< " expects two sets of the same type. Found types '" << setType |
49 |
2 |
<< "' and '" << secondSetType << "'."; |
50 |
2 |
throw TypeCheckingExceptionPrivate(n, ss.str()); |
51 |
|
} |
52 |
|
} |
53 |
7389 |
return setType; |
54 |
|
} |
55 |
|
|
56 |
4224 |
bool SetsBinaryOperatorTypeRule::computeIsConst(NodeManager* nodeManager, |
57 |
|
TNode n) |
58 |
|
{ |
59 |
|
// only UNION has a const rule in kinds. |
60 |
|
// INTERSECTION and SETMINUS are not used in the canonical representation of |
61 |
|
// sets and therefore they do not have const rules in kinds |
62 |
4224 |
Assert(n.getKind() == kind::UNION); |
63 |
4224 |
return NormalForm::checkNormalConstant(n); |
64 |
|
} |
65 |
|
|
66 |
370 |
TypeNode SubsetTypeRule::computeType(NodeManager* nodeManager, |
67 |
|
TNode n, |
68 |
|
bool check) |
69 |
|
{ |
70 |
370 |
Assert(n.getKind() == kind::SUBSET); |
71 |
740 |
TypeNode setType = n[0].getType(check); |
72 |
370 |
if (check) |
73 |
|
{ |
74 |
370 |
if (!setType.isSet()) |
75 |
|
{ |
76 |
|
throw TypeCheckingExceptionPrivate(n, "set subset operating on non-set"); |
77 |
|
} |
78 |
740 |
TypeNode secondSetType = n[1].getType(check); |
79 |
370 |
if (secondSetType != setType) |
80 |
|
{ |
81 |
|
if (!setType.isComparableTo(secondSetType)) |
82 |
|
{ |
83 |
|
throw TypeCheckingExceptionPrivate( |
84 |
|
n, "set subset operating on sets of different types"); |
85 |
|
} |
86 |
|
} |
87 |
|
} |
88 |
740 |
return nodeManager->booleanType(); |
89 |
|
} |
90 |
|
|
91 |
23278 |
TypeNode MemberTypeRule::computeType(NodeManager* nodeManager, |
92 |
|
TNode n, |
93 |
|
bool check) |
94 |
|
{ |
95 |
23278 |
Assert(n.getKind() == kind::MEMBER); |
96 |
46556 |
TypeNode setType = n[1].getType(check); |
97 |
23278 |
if (check) |
98 |
|
{ |
99 |
23278 |
if (!setType.isSet()) |
100 |
|
{ |
101 |
|
throw TypeCheckingExceptionPrivate( |
102 |
|
n, "checking for membership in a non-set"); |
103 |
|
} |
104 |
46556 |
TypeNode elementType = n[0].getType(check); |
105 |
|
// e.g. (member 1 (singleton 1.0)) is true whereas |
106 |
|
// (member 1.0 (singleton 1)) throws a typing error |
107 |
23278 |
if (!elementType.isSubtypeOf(setType.getSetElementType())) |
108 |
|
{ |
109 |
|
std::stringstream ss; |
110 |
|
ss << "member operating on sets of different types:\n" |
111 |
|
<< "child type: " << elementType << "\n" |
112 |
|
<< "not subtype: " << setType.getSetElementType() << "\n" |
113 |
|
<< "in term : " << n; |
114 |
|
throw TypeCheckingExceptionPrivate(n, ss.str()); |
115 |
|
} |
116 |
|
} |
117 |
46556 |
return nodeManager->booleanType(); |
118 |
|
} |
119 |
|
|
120 |
3146 |
TypeNode SingletonTypeRule::computeType(NodeManager* nodeManager, |
121 |
|
TNode n, |
122 |
|
bool check) |
123 |
|
{ |
124 |
3146 |
Assert(n.getKind() == kind::SINGLETON && n.hasOperator() |
125 |
|
&& n.getOperator().getKind() == kind::SINGLETON_OP); |
126 |
|
|
127 |
6292 |
SingletonOp op = n.getOperator().getConst<SingletonOp>(); |
128 |
6292 |
TypeNode type1 = op.getType(); |
129 |
3146 |
if (check) |
130 |
|
{ |
131 |
6292 |
TypeNode type2 = n[0].getType(check); |
132 |
6292 |
TypeNode leastCommonType = TypeNode::leastCommonTypeNode(type1, type2); |
133 |
|
// the type of the element should be a subtype of the type of the operator |
134 |
|
// e.g. (singleton (singleton_op Real) 1) where 1 is an Int |
135 |
3146 |
if (leastCommonType.isNull() || leastCommonType != type1) |
136 |
|
{ |
137 |
|
std::stringstream ss; |
138 |
|
ss << "The type '" << type2 << "' of the element is not a subtype of '" |
139 |
|
<< type1 << "' in term : " << n; |
140 |
|
throw TypeCheckingExceptionPrivate(n, ss.str()); |
141 |
|
} |
142 |
|
} |
143 |
6292 |
return nodeManager->mkSetType(type1); |
144 |
|
} |
145 |
|
|
146 |
2941 |
bool SingletonTypeRule::computeIsConst(NodeManager* nodeManager, TNode n) |
147 |
|
{ |
148 |
2941 |
Assert(n.getKind() == kind::SINGLETON); |
149 |
2941 |
return n[0].isConst(); |
150 |
|
} |
151 |
|
|
152 |
1991 |
TypeNode EmptySetTypeRule::computeType(NodeManager* nodeManager, |
153 |
|
TNode n, |
154 |
|
bool check) |
155 |
|
{ |
156 |
1991 |
Assert(n.getKind() == kind::EMPTYSET); |
157 |
3982 |
EmptySet emptySet = n.getConst<EmptySet>(); |
158 |
3982 |
return emptySet.getType(); |
159 |
|
} |
160 |
|
|
161 |
2719 |
TypeNode CardTypeRule::computeType(NodeManager* nodeManager, |
162 |
|
TNode n, |
163 |
|
bool check) |
164 |
|
{ |
165 |
2719 |
Assert(n.getKind() == kind::CARD); |
166 |
5438 |
TypeNode setType = n[0].getType(check); |
167 |
2719 |
if (check) |
168 |
|
{ |
169 |
2719 |
if (!setType.isSet()) |
170 |
|
{ |
171 |
|
throw TypeCheckingExceptionPrivate( |
172 |
|
n, "cardinality operates on a set, non-set object found"); |
173 |
|
} |
174 |
|
} |
175 |
5438 |
return nodeManager->integerType(); |
176 |
|
} |
177 |
|
|
178 |
23 |
TypeNode ComplementTypeRule::computeType(NodeManager* nodeManager, |
179 |
|
TNode n, |
180 |
|
bool check) |
181 |
|
{ |
182 |
23 |
Assert(n.getKind() == kind::COMPLEMENT); |
183 |
23 |
TypeNode setType = n[0].getType(check); |
184 |
23 |
if (check) |
185 |
|
{ |
186 |
23 |
if (!setType.isSet()) |
187 |
|
{ |
188 |
|
throw TypeCheckingExceptionPrivate( |
189 |
|
n, "COMPLEMENT operates on a set, non-set object found"); |
190 |
|
} |
191 |
|
} |
192 |
23 |
return setType; |
193 |
|
} |
194 |
|
|
195 |
134 |
TypeNode UniverseSetTypeRule::computeType(NodeManager* nodeManager, |
196 |
|
TNode n, |
197 |
|
bool check) |
198 |
|
{ |
199 |
134 |
Assert(n.getKind() == kind::UNIVERSE_SET); |
200 |
|
// for nullary operators, we only computeType for check=true, since they are |
201 |
|
// given TypeAttr() on creation |
202 |
134 |
Assert(check); |
203 |
134 |
TypeNode setType = n.getType(); |
204 |
134 |
if (!setType.isSet()) |
205 |
|
{ |
206 |
|
throw TypeCheckingExceptionPrivate(n, |
207 |
|
"Non-set type found for universe set"); |
208 |
|
} |
209 |
134 |
return setType; |
210 |
|
} |
211 |
|
|
212 |
53 |
TypeNode ComprehensionTypeRule::computeType(NodeManager* nodeManager, |
213 |
|
TNode n, |
214 |
|
bool check) |
215 |
|
{ |
216 |
53 |
Assert(n.getKind() == kind::COMPREHENSION); |
217 |
53 |
if (check) |
218 |
|
{ |
219 |
53 |
if (n[0].getType(check) != nodeManager->boundVarListType()) |
220 |
|
{ |
221 |
|
throw TypeCheckingExceptionPrivate( |
222 |
|
n, "first argument of set comprehension is not bound var list"); |
223 |
|
} |
224 |
53 |
if (n[1].getType(check) != nodeManager->booleanType()) |
225 |
|
{ |
226 |
|
throw TypeCheckingExceptionPrivate( |
227 |
|
n, "body of set comprehension is not boolean"); |
228 |
|
} |
229 |
|
} |
230 |
53 |
return nodeManager->mkSetType(n[2].getType(check)); |
231 |
|
} |
232 |
|
|
233 |
18 |
TypeNode ChooseTypeRule::computeType(NodeManager* nodeManager, |
234 |
|
TNode n, |
235 |
|
bool check) |
236 |
|
{ |
237 |
18 |
Assert(n.getKind() == kind::CHOOSE); |
238 |
36 |
TypeNode setType = n[0].getType(check); |
239 |
18 |
if (check) |
240 |
|
{ |
241 |
18 |
if (!setType.isSet()) |
242 |
|
{ |
243 |
|
throw TypeCheckingExceptionPrivate( |
244 |
|
n, "CHOOSE operator expects a set, a non-set is found"); |
245 |
|
} |
246 |
|
} |
247 |
36 |
return setType.getSetElementType(); |
248 |
|
} |
249 |
|
|
250 |
29 |
TypeNode IsSingletonTypeRule::computeType(NodeManager* nodeManager, |
251 |
|
TNode n, |
252 |
|
bool check) |
253 |
|
{ |
254 |
29 |
Assert(n.getKind() == kind::IS_SINGLETON); |
255 |
58 |
TypeNode setType = n[0].getType(check); |
256 |
29 |
if (check) |
257 |
|
{ |
258 |
29 |
if (!setType.isSet()) |
259 |
|
{ |
260 |
|
throw TypeCheckingExceptionPrivate( |
261 |
|
n, "IS_SINGLETON operator expects a set, a non-set is found"); |
262 |
|
} |
263 |
|
} |
264 |
58 |
return nodeManager->booleanType(); |
265 |
|
} |
266 |
|
|
267 |
31 |
TypeNode InsertTypeRule::computeType(NodeManager* nodeManager, |
268 |
|
TNode n, |
269 |
|
bool check) |
270 |
|
{ |
271 |
31 |
Assert(n.getKind() == kind::INSERT); |
272 |
31 |
size_t numChildren = n.getNumChildren(); |
273 |
31 |
Assert(numChildren >= 2); |
274 |
31 |
TypeNode setType = n[numChildren - 1].getType(check); |
275 |
31 |
if (check) |
276 |
|
{ |
277 |
31 |
if (!setType.isSet()) |
278 |
|
{ |
279 |
|
throw TypeCheckingExceptionPrivate(n, "inserting into a non-set"); |
280 |
|
} |
281 |
110 |
for (size_t i = 0; i < numChildren - 1; ++i) |
282 |
|
{ |
283 |
158 |
TypeNode elementType = n[i].getType(check); |
284 |
79 |
if (elementType != setType.getSetElementType()) |
285 |
|
{ |
286 |
|
throw TypeCheckingExceptionPrivate( |
287 |
|
n, |
288 |
|
"type of element should be same as element type of set being " |
289 |
|
"inserted into"); |
290 |
|
} |
291 |
|
} |
292 |
|
} |
293 |
31 |
return setType; |
294 |
|
} |
295 |
|
|
296 |
365 |
TypeNode RelBinaryOperatorTypeRule::computeType(NodeManager* nodeManager, |
297 |
|
TNode n, |
298 |
|
bool check) |
299 |
|
{ |
300 |
365 |
Assert(n.getKind() == kind::PRODUCT || n.getKind() == kind::JOIN); |
301 |
|
|
302 |
730 |
TypeNode firstRelType = n[0].getType(check); |
303 |
730 |
TypeNode secondRelType = n[1].getType(check); |
304 |
365 |
TypeNode resultType = firstRelType; |
305 |
|
|
306 |
365 |
if (!firstRelType.isSet() || !secondRelType.isSet()) |
307 |
|
{ |
308 |
|
throw TypeCheckingExceptionPrivate( |
309 |
|
n, " Relational operator operates on non-sets"); |
310 |
|
} |
311 |
365 |
if (!firstRelType[0].isTuple() || !secondRelType[0].isTuple()) |
312 |
|
{ |
313 |
|
throw TypeCheckingExceptionPrivate( |
314 |
|
n, " Relational operator operates on non-relations (sets of tuples)"); |
315 |
|
} |
316 |
|
|
317 |
730 |
std::vector<TypeNode> newTupleTypes; |
318 |
730 |
std::vector<TypeNode> firstTupleTypes = firstRelType[0].getTupleTypes(); |
319 |
730 |
std::vector<TypeNode> secondTupleTypes = secondRelType[0].getTupleTypes(); |
320 |
|
|
321 |
|
// JOIN is not allowed to apply on two unary sets |
322 |
365 |
if (n.getKind() == kind::JOIN) |
323 |
|
{ |
324 |
318 |
if ((firstTupleTypes.size() == 1) && (secondTupleTypes.size() == 1)) |
325 |
|
{ |
326 |
|
throw TypeCheckingExceptionPrivate( |
327 |
|
n, " Join operates on two unary relations"); |
328 |
|
} |
329 |
318 |
else if (firstTupleTypes.back() != secondTupleTypes.front()) |
330 |
|
{ |
331 |
|
throw TypeCheckingExceptionPrivate( |
332 |
|
n, " Join operates on two non-joinable relations"); |
333 |
|
} |
334 |
954 |
newTupleTypes.insert(newTupleTypes.end(), |
335 |
|
firstTupleTypes.begin(), |
336 |
1272 |
firstTupleTypes.end() - 1); |
337 |
954 |
newTupleTypes.insert(newTupleTypes.end(), |
338 |
636 |
secondTupleTypes.begin() + 1, |
339 |
1272 |
secondTupleTypes.end()); |
340 |
|
} |
341 |
47 |
else if (n.getKind() == kind::PRODUCT) |
342 |
|
{ |
343 |
47 |
newTupleTypes.insert( |
344 |
94 |
newTupleTypes.end(), firstTupleTypes.begin(), firstTupleTypes.end()); |
345 |
47 |
newTupleTypes.insert( |
346 |
94 |
newTupleTypes.end(), secondTupleTypes.begin(), secondTupleTypes.end()); |
347 |
|
} |
348 |
365 |
resultType = nodeManager->mkSetType(nodeManager->mkTupleType(newTupleTypes)); |
349 |
|
|
350 |
730 |
return resultType; |
351 |
|
} |
352 |
|
|
353 |
119 |
TypeNode RelTransposeTypeRule::computeType(NodeManager* nodeManager, |
354 |
|
TNode n, |
355 |
|
bool check) |
356 |
|
{ |
357 |
119 |
Assert(n.getKind() == kind::TRANSPOSE); |
358 |
238 |
TypeNode setType = n[0].getType(check); |
359 |
119 |
if (check && (!setType.isSet() || !setType.getSetElementType().isTuple())) |
360 |
|
{ |
361 |
|
throw TypeCheckingExceptionPrivate( |
362 |
|
n, "relation transpose operates on non-relation"); |
363 |
|
} |
364 |
238 |
std::vector<TypeNode> tupleTypes = setType[0].getTupleTypes(); |
365 |
119 |
std::reverse(tupleTypes.begin(), tupleTypes.end()); |
366 |
238 |
return nodeManager->mkSetType(nodeManager->mkTupleType(tupleTypes)); |
367 |
|
} |
368 |
|
|
369 |
44 |
TypeNode RelTransClosureTypeRule::computeType(NodeManager* nodeManager, |
370 |
|
TNode n, |
371 |
|
bool check) |
372 |
|
{ |
373 |
44 |
Assert(n.getKind() == kind::TCLOSURE); |
374 |
44 |
TypeNode setType = n[0].getType(check); |
375 |
44 |
if (check) |
376 |
|
{ |
377 |
44 |
if (!setType.isSet() || !setType.getSetElementType().isTuple()) |
378 |
|
{ |
379 |
|
throw TypeCheckingExceptionPrivate( |
380 |
|
n, " transitive closure operates on non-relation"); |
381 |
|
} |
382 |
88 |
std::vector<TypeNode> tupleTypes = setType[0].getTupleTypes(); |
383 |
44 |
if (tupleTypes.size() != 2) |
384 |
|
{ |
385 |
|
throw TypeCheckingExceptionPrivate( |
386 |
|
n, " transitive closure operates on non-binary relations"); |
387 |
|
} |
388 |
44 |
if (tupleTypes[0] != tupleTypes[1]) |
389 |
|
{ |
390 |
|
throw TypeCheckingExceptionPrivate( |
391 |
|
n, |
392 |
|
" transitive closure operates on non-homogeneous binary relations"); |
393 |
|
} |
394 |
|
} |
395 |
44 |
return setType; |
396 |
|
} |
397 |
|
|
398 |
38 |
TypeNode JoinImageTypeRule::computeType(NodeManager* nodeManager, |
399 |
|
TNode n, |
400 |
|
bool check) |
401 |
|
{ |
402 |
38 |
Assert(n.getKind() == kind::JOIN_IMAGE); |
403 |
|
|
404 |
76 |
TypeNode firstRelType = n[0].getType(check); |
405 |
|
|
406 |
38 |
if (!firstRelType.isSet()) |
407 |
|
{ |
408 |
|
throw TypeCheckingExceptionPrivate( |
409 |
|
n, " JoinImage operator operates on non-relations"); |
410 |
|
} |
411 |
38 |
if (!firstRelType[0].isTuple()) |
412 |
|
{ |
413 |
|
throw TypeCheckingExceptionPrivate( |
414 |
|
n, " JoinImage operator operates on non-relations (sets of tuples)"); |
415 |
|
} |
416 |
|
|
417 |
76 |
std::vector<TypeNode> tupleTypes = firstRelType[0].getTupleTypes(); |
418 |
38 |
if (tupleTypes.size() != 2) |
419 |
|
{ |
420 |
|
throw TypeCheckingExceptionPrivate( |
421 |
|
n, " JoinImage operates on a non-binary relation"); |
422 |
|
} |
423 |
76 |
TypeNode valType = n[1].getType(check); |
424 |
38 |
if (valType != nodeManager->integerType()) |
425 |
|
{ |
426 |
|
throw TypeCheckingExceptionPrivate( |
427 |
|
n, " JoinImage cardinality constraint must be integer"); |
428 |
|
} |
429 |
76 |
std::vector<TypeNode> newTupleTypes; |
430 |
38 |
newTupleTypes.push_back(tupleTypes[0]); |
431 |
76 |
return nodeManager->mkSetType(nodeManager->mkTupleType(newTupleTypes)); |
432 |
|
} |
433 |
|
|
434 |
9 |
TypeNode RelIdenTypeRule::computeType(NodeManager* nodeManager, |
435 |
|
TNode n, |
436 |
|
bool check) |
437 |
|
{ |
438 |
9 |
Assert(n.getKind() == kind::IDEN); |
439 |
18 |
TypeNode setType = n[0].getType(check); |
440 |
9 |
if (check) |
441 |
|
{ |
442 |
9 |
if (!setType.isSet() && !setType.getSetElementType().isTuple()) |
443 |
|
{ |
444 |
|
throw TypeCheckingExceptionPrivate(n, |
445 |
|
" Identity operates on non-relation"); |
446 |
|
} |
447 |
9 |
if (setType[0].getTupleTypes().size() != 1) |
448 |
|
{ |
449 |
|
throw TypeCheckingExceptionPrivate( |
450 |
|
n, " Identity operates on non-unary relations"); |
451 |
|
} |
452 |
|
} |
453 |
18 |
std::vector<TypeNode> tupleTypes = setType[0].getTupleTypes(); |
454 |
9 |
tupleTypes.push_back(tupleTypes[0]); |
455 |
18 |
return nodeManager->mkSetType(nodeManager->mkTupleType(tupleTypes)); |
456 |
|
} |
457 |
|
|
458 |
|
Cardinality SetsProperties::computeCardinality(TypeNode type) |
459 |
|
{ |
460 |
|
Assert(type.getKind() == kind::SET_TYPE); |
461 |
|
Cardinality elementCard = 2; |
462 |
|
elementCard ^= type[0].getCardinality(); |
463 |
|
return elementCard; |
464 |
|
} |
465 |
|
|
466 |
|
bool SetsProperties::isWellFounded(TypeNode type) |
467 |
|
{ |
468 |
|
return type[0].isWellFounded(); |
469 |
|
} |
470 |
|
|
471 |
6 |
Node SetsProperties::mkGroundTerm(TypeNode type) |
472 |
|
{ |
473 |
6 |
Assert(type.isSet()); |
474 |
6 |
return NodeManager::currentNM()->mkConst(EmptySet(type)); |
475 |
|
} |
476 |
|
|
477 |
|
} // namespace sets |
478 |
|
} // namespace theory |
479 |
29511 |
} // namespace cvc5 |