GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/type_node.h Lines: 181 212 85.4 %
Date: 2021-03-23 Branches: 173 827 20.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file type_node.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Morgan Deters, Dejan Jovanovic, Andrew Reynolds
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
17
#include "cvc4_private.h"
18
19
// circular dependency
20
#include "expr/node_value.h"
21
22
#ifndef CVC4__TYPE_NODE_H
23
#define CVC4__TYPE_NODE_H
24
25
#include <iostream>
26
#include <string>
27
#include <unordered_map>
28
#include <vector>
29
30
#include "base/check.h"
31
#include "expr/kind.h"
32
#include "expr/metakind.h"
33
#include "util/cardinality.h"
34
35
namespace CVC4 {
36
37
class NodeManager;
38
class DType;
39
40
namespace expr {
41
  class NodeValue;
42
}/* CVC4::expr namespace */
43
44
/**
45
 * Encapsulation of an NodeValue pointer for Types. The reference count is
46
 * maintained in the NodeValue.
47
 */
48
class TypeNode {
49
50
public:
51
52
  // for hash_maps, hash_sets..
53
  struct HashFunction {
54
3364641
    size_t operator()(TypeNode node) const {
55
3364641
      return (size_t) node.getId();
56
    }
57
  };/* struct HashFunction */
58
59
private:
60
61
  /**
62
   * The NodeValue has access to the private constructors, so that the
63
   * iterators can can create new types.
64
   */
65
  friend class expr::NodeValue;
66
67
  /** A convenient null-valued encapsulated pointer */
68
  static TypeNode s_null;
69
70
  /** The referenced NodeValue */
71
  expr::NodeValue* d_nv;
72
73
  /**
74
   * This constructor is reserved for use by the TypeNode package.
75
   */
76
  explicit TypeNode(const expr::NodeValue*);
77
78
  friend class NodeManager;
79
80
  template <unsigned nchild_thresh>
81
  friend class NodeBuilder;
82
83
  /**
84
   * Assigns the expression value and does reference counting. No
85
   * assumptions are made on the expression, and should only be used
86
   * if we know what we are doing.
87
   *
88
   * @param ev the expression value to assign
89
   */
90
  void assignNodeValue(expr::NodeValue* ev);
91
92
  /**
93
   * Cache-aware, recursive version of substitute() used by the public
94
   * member function with a similar signature.
95
   */
96
  TypeNode substitute(const TypeNode& type, const TypeNode& replacement,
97
                      std::unordered_map<TypeNode, TypeNode, HashFunction>& cache) const;
98
99
  /**
100
   * Cache-aware, recursive version of substitute() used by the public
101
   * member function with a similar signature.
102
   */
103
  template <class Iterator1, class Iterator2>
104
  TypeNode substitute(Iterator1 typesBegin, Iterator1 typesEnd,
105
                      Iterator2 replacementsBegin, Iterator2 replacementsEnd,
106
                      std::unordered_map<TypeNode, TypeNode, HashFunction>& cache) const;
107
108
public:
109
110
  /** Default constructor, makes a null expression. */
111
805206901
  TypeNode() : d_nv(&expr::NodeValue::null()) { }
112
113
  /** Copy constructor */
114
  TypeNode(const TypeNode& node);
115
116
  /**
117
   * Destructor. If ref_count is true it will decrement the reference count
118
   * and, if zero, collect the NodeValue.
119
   */
120
  ~TypeNode();
121
122
  /**
123
   * Assignment operator for nodes, copies the relevant information from node
124
   * to this node.
125
   *
126
   * @param typeNode the node to copy
127
   * @return reference to this node
128
   */
129
  TypeNode& operator=(const TypeNode& typeNode);
130
131
  /**
132
   * Return the null node.
133
   *
134
   * @return the null node
135
   */
136
4146
  static TypeNode null() {
137
4146
    return s_null;
138
  }
139
140
  /**
141
   * Substitution of TypeNodes.
142
   */
143
  inline TypeNode
144
  substitute(const TypeNode& type, const TypeNode& replacement) const;
145
146
  /**
147
   * Simultaneous substitution of TypeNodes.
148
   */
149
  template <class Iterator1, class Iterator2>
150
  inline TypeNode
151
  substitute(Iterator1 typesBegin, Iterator1 typesEnd,
152
             Iterator2 replacementsBegin, Iterator2 replacementsEnd) const;
153
154
  /**
155
   * Structural comparison operator for expressions.
156
   *
157
   * @param typeNode the type node to compare to
158
   * @return true if expressions are equal, false otherwise
159
   */
160
41418626
  bool operator==(const TypeNode& typeNode) const {
161
41418626
    return d_nv == typeNode.d_nv;
162
  }
163
164
  /**
165
   * Structural comparison operator for expressions.
166
   *
167
   * @param typeNode the type node to compare to
168
   * @return true if expressions are equal, false otherwise
169
   */
170
10245688
  bool operator!=(const TypeNode& typeNode) const {
171
10245688
    return !(*this == typeNode);
172
  }
173
174
  /**
175
   * We compare by expression ids so, keeping things deterministic and having
176
   * that subexpressions have to be smaller than the enclosing expressions.
177
   *
178
   * @param typeNode the node to compare to
179
   * @return true if this expression is lesser
180
   */
181
59444802
  inline bool operator<(const TypeNode& typeNode) const {
182
59444802
    return d_nv->d_id < typeNode.d_nv->d_id;
183
  }
184
185
  /**
186
   * We compare by expression ids so, keeping things deterministic and having
187
   * that subexpressions have to be smaller than the enclosing expressions.
188
   *
189
   * @param typeNode the node to compare to
190
   * @return true if this expression is lesser or equal
191
   */
192
4
  inline bool operator<=(const TypeNode& typeNode) const {
193
4
    return d_nv->d_id <= typeNode.d_nv->d_id;
194
  }
195
196
  /**
197
   * We compare by expression ids so, keeping things deterministic and having
198
   * that subexpressions have to be smaller than the enclosing expressions.
199
   *
200
   * @param typeNode the node to compare to
201
   * @return true if this expression is greater
202
   */
203
6
  inline bool operator>(const TypeNode& typeNode) const {
204
6
    return d_nv->d_id > typeNode.d_nv->d_id;
205
  }
206
207
  /**
208
   * We compare by expression ids so, keeping things deterministic and having
209
   * that subexpressions have to be smaller than the enclosing expressions.
210
   *
211
   * @param typeNode the node to compare to
212
   * @return true if this expression is greater or equal
213
   */
214
6
  inline bool operator>=(const TypeNode& typeNode) const {
215
6
    return d_nv->d_id >= typeNode.d_nv->d_id;
216
  }
217
218
  /**
219
   * Returns the i-th child of this node.
220
   *
221
   * @param i the index of the child
222
   * @return the node representing the i-th child
223
   */
224
5306719
  inline TypeNode operator[](int i) const {
225
5306719
    return TypeNode(d_nv->getChild(i));
226
  }
227
228
  /**
229
   * PARAMETERIZED-metakinded types (the SORT_TYPE is one of these)
230
   * have an operator.  "Little-p parameterized" types (like Array),
231
   * are OPERATORs, not PARAMETERIZEDs.
232
   */
233
  inline Node getOperator() const {
234
    Assert(getMetaKind() == kind::metakind::PARAMETERIZED);
235
    return Node(d_nv->getOperator());
236
  }
237
238
  /**
239
   * Returns the unique id of this node
240
   *
241
   * @return the id
242
   */
243
3364646
  inline unsigned long getId() const {
244
3364646
    return d_nv->getId();
245
  }
246
247
  /**
248
   * Returns the kind of this type node.
249
   *
250
   * @return the kind
251
   */
252
447912393
  inline Kind getKind() const {
253
447912393
    return Kind(d_nv->d_kind);
254
  }
255
256
  /**
257
   * Returns the metakind of this type node.
258
   *
259
   * @return the metakind
260
   */
261
1960
  inline kind::MetaKind getMetaKind() const {
262
1960
    return kind::metaKindOf(getKind());
263
  }
264
265
  /**
266
   * Returns the number of children this node has.
267
   *
268
   * @return the number of children
269
   */
270
  inline size_t getNumChildren() const;
271
272
  /**
273
   * If this is a CONST_* TypeNode, extract the constant from it.
274
   */
275
  template <class T>
276
  inline const T& getConst() const;
277
278
  /**
279
   * Returns the value of the given attribute that this has been attached.
280
   *
281
   * @param attKind the kind of the attribute
282
   * @return the value of the attribute
283
   */
284
  template <class AttrKind>
285
  inline typename AttrKind::value_type
286
  getAttribute(const AttrKind& attKind) const;
287
288
  // Note that there are two, distinct hasAttribute() declarations for
289
  // a reason (rather than using a pointer-valued argument with a
290
  // default value): they permit more optimized code in the underlying
291
  // hasAttribute() implementations.
292
293
  /**
294
   * Returns true if this node has been associated an attribute of
295
   * given kind.  Additionally, if a pointer to the value_kind is
296
   * give, and the attribute value has been set for this node, it will
297
   * be returned.
298
   *
299
   * @param attKind the kind of the attribute
300
   * @return true if this node has the requested attribute
301
   */
302
  template <class AttrKind>
303
  inline bool hasAttribute(const AttrKind& attKind) const;
304
305
  /**
306
   * Returns true if this node has been associated an attribute of given kind.
307
   * Additionaly, if a pointer to the value_kind is give, and the attribute
308
   * value has been set for this node, it will be returned.
309
   *
310
   * @param attKind the kind of the attribute
311
   * @param value where to store the value if it exists
312
   * @return true if this node has the requested attribute
313
   */
314
  template <class AttrKind>
315
  inline bool getAttribute(const AttrKind& attKind,
316
                           typename AttrKind::value_type& value) const;
317
318
  /**
319
   * Sets the given attribute of this node to the given value.
320
   *
321
   * @param attKind the kind of the atribute
322
   * @param value the value to set the attribute to
323
   */
324
  template <class AttrKind>
325
  inline void setAttribute(const AttrKind& attKind,
326
                           const typename AttrKind::value_type& value);
327
328
  /** Iterator allowing for scanning through the children. */
329
  typedef expr::NodeValue::iterator<TypeNode> iterator;
330
  /** Constant iterator allowing for scanning through the children. */
331
  typedef expr::NodeValue::iterator<TypeNode> const_iterator;
332
333
  /**
334
   * Returns the iterator pointing to the first child.
335
   *
336
   * @return the iterator
337
   */
338
597880
  inline iterator begin() {
339
597880
    return d_nv->begin<TypeNode>();
340
  }
341
342
  /**
343
   * Returns the iterator pointing to the end of the children (one
344
   * beyond the last one.
345
   *
346
   * @return the end of the children iterator.
347
   */
348
11120
  inline iterator end() {
349
11120
    return d_nv->end<TypeNode>();
350
  }
351
352
  /**
353
   * Returns the const_iterator pointing to the first child.
354
   *
355
   * @return the const_iterator
356
   */
357
1960
  inline const_iterator begin() const {
358
1960
    return d_nv->begin<TypeNode>();
359
  }
360
361
  /**
362
   * Returns the const_iterator pointing to the end of the children
363
   * (one beyond the last one.
364
   *
365
   * @return the end of the children const_iterator.
366
   */
367
1960
  inline const_iterator end() const {
368
1960
    return d_nv->end<TypeNode>();
369
  }
370
371
  /**
372
   * Converts this type into a string representation.
373
   *
374
   * @return the string representation of this type.
375
   */
376
  std::string toString() const;
377
378
  /**
379
   * Converts this node into a string representation and sends it to the
380
   * given stream
381
   *
382
   * @param out the stream to serialize this node to
383
   * @param language the language in which to output
384
   */
385
23475
  inline void toStream(std::ostream& out, OutputLanguage language = language::output::LANG_AUTO) const {
386
23475
    d_nv->toStream(out, -1, 0, language);
387
23475
  }
388
389
  /**
390
   * Very basic pretty printer for Node.
391
   *
392
   * @param out output stream to print to.
393
   * @param indent number of spaces to indent the formula by.
394
   */
395
  void printAst(std::ostream& out, int indent = 0) const;
396
397
  /**
398
   * Returns true if this type is a null type.
399
   *
400
   * @return true if null
401
   */
402
30985703
  bool isNull() const {
403
30985703
    return d_nv == &expr::NodeValue::null();
404
  }
405
406
  /**
407
   * Returns the cardinality of this type.
408
   *
409
   * @return a finite or infinite cardinality
410
   */
411
  Cardinality getCardinality() const;
412
413
  /**
414
   * Is this type finite? This assumes uninterpreted sorts have infinite
415
   * cardinality.
416
   */
417
  bool isFinite();
418
419
  /**
420
   * Is this type interpreted as finite.
421
   * If finite model finding is enabled, this assumes all uninterpreted sorts
422
   *   are interpreted as finite.
423
   */
424
  bool isInterpretedFinite();
425
426
  /** is closed enumerable type
427
   *
428
   * This returns true if this type has an enumerator that produces constants
429
   * that are fully handled by CVC4's quantifier-free theory solvers. Examples
430
   * of types that are not closed enumerable are:
431
   * (1) uninterpreted sorts,
432
   * (2) arrays,
433
   * (3) codatatypes,
434
   * (4) functions,
435
   * (5) parametric sorts involving any of the above.
436
   */
437
  bool isClosedEnumerable();
438
439
  /**
440
   * Is this a first-class type?
441
   * First-class types are types for which:
442
   * (1) we handle equalities between terms of that type, and
443
   * (2) they are allowed to be parameters of parametric types (e.g. index or element types of arrays).
444
   *
445
   * Examples of types that are not first-class include constructor types,
446
   * selector types, tester types, regular expressions and SExprs.
447
   */
448
  bool isFirstClass() const;
449
450
  /**
451
   * Returns whether this type is well-founded.
452
   *
453
   * @return true iff the type is well-founded
454
   */
455
  bool isWellFounded() const;
456
457
  /**
458
   * Construct and return a ground term of this type.  If the type is
459
   * not well founded, this function throws an exception.
460
   *
461
   * @return a ground term of the type
462
   */
463
  Node mkGroundTerm() const;
464
465
  /**
466
   * Construct and return a ground value of this type.  If the type is
467
   * not well founded, this function throws an exception.
468
   *
469
   * @return a ground value of the type
470
   */
471
  Node mkGroundValue() const;
472
473
  /**
474
   * Is this type a subtype of the given type?
475
   */
476
  bool isSubtypeOf(TypeNode t) const;
477
478
  /**
479
   * Is this type comparable to the given type (i.e., do they share
480
   * a common ancestor in the subtype tree)?
481
   */
482
  bool isComparableTo(TypeNode t) const;
483
484
  /** Is this the Boolean type? */
485
  bool isBoolean() const;
486
487
  /** Is this the Integer type? */
488
  bool isInteger() const;
489
490
  /** Is this the Real type? */
491
  bool isReal() const;
492
493
  /** Is this the String type? */
494
  bool isString() const;
495
496
  /** Is this a string-like type? (string or sequence) */
497
  bool isStringLike() const;
498
499
  /** Is this the Rounding Mode type? */
500
  bool isRoundingMode() const;
501
502
  /** Is this an array type? */
503
  bool isArray() const;
504
505
  /** Is this a Set type? */
506
  bool isSet() const;
507
508
  /** Is this a Bag type? */
509
  bool isBag() const;
510
511
  /** Is this a Sequence type? */
512
  bool isSequence() const;
513
514
  /** Get the index type (for array types) */
515
  TypeNode getArrayIndexType() const;
516
517
  /** Get the element type (for array types) */
518
  TypeNode getArrayConstituentType() const;
519
520
  /** Get the return type (for constructor types) */
521
  TypeNode getConstructorRangeType() const;
522
523
  /** Get the domain type (for selector types) */
524
  TypeNode getSelectorDomainType() const;
525
526
  /** Get the return type (for selector types) */
527
  TypeNode getSelectorRangeType() const;
528
529
  /** Get the domain type (for tester types) */
530
  TypeNode getTesterDomainType() const;
531
532
  /** Get the element type (for set types) */
533
  TypeNode getSetElementType() const;
534
535
  /** Get the element type (for bag types) */
536
  TypeNode getBagElementType() const;
537
538
  /** Get the element type (for sequence types) */
539
  TypeNode getSequenceElementType() const;
540
  /**
541
   * Is this a function type?  Function-like things (e.g. datatype
542
   * selectors) that aren't actually functions are NOT considered
543
   * functions, here.
544
   */
545
  bool isFunction() const;
546
547
  /**
548
   * Is this a function-LIKE type?  Function-like things
549
   * (e.g. datatype selectors) that aren't actually functions ARE
550
   * considered functions, here.  The main point is that this is used
551
   * to avoid anything higher-order: anything function-like cannot be
552
   * the argument or return value for anything else function-like.
553
   *
554
   * Arrays are explicitly *not* function-like for the purposes of
555
   * this test.  However, functions still cannot contain anything
556
   * function-like.
557
   */
558
  bool isFunctionLike() const;
559
560
  /**
561
   * Get the argument types of a function, datatype constructor,
562
   * datatype selector, or datatype tester.
563
   */
564
  std::vector<TypeNode> getArgTypes() const;
565
566
  /**
567
   * Get the paramater types of a parameterized datatype.  Fails an
568
   * assertion if this type is not a parametric datatype.
569
   */
570
  std::vector<TypeNode> getParamTypes() const;
571
572
  /**
573
   * Get the range type (i.e., the type of the result) of a function,
574
   * datatype constructor, datatype selector, or datatype tester.
575
   */
576
  TypeNode getRangeType() const;
577
578
  /**
579
   * Is this a predicate type?  NOTE: all predicate types are also
580
   * function types (so datatype testers are NOT considered
581
   * "predicates" for the purpose of this function).
582
   */
583
  bool isPredicate() const;
584
585
  /**
586
   * Is this a predicate-LIKE type?  Predicate-like things
587
   * (e.g. datatype testers) that aren't actually predicates ARE
588
   * considered predicates, here.
589
   *
590
   * Arrays are explicitly *not* predicate-like for the purposes of
591
   * this test.
592
   */
593
  bool isPredicateLike() const;
594
595
  /** Is this a tuple type? */
596
  bool isTuple() const;
597
598
  /** Is this a record type? */
599
  bool isRecord() const;
600
601
  /** Get the length of a tuple type */
602
  size_t getTupleLength() const;
603
604
  /** Get the constituent types of a tuple type */
605
  std::vector<TypeNode> getTupleTypes() const;
606
607
  /** Is this a symbolic expression type? */
608
  bool isSExpr() const;
609
610
  /** Get the constituent types of a symbolic expression type */
611
  std::vector<TypeNode> getSExprTypes() const;
612
613
  /** Is this a regexp type */
614
  bool isRegExp() const;
615
616
  /** Is this a floating-point type */
617
  bool isFloatingPoint() const;
618
619
  /** Is this a floating-point type of with <code>exp</code> exponent bits
620
      and <code>sig</code> significand bits */
621
  bool isFloatingPoint(unsigned exp, unsigned sig) const;
622
623
  /** Is this a bit-vector type */
624
  bool isBitVector() const;
625
626
  /** Is this a bit-vector type of size <code>size</code> */
627
  bool isBitVector(unsigned size) const;
628
629
  /** Is this a datatype type */
630
  bool isDatatype() const;
631
632
  /** Is this a parameterized datatype type */
633
  bool isParametricDatatype() const;
634
635
  /** Is this a codatatype type */
636
  bool isCodatatype() const;
637
638
  /** Is this a fully instantiated datatype type */
639
  bool isInstantiatedDatatype() const;
640
641
  /** Is this a sygus datatype type */
642
  bool isSygusDatatype() const;
643
644
  /**
645
   * Get instantiated datatype type. The type on which this method is called
646
   * should be a parametric datatype whose parameter list is the same size as
647
   * argument params. This constructs the instantiated version of this
648
   * parametric datatype, e.g. passing (par (A) (List A)), { Int } ) to this
649
   * method returns (List Int).
650
   */
651
  TypeNode instantiateParametricDatatype(
652
      const std::vector<TypeNode>& params) const;
653
654
  /** Is this an instantiated datatype parameter */
655
  bool isParameterInstantiatedDatatype(unsigned n) const;
656
657
  /** Is this a constructor type */
658
  bool isConstructor() const;
659
660
  /** Is this a selector type */
661
  bool isSelector() const;
662
663
  /** Is this a tester type */
664
  bool isTester() const;
665
666
  /** Get the internal Datatype specification from a datatype type */
667
  const DType& getDType() const;
668
669
  /** Get the exponent size of this floating-point type */
670
  unsigned getFloatingPointExponentSize() const;
671
672
  /** Get the significand size of this floating-point type */
673
  unsigned getFloatingPointSignificandSize() const;
674
675
  /** Get the size of this bit-vector type */
676
  unsigned getBitVectorSize() const;
677
678
  /** Is this a sort kind */
679
  bool isSort() const;
680
681
  /** Is this a sort constructor kind */
682
  bool isSortConstructor() const;
683
684
  /** Get sort constructor arity */
685
  uint64_t getSortConstructorArity() const;
686
687
  /**
688
   * Get name, for uninterpreted sorts and uninterpreted sort constructors.
689
   */
690
  std::string getName() const;
691
692
  /**
693
   * Instantiate a sort constructor type. The type on which this method is
694
   * called should be a sort constructor type whose parameter list is the
695
   * same size as argument params. This constructs the instantiated version of
696
   * this sort constructor. For example, this is a sort constructor, e.g.
697
   * declared via (declare-sort U 2), then calling this method with
698
   * { Int, Int } will generate the instantiated sort (U Int Int).
699
   */
700
  TypeNode instantiateSortConstructor(
701
      const std::vector<TypeNode>& params) const;
702
703
  /** Get the most general base type of the type */
704
  TypeNode getBaseType() const;
705
706
  /**
707
   * Returns the leastUpperBound in the extended type lattice of the two types.
708
   * If this is \top, i.e. there is no inhabited type that contains both,
709
   * a TypeNode such that isNull() is true is returned.
710
   *
711
   * For more information see: http://cvc4.cs.nyu.edu/wiki/Cvc4_Type_Lattice
712
   */
713
  static TypeNode leastCommonTypeNode(TypeNode t0, TypeNode t1);
714
  static TypeNode mostCommonTypeNode(TypeNode t0, TypeNode t1);
715
716
  /** get ensure type condition
717
   *  Return value is a condition that implies that n has type tn.
718
  */
719
  static Node getEnsureTypeCondition( Node n, TypeNode tn );
720
private:
721
  static TypeNode commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast);
722
723
  /**
724
   * Is this type interpreted as finite.
725
   * If the flag usortFinite is true, this assumes all uninterpreted sorts
726
   *   are interpreted as finite.
727
   */
728
  bool isFiniteInternal(bool usortFinite);
729
730
  /**
731
   * Indents the given stream a given amount of spaces.
732
   *
733
   * @param out the stream to indent
734
   * @param indent the number of spaces
735
   */
736
  static void indent(std::ostream& out, int indent) {
737
    for(int i = 0; i < indent; i++) {
738
      out << ' ';
739
    }
740
  }
741
742
};/* class TypeNode */
743
744
/**
745
 * Serializes a given node to the given stream.
746
 *
747
 * @param out the output stream to use
748
 * @param n the node to output to the stream
749
 * @return the stream
750
 */
