GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/datatypes/theory_datatypes_type_rules.h Lines: 231 298 77.5 %
Date: 2021-03-22 Branches: 447 1416 31.6 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_datatypes_type_rules.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Morgan Deters, Tim King
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 Theory of datatypes
13
 **
14
 ** Theory of datatypes.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H
20
#define CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H
21
22
#include "expr/dtype.h"
23
#include "expr/dtype_cons.h"
24
#include "expr/type_matcher.h"
25
#include "theory/datatypes/theory_datatypes_utils.h"
26
27
namespace CVC4 {
28
namespace theory {
29
namespace datatypes {
30
31
struct DatatypeConstructorTypeRule {
32
135000
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
33
                                     bool check) {
34
135000
    Assert(n.getKind() == kind::APPLY_CONSTRUCTOR);
35
270000
    TypeNode consType = n.getOperator().getType(check);
36
270000
    TypeNode t = consType.getConstructorRangeType();
37
135000
    Assert(t.isDatatype());
38
135000
    TNode::iterator child_it = n.begin();
39
135000
    TNode::iterator child_it_end = n.end();
40
135000
    TypeNode::iterator tchild_it = consType.begin();
41
404589
    if ((t.isParametricDatatype() || check)
42
270000
        && n.getNumChildren() != consType.getNumChildren() - 1)
43
    {
44
      throw TypeCheckingExceptionPrivate(
45
6
          n, "number of arguments does not match the constructor type");
46
    }
47
134994
    if (t.isParametricDatatype())
48
    {
49
814
      Debug("typecheck-idt") << "typecheck parameterized datatype " << n
50
407
                             << std::endl;
51
814
      TypeMatcher m(t);
52
1721
      for (; child_it != child_it_end; ++child_it, ++tchild_it) {
53
1314
        TypeNode childType = (*child_it).getType(check);
54
657
        if (!m.doMatching(*tchild_it, childType)) {
55
          throw TypeCheckingExceptionPrivate(
56
              n, "matching failed for parameterized constructor");
57
        }
58
      }
59
814
      std::vector<TypeNode> instTypes;
60
407
      m.getMatches(instTypes);
61
814
      TypeNode range = t.instantiateParametricDatatype(instTypes);
62
407
      Debug("typecheck-idt") << "Return " << range << std::endl;
63
407
      return range;
64
    }
65
    else
66
    {
67
134587
      if (check) {
68
269174
        Debug("typecheck-idt") << "typecheck cons: " << n << " "
69
134587
                               << n.getNumChildren() << std::endl;
70
269174
        Debug("typecheck-idt") << "cons type: " << consType << " "
71
134587
                               << consType.getNumChildren() << std::endl;
72
651185
        for (; child_it != child_it_end; ++child_it, ++tchild_it) {
73
516598
          TypeNode childType = (*child_it).getType(check);
74
516598
          Debug("typecheck-idt") << "typecheck cons arg: " << childType << " "
75
258299
                                 << (*tchild_it) << std::endl;
76
516598
          TypeNode argumentType = *tchild_it;
77
258299
          if (!childType.isSubtypeOf(argumentType)) {
78
            std::stringstream ss;
79
            ss << "bad type for constructor argument:\n"
80
               << "child type:  " << childType << "\n"
81
               << "not subtype: " << argumentType << "\n"
82
               << "in term : " << n;
83
            throw TypeCheckingExceptionPrivate(n, ss.str());
84
          }
85
        }
86
      }
87
134587
      return consType.getConstructorRangeType();
88
    }
89
  }
90
91
118089
  inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
92
118089
    Assert(n.getKind() == kind::APPLY_CONSTRUCTOR);
93
236178
    NodeManagerScope nms(nodeManager);
94
276800
    for (TNode::const_iterator i = n.begin(); i != n.end(); ++i) {
95
197525
      if (!(*i).isConst()) {
96
38814
        return false;
97
      }
98
    }
99
79275
    return true;
100
  }
101
}; /* struct DatatypeConstructorTypeRule */
102
103
struct DatatypeSelectorTypeRule {
104
60138
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
105
                                     bool check) {
106
60138
    Assert(n.getKind() == kind::APPLY_SELECTOR
107
           || n.getKind() == kind::APPLY_SELECTOR_TOTAL);
108
120276
    TypeNode selType = n.getOperator().getType(check);
109
120276
    TypeNode t = selType[0];
110
60138
    Assert(t.isDatatype());
111
60138
    if ((t.isParametricDatatype() || check) && n.getNumChildren() != 1)
112
    {
113
      throw TypeCheckingExceptionPrivate(
114
          n, "number of arguments does not match the selector type");
115
    }
116
60138
    if (t.isParametricDatatype())
117
    {
118
1042
      Debug("typecheck-idt") << "typecheck parameterized sel: " << n
119
521
                             << std::endl;
120
1042
      TypeMatcher m(t);
121
1042
      TypeNode childType = n[0].getType(check);
122
521
      if (!childType.isInstantiatedDatatype()) {
123
        throw TypeCheckingExceptionPrivate(
124
            n, "Datatype type not fully instantiated");
125
      }
126
521
      if (!m.doMatching(selType[0], childType)) {
127
        throw TypeCheckingExceptionPrivate(
128
            n,
129
            "matching failed for selector argument of parameterized datatype");
130
      }
131
1042
      std::vector<TypeNode> types, matches;
132
521
      m.getTypes(types);
133
521
      m.getMatches(matches);
134
1042
      TypeNode range = selType[1];
135
521
      range = range.substitute(
136
          types.begin(), types.end(), matches.begin(), matches.end());
137
521
      Debug("typecheck-idt") << "Return " << range << std::endl;
138
521
      return range;
139
    }
140
    else
141
    {
142
59617
      if (check) {
143
59617
        Debug("typecheck-idt") << "typecheck sel: " << n << std::endl;
144
59617
        Debug("typecheck-idt") << "sel type: " << selType << std::endl;
145
119234
        TypeNode childType = n[0].getType(check);
146
59617
        if (!selType[0].isComparableTo(childType)) {
147
          Debug("typecheck-idt") << "ERROR: " << selType[0].getKind() << " "
148
                                 << childType.getKind() << std::endl;
149
          throw TypeCheckingExceptionPrivate(n,
150
                                             "bad type for selector argument");
151
        }
152
      }
153
59617
      return selType[1];
154
    }
155
  }
156
}; /* struct DatatypeSelectorTypeRule */
157
158
struct DatatypeTesterTypeRule {
159
31194
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
160
                                     bool check) {
161
31194
    Assert(n.getKind() == kind::APPLY_TESTER);
162
31194
    if (check) {
163
31194
      if (n.getNumChildren() != 1) {
164
        throw TypeCheckingExceptionPrivate(
165
            n, "number of arguments does not match the tester type");
166
      }
167
62388
      TypeNode testType = n.getOperator().getType(check);
168
62388
      TypeNode childType = n[0].getType(check);
169
62388
      TypeNode t = testType[0];
170
31194
      Assert(t.isDatatype());
171
31194
      if (t.isParametricDatatype())
172
      {
173
230
        Debug("typecheck-idt") << "typecheck parameterized tester: " << n
174
115
                               << std::endl;
175
230
        TypeMatcher m(t);
176
115
        if (!m.doMatching(testType[0], childType)) {
177
          throw TypeCheckingExceptionPrivate(
178
              n,
179
              "matching failed for tester argument of parameterized datatype");
180
        }
181
      }
182
      else
183
      {
184
31079
        Debug("typecheck-idt") << "typecheck test: " << n << std::endl;
185
31079
        Debug("typecheck-idt") << "test type: " << testType << std::endl;
186
31079
        if (!testType[0].isComparableTo(childType)) {
187
          throw TypeCheckingExceptionPrivate(n, "bad type for tester argument");
188
        }
189
      }
190
    }
191
31194
    return nodeManager->booleanType();
192
  }
