GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/type_node.cpp Lines: 281 331 84.9 %
Date: 2021-03-23 Branches: 426 1116 38.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file type_node.cpp
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 Reference-counted encapsulation of a pointer to node information.
13
 **
14
 ** Reference-counted encapsulation of a pointer to node information.
15
 **/
16
#include "expr/type_node.h"
17
18
#include <vector>
19
20
#include "expr/node_manager_attributes.h"
21
#include "expr/type_properties.h"
22
#include "options/base_options.h"
23
#include "options/quantifiers_options.h"
24
#include "theory/type_enumerator.h"
25
26
using namespace std;
27
28
namespace CVC4 {
29
30
8895
TypeNode TypeNode::s_null( &expr::NodeValue::null() );
31
32
2
TypeNode TypeNode::substitute(const TypeNode& type,
33
                              const TypeNode& replacement,
34
                              std::unordered_map<TypeNode, TypeNode, HashFunction>& cache) const {
35
  // in cache?
36
2
  std::unordered_map<TypeNode, TypeNode, HashFunction>::const_iterator i = cache.find(*this);
37
2
  if(i != cache.end()) {
38
    return (*i).second;
39
  }
40
41
  // otherwise compute
42
4
  NodeBuilder<> nb(getKind());
43
2
  if(getMetaKind() == kind::metakind::PARAMETERIZED) {
44
    // push the operator
45
    nb << TypeNode(d_nv->d_children[0]);
46
  }
47
6
  for (TypeNode::const_iterator j = begin(), iend = end(); j != iend; ++j)
48
  {
49
4
    if (*j == type)
50
    {
51
4
      nb << replacement;
52
    }
53
    else
54
    {
55
      (*j).substitute(type, replacement);
56
    }
57
  }
58
59
  // put in cache
60
4
  TypeNode tn = nb.constructTypeNode();
61
2
  cache[*this] = tn;
62
2
  return tn;
63
}
64
65
16950
Cardinality TypeNode::getCardinality() const {
66
16950
  return kind::getCardinality(*this);
67
}
68
69
/** Attribute true for types that are finite */
70
struct IsFiniteTag
71
{
72
};
73
typedef expr::Attribute<IsFiniteTag, bool> IsFiniteAttr;
74
/** Attribute true for types which we have computed the above attribute */
75
struct IsFiniteComputedTag
76
{
77
};
78
typedef expr::Attribute<IsFiniteComputedTag, bool> IsFiniteComputedAttr;
79
80
/** Attribute true for types that are interpreted as finite */
81
struct IsInterpretedFiniteTag
82
{
83
};
84
typedef expr::Attribute<IsInterpretedFiniteTag, bool> IsInterpretedFiniteAttr;
85
/** Attribute true for types which we have computed the above attribute */
86
struct IsInterpretedFiniteComputedTag
87
{
88
};
89
typedef expr::Attribute<IsInterpretedFiniteComputedTag, bool>
90
    IsInterpretedFiniteComputedAttr;
91
92
7270
bool TypeNode::isFinite() { return isFiniteInternal(false); }
93
94
6371857
bool TypeNode::isInterpretedFinite()
95
{
96
6371857
  return isFiniteInternal(options::finiteModelFind());
97
}
98
99
6381420
bool TypeNode::isFiniteInternal(bool usortFinite)
100
{
101
  // check it is already cached
102
6381420
  if (usortFinite)
103
  {
104
194494
    if (getAttribute(IsInterpretedFiniteComputedAttr()))
105
    {
106
193621
      return getAttribute(IsInterpretedFiniteAttr());
107
    }
108
  }
109
6186926
  else if (getAttribute(IsFiniteComputedAttr()))
110
  {
111
6172570
    return getAttribute(IsFiniteAttr());
112
  }
113
15229
  bool ret = false;
114
15229
  if (isSort())
115
  {
116
2010
    ret = usortFinite;
117
  }
118
39421
  else if (isBoolean() || isBitVector() || isFloatingPoint()
119
21751
           || isRoundingMode())
120
  {
121
4702
    ret = true;
122
  }
123
8517
  else if (isString() || isRegExp() || isSequence() || isReal())
124
  {
125
4303
    ret = false;
126
  }
127
  else
128
  {
129
    // recursive case (this may be a parametric sort), we assume infinite for
130
    // the moment here to prevent infinite loops
131
4214
    if (usortFinite)
132
    {
133
293
      setAttribute(IsInterpretedFiniteAttr(), false);
134
293
      setAttribute(IsInterpretedFiniteComputedAttr(), true);
135
    }
136
    else
137
    {
138
3921
      setAttribute(IsFiniteAttr(), false);
139
3921
      setAttribute(IsFiniteComputedAttr(), true);
140
    }
141
4214
    if (isDatatype())
142
    {
143
4644
      TypeNode tn = *this;
144
2322
      const DType& dt = getDType();
145
2322
      ret = usortFinite ? dt.isInterpretedFinite(tn) : dt.isFinite(tn);
146
    }
147
1892
    else if (isArray())
148
    {
149
916
      TypeNode tnc = getArrayConstituentType();
150
458
      if (!tnc.isFiniteInternal(usortFinite))
151
      {
152
        // arrays with constituent type that is infinite are infinite
153
204
        ret = false;
154
      }
155
254
      else if (getArrayIndexType().isFiniteInternal(usortFinite))
156
      {
157
        // arrays with both finite constituent and index types are finite
158
245
        ret = true;
159
      }
160
      else
161
      {
162
        // If the consistuent type of the array has cardinality one, then the
163
        // array type has cardinality one, independent of the index type.
164
9
        ret = tnc.getCardinality().isOne();
165
      }
166
    }
167
1434
    else if (isSet())
168
    {
169
914
      ret = getSetElementType().isFiniteInternal(usortFinite);
170
    }
171
520
    else if (isBag())
172
    {
173
      // there are infinite bags for all element types
174
29
      ret = false;
175
    }
176
491
    else if (isFunction())
177
    {
178
491
      ret = true;
179
982
      TypeNode tnr = getRangeType();
180
491
      if (!tnr.isFiniteInternal(usortFinite))
181
      {
182
336
        ret = false;
183
      }
184
      else
185
      {
186
310
        std::vector<TypeNode> argTypes = getArgTypes();
187
222
        for (unsigned i = 0, nargs = argTypes.size(); i < nargs; i++)
188
        {
189
176
          if (!argTypes[i].isFiniteInternal(usortFinite))
190
          {
191
109
            ret = false;
192
109
            break;
193
          }
194
        }
195
155
        if (!ret)
196
        {
197
          // similar to arrays, functions are finite if their range type
198
          // has cardinality one, regardless of the arguments.
199
109
          ret = tnr.getCardinality().isOne();
200
        }
201
      }
202
    }
203
    else
204
    {
205
      // all types should be handled above
206
      Assert(false);
207
      // by default, compute the exact cardinality for the type and check
208
      // whether it is finite. This should be avoided in general, since
209
      // computing cardinalities for types can be highly expensive.
210
      ret = getCardinality().isFinite();
211
    }
212
  }
213
15229
  if (usortFinite)
214
  {
215
873
    setAttribute(IsInterpretedFiniteAttr(), ret);
216
873
    setAttribute(IsInterpretedFiniteComputedAttr(), true);
217
  }
218
  else
219
  {
220
14356
    setAttribute(IsFiniteAttr(), ret);
221
14356
    setAttribute(IsFiniteComputedAttr(), true);
222
  }
223
15229
  return ret;
224
}
225
226
/** Attribute true for types that are closed enumerable */
227
struct IsClosedEnumerableTag
228
{
229
};
230
struct IsClosedEnumerableComputedTag
231
{
232
};
233
typedef expr::Attribute<IsClosedEnumerableTag, bool> IsClosedEnumerableAttr;
234
typedef expr::Attribute<IsClosedEnumerableComputedTag, bool>
235
    IsClosedEnumerableComputedAttr;
236
237
79905
bool TypeNode::isClosedEnumerable()
238
{
239
  // check it is already cached
240
79905
  if (!getAttribute(IsClosedEnumerableComputedAttr()))
241
  {
242
2077
    bool ret = true;
243
2077
    if (isArray() || isSort() || isCodatatype() || isFunction())
244
    {
245
467
      ret = false;
246
    }
247
1610
    else if (isSet())
248
    {
249
9
      ret = getSetElementType().isClosedEnumerable();
250
    }
251
1601
    else if (isSequence())
252
    {
253
3
      ret = getSequenceElementType().isClosedEnumerable();
254
    }
255
1598
    else if (isDatatype())
256
    {
257
      // avoid infinite loops: initially set to true
258
320
      setAttribute(IsClosedEnumerableAttr(), ret);
259
320
      setAttribute(IsClosedEnumerableComputedAttr(), true);
260
640
      TypeNode tn = *this;
261
320
      const DType& dt = getDType();
262
765
      for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
263
      {
264
1097
        for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
265
        {
266
1141
          TypeNode ctn = dt[i][j].getRangeType();
267
652
          if (tn != ctn && !ctn.isClosedEnumerable())
268
          {
269
163
            ret = false;
270
163
            break;
271
          }
272
        }
273
608
        if (!ret)
274
        {
275
163
          break;
276
        }
277
      }
278
    }
279
2077
    setAttribute(IsClosedEnumerableAttr(), ret);
280
2077
    setAttribute(IsClosedEnumerableComputedAttr(), true);
281
2077
    return ret;
282
  }
283
77828
  return getAttribute(IsClosedEnumerableAttr());
284
}
285
286
1266642
bool TypeNode::isFirstClass() const {
287
2533284
  return getKind() != kind::CONSTRUCTOR_TYPE && getKind() != kind::SELECTOR_TYPE
288
1266642
         && getKind() != kind::TESTER_TYPE && getKind() != kind::SEXPR_TYPE
289
3799004
         && (getKind() != kind::TYPE_CONSTANT
290
1734694
             || getConst<TypeConstant>() != REGEXP_TYPE);
291
}
292
293
bool TypeNode::isWellFounded() const {
294
  return kind::isWellFounded(*this);
295
}
296
297
156151
Node TypeNode::mkGroundTerm() const {
298
156151
  return kind::mkGroundTerm(*this);
299
}
300
301
156742
Node TypeNode::mkGroundValue() const
302
{
303
313484
  theory::TypeEnumerator te(*this);
304
313484
  return *te;
305
}
306
307
3067106
bool TypeNode::isStringLike() const { return isString() || isSequence(); }
308
309
10140425
bool TypeNode::isSubtypeOf(TypeNode t) const {
310
10140425
  if(*this == t) {
311
9357634
    return true;
312
  }
313
782791
  if(getKind() == kind::TYPE_CONSTANT) {
314
234321
    switch(getConst<TypeConstant>()) {
315
179618
    case INTEGER_TYPE:
316
179618
      return t.getKind() == kind::TYPE_CONSTANT && t.getConst<TypeConstant>() == REAL_TYPE;
317
54703
    default:
318
54703
      return false;
319
    }
320
  }
321
548470
  if (isFunction() && t.isFunction())
322
  {
323
    if (!isComparableTo(t))
324
    {
325
      // incomparable, not subtype
326
      return false;
327
    }
328
    return getRangeType().isSubtypeOf(t.getRangeType());
329
  }
330
  // this should only return true for types T1, T2 where we handle equalities between T1 and T2
331
  // (more cases go here, if we want to support such cases)
332
548470
  return false;
333
}
334
335
8339226
bool TypeNode::isComparableTo(TypeNode t) const {
336
8339226
  if(*this == t) {
337
8321672
    return true;
338
  }
339
17554
  if(isSubtypeOf(NodeManager::currentNM()->realType())) {
340
15323
    return t.isSubtypeOf(NodeManager::currentNM()->realType());
341
  }
342
2231
  if (isFunction() && t.isFunction())
343
  {
344
    // comparable if they have a common type node
345
1
    return !leastCommonTypeNode(*this, t).isNull();
346
  }
347
2230
  return false;
348
}
349
350
14
TypeNode TypeNode::getTesterDomainType() const
351
{
352
14
  Assert(isTester());
353
14
  return (*this)[0];
354
}
355
356
10101
TypeNode TypeNode::getSequenceElementType() const
357
{
358
10101
  Assert(isSequence());
359
10101
  return (*this)[0];
360
}
361
362
770249
TypeNode TypeNode::getBaseType() const {
363
1540498
  TypeNode realt = NodeManager::currentNM()->realType();
364
770249
  if (isSubtypeOf(realt)) {
365
174008
    return realt;
366
596241
  } else if (isParametricDatatype()) {
367
1920
    std::vector<TypeNode> v;
368
2135
    for(size_t i = 1; i < getNumChildren(); ++i) {
369
1175
      v.push_back((*this)[i].getBaseType());
370
    }
371
960
    return (*this)[0].getDType().getTypeNode().instantiateParametricDatatype(v);
372
  }
373
595281
  return *this;
374
}
375
376
11911
std::vector<TypeNode> TypeNode::getArgTypes() const {
377
11911
  vector<TypeNode> args;
378
11911
  if(isTester()) {
379
    Assert(getNumChildren() == 1);
380
    args.push_back((*this)[0]);
381
  } else {
382
11911
    Assert(isFunction() || isConstructor() || isSelector());
383
33465
    for(unsigned i = 0, i_end = getNumChildren() - 1; i < i_end; ++i) {
384
21554
      args.push_back((*this)[i]);
385
    }
386
  }
387
11911
  return args;
388
}
389
390
2014
std::vector<TypeNode> TypeNode::getParamTypes() const {
391
2014
  vector<TypeNode> params;
392
2014
  Assert(isParametricDatatype());
393
4548
  for(unsigned i = 1, i_end = getNumChildren(); i < i_end; ++i) {
394
2534
    params.push_back((*this)[i]);
395
  }
396
2014
  return params;
397
}
398
399
112270
bool TypeNode::isTuple() const
400
{
401
112270
  return (getKind() == kind::DATATYPE_TYPE && getDType().isTuple());
402
}
403
404
177
bool TypeNode::isRecord() const
405
{
406
177
  return (getKind() == kind::DATATYPE_TYPE && getDType().isRecord());
407
}
408
409
32813
size_t TypeNode::getTupleLength() const {
410
32813
  Assert(isTuple());
411
32813
  const DType& dt = getDType();
412
32813
  Assert(dt.getNumConstructors() == 1);
413
32813
  return dt[0].getNumArgs();
414
}
415
416
14918
vector<TypeNode> TypeNode::getTupleTypes() const {
417
14918
  Assert(isTuple());
418
14918
  const DType& dt = getDType();
419
14918
  Assert(dt.getNumConstructors() == 1);
420
14918
  vector<TypeNode> types;
421
44846
  for(unsigned i = 0; i < dt[0].getNumArgs(); ++i) {
422
29928
    types.push_back(dt[0][i].getRangeType());
423
  }
424
14918
  return types;
425
}
426
427
vector<TypeNode> TypeNode::getSExprTypes() const {
428
  Assert(isSExpr());
429
  vector<TypeNode> types;
430
  for(unsigned i = 0, i_end = getNumChildren(); i < i_end; ++i) {
431
    types.push_back((*this)[i]);
432
  }
433
  return types;
434
}
435
436
/** Is this an instantiated datatype type */
437
1237
bool TypeNode::isInstantiatedDatatype() const {
438
1237
  if(getKind() == kind::DATATYPE_TYPE) {
439
716
    return true;
440
  }
441
521
  if(getKind() != kind::PARAMETRIC_DATATYPE) {
442
    return false;
443
  }
444
521
  const DType& dt = (*this)[0].getDType();
445
521
  unsigned n = dt.getNumParameters();
446
521
  Assert(n < getNumChildren());
447
1234
  for(unsigned i = 0; i < n; ++i) {
448
713
    if (dt.getParameter(i) == (*this)[i + 1])
449
    {
450
      return false;
451
    }
452
  }
453
521
  return true;
454
}
455
456
1606
TypeNode TypeNode::instantiateParametricDatatype(
457
    const std::vector<TypeNode>& params) const
458
{
459
1606
  AssertArgument(getKind() == kind::PARAMETRIC_DATATYPE, *this);
460
1606
  AssertArgument(params.size() == getNumChildren() - 1, *this);
461
1606
  NodeManager* nm = NodeManager::currentNM();
462
3212
  TypeNode cons = nm->mkTypeConst((*this)[0].getConst<DatatypeIndexConstant>());
463
3212
  std::vector<TypeNode> paramsNodes;
464
1606
  paramsNodes.push_back(cons);
465
3610
  for (const TypeNode& t : params)
466
  {
467
2004
    paramsNodes.push_back(t);
468
  }
469
3212
  return nm->mkTypeNode(kind::PARAMETRIC_DATATYPE, paramsNodes);
470
}
471
472
53
uint64_t TypeNode::getSortConstructorArity() const
473
{
474
53
  Assert(isSortConstructor() && hasAttribute(expr::SortArityAttr()));
475
53
  return getAttribute(expr::SortArityAttr());
476
}
477
478
4
std::string TypeNode::getName() const
479
{
480
4
  Assert(isSort() || isSortConstructor());
481
4
  return getAttribute(expr::VarNameAttr());
482
}
483
484
49
TypeNode TypeNode::instantiateSortConstructor(
485
    const std::vector<TypeNode>& params) const
486
{
487
49
  Assert(isSortConstructor());
488
49
  return NodeManager::currentNM()->mkSort(*this, params);
489
}
490
491
/** Is this an instantiated datatype parameter */
492
2340
bool TypeNode::isParameterInstantiatedDatatype(unsigned n) const {
493
2340
  AssertArgument(getKind() == kind::PARAMETRIC_DATATYPE, *this);
494
2340
  const DType& dt = (*this)[0].getDType();
495
2340
  AssertArgument(n < dt.getNumParameters(), *this);
496
2340
  return dt.getParameter(n) != (*this)[n + 1];
497
}
498
499
6763815
TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){
500
6763815
  return commonTypeNode( t0, t1, true );
501
}
502
503
136623
TypeNode TypeNode::mostCommonTypeNode(TypeNode t0, TypeNode t1){
504
136623
  return commonTypeNode( t0, t1, false );
505
}
506
507
6900462
TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) {
508
6900462
  Assert(NodeManager::currentNM() != NULL)
509
      << "There is no current CVC4::NodeManager associated to this thread.\n"
510
         "Perhaps a public-facing function is missing a NodeManagerScope ?";
511
512
6900462
  Assert(!t0.isNull());
513
6900462
  Assert(!t1.isNull());
514
515
6900462
  if(__builtin_expect( (t0 == t1), true )) {
516
6855254
    return t0;
517
  }
518
519
  // t0 != t1 &&
520
45208
  if(t0.getKind() == kind::TYPE_CONSTANT) {
521
45154
    switch(t0.getConst<TypeConstant>()) {
522
13265
    case INTEGER_TYPE:
523
13265
      if(t1.isInteger()) {
524
        // t0 == IntegerType && t1.isInteger()
525
        return t0; //IntegerType
526
13265
      } else if(t1.isReal()) {
527
        // t0 == IntegerType && t1.isReal() && !t1.isInteger()
528
13233
        return isLeast ? t1 : t0; // RealType
529
      } else {
530
32
        return TypeNode(); // null type
531
      }
532
31829
    case REAL_TYPE:
533
31829
      if(t1.isReal()) {
534
31829
        return isLeast ? t0 : t1; // RealType
535
      } else {
536
        return TypeNode(); // null type
537
      }
538
60
    default:
539
60
      return TypeNode(); // null type
540
    }
541
54
  } else if(t1.getKind() == kind::TYPE_CONSTANT) {
542
22
    return commonTypeNode(t1, t0, isLeast); // decrease the number of special cases
543
  }
544
545
  // t0 != t1 &&
546
  // t0.getKind() == kind::TYPE_CONSTANT &&
547
  // t1.getKind() == kind::TYPE_CONSTANT
548
32
  switch(t0.getKind()) {
549
8
    case kind::FUNCTION_TYPE:
550
    {
551
8
      if (t1.getKind() != kind::FUNCTION_TYPE)
552
      {
553
4
        return TypeNode();
554
      }
555
      // must have equal arguments
556
8
      std::vector<TypeNode> t0a = t0.getArgTypes();
557
8
      std::vector<TypeNode> t1a = t1.getArgTypes();
558
4
      if (t0a.size() != t1a.size())
559
      {
560
        // different arities
561
        return TypeNode();
562
      }
563
6
      for (unsigned i = 0, nargs = t0a.size(); i < nargs; i++)
564
      {
565
4
        if (t0a[i] != t1a[i])
566
        {
567
          // an argument is different
568
2
          return TypeNode();
569
        }
570
      }
571
4
      TypeNode t0r = t0.getRangeType();
572
4
      TypeNode t1r = t1.getRangeType();
573
4
      TypeNode tr = commonTypeNode(t0r, t1r, isLeast);
574
4
      std::vector<TypeNode> ftypes;
575
2
      ftypes.insert(ftypes.end(), t0a.begin(), t0a.end());
576
2
      ftypes.push_back(tr);
577
2
      return NodeManager::currentNM()->mkFunctionType(ftypes);
578
    }
579
    break;
580
24
    case kind::BITVECTOR_TYPE:
581
    case kind::FLOATINGPOINT_TYPE:
582
    case kind::SORT_TYPE:
583
    case kind::CONSTRUCTOR_TYPE:
584
    case kind::SELECTOR_TYPE:
585
    case kind::TESTER_TYPE:
586
    case kind::ARRAY_TYPE:
587
    case kind::DATATYPE_TYPE:
588
    case kind::PARAMETRIC_DATATYPE:
589
    case kind::SEQUENCE_TYPE:
590
    case kind::SET_TYPE:
591
    case kind::BAG_TYPE:
592
    case kind::SEXPR_TYPE:
593
    {
594
      // we don't support subtyping except for built in types Int and Real.
595
24
      return TypeNode();  // return null type
596
    }
597
    default:
598
      Unimplemented() << "don't have a commonType for types `" << t0
599
                      << "' and `" << t1 << "'";
600
  }
601
}
602
603
26
Node TypeNode::getEnsureTypeCondition( Node n, TypeNode tn ) {
604
52
  TypeNode ntn = n.getType();
605
26
  Assert(ntn.isComparableTo(tn));
606
26
  if( !ntn.isSubtypeOf( tn ) ){
607
    if( tn.isInteger() ){
608
      if( tn.isSubtypeOf( ntn ) ){
609
        return NodeManager::currentNM()->mkNode( kind::IS_INTEGER, n );
610
      }
611
    }else if( tn.isDatatype() && ntn.isDatatype() ){
612
      if( tn.isTuple() && ntn.isTuple() ){
613
        const DType& dt1 = tn.getDType();
614
        const DType& dt2 = ntn.getDType();
615
        NodeManager* nm = NodeManager::currentNM();
616
        if( dt1[0].getNumArgs()==dt2[0].getNumArgs() ){
617
          std::vector< Node > conds;
618
          for( unsigned i=0; i<dt2[0].getNumArgs(); i++ ){
619
            Node s = nm->mkNode(
620
                kind::APPLY_SELECTOR_TOTAL, dt2[0][i].getSelector(), n);
621
            Node etc = getEnsureTypeCondition(s, dt1[0][i].getRangeType());
622
            if( etc.isNull() ){
623
              return Node::null();
624
            }else{
625
              conds.push_back( etc );
626
            }
627
          }
628
          if( conds.empty() ){
629
            return nm->mkConst(true);
630
          }else if( conds.size()==1 ){
631
            return conds[0];
632
          }else{
633
            return nm->mkNode(kind::AND, conds);
634
          }
635
        }
636
      }
637
    }
638
    return Node::null();
639
  }else{
640
26
    return NodeManager::currentNM()->mkConst( true );
641
  }
642
}
643
644
/** Is this a sort kind */
645
1689212
bool TypeNode::isSort() const {
646
1689212
  return ( getKind() == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr()) );
