GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/type_node.cpp Lines: 284 334 85.0 %
Date: 2021-03-22 Branches: 430 1120 38.4 %

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