751
23473
inline std::ostream& operator<<(std::ostream& out, const TypeNode& n) {
752
23473
  n.toStream(out, Node::setlanguage::getLanguage(out));
753
23473
  return out;
754
}
755
756
typedef TypeNode::HashFunction TypeNodeHashFunction;
757
758
}/* CVC4 namespace */
759
760
#include "expr/node_manager.h"
761
762
namespace CVC4 {
763
764
inline TypeNode
765
2
TypeNode::substitute(const TypeNode& type,
766
                     const TypeNode& replacement) const {
767
4
  std::unordered_map<TypeNode, TypeNode, HashFunction> cache;
768
4
  return substitute(type, replacement, cache);
769
}
770
771
template <class Iterator1, class Iterator2>
772
inline TypeNode
773
20029
TypeNode::substitute(Iterator1 typesBegin,
774
                     Iterator1 typesEnd,
775
                     Iterator2 replacementsBegin,
776
                     Iterator2 replacementsEnd) const {
777
40058
  std::unordered_map<TypeNode, TypeNode, HashFunction> cache;
778
  return substitute(typesBegin, typesEnd,
779
40058
                    replacementsBegin, replacementsEnd, cache);
780
}
781
782
template <class Iterator1, class Iterator2>
783
24411
TypeNode TypeNode::substitute(Iterator1 typesBegin,
784
                              Iterator1 typesEnd,
785
                              Iterator2 replacementsBegin,
786
                              Iterator2 replacementsEnd,
787
                              std::unordered_map<TypeNode, TypeNode, HashFunction>& cache) const {
788
  // in cache?
789
24411
  std::unordered_map<TypeNode, TypeNode, HashFunction>::const_iterator i = cache.find(*this);
790
24411
  if(i != cache.end()) {
791
1109
    return (*i).second;
792
  }
793
794
  // otherwise compute
795
23302
  Assert(typesEnd - typesBegin == replacementsEnd - replacementsBegin)
796
      << "Substitution iterator ranges must be equal size";
797
23302
  Iterator1 j = find(typesBegin, typesEnd, *this);
798
23302
  if(j != typesEnd) {
799
37740
    TypeNode tn = *(replacementsBegin + (j - typesBegin));
800
18870
    cache[*this] = tn;
801
18870
    return tn;
802
4432
  } else if(getNumChildren() == 0) {
803
2474
    cache[*this] = *this;
804
2474
    return *this;
805
  } else {
806
3916
    NodeBuilder<> nb(getKind());
807
1958
    if(getMetaKind() == kind::metakind::PARAMETERIZED) {
808
      // push the operator
809
      nb << TypeNode(d_nv->d_children[0]);
810
    }
811
6340
    for (const TypeNode& tn : *this)
812
    {
813
4382
      nb << tn.substitute(
814
          typesBegin, typesEnd, replacementsBegin, replacementsEnd, cache);
815
    }
816
3916
    TypeNode tn = nb.constructTypeNode();
817
1958
    cache[*this] = tn;
818
1958
    return tn;
819
  }
820
}
821
822
5515099
inline size_t TypeNode::getNumChildren() const {
823
5515099
  return d_nv->getNumChildren();
824
}
825
826
template <class T>
827
357826856
inline const T& TypeNode::getConst() const {
828
357826856
  return d_nv->getConst<T>();
829
}
830
831
42814477
inline TypeNode::TypeNode(const expr::NodeValue* ev) :
832
42814477
  d_nv(const_cast<expr::NodeValue*> (ev)) {
833
42814477
  Assert(d_nv != NULL) << "Expecting a non-NULL expression value!";
834
42814477
  d_nv->inc();
835
42814477
}
836
837
811313992
inline TypeNode::TypeNode(const TypeNode& typeNode) {
838
811313992
  Assert(typeNode.d_nv != NULL) << "Expecting a non-NULL expression value!";
839
811313992
  d_nv = typeNode.d_nv;
840
811313992
  d_nv->inc();
841
811313992
}
842
843
3318667100
inline TypeNode::~TypeNode() {
844
1659333550
  Assert(d_nv != NULL) << "Expecting a non-NULL expression value!";
845
1659333550
  d_nv->dec();
846
1659333550
}
847
848
inline void TypeNode::assignNodeValue(expr::NodeValue* ev) {
849
  d_nv = ev;
850
  d_nv->inc();
851
}
852
853
765491459
inline TypeNode& TypeNode::operator=(const TypeNode& typeNode) {
854
765491459
  Assert(d_nv != NULL) << "Expecting a non-NULL expression value!";
855
765491459
  Assert(typeNode.d_nv != NULL)
856
      << "Expecting a non-NULL expression value on RHS!";
857
765491459
  if(__builtin_expect( ( d_nv != typeNode.d_nv ), true )) {
858
765156317
    d_nv->dec();
859
765156317
    d_nv = typeNode.d_nv;
860
765156317
    d_nv->inc();
861
  }
862
765491459
  return *this;
863
}
864
865
template <class AttrKind>
866
13337666
inline typename AttrKind::value_type TypeNode::
867
getAttribute(const AttrKind&) const {
868
13337666
  Assert(NodeManager::currentNM() != NULL)
869
      << "There is no current CVC4::NodeManager associated to this thread.\n"
870
         "Perhaps a public-facing function is missing a NodeManagerScope ?";
871
13337666
  return NodeManager::currentNM()->getAttribute(d_nv, AttrKind());
872
}
873
874
template <class AttrKind>
875
701784
inline bool TypeNode::
876
hasAttribute(const AttrKind&) const {
877
701784
  Assert(NodeManager::currentNM() != NULL)
878
      << "There is no current CVC4::NodeManager associated to this thread.\n"
879
         "Perhaps a public-facing function is missing a NodeManagerScope ?";
880
701784
  return NodeManager::currentNM()->hasAttribute(d_nv, AttrKind());
881
}
882
883
template <class AttrKind>
884
inline bool TypeNode::getAttribute(const AttrKind&, typename AttrKind::value_type& ret) const {
885
  Assert(NodeManager::currentNM() != NULL)
886
      << "There is no current CVC4::NodeManager associated to this thread.\n"
887
         "Perhaps a public-facing function is missing a NodeManagerScope ?";
888
  return NodeManager::currentNM()->getAttribute(d_nv, AttrKind(), ret);
889
}
890
891
template <class AttrKind>
892
52498
inline void TypeNode::
893
setAttribute(const AttrKind&, const typename AttrKind::value_type& value) {
894
52498
  Assert(NodeManager::currentNM() != NULL)
895
      << "There is no current CVC4::NodeManager associated to this thread.\n"
896
         "Perhaps a public-facing function is missing a NodeManagerScope ?";
897
52498
  NodeManager::currentNM()->setAttribute(d_nv, AttrKind(), value);
898
52498
}
899
900
inline void TypeNode::printAst(std::ostream& out, int indent) const {
901
  d_nv->printAst(out, indent);
902
}
903
904
93256664
inline bool TypeNode::isBoolean() const {
905
  return
906
93256664
    ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == BOOLEAN_TYPE );
907
}
908
909
204081388
inline bool TypeNode::isInteger() const {
910
  return
911
204081388
    ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == INTEGER_TYPE );