647
}
648
649
/** Is this a sort constructor kind */
650
1455
bool TypeNode::isSortConstructor() const {
651
1455
  return getKind() == kind::SORT_TYPE && hasAttribute(expr::SortArityAttr());
652
}
653
654
/** Is this a codatatype type */
655
691351
bool TypeNode::isCodatatype() const
656
{
657
691351
  if (isDatatype())
658
  {
659
690057
    return getDType().isCodatatype();
660
  }
661
1294
  return false;
662
}
663
664
294
bool TypeNode::isSygusDatatype() const
665
{
666
294
  if (isDatatype())
667
  {
668
    return getDType().isSygus();
669
  }
670
294
  return false;
671
}
672
673
3195
std::string TypeNode::toString() const {
674
6390
  std::stringstream ss;
675
3195
  OutputLanguage outlang = (this == &s_null) ? language::output::LANG_AUTO : options::outputLanguage();
676
3195
  d_nv->toStream(ss, -1, 0, outlang);
677
6390
  return ss.str();
678
}
679
680
5917559
const DType& TypeNode::getDType() const
681
{
682
5917559
  if (getKind() == kind::DATATYPE_TYPE)
683
  {
684
5911839
    DatatypeIndexConstant dic = getConst<DatatypeIndexConstant>();
685
5911839
    return NodeManager::currentNM()->getDTypeForIndex(dic.getIndex());
686
  }
687
5720
  Assert(getKind() == kind::PARAMETRIC_DATATYPE);
688
5720
  return (*this)[0].getDType();
689
}
690
691
32424
bool TypeNode::isBag() const
692
{
693
32424
  return getKind() == kind::BAG_TYPE;
694
}
695
696
2797
TypeNode TypeNode::getBagElementType() const
697
{
698
2797
  Assert(isBag());
699
2797
  return (*this)[0];
700
}
701
702
26685
}/* CVC4 namespace */