Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Typing and cardinality rules for the theory of datatypes.
11 : : */
12 : :
13 : : #include "theory/datatypes/theory_datatypes_type_rules.h"
14 : :
15 : : #include <sstream>
16 : :
17 : : #include "expr/ascription_type.h"
18 : : #include "expr/codatatype_bound_variable.h"
19 : : #include "expr/dtype.h"
20 : : #include "expr/dtype_cons.h"
21 : : #include "expr/type_matcher.h"
22 : : #include "theory/datatypes/project_op.h"
23 : : #include "theory/datatypes/theory_datatypes_utils.h"
24 : : #include "theory/datatypes/tuple_utils.h"
25 : : #include "util/rational.h"
26 : :
27 : : namespace cvc5::internal {
28 : : namespace theory {
29 : : namespace datatypes {
30 : :
31 : 0 : TypeNode DatatypeConstructorTypeRule::preComputeType(
32 : : CVC5_UNUSED NodeManager* nm, TNode n)
33 : : {
34 : 0 : TypeNode consType = n.getOperator().getTypeOrNull();
35 [ - - ]: 0 : if (consType.isDatatypeConstructor())
36 : : {
37 : 0 : TypeNode t = consType.getDatatypeConstructorRangeType();
38 : : // if not parametric, the return type can be obtained from constructor op
39 [ - - ]: 0 : if (!t.isParametricDatatype())
40 : : {
41 : 0 : return t;
42 : : }
43 [ - - ]: 0 : }
44 : 0 : return TypeNode::null();
45 : 0 : }
46 : 325614 : TypeNode DatatypeConstructorTypeRule::computeType(
47 : : CVC5_UNUSED NodeManager* nodeManager,
48 : : TNode n,
49 : : bool check,
50 : : std::ostream* errOut)
51 : : {
52 [ - + ][ - + ]: 325614 : Assert(n.getKind() == Kind::APPLY_CONSTRUCTOR);
[ - - ]
53 : 325614 : TypeNode consType = n.getOperator().getTypeOrNull();
54 : : // note that datatype constructors cannot be abstracted
55 [ + + ]: 325614 : if (!consType.isDatatypeConstructor())
56 : : {
57 [ + + ]: 3 : if (errOut)
58 : : {
59 : 1 : (*errOut) << "expected constructor to apply";
60 : : }
61 : 3 : return TypeNode::null();
62 : : }
63 : 325611 : TypeNode t = consType.getDatatypeConstructorRangeType();
64 [ - + ][ - + ]: 325611 : Assert(t.isDatatype());
[ - - ]
65 : 325611 : TNode::iterator child_it = n.begin();
66 : 325611 : TNode::iterator child_it_end = n.end();
67 : 325611 : TypeNode::iterator tchild_it = consType.begin();
68 [ + - ]: 650100 : if ((t.isParametricDatatype() || check)
69 [ + + ][ + + ]: 650100 : && n.getNumChildren() != consType.getNumChildren() - 1)
[ + + ]
70 : : {
71 [ + + ]: 18 : if (errOut)
72 : : {
73 : 6 : (*errOut) << "number of arguments does not match the constructor type";
74 : : }
75 : 18 : return TypeNode::null();
76 : : }
77 [ + + ]: 325593 : if (t.isParametricDatatype())
78 : : {
79 [ + - ]: 2220 : Trace("typecheck-idt") << "typecheck parameterized datatype " << n
80 : 1110 : << std::endl;
81 : 1110 : TypeMatcher m(t);
82 [ + + ]: 2484 : for (; child_it != child_it_end; ++child_it, ++tchild_it)
83 : : {
84 : 1374 : TypeNode childType = (*child_it).getTypeOrNull();
85 [ - + ]: 1374 : if (!m.doMatching(*tchild_it, childType))
86 : : {
87 [ - - ]: 0 : if (errOut)
88 : : {
89 : 0 : (*errOut) << "matching failed for parameterized constructor";
90 : : }
91 : 0 : return TypeNode::null();
92 : : }
93 [ + - ]: 1374 : }
94 : 1110 : std::vector<TypeNode> instTypes;
95 : 1110 : m.getMatches(instTypes);
96 : 1110 : TypeNode range = t.instantiate(instTypes);
97 [ + - ]: 2220 : Trace("typecheck-idt") << "Return (constructor) " << range << " for " << n
98 : 1110 : << std::endl;
99 : 1110 : return range;
100 : 1110 : }
101 : : else
102 : : {
103 [ + - ]: 324483 : if (check)
104 : : {
105 [ + - ]: 648966 : Trace("typecheck-idt")
106 : 324483 : << "typecheck cons: " << n << " " << n.getNumChildren() << std::endl;
107 [ + - ]: 648966 : Trace("typecheck-idt") << "cons type: " << consType << " "
108 : 324483 : << consType.getNumChildren() << std::endl;
109 [ + + ]: 899163 : for (; child_it != child_it_end; ++child_it, ++tchild_it)
110 : : {
111 : 574680 : TypeNode childType = (*child_it).getTypeOrNull();
112 [ + - ]: 1149360 : Trace("typecheck-idt") << "typecheck cons arg: " << childType << " "
113 [ - + ][ - - ]: 574680 : << (*tchild_it) << std::endl;
114 : 574680 : TypeNode argumentType = *tchild_it;
115 [ - + ]: 574680 : if (!childType.isComparableTo(argumentType))
116 : : {
117 [ - - ]: 0 : if (errOut)
118 : : {
119 : : (*errOut) << "bad type for constructor argument:\n"
120 : 0 : << "child type: " << childType << "\n"
121 : 0 : << "not type: " << argumentType << "\n"
122 : 0 : << "in term : " << n;
123 : : }
124 : 0 : return TypeNode::null();
125 : : }
126 [ + - ][ + - ]: 574680 : }
127 : : }
128 : 324483 : return t;
129 : : }
130 : 325614 : }
131 : :
132 : 179320 : bool DatatypeConstructorTypeRule::computeIsConst(
133 : : CVC5_UNUSED NodeManager* nodeManager, TNode n)
134 : : {
135 [ - + ][ - + ]: 179320 : Assert(n.getKind() == Kind::APPLY_CONSTRUCTOR);
[ - - ]
136 [ + + ]: 349127 : for (TNode::const_iterator i = n.begin(); i != n.end(); ++i)
137 : : {
138 [ + + ]: 270079 : if (!(*i).isConst())
139 : : {
140 : 100272 : return false;
141 : : }
142 : : }
143 : 79048 : return true;
144 : : }
145 : :
146 : 0 : TypeNode DatatypeSelectorTypeRule::preComputeType(CVC5_UNUSED NodeManager* nm,
147 : : CVC5_UNUSED TNode n)
148 : : {
149 : 0 : return TypeNode::null();
150 : : }
151 : 102420 : TypeNode DatatypeSelectorTypeRule::computeType(
152 : : CVC5_UNUSED NodeManager* nodeManager,
153 : : TNode n,
154 : : bool check,
155 : : std::ostream* errOut)
156 : : {
157 [ - + ][ - + ]: 102420 : Assert(n.getKind() == Kind::APPLY_SELECTOR);
[ - - ]
158 : 102420 : TypeNode selType = n.getOperator().getTypeOrNull();
159 [ - + ]: 102420 : if (!selType.isDatatypeSelector())
160 : : {
161 [ - - ]: 0 : if (errOut)
162 : : {
163 : 0 : (*errOut) << "expected selector to apply";
164 : : }
165 : 0 : return TypeNode::null();
166 : : }
167 : 102420 : TypeNode t = selType.getDatatypeSelectorDomainType();
168 [ - + ][ - + ]: 102420 : Assert(t.isDatatype());
[ - - ]
169 [ + + ][ + - ]: 102420 : if ((t.isParametricDatatype() || check) && n.getNumChildren() != 1)
[ - + ][ - + ]
170 : : {
171 [ - - ]: 0 : if (errOut)
172 : : {
173 : 0 : (*errOut) << "number of arguments does not match the selector type";
174 : : }
175 : 0 : return TypeNode::null();
176 : : }
177 [ + + ]: 102420 : if (t.isParametricDatatype())
178 : : {
179 [ + - ]: 1499 : Trace("typecheck-idt") << "typecheck parameterized sel: " << n << std::endl;
180 : 1499 : TypeMatcher m(t);
181 : 1499 : TypeNode childType = n[0].getTypeOrNull();
182 [ - + ]: 1499 : if (!childType.isInstantiatedDatatype())
183 : : {
184 [ - - ]: 0 : if (errOut)
185 : : {
186 : 0 : (*errOut) << "Datatype type not fully instantiated";
187 : : }
188 : 0 : return TypeNode::null();
189 : : }
190 : : // note that parametric datatype matching does not account for gradual
191 : : // types.
192 [ - + ]: 1499 : if (!m.doMatching(t, childType))
193 : : {
194 [ - - ]: 0 : if (errOut)
195 : : {
196 : : (*errOut) << "matching failed for selector argument of parameterized "
197 : 0 : "datatype";
198 : : }
199 : 0 : return TypeNode::null();
200 : : }
201 : 1499 : std::vector<TypeNode> types, matches;
202 : 1499 : m.getTypes(types);
203 : 1499 : m.getMatches(matches);
204 : 1499 : TypeNode range = selType.getDatatypeSelectorRangeType();
205 : 2998 : range = range.substitute(
206 : 1499 : types.begin(), types.end(), matches.begin(), matches.end());
207 [ + - ]: 2998 : Trace("typecheck-idt") << "Return (selector) " << range << " for " << n
208 [ - + ][ - - ]: 1499 : << " from " << selType.getDatatypeSelectorRangeType()
209 : 1499 : << std::endl;
210 : 1499 : return range;
211 : 1499 : }
212 : : else
213 : : {
214 [ + - ]: 100921 : if (check)
215 : : {
216 [ + - ]: 100921 : Trace("typecheck-idt") << "typecheck sel: " << n << std::endl;
217 [ + - ]: 100921 : Trace("typecheck-idt") << "sel type: " << selType << std::endl;
218 : 100921 : TypeNode childType = n[0].getTypeOrNull();
219 [ - + ]: 100921 : if (!t.isComparableTo(childType))
220 : : {
221 [ - - ]: 0 : Trace("typecheck-idt") << "ERROR: " << t.getKind() << " "
222 : 0 : << childType.getKind() << std::endl;
223 [ - - ]: 0 : if (errOut)
224 : : {
225 : 0 : (*errOut) << "bad type for selector argument";
226 : : }
227 : 0 : return TypeNode::null();
228 : : }
229 [ + - ]: 100921 : }
230 : 100921 : return selType.getDatatypeSelectorRangeType();
231 : : }
232 : 102420 : }
233 : :
234 : 0 : TypeNode DatatypeTesterTypeRule::preComputeType(NodeManager* nm,
235 : : CVC5_UNUSED TNode n)
236 : : {
237 : 0 : return nm->booleanType();
238 : : }
239 : 56803 : TypeNode DatatypeTesterTypeRule::computeType(NodeManager* nodeManager,
240 : : TNode n,
241 : : bool check,
242 : : std::ostream* errOut)
243 : : {
244 [ - + ][ - + ]: 56803 : Assert(n.getKind() == Kind::APPLY_TESTER);
[ - - ]
245 [ + - ]: 56803 : if (check)
246 : : {
247 [ - + ]: 56803 : if (n.getNumChildren() != 1)
248 : : {
249 [ - - ]: 0 : if (errOut)
250 : : {
251 : 0 : (*errOut) << "number of arguments does not match the tester type";
252 : : }
253 : 0 : return TypeNode::null();
254 : : }
255 : 56803 : TypeNode testType = n.getOperator().getTypeOrNull();
256 : 56803 : TypeNode childType = n[0].getTypeOrNull();
257 : 56803 : TypeNode t = testType[0];
258 [ - + ][ - + ]: 56803 : Assert(t.isDatatype());
[ - - ]
259 [ + + ]: 56803 : if (t.isParametricDatatype())
260 : : {
261 [ + - ]: 596 : Trace("typecheck-idt")
262 : 298 : << "typecheck parameterized tester: " << n << std::endl;
263 : 298 : TypeMatcher m(t);
264 [ - + ]: 298 : if (!m.doMatching(testType[0], childType))
265 : : {
266 [ - - ]: 0 : if (errOut)
267 : : {
268 : : (*errOut) << "matching failed for tester argument of parameterized "
269 : 0 : "datatype";
270 : : }
271 : 0 : return TypeNode::null();
272 : : }
273 [ + - ]: 298 : }
274 : : else
275 : : {
276 [ + - ]: 56505 : Trace("typecheck-idt") << "typecheck test: " << n << std::endl;
277 [ + - ]: 56505 : Trace("typecheck-idt") << "test type: " << testType << std::endl;
278 [ - + ]: 56505 : if (testType[0] != childType)
279 : : {
280 [ - - ]: 0 : if (errOut)
281 : : {
282 : 0 : (*errOut) << "bad type for tester argument";
283 : : }
284 : 0 : return TypeNode::null();
285 : : }
286 : : }
287 [ + - ][ + - ]: 56803 : }
[ + - ]
288 : 56803 : return nodeManager->booleanType();
289 : : }
290 : :
291 : 0 : TypeNode DatatypeUpdateTypeRule::preComputeType(CVC5_UNUSED NodeManager* nm,
292 : : CVC5_UNUSED TNode n)
293 : : {
294 : 0 : return TypeNode::null();
295 : : }
296 : 186 : TypeNode DatatypeUpdateTypeRule::computeType(
297 : : CVC5_UNUSED NodeManager* nodeManager,
298 : : TNode n,
299 : : bool check,
300 : : std::ostream* errOut)
301 : : {
302 [ - + ][ - + ]: 186 : Assert(n.getKind() == Kind::APPLY_UPDATER);
[ - - ]
303 : 186 : TypeNode updType = n.getOperator().getTypeOrNull();
304 [ - + ][ - + ]: 186 : Assert(updType.getNumChildren() == 2);
[ - - ]
305 [ + - ]: 186 : if (check)
306 : : {
307 : 186 : TypeNode t = updType[0];
308 [ + + ]: 555 : for (size_t i = 0; i < 2; i++)
309 : : {
310 : 372 : TypeNode childType = n[i].getTypeOrNull();
311 : 372 : TypeNode targ = updType[i];
312 [ + - ]: 744 : Trace("typecheck-idt") << "typecheck update: " << n << "[" << i
313 : 372 : << "]: " << targ << " " << childType << std::endl;
314 [ + + ]: 372 : if (t.isParametricDatatype())
315 : : {
316 : 42 : TypeMatcher m(t);
317 [ - + ]: 42 : if (!m.doMatching(targ, childType))
318 : : {
319 [ - - ]: 0 : if (errOut)
320 : : {
321 : : (*errOut) << "matching failed for update argument of parameterized "
322 : 0 : "datatype";
323 : : }
324 : 0 : return TypeNode::null();
325 : : }
326 [ + - ]: 42 : }
327 [ + + ]: 330 : else if (targ != childType)
328 : : {
329 [ + + ]: 3 : if (errOut)
330 : : {
331 : 1 : (*errOut) << "bad type for update argument";
332 : : }
333 : 3 : return TypeNode::null();
334 : : }
335 [ + + ][ + + ]: 375 : }
336 [ + + ]: 186 : }
337 : : // type is the first argument
338 : 183 : return n[0].getTypeOrNull();
339 : 186 : }
340 : :
341 : 0 : TypeNode DatatypeAscriptionTypeRule::preComputeType(CVC5_UNUSED NodeManager* nm,
342 : : TNode n)
343 : : {
344 : 0 : return n.getOperator().getConst<AscriptionType>().getType();
345 : : }
346 : 228 : TypeNode DatatypeAscriptionTypeRule::computeType(
347 : : CVC5_UNUSED NodeManager* nodeManager,
348 : : TNode n,
349 : : bool check,
350 : : std::ostream* errOut)
351 : : {
352 [ + - ]: 228 : Trace("typecheck-idt") << "typechecking ascription: " << n << std::endl;
353 [ - + ][ - + ]: 228 : Assert(n.getKind() == Kind::APPLY_TYPE_ASCRIPTION);
[ - - ]
354 : 228 : TypeNode t = n.getOperator().getConst<AscriptionType>().getType();
355 [ + - ]: 228 : if (check)
356 : : {
357 : 228 : TypeNode childType = n[0].getTypeOrNull();
358 : :
359 : 228 : TypeMatcher m;
360 [ + - ]: 228 : if (childType.getKind() == Kind::CONSTRUCTOR_TYPE)
361 : : {
362 : 228 : m.addTypesFromDatatype(childType.getDatatypeConstructorRangeType());
363 : : }
364 [ - - ]: 0 : else if (childType.isDatatype())
365 : : {
366 : 0 : m.addTypesFromDatatype(childType);
367 : : }
368 [ - + ]: 228 : if (!m.doMatching(childType, t))
369 : : {
370 [ - - ]: 0 : if (errOut)
371 : : {
372 : : (*errOut) << "matching failed for type ascription argument of "
373 : 0 : "parameterized datatype";
374 : : }
375 : 0 : return TypeNode::null();
376 : : }
377 [ + - ][ + - ]: 228 : }
378 : 228 : return t;
379 : 228 : }
380 : :
381 : 1 : Cardinality ConstructorProperties::computeCardinality(TypeNode type)
382 : : {
383 : : // Constructors aren't exactly functions, they're like
384 : : // parameterized ground terms. So the cardinality is more like
385 : : // that of a tuple than that of a function.
386 [ - + ]: 1 : AssertArgument(type.isDatatypeConstructor(), type);
387 : 1 : Cardinality c = 1;
388 [ - + ]: 1 : for (unsigned i = 0, i_end = type.getNumChildren(); i < i_end - 1; ++i)
389 : : {
390 : 0 : c *= type[i].getCardinality();
391 : : }
392 : 1 : return c;
393 : 0 : }
394 : :
395 : 0 : TypeNode DtSizeTypeRule::preComputeType(NodeManager* nm, CVC5_UNUSED TNode n)
396 : : {
397 : 0 : return nm->integerType();
398 : : }
399 : 22645 : TypeNode DtSizeTypeRule::computeType(NodeManager* nodeManager,
400 : : TNode n,
401 : : bool check,
402 : : std::ostream* errOut)
403 : : {
404 [ + - ]: 22645 : if (check)
405 : : {
406 : 22645 : TypeNode t = n[0].getTypeOrNull();
407 [ - + ]: 22645 : if (!t.isDatatype())
408 : : {
409 [ - - ]: 0 : if (errOut)
410 : : {
411 : 0 : (*errOut) << "expecting datatype size term to have datatype argument.";
412 : : }
413 : 0 : return TypeNode::null();
414 : : }
415 [ + - ]: 22645 : }
416 : 22645 : return nodeManager->integerType();
417 : : }
418 : :
419 : 0 : TypeNode DtBoundTypeRule::preComputeType(NodeManager* nm, CVC5_UNUSED TNode n)
420 : : {
421 : 0 : return nm->booleanType();
422 : : }
423 : 1747 : TypeNode DtBoundTypeRule::computeType(NodeManager* nodeManager,
424 : : TNode n,
425 : : bool check,
426 : : std::ostream* errOut)
427 : : {
428 [ + - ]: 1747 : if (check)
429 : : {
430 : 1747 : TypeNode t = n[0].getTypeOrNull();
431 [ - + ]: 1747 : if (!t.isDatatype())
432 : : {
433 [ - - ]: 0 : if (errOut)
434 : : {
435 : 0 : (*errOut) << "expecting datatype bound term to have datatype argument.";
436 : : }
437 : 0 : return TypeNode::null();
438 : : }
439 : 1747 : if (!n[1].isConst() || !n[1].getTypeOrNull().isInteger())
440 : : {
441 [ - - ]: 0 : if (errOut)
442 : : {
443 : 0 : (*errOut) << "datatype bound must be a constant integer";
444 : : }
445 : 0 : return TypeNode::null();
446 : : }
447 [ - + ]: 1747 : if (n[1].getConst<Rational>().getNumerator().sgn() == -1)
448 : : {
449 [ - - ]: 0 : if (errOut)
450 : : {
451 : 0 : (*errOut) << "datatype bound must be non-negative";
452 : : }
453 : 0 : return TypeNode::null();
454 : : }
455 [ + - ]: 1747 : }
456 : 1747 : return nodeManager->booleanType();
457 : : }
458 : :
459 : 0 : TypeNode DtSygusEvalTypeRule::preComputeType(CVC5_UNUSED NodeManager* nm,
460 : : CVC5_UNUSED TNode n)
461 : : {
462 : 0 : return TypeNode::null();
463 : : }
464 : 141048 : TypeNode DtSygusEvalTypeRule::computeType(CVC5_UNUSED NodeManager* nodeManager,
465 : : TNode n,
466 : : bool check,
467 : : std::ostream* errOut)
468 : : {
469 : 141048 : TypeNode headType = n[0].getTypeOrNull();
470 [ - + ]: 141048 : if (!headType.isDatatype())
471 : : {
472 [ - - ]: 0 : if (errOut)
473 : : {
474 : 0 : (*errOut) << "datatype sygus eval takes a datatype head";
475 : : }
476 : 0 : return TypeNode::null();
477 : : }
478 : 141048 : const DType& dt = headType.getDType();
479 [ - + ]: 141048 : if (!dt.isSygus())
480 : : {
481 [ - - ]: 0 : if (errOut)
482 : : {
483 : : (*errOut)
484 : 0 : << "datatype sygus eval must have a datatype head that is sygus";
485 : : }
486 : 0 : return TypeNode::null();
487 : : }
488 [ + - ]: 141048 : if (check)
489 : : {
490 : 141048 : Node svl = dt.getSygusVarList();
491 [ - + ]: 141048 : if (svl.getNumChildren() + 1 != n.getNumChildren())
492 : : {
493 [ - - ]: 0 : if (errOut)
494 : : {
495 : : (*errOut) << "wrong number of arguments to a datatype sygus evaluation "
496 : 0 : "function";
497 : : }
498 : 0 : return TypeNode::null();
499 : : }
500 [ + + ]: 676738 : for (unsigned i = 0, nvars = svl.getNumChildren(); i < nvars; i++)
501 : : {
502 : 535690 : TypeNode vtype = svl[i].getTypeOrNull();
503 : 535690 : TypeNode atype = n[i + 1].getTypeOrNull();
504 [ - + ]: 535690 : if (vtype != atype)
505 : : {
506 [ - - ]: 0 : if (errOut)
507 : : {
508 : : (*errOut) << "argument type mismatch in a datatype sygus evaluation "
509 : 0 : "function";
510 : : }
511 : 0 : return TypeNode::null();
512 : : }
513 [ + - ][ + - ]: 535690 : }
514 [ + - ]: 141048 : }
515 : 141048 : return dt.getSygusType();
516 : 141048 : }
517 : :
518 : 0 : TypeNode MatchTypeRule::preComputeType(CVC5_UNUSED NodeManager* nm,
519 : : CVC5_UNUSED TNode n)
520 : : {
521 : 0 : return TypeNode::null();
522 : : }
523 : 231 : TypeNode MatchTypeRule::computeType(CVC5_UNUSED NodeManager* nodeManager,
524 : : TNode n,
525 : : CVC5_UNUSED bool check,
526 : : std::ostream* errOut)
527 : : {
528 [ - + ][ - + ]: 231 : Assert(n.getKind() == Kind::MATCH);
[ - - ]
529 : :
530 : 231 : TypeNode retType;
531 : :
532 : 231 : TypeNode headType = n[0].getTypeOrNull();
533 [ - + ]: 231 : if (!headType.isDatatype())
534 : : {
535 [ - - ]: 0 : if (errOut)
536 : : {
537 : 0 : (*errOut) << "expecting datatype head in match";
538 : : }
539 : 0 : return TypeNode::null();
540 : : }
541 : 231 : const DType& hdt = headType.getDType();
542 : :
543 : 231 : std::unordered_set<unsigned> patIndices;
544 : 231 : bool patHasVariable = false;
545 : : // the type of a match case list is the least common type of its cases
546 [ + + ]: 749 : for (unsigned i = 1, nchildren = n.getNumChildren(); i < nchildren; i++)
547 : : {
548 : 520 : Node nc = n[i];
549 : 520 : Kind nck = nc.getKind();
550 : 520 : std::unordered_set<Node> bvs;
551 [ + + ]: 520 : if (nck == Kind::MATCH_BIND_CASE)
552 : : {
553 [ + + ]: 663 : for (const Node& v : nc[0])
554 : : {
555 [ - + ][ - + ]: 385 : Assert(v.getKind() == Kind::BOUND_VARIABLE);
[ - - ]
556 : 385 : bvs.insert(v);
557 : 663 : }
558 : : }
559 [ - + ]: 242 : else if (nck != Kind::MATCH_CASE)
560 : : {
561 [ - - ]: 0 : if (errOut)
562 : : {
563 : 0 : (*errOut) << "expected a match case in match expression";
564 : : }
565 : 0 : return TypeNode::null();
566 : : }
567 : : // get the pattern type
568 : 520 : uint32_t pindex = nck == Kind::MATCH_CASE ? 0 : 1;
569 : 520 : TypeNode patType = nc[pindex].getTypeOrNull();
570 : : // should be caught in the above call
571 [ - + ]: 520 : if (!patType.isDatatype())
572 : : {
573 [ - - ]: 0 : if (errOut)
574 : : {
575 : 0 : (*errOut) << "expecting datatype pattern in match";
576 : : }
577 : 0 : return TypeNode::null();
578 : : }
579 : 520 : Kind ncpk = nc[pindex].getKind();
580 [ + + ]: 520 : if (ncpk == Kind::APPLY_CONSTRUCTOR)
581 : : {
582 [ + + ]: 869 : for (const Node& arg : nc[pindex])
583 : : {
584 [ - + ]: 367 : if (bvs.find(arg) == bvs.end())
585 : : {
586 [ - - ]: 0 : if (errOut)
587 : : {
588 : : (*errOut) << "expecting distinct bound variable as argument to "
589 : 0 : "constructor in pattern of match";
590 : : }
591 : 0 : return TypeNode::null();
592 : : }
593 : 367 : bvs.erase(arg);
594 [ + - ][ + - ]: 869 : }
595 : 502 : size_t ci = utils::indexOf(nc[pindex].getOperator());
596 : 502 : patIndices.insert(ci);
597 : : }
598 [ + - ]: 18 : else if (ncpk == Kind::BOUND_VARIABLE)
599 : : {
600 : 18 : patHasVariable = true;
601 : : }
602 : : else
603 : : {
604 [ - - ]: 0 : if (errOut)
605 : : {
606 : 0 : (*errOut) << "unexpected kind of term in pattern in match";
607 : : }
608 : 0 : return TypeNode::null();
609 : : }
610 : 520 : const DType& pdt = patType.getDType();
611 : : // compare datatypes instead of the types to catch parametric case,
612 : : // where the pattern has parametric type.
613 [ - + ]: 1560 : if (!CVC5_EQUAL(hdt.getTypeNode(), pdt.getTypeNode()))
614 : : {
615 [ - - ]: 0 : if (errOut)
616 : : {
617 : : (*errOut)
618 : 0 : << "pattern of a match case does not match the head type in match";
619 : : }
620 : 0 : return TypeNode::null();
621 : : }
622 : 520 : TypeNode currType = nc.getTypeOrNull();
623 [ + + ]: 520 : if (i == 1)
624 : : {
625 : 231 : retType = currType;
626 : : }
627 [ + + ]: 289 : else if (retType != currType)
628 : : {
629 : 2 : std::stringstream ss;
630 : 2 : ss << "incomparable types in match case list" << std::endl;
631 : 2 : ss << nc[1] << ": " << currType << std::endl;
632 : 2 : ss << "expected: " << retType << std::endl;
633 : 2 : throw TypeCheckingExceptionPrivate(n, ss.str());
634 : 2 : }
635 [ + - ][ + - ]: 526 : }
[ + - ]
636 : : // it is mandatory to check this here to ensure the match is exhaustive
637 [ + + ][ - + ]: 229 : if (!patHasVariable && patIndices.size() < hdt.getNumConstructors())
[ - + ]
638 : : {
639 [ - - ]: 0 : if (errOut)
640 : : {
641 : 0 : (*errOut) << "cases for match term are not exhaustive";
642 : : }
643 : 0 : return TypeNode::null();
644 : : }
645 : 229 : return retType;
646 : 235 : }
647 : :
648 : 0 : TypeNode MatchCaseTypeRule::preComputeType(CVC5_UNUSED NodeManager* nm,
649 : : CVC5_UNUSED TNode n)
650 : : {
651 : 0 : return TypeNode::null();
652 : : }
653 : 207 : TypeNode MatchCaseTypeRule::computeType(CVC5_UNUSED NodeManager* nodeManager,
654 : : TNode n,
655 : : bool check,
656 : : std::ostream* errOut)
657 : : {
658 [ - + ][ - + ]: 207 : Assert(n.getKind() == Kind::MATCH_CASE);
[ - - ]
659 [ + - ]: 207 : if (check)
660 : : {
661 : 207 : TypeNode patType = n[0].getTypeOrNull();
662 [ - + ]: 207 : if (!patType.isDatatype())
663 : : {
664 [ - - ]: 0 : if (errOut)
665 : : {
666 : 0 : (*errOut) << "expecting datatype pattern in match case";
667 : : }
668 : 0 : return TypeNode::null();
669 : : }
670 [ + - ]: 207 : }
671 : 207 : return n[1].getTypeOrNull();
672 : : }
673 : :
674 : 0 : TypeNode MatchBindCaseTypeRule::preComputeType(CVC5_UNUSED NodeManager* nm,
675 : : CVC5_UNUSED TNode n)
676 : : {
677 : 0 : return TypeNode::null();
678 : : }
679 : 237 : TypeNode MatchBindCaseTypeRule::computeType(
680 : : CVC5_UNUSED NodeManager* nodeManager,
681 : : TNode n,
682 : : bool check,
683 : : std::ostream* errOut)
684 : : {
685 [ - + ][ - + ]: 237 : Assert(n.getKind() == Kind::MATCH_BIND_CASE);
[ - - ]
686 [ + - ]: 237 : if (check)
687 : : {
688 [ - + ]: 237 : if (n[0].getKind() != Kind::BOUND_VAR_LIST)
689 : : {
690 [ - - ]: 0 : if (errOut)
691 : : {
692 : 0 : (*errOut) << "expected a bound variable list in match bind case";
693 : : }
694 : 0 : return TypeNode::null();
695 : : }
696 : 237 : TypeNode patType = n[1].getTypeOrNull();
697 [ - + ]: 237 : if (!patType.isDatatype())
698 : : {
699 [ - - ]: 0 : if (errOut)
700 : : {
701 : 0 : (*errOut) << "expecting datatype pattern in match bind case";
702 : : }
703 : 0 : return TypeNode::null();
704 : : }
705 [ + - ]: 237 : }
706 : 237 : return n[2].getTypeOrNull();
707 : : }
708 : :
709 : 0 : TypeNode TupleProjectTypeRule::preComputeType(CVC5_UNUSED NodeManager* nm,
710 : : CVC5_UNUSED TNode n)
711 : : {
712 : 0 : return TypeNode::null();
713 : : }
714 : :
715 : 149 : TypeNode TupleProjectTypeRule::computeType(CVC5_UNUSED NodeManager* nm,
716 : : TNode n,
717 : : bool check,
718 : : std::ostream* errOut)
719 : : {
720 : 149 : Assert(n.getKind() == Kind::TUPLE_PROJECT && n.hasOperator()
721 : : && n.getOperator().getKind() == Kind::TUPLE_PROJECT_OP);
722 : 149 : ProjectOp op = n.getOperator().getConst<ProjectOp>();
723 : 149 : const std::vector<uint32_t>& indices = op.getIndices();
724 [ + - ]: 149 : if (check)
725 : : {
726 [ - + ]: 149 : if (n.getNumChildren() != 1)
727 : : {
728 [ - - ]: 0 : if (errOut)
729 : : {
730 : 0 : (*errOut) << "operands in term " << n << " are " << n.getNumChildren()
731 : 0 : << ", but TUPLE_PROJECT expects 1 operand.";
732 : : }
733 : 12 : return TypeNode::null();
734 : : }
735 : 149 : TypeNode tupleType = n[0].getTypeOrNull();
736 [ - + ]: 149 : if (!tupleType.isMaybeKind(Kind::TUPLE_TYPE))
737 : : {
738 [ - - ]: 0 : if (errOut)
739 : : {
740 : 0 : (*errOut) << "TUPLE_PROJECT expects a tuple for " << n[0] << ". Found"
741 : 0 : << tupleType;
742 : : }
743 : 0 : return TypeNode::null();
744 : : }
745 : :
746 : : // check indicies if we are a concrete tuple
747 [ + - ]: 149 : if (tupleType.isTuple())
748 : : {
749 : : // make sure all indices are less than the length of the tuple type
750 : 149 : const DType& dType = tupleType.getDType();
751 : 149 : DTypeConstructor constructor = dType[0];
752 : 149 : size_t numArgs = constructor.getNumArgs();
753 [ + + ]: 587 : for (uint32_t index : indices)
754 : : {
755 [ + + ]: 450 : if (index >= numArgs)
756 : : {
757 [ + + ]: 12 : if (errOut)
758 : : {
759 : 8 : (*errOut) << "Project index " << index << " in term " << n
760 : 4 : << " is >= " << numArgs
761 : 4 : << " which is the length of tuple " << n[0] << std::endl;
762 : : }
763 : 12 : return TypeNode::null();
764 : : }
765 : : }
766 [ + + ]: 149 : }
767 [ + + ]: 149 : }
768 : 137 : TypeNode tupleType = n[0].getTypeOrNull();
769 : 137 : return TupleUtils::getTupleProjectionType(indices, tupleType);
770 : 149 : }
771 : :
772 : 0 : TypeNode CodatatypeBoundVariableTypeRule::preComputeType(
773 : : CVC5_UNUSED NodeManager* nm, CVC5_UNUSED TNode n)
774 : : {
775 : 0 : return TypeNode::null();
776 : : }
777 : 135 : TypeNode CodatatypeBoundVariableTypeRule::computeType(
778 : : CVC5_UNUSED NodeManager* nodeManager,
779 : : TNode n,
780 : : CVC5_UNUSED bool check,
781 : : CVC5_UNUSED std::ostream* errOut)
782 : : {
783 : 135 : return n.getConst<CodatatypeBoundVariable>().getType();
784 : : }
785 : :
786 : 0 : TypeNode NullableLiftTypeRule::preComputeType(CVC5_UNUSED NodeManager* nm,
787 : : CVC5_UNUSED TNode n)
788 : : {
789 : 0 : return TypeNode::null();
790 : : }
791 : :
792 : 178 : TypeNode NullableLiftTypeRule::computeType(NodeManager* nodeManager,
793 : : TNode n,
794 : : bool check,
795 : : CVC5_UNUSED std::ostream* errOut)
796 : : {
797 [ - + ][ - + ]: 178 : Assert(n.getKind() == Kind::NULLABLE_LIFT);
[ - - ]
798 [ + - ]: 178 : if (check)
799 : : {
800 : 178 : std::vector<TypeNode> argTypes;
801 : 178 : TypeNode functionType = n[0].getType(check);
802 [ - + ]: 178 : if (!functionType.isFunction())
803 : : {
804 : 0 : std::stringstream ss;
805 : 0 : ss << "Argument 0 '" << n[0] << "' in term " << n << " has type '"
806 : 0 : << functionType << "' which is not a function type.";
807 : 0 : throw TypeCheckingExceptionPrivate(n, ss.str());
808 : 0 : }
809 : 178 : std::vector<TypeNode> funArgTypes = functionType.getArgTypes();
810 [ + + ]: 534 : for (size_t i = 1; i < n.getNumChildren(); i++)
811 : : {
812 : 356 : TypeNode argType = n[i].getType(check);
813 [ - + ]: 356 : if (!argType.isNullable())
814 : : {
815 : 0 : std::stringstream ss;
816 : 0 : ss << "Argument " << i << " '" << n[i] << "' in term " << n
817 : 0 : << " has type '" << argType << "' which is not a nullable type.";
818 : 0 : throw TypeCheckingExceptionPrivate(n, ss.str());
819 : 0 : }
820 : 356 : TypeNode elementType = argType[0];
821 [ - + ]: 356 : if (funArgTypes[i - 1] != elementType)
822 : : {
823 : 0 : std::stringstream ss;
824 : 0 : ss << "Argument " << (i - 1) << " in function '" << n[0] << " has type "
825 : 0 : << funArgTypes[i - 1] << ". Expected '" << n[i] << "' to have type "
826 : 0 : << nodeManager->mkNullableType(funArgTypes[i - 1]) << " instead of "
827 : 0 : << argType;
828 : 0 : throw TypeCheckingExceptionPrivate(n, ss.str());
829 : 0 : }
830 : 356 : }
831 : 178 : }
832 : 356 : return nodeManager->mkNullableType(n[0].getType().getRangeType());
833 : : }
834 : :
835 : : } // namespace datatypes
836 : : } // namespace theory
837 : : } // namespace cvc5::internal
|