912
}
913
914
11234699
inline bool TypeNode::isReal() const {
915
  return
916
20500722
    ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == REAL_TYPE ) ||
917
20500722
    isInteger();
918
}
919
920
5021245
inline bool TypeNode::isString() const {
921
9980660
  return getKind() == kind::TYPE_CONSTANT &&
922
9980660
    getConst<TypeConstant>() == STRING_TYPE;
923
}
924
925
/** Is this a regexp type */
926
1414063
inline bool TypeNode::isRegExp() const {
927
2819155
  return getKind() == kind::TYPE_CONSTANT &&
928
2819155
    getConst<TypeConstant>() == REGEXP_TYPE;
929
 }
930
931
34939
inline bool TypeNode::isRoundingMode() const {
932
43165
  return getKind() == kind::TYPE_CONSTANT &&
933
43165
    getConst<TypeConstant>() == ROUNDINGMODE_TYPE;
934
}
935
936
1478496
inline bool TypeNode::isArray() const {
937
1478496
  return getKind() == kind::ARRAY_TYPE;
938
}
939
940
35084
inline TypeNode TypeNode::getArrayIndexType() const {
941
35084
  Assert(isArray());
942
35084
  return (*this)[0];
943
}
944
945
43932
inline TypeNode TypeNode::getArrayConstituentType() const {
946
43932
  Assert(isArray());
947
43932
  return (*this)[1];
948
}
949
950
271125
inline TypeNode TypeNode::getConstructorRangeType() const {
951
271125
  Assert(isConstructor());
952
271125
  return (*this)[getNumChildren()-1];
953
}
954
955
425089
inline TypeNode TypeNode::getSelectorDomainType() const
956
{
957
425089
  Assert(isSelector());
958
425089
  return (*this)[0];
959
}
960
961
861011
inline TypeNode TypeNode::getSelectorRangeType() const
962
{
963
861011
  Assert(isSelector());
964
861011
  return (*this)[1];
965
}
966
967
1340485
inline bool TypeNode::isSet() const {
968
1340485
  return getKind() == kind::SET_TYPE;
969
}
970
971
881551
inline bool TypeNode::isSequence() const
972
{
973
881551
  return getKind() == kind::SEQUENCE_TYPE;
974
}
975
976
681262
inline TypeNode TypeNode::getSetElementType() const {
977
681262
  Assert(isSet());
978
681262
  return (*this)[0];
979
}
980
981
8994426
inline bool TypeNode::isFunction() const {
982
8994426
  return getKind() == kind::FUNCTION_TYPE;
983
}
984
985
44238
inline bool TypeNode::isFunctionLike() const {
986
  return
987
88397
    getKind() == kind::FUNCTION_TYPE ||
988
88318
    getKind() == kind::CONSTRUCTOR_TYPE ||
989
132517
    getKind() == kind::SELECTOR_TYPE ||
990
88358
    getKind() == kind::TESTER_TYPE;
991
}
992
993
130038
inline bool TypeNode::isPredicate() const {
994
130038
  return isFunction() && getRangeType().isBoolean();
995
}
996
997
inline bool TypeNode::isPredicateLike() const {
998
  return isFunctionLike() && getRangeType().isBoolean();
999
}
1000
1001
667742
inline TypeNode TypeNode::getRangeType() const {
1002
667742
  if(isTester()) {
1003
    return NodeManager::currentNM()->booleanType();
1004
  }
1005
667742
  Assert(isFunction() || isConstructor() || isSelector())
1006
      << "Cannot get range type of " << *this;
1007
667742
  return (*this)[getNumChildren() - 1];
1008
}
1009
1010
/** Is this a symbolic expression type? */
1011
inline bool TypeNode::isSExpr() const {
1012
  return getKind() == kind::SEXPR_TYPE;
1013
}
1014
1015
/** Is this a floating-point type */
1016
138441
inline bool TypeNode::isFloatingPoint() const {
1017
138441
  return getKind() == kind::FLOATINGPOINT_TYPE;
1018
}
1019
1020
/** Is this a bit-vector type */
1021
10985915
inline bool TypeNode::isBitVector() const {
1022
10985915
  return getKind() == kind::BITVECTOR_TYPE;
1023
}
1024
1025
/** Is this a datatype type */
1026
9766576
inline bool TypeNode::isDatatype() const {
1027
9766576
  return getKind() == kind::DATATYPE_TYPE || getKind() == kind::PARAMETRIC_DATATYPE;
1028
}
1029
1030
/** Is this a parametric datatype type */
1031
1124137
inline bool TypeNode::isParametricDatatype() const {
1032
1124137
  return getKind() == kind::PARAMETRIC_DATATYPE;
1033
}
1034
1035
/** Is this a constructor type */
1036
8429956
inline bool TypeNode::isConstructor() const {
1037
8429956
  return getKind() == kind::CONSTRUCTOR_TYPE;
1038
}
1039
1040
/** Is this a selector type */
1041
1942077
inline bool TypeNode::isSelector() const {
1042
1942077
  return getKind() == kind::SELECTOR_TYPE;
1043
}
1044
1045
/** Is this a tester type */
1046
2380002
inline bool TypeNode::isTester() const {
1047
2380002
  return getKind() == kind::TESTER_TYPE;
1048
}
1049
1050
/** Is this a floating-point type of with <code>exp</code> exponent bits
1051
    and <code>sig</code> significand bits */