193
}; /* struct DatatypeTesterTypeRule */
194
195
struct DatatypeAscriptionTypeRule {
196
102
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
197
                                     bool check) {
198
102
    Debug("typecheck-idt") << "typechecking ascription: " << n << std::endl;
199
102
    Assert(n.getKind() == kind::APPLY_TYPE_ASCRIPTION);
200
102
    TypeNode t = n.getOperator().getConst<AscriptionType>().getType();
201
102
    if (check) {
202
204
      TypeNode childType = n[0].getType(check);
203
204
204
      TypeMatcher m;
205
102
      if (childType.getKind() == kind::CONSTRUCTOR_TYPE) {
206
94
        m.addTypesFromDatatype(childType.getConstructorRangeType());
207
8
      } else if (childType.getKind() == kind::DATATYPE_TYPE) {
208
        m.addTypesFromDatatype(childType);
209
      }
210
102
      if (!m.doMatching(childType, t)) {
211
        throw TypeCheckingExceptionPrivate(n,
212
                                           "matching failed for type "
213
                                           "ascription argument of "
214
                                           "parameterized datatype");
215
      }
216
    }
217
102
    return t;
218
  }
219
}; /* struct DatatypeAscriptionTypeRule */
220
221
struct ConstructorProperties {
222
2
  inline static Cardinality computeCardinality(TypeNode type) {
223
    // Constructors aren't exactly functions, they're like
224
    // parameterized ground terms.  So the cardinality is more like
225
    // that of a tuple than that of a function.
226
2
    AssertArgument(type.isConstructor(), type);
227
2
    Cardinality c = 1;
228
2
    for (unsigned i = 0, i_end = type.getNumChildren(); i < i_end - 1; ++i) {
229
      c *= type[i].getCardinality();
230
    }
231
2
    return c;
232
  }
233
}; /* struct ConstructorProperties */
234
235
struct TupleUpdateTypeRule {
236
2
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
237
                                     bool check) {
238
2
    Assert(n.getKind() == kind::TUPLE_UPDATE);
239
2
    const TupleUpdate& tu = n.getOperator().getConst<TupleUpdate>();
240
2
    TypeNode tupleType = n[0].getType(check);
241
4
    TypeNode newValue = n[1].getType(check);
242
2
    if (check) {
243
2
      if (!tupleType.isTuple()) {
244
        throw TypeCheckingExceptionPrivate(
245
            n, "Tuple-update expression formed over non-tuple");
246
      }
247
2
      if (tu.getIndex() >= tupleType.getTupleLength()) {
248
        std::stringstream ss;
249
        ss << "Tuple-update expression index `" << tu.getIndex()
250
           << "' is not a valid index; tuple type only has "
251
           << tupleType.getTupleLength() << " fields";
252
        throw TypeCheckingExceptionPrivate(n, ss.str().c_str());
253
      }
254
    }
255
4
    return tupleType;
256
  }