1052
inline bool TypeNode::isFloatingPoint(unsigned exp, unsigned sig) const {
1053
  return (getKind() == kind::FLOATINGPOINT_TYPE
1054
          && getConst<FloatingPointSize>().exponentWidth() == exp
1055
          && getConst<FloatingPointSize>().significandWidth() == sig);
1056
}
1057
1058
/** Is this a bit-vector type of size <code>size</code> */
1059
1640
inline bool TypeNode::isBitVector(unsigned size) const {
1060
  return
1061
1640
    ( getKind() == kind::BITVECTOR_TYPE && getConst<BitVectorSize>() == size );
1062
}
1063
1064
/** Get the exponent size of this floating-point type */
1065
147
inline unsigned TypeNode::getFloatingPointExponentSize() const {
1066
147
  Assert(isFloatingPoint());
1067
147
  return getConst<FloatingPointSize>().exponentWidth();
1068
}
1069
1070
/** Get the significand size of this floating-point type */
1071
147
inline unsigned TypeNode::getFloatingPointSignificandSize() const {
1072
147
  Assert(isFloatingPoint());
1073
147
  return getConst<FloatingPointSize>().significandWidth();
1074
}
1075
1076
/** Get the size of this bit-vector type */
1077
5591051
inline unsigned TypeNode::getBitVectorSize() const {
1078
5591051
  Assert(isBitVector());
1079
5591051
  return getConst<BitVectorSize>();
1080
}
1081
1082
#ifdef CVC4_DEBUG
1083
/**
1084
 * Pretty printer for use within gdb.  This is not intended to be used
1085
 * outside of gdb.  This writes to the Warning() stream and immediately
1086
 * flushes the stream.
1087
 *
1088
 * Note that this function cannot be a template, since the compiler
1089
 * won't instantiate it.  Even if we explicitly instantiate.  (Odd?)
1090
 * So we implement twice.  We mark as __attribute__((used)) so that
1091
 * GCC emits code for it even though static analysis indicates it's
1092
 * never called.
1093
 *
1094
 * Tim's Note: I moved this into the node.h file because this allows gdb
1095
 * to find the symbol, and use it, which is the first standard this code needs
1096
 * to meet. A cleaner solution is welcomed.
1097
 */
1098
static void __attribute__((used)) debugPrintTypeNode(const TypeNode& n) {
1099
  Warning() << Node::setdepth(-1)
1100
            << Node::dag(true)
1101
            << Node::setlanguage(language::output::LANG_AST)
1102
            << n << std::endl;
1103
  Warning().flush();
1104
}
1105
static void __attribute__((used)) debugPrintTypeNodeNoDag(const TypeNode& n) {
1106
  Warning() << Node::setdepth(-1)
1107
            << Node::dag(false)
1108
            << Node::setlanguage(language::output::LANG_AST)
1109
            << n << std::endl;
1110
  Warning().flush();
1111
}
1112
static void __attribute__((used)) debugPrintRawTypeNode(const TypeNode& n) {
1113
  n.printAst(Warning(), 0);
1114
  Warning().flush();
1115
}
1116
#endif /* CVC4_DEBUG */
1117
1118
}/* CVC4 namespace */
1119
1120
#endif /* CVC4__NODE_H */