257
}; /* struct TupleUpdateTypeRule */
258
259
class TupleUpdateOpTypeRule
260
{
261
 public:
262
3
  inline static TypeNode computeType(NodeManager* nodeManager,
263
                                     TNode n,
264
                                     bool check)
265
  {
266
3
    Assert(n.getKind() == kind::TUPLE_UPDATE_OP);
267
3
    return nodeManager->builtinOperatorType();
268
  }
269
}; /* class TupleUpdateOpTypeRule */
270
271
struct RecordUpdateTypeRule {
272
8
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
273
                                     bool check) {
274
8
    Assert(n.getKind() == kind::RECORD_UPDATE);
275
16
    NodeManagerScope nms(nodeManager);
276
8
    const RecordUpdate& ru = n.getOperator().getConst<RecordUpdate>();
277
8
    TypeNode recordType = n[0].getType(check);
278
16
    TypeNode newValue = n[1].getType(check);
279
8
    if (check) {
280
8
      if (!recordType.isRecord())
281
      {
282
        throw TypeCheckingExceptionPrivate(
283
            n, "Record-update expression formed over non-record");
284
      }
285
8
      const DType& dt = recordType.getDType();
286
8
      const DTypeConstructor& recCons = dt[0];
287
8
      if (recCons.getSelectorIndexForName(ru.getField()) == -1)
288
      {
289
        std::stringstream ss;
290
        ss << "Record-update field `" << ru.getField()
291
           << "' is not a valid field name for the record type";
292
        throw TypeCheckingExceptionPrivate(n, ss.str().c_str());
293
      }
294
    }
295
16
    return recordType;
296
  }
297
}; /* struct RecordUpdateTypeRule */
298
299
class RecordUpdateOpTypeRule
300
{
301
 public:
302
9
  inline static TypeNode computeType(NodeManager* nodeManager,
303
                                     TNode n,
304
                                     bool check)
305
  {
306
9
    Assert(n.getKind() == kind::RECORD_UPDATE_OP);
307
9
    return nodeManager->builtinOperatorType();
308
  }
309
}; /* class RecordUpdateOpTypeRule */
310
311
class DtSizeTypeRule {
312
 public:
313
17493
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
314
                                     bool check) {
315
17493
    if (check) {
316
34986
      TypeNode t = n[0].getType(check);
317
17493
      if (!t.isDatatype()) {
318
        throw TypeCheckingExceptionPrivate(
319
            n, "expecting datatype size term to have datatype argument.");
320
      }
321
    }
322
17493
    return nodeManager->integerType();
323
  }
324
}; /* class DtSizeTypeRule */
325
326
class DtBoundTypeRule {
327
 public:
328
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
329
                                     bool check) {
330
    if (check) {
331
      TypeNode t = n[0].getType(check);
332
      if (!t.isDatatype()) {
333
        throw TypeCheckingExceptionPrivate(
334
            n,
335
            "expecting datatype bound term to have datatype argument.");
336
      }
337
      if (n[1].getKind() != kind::CONST_RATIONAL) {
338
        throw TypeCheckingExceptionPrivate(
339
            n, "datatype bound must be a constant");
340
      }
341
      if (n[1].getConst<Rational>().getNumerator().sgn() == -1) {
342
        throw TypeCheckingExceptionPrivate(
343
            n, "datatype bound must be non-negative");
344
      }
345
    }
346
    return nodeManager->booleanType();
347
  }
348
}; /* class DtBoundTypeRule */
349
350
class DtSygusBoundTypeRule {
351
 public:
352
761
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
353
                                     bool check) {
354
761
    if (check) {
355
761
      if (!n[0].getType().isDatatype()) {
356
        throw TypeCheckingExceptionPrivate(
357
            n, "datatype sygus bound takes a datatype");
358
      }
359
761
      if (n[1].getKind() != kind::CONST_RATIONAL) {
360
        throw TypeCheckingExceptionPrivate(
361
            n, "datatype sygus bound must be a constant");
362
      }
363
761
      if (n[1].getConst<Rational>().getNumerator().sgn() == -1) {
364
        throw TypeCheckingExceptionPrivate(
365
            n, "datatype sygus bound must be non-negative");
366
      }
367
    }
368
761
    return nodeManager->booleanType();
369
  }
370
}; /* class DtSygusBoundTypeRule */
371
372
class DtSyguEvalTypeRule
373
{
374
 public:
375
123244
  inline static TypeNode computeType(NodeManager* nodeManager,
376
                                     TNode n,
377
                                     bool check)
378
  {
379
246488
    TypeNode headType = n[0].getType(check);
380
123244
    if (!headType.isDatatype())
381
    {
382
      throw TypeCheckingExceptionPrivate(
383
          n, "datatype sygus eval takes a datatype head");
384
    }
385
123244
    const DType& dt = headType.getDType();
386
123244
    if (!dt.isSygus())
387
    {
388
      throw TypeCheckingExceptionPrivate(
389
          n, "datatype sygus eval must have a datatype head that is sygus");
390
    }
391
123244
    if (check)
392
    {
393
246488
      Node svl = dt.getSygusVarList();
394
123244
      if (svl.getNumChildren() + 1 != n.getNumChildren())
395
      {
396
        throw TypeCheckingExceptionPrivate(n,
397
                                           "wrong number of arguments to a "
398
                                           "datatype sygus evaluation "
399
                                           "function");
400
      }
401
901482
      for (unsigned i = 0, nvars = svl.getNumChildren(); i < nvars; i++)
402
      {
403
1556476
        TypeNode vtype = svl[i].getType(check);
404
1556476
        TypeNode atype = n[i + 1].getType(check);
405
778238
        if (!vtype.isComparableTo(atype))
406
        {
407
          throw TypeCheckingExceptionPrivate(
408
              n,
409
              "argument type mismatch in a datatype sygus evaluation function");
410
        }
411
      }
412
    }
413
246488
    return dt.getSygusType();
414
  }
415
}; /* class DtSyguEvalTypeRule */
416
417
class MatchTypeRule
418
{
419
 public:
420
20
  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
421
  {
422
20
    Assert(n.getKind() == kind::MATCH);
423
424
20
    TypeNode retType;
425
426
40
    TypeNode headType = n[0].getType(check);
427
20
    if (!headType.isDatatype())
428
    {
429
      throw TypeCheckingExceptionPrivate(n, "expecting datatype head in match");
430
    }
431
20
    const DType& hdt = headType.getDType();
432
433
40
    std::unordered_set<unsigned> patIndices;
434
20
    bool patHasVariable = false;
435
    // the type of a match case list is the least common type of its cases
436
71
    for (unsigned i = 1, nchildren = n.getNumChildren(); i < nchildren; i++)
437
    {
438
102
      Node nc = n[i];
439
51
      if (check)
440
      {
441
51
        Kind nck = nc.getKind();
442
102
        std::unordered_set<Node, NodeHashFunction> bvs;
443
51
        if (nck == kind::MATCH_BIND_CASE)
444
        {
445
48
          for (const Node& v : nc[0])
446
          {
447
31
            Assert(v.getKind() == kind::BOUND_VARIABLE);
448
31
            bvs.insert(v);
449
          }
450
        }
451
34
        else if (nck != kind::MATCH_CASE)
452
        {
453
          throw TypeCheckingExceptionPrivate(
454
              n, "expected a match case in match expression");
455
        }
456
        // get the pattern type
457
51
        unsigned pindex = nck == kind::MATCH_CASE ? 0 : 1;
458
102
        TypeNode patType = nc[pindex].getType();
459
        // should be caught in the above call
460
51
        if (!patType.isDatatype())
461
        {
462
          throw TypeCheckingExceptionPrivate(
463
              n, "expecting datatype pattern in match");
464
        }
465
51
        Kind ncpk = nc[pindex].getKind();
466
51
        if (ncpk == kind::APPLY_CONSTRUCTOR)
467
        {
468
76
          for (const Node& arg : nc[pindex])
469
          {
470
28
            if (bvs.find(arg) == bvs.end())
471
            {
472
              throw TypeCheckingExceptionPrivate(
473
                  n,
474
                  "expecting distinct bound variable as argument to "
475
                  "constructor in pattern of match");
476
            }
477
28
            bvs.erase(arg);
478
          }
479
48
          unsigned ci = utils::indexOf(nc[pindex].getOperator());
480
48
          patIndices.insert(ci);
481
        }
482
3
        else if (ncpk == kind::BOUND_VARIABLE)
483
        {
484
3
          patHasVariable = true;
485
        }
486
        else
487
        {
488
          throw TypeCheckingExceptionPrivate(
489
              n, "unexpected kind of term in pattern in match");
490
        }
491
51
        const DType& pdt = patType.getDType();
492
        // compare datatypes instead of the types to catch parametric case,
493
        // where the pattern has parametric type.
494
51
        if (hdt.getTypeNode() != pdt.getTypeNode())
495
        {
496
          std::stringstream ss;
497
          ss << "pattern of a match case does not match the head type in match";
498
          throw TypeCheckingExceptionPrivate(n, ss.str());
499
        }
500
      }
501
102
      TypeNode currType = nc.getType(check);
502
51
      if (i == 1)
503
      {
504
20
        retType = currType;
505
      }
506
      else
507
      {
508
31
        retType = TypeNode::leastCommonTypeNode(retType, currType);
509
31
        if (retType.isNull())
510
        {
511
          throw TypeCheckingExceptionPrivate(
512
              n, "incomparable types in match case list");
513
        }
514
      }
515
    }
516
20
    if (check)
517
    {
518
20
      if (!patHasVariable && patIndices.size() < hdt.getNumConstructors())
519
      {
520
        throw TypeCheckingExceptionPrivate(
521
            n, "cases for match term are not exhaustive");
522
      }
523
    }
524
40
    return retType;
525
  }
526
}; /* class MatchTypeRule */
527
528
class MatchCaseTypeRule
529
{
530
 public:
531
34
  inline static TypeNode computeType(NodeManager* nodeManager,
532
                                     TNode n,
533
                                     bool check)
534
  {
535
34
    Assert(n.getKind() == kind::MATCH_CASE);
536
34
    if (check)
537
    {
538
68
      TypeNode patType = n[0].getType(check);
539
34
      if (!patType.isDatatype())
540
      {
541
        throw TypeCheckingExceptionPrivate(
542
            n, "expecting datatype pattern in match case");
543
      }
544
    }
545
34
    return n[1].getType(check);
546
  }
547
}; /* class MatchCaseTypeRule */
548
549
class MatchBindCaseTypeRule
550
{
551
 public:
552
15
  inline static TypeNode computeType(NodeManager* nodeManager,
553
                                     TNode n,
554
                                     bool check)
555
  {
556
15
    Assert(n.getKind() == kind::MATCH_BIND_CASE);
557
15
    if (check)
558
    {
559
15
      if (n[0].getKind() != kind::BOUND_VAR_LIST)
560
      {
561
        throw TypeCheckingExceptionPrivate(
562
            n, "expected a bound variable list in match bind case");
563
      }
564
30
      TypeNode patType = n[1].getType(check);
565
15
      if (!patType.isDatatype())
566
      {
567
        throw TypeCheckingExceptionPrivate(
568
            n, "expecting datatype pattern in match bind case");
569
      }
570
    }
571
15
    return n[2].getType(check);
572
  }
573
}; /* class MatchBindCaseTypeRule */
574
575
class TupleProjectTypeRule
576
{
577
 public:
578
18
  static TypeNode computeType(NodeManager* nm, TNode n, bool check)
579
  {
580
18
    Assert(n.getKind() == kind::TUPLE_PROJECT && n.hasOperator()
581
           && n.getOperator().getKind() == kind::TUPLE_PROJECT_OP);
582
36
    TupleProjectOp op = n.getOperator().getConst<TupleProjectOp>();
583
18
    const std::vector<uint32_t>& indices = op.getIndices();
584
18
    if (check)
585
    {
586
18
      if (n.getNumChildren() != 1)
587
      {
588
        std::stringstream ss;
589
        ss << "operands in term " << n << " are " << n.getNumChildren()
590
           << ", but TUPLE_PROJECT expects 1 operand.";
591
        throw TypeCheckingExceptionPrivate(n, ss.str());
592
      }
593
36
      TypeNode tupleType = n[0].getType(check);
594
18
      if (!tupleType.isTuple())
595
      {
596
        std::stringstream ss;
597
        ss << "TUPLE_PROJECT expects a tuple for " << n[0] << ". Found" << tupleType;
598
        throw TypeCheckingExceptionPrivate(n, ss.str());
599
      }
600
601
      // make sure all indices are less than the length of the tuple type
602
36
      DType dType = tupleType.getDType();
603
36
      DTypeConstructor constructor = dType[0];
604
18
      size_t numArgs = constructor.getNumArgs();
605
56
      for (uint32_t index : indices)
606
      {
607
84
        std::stringstream ss;
608
42
        if (index >= numArgs)
609
        {
610
8
          ss << "Project index " << index << " in term " << n
611
8
             << " is >= " << numArgs << " which is the length of tuple " << n[0]
612
4
             << std::endl;
613
4
          throw TypeCheckingExceptionPrivate(n, ss.str());
614
        }
615
      }
616
    }
617
28
    TypeNode tupleType = n[0].getType(check);
618
28
    std::vector<TypeNode> types;
619
28
    DType dType = tupleType.getDType();
620
28
    DTypeConstructor constructor = dType[0];
621
50
    for (uint32_t index : indices)
622
    {
623
36
      types.push_back(constructor.getArgType(index));
624
    }
625
28
    return nm->mkTupleType(types);
626
  }
627
}; /* class TupleProjectTypeRule */
628
629
} /* CVC4::theory::datatypes namespace */
630
} /* CVC4::theory namespace */
631
} /* CVC4 namespace */
632
633
#endif /* CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H */