GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/dtype.h Lines: 1 2 50.0 %
Date: 2021-03-22 Branches: 16 35 45.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file dtype.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 A class representing a datatype definition
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__EXPR__DTYPE_H
18
#define CVC4__EXPR__DTYPE_H
19
20
#include <map>
21
#include <string>
22
#include <vector>
23
#include "expr/attribute.h"
24
#include "expr/node.h"
25
#include "expr/type_node.h"
26
27
namespace CVC4 {
28
29
// ----------------------- datatype attributes
30
/**
31
 * Attribute for the index of an expression within a datatype, which is either:
32
 * (1) If the expression is a constructor, then its index refers to its
33
 * placement in the constructor list of the datatype that owns it, (2) If the
34
 * expression is a selector, then its index refers to its placement in the
35
 * argument list of the constructor that owns it.
36
 */
37
struct DTypeIndexTag
38
{
39
};
40
typedef expr::Attribute<DTypeIndexTag, size_t> DTypeIndexAttr;
41
/**
42
 * Attribute for the constructor index of a selector. This indicates the index
43
 * (DTypeIndexAttr) of the constructor that owns this selector.
44
 */
45
struct DTypeConsIndexTag
46
{
47
};
48
typedef expr::Attribute<DTypeConsIndexTag, size_t> DTypeConsIndexAttr;
49
/** Attribute true for datatype types that are finite. */
50
struct DTypeFiniteTag
51
{
52
};
53
typedef expr::Attribute<DTypeFiniteTag, bool> DTypeFiniteAttr;
54
/** Attribute true when we have computed whether a datatype type is finite */
55
struct DTypeFiniteComputedTag
56
{
57
};
58
typedef expr::Attribute<DTypeFiniteComputedTag, bool> DTypeFiniteComputedAttr;
59
/**
60
 * Attribute true for datatype types that are interpreted as finite (see
61
 * TypeNode::isInterpretedFinite).
62
 */
63
struct DTypeUFiniteTag
64
{
65
};
66
typedef expr::Attribute<DTypeUFiniteTag, bool> DTypeUFiniteAttr;
67
/**
68
 * Attribute true when we have computed whether a datatype type is interpreted
69
 * as finite.
70
 */
71
struct DTypeUFiniteComputedTag
72
{
73
};
74
typedef expr::Attribute<DTypeUFiniteComputedTag, bool> DTypeUFiniteComputedAttr;
75
// ----------------------- end datatype attributes
76
77
class DTypeConstructor;
78
79
/**
80
 * The Node-level representation of an inductive datatype, which currently
81
 * resides within the Expr-level Datatype class (expr/datatype.h).
82
 *
83
 * Notice that this class is a specification for a datatype, and is not
84
 * itself a type. The type that this specification corresponds to can be
85
 * retrieved (after resolution as described in the following) via getTypeNode.
86
 *
87
 * This is far more complicated than it first seems.  Consider this
88
 * datatype definition:
89
 *
90
 *   DATATYPE nat =
91
 *     succ(pred: nat)
92
 *   | zero
93
 *   END;
94
 *
95
 * You cannot define "nat" until you have a Type for it, but you
96
 * cannot have a Type for it until you fill in the type of the "pred"
97
 * selector, which needs the Type.  So we have a chicken-and-egg
98
 * problem.  It's even more complicated when we have mutual recursion
99
 * between datatypes, since the CVC presentation language does not
100
 * require forward-declarations.  Here, we define trees of lists that
101
 * contain trees of lists (etc):
102
 *
103
 *   DATATYPE
104
 *     tree = node(left: tree, right: tree) | leaf(list),
105
 *     list = cons(car: tree, cdr: list) | nil
106
 *   END;
107
 *
108
 * We build DType objects to describe "tree" and "list", and their constructors
109
 * and constructor arguments, but leave any unknown types (including
110
 * self-references) in an "unresolved" state.  After parsing the whole DATATYPE
111
 * block, we create a TypeNode through ExprManager::mkMutualDatatypeTypes().
112
 * The ExprManager creates a Type for each, but before "releasing" this type
113
 * into the wild, it does a round of in-place "resolution" on each DType by
114
 * calling DType::resolve() with a map of string -> TypeNode to
115
 * allow the datatype to construct the necessary testers and selectors.
116
 *
117
 * An additional point to make is that we want to ease the burden on
118
 * both the parser AND the users of the CVC4 API, so this class takes
119
 * on the task of generating its own selectors and testers, for
120
 * instance.  That means that, after reifying the DType with the
121
 * NodeManager, the parser needs to go through the (now-resolved)
122
 * DType and request the constructor, selector, and tester terms.
123
 * See src/parser/parser.cpp for how this is done.  For API usage
124
 * ideas, see test/unit/util/datatype_black.h.
125
 *
126
 * DTypes may also be defined parametrically, such as this example:
127
 *
128
 *  DATATYPE
129
 *    list[T] = cons(car : T, cdr : list[T]) | null,
130
 *    tree = node(children : list[tree]) | leaf
131
 *  END;
132
 *
133
 * Here, the definition of the parametric datatype list, where T is a type
134
 * variable. In other words, this defines a family of types list[C] where C is
135
 * any concrete type.  DTypes can be parameterized over multiple type variables
136
 * using the syntax sym[ T1, ..., Tn ] = ...,
137
 *
138
 */
139
21558
class DType
140
{
141
  friend class DTypeConstructor;
142
  friend class NodeManager;  // for access to resolve()
143
144
 public:
145
  /**
146
   * Get the datatype of a constructor, selector, or tester operator.
147
   */
148
  static const DType& datatypeOf(Node item);
149
150
  /**
151
   * Get the index of a constructor or tester in its datatype, or the
152
   * index of a selector in its constructor.  (Zero is always the
153
   * first index.)
154
   */
155
  static size_t indexOf(Node item);
156
157
  /**
158
   * Get the index of constructor corresponding to selector.  (Zero is
159
   * always the first index.)
160
   */
161
  static size_t cindexOf(Node item);
162
163
  /**
164
   * Same as above, but without checks. These methods should be used by
165
   * internal (Node-level) code.
166
   */
167
  static size_t indexOfInternal(Node item);
168
  static size_t cindexOfInternal(Node item);
169
170
  /** Create a new DType of the given name. */
171
  DType(std::string name, bool isCo = false);
172
173
  /**
174
   * Create a new DType of the given name, with the given
175
   * parameterization.
176
   */
177
  DType(std::string name,
178
        const std::vector<TypeNode>& params,
179
        bool isCo = false);
180
181
  ~DType();
182
183
  /** Add a constructor to this DType.
184
   *
185
   * Notice that constructor names need not
186
   * be unique; they are for convenience and pretty-printing only.
187
   */
188
  void addConstructor(std::shared_ptr<DTypeConstructor> c);
189
  /** add sygus constructor
190
   *
191
   * This adds a sygus constructor to this datatype, where
192
   * this datatype should be currently unresolved. Note this method is
193
   * syntactic sugar for adding a normal constructor and setting it to be a
194
   * sygus constructor, and following a naming convention that avoids
195
   * constructors with the same name.
196
   *
197
   * @param op : the builtin operator, constant, or variable that this
198
   * constructor encodes
199
   * @param cname the name of the constructor (for printing only)
200
   * @param cargs the arguments of the constructor.
201
   * It should be the case that cargs are sygus datatypes that
202
   * encode the arguments of op. For example, a sygus constructor
203
   * with op = PLUS should be such that cargs.size()>=2 and
204
   * the sygus type of cargs[i] is Real/Int for each i.
205
   * @param weight denotes the value added by the constructor when computing the
206
   * size of datatype terms. Passing a value < 0 denotes the default weight for
207
   * the constructor, which is 0 for nullary constructors and 1 for non-nullary
208
   * constructors.
209
   */
210
  void addSygusConstructor(Node op,
211
                           const std::string& cname,
212
                           const std::vector<TypeNode>& cargs,
213
                           int weight = -1);
214
215
  /** set sygus
216
   *
217
   * This marks this datatype as a sygus datatype.
218
   * A sygus datatype is one that represents terms of type st
219
   * via a deep embedding described in Section 4 of
220
   * Reynolds et al. CAV 2015. We say that this sygus datatype
221
   * "encodes" its sygus type st in the following.
222
   *
223
   * st : the type this datatype encodes (this can be Int, Bool, etc.),
224
   * bvl : the list of arguments for the synth-fun
225
   * allow_const : whether all constants are (implicitly) allowed by the
226
   * datatype
227
   * allow_all : whether all terms are (implicitly) allowed by the datatype
228
   *
229
   * Notice that allow_const/allow_all do not reflect the constructors
230
   * for this datatype, and instead are used solely for relaxing constraints
231
   * when doing solution reconstruction (Figure 5 of Reynolds et al.
232
   * CAV 2015).
233
   */
234
  void setSygus(TypeNode st, Node bvl, bool allowConst, bool allowAll);
235
236
  /** set that this datatype is a tuple */
237
  void setTuple();
238
239
  /** set that this datatype is a record */
240
  void setRecord();
241
242
  /** Get the name of this DType. */
243
  std::string getName() const;
244
245
  /** Get the number of constructors (so far) for this DType. */
246
  size_t getNumConstructors() const;
247
248
  /** Is this datatype parametric? */
249
  bool isParametric() const;
250
251
  /** Get the number of type parameters */
252
  size_t getNumParameters() const;
253
254
  /** Get parameter */
255
  TypeNode getParameter(size_t i) const;
256
257
  /** Get parameters */
258
  std::vector<TypeNode> getParameters() const;
259
260
  /** is this a co-datatype? */
261
  bool isCodatatype() const;
262
263
  /** is this a sygus datatype? */
264
  bool isSygus() const;
265
266
  /** is this a tuple datatype? */
267
  bool isTuple() const;
268
269
  /** is this a record datatype? */
270
  bool isRecord() const;
271
272
  /**
273
   * Return the cardinality of this datatype.
274
   * The DType must be resolved.
275
   *
276
   * The version of this method that takes type t is required
277
   * for parametric datatypes, where t is an instantiated
278
   * parametric datatype type whose datatype is this class.
279
   */
280
  Cardinality getCardinality(TypeNode t) const;
281
  Cardinality getCardinality() const;
282
283
  /**
284
   * Return true iff this DType has finite cardinality. If the
285
   * datatype is not well-founded, this method returns false. The
286
   * DType must be resolved or an assertion is violated.
287
   *
288
   * The version of this method that takes type t is required
289
   * for parametric datatypes, where t is an instantiated
290
   * parametric datatype type whose datatype is this class.
291
   */
292
  bool isFinite(TypeNode t) const;
293
  bool isFinite() const;
294
295
  /**
296
   * Return true iff this  DType is finite (all constructors are
297
   * finite, i.e., there  are finitely  many ground terms) under the
298
   * assumption that unintepreted sorts are finite. If the
299
   * datatype is  not well-founded, this method returns false.  The
300
   * DType must be resolved or an assertion is violated.
301
   *
302
   * The versions of these methods that takes type t is required
303
   * for parametric datatypes, where t is an instantiated
304
   * parametric datatype type whose datatype is this class.
305
   */
306
  bool isInterpretedFinite(TypeNode t) const;
307
  bool isInterpretedFinite() const;
308
309
  /** is well-founded
310
   *
311
   * Return true iff this datatype is well-founded (there exist finite
312
   * values of this type). This datatype must be resolved or an assertion is
313
   * violated.
314
   */
315
  bool isWellFounded() const;
316
  /**
317
   * Does this datatype have nested recursion? This is true if this datatype
318
   * definition contains itself as an alien subfield type, or a variant
319
   * of itself as an alien subfield type (if this datatype is parametric).
320
   * For details see getAlienSubfieldTypes below.
321
   *
322
   * Notice that a type having no nested recursion may have a subfield type that
323
   * has nested recursion.
324
   */
325
  bool hasNestedRecursion() const;
326
327
  /** is recursive singleton
328
   *
329
   * Return true iff this datatype is a recursive singleton
330
   * (a recursive singleton is a recursive datatype with only
331
   * one infinite value). For details, see Reynolds et al. CADE 2015.
332
   *
333
   * The versions of these methods that takes type t is required
334
   * for parametric datatypes, where t is an instantiated
335
   * parametric datatype type whose datatype is this class.
336
   */
337
  bool isRecursiveSingleton(TypeNode t) const;
338
  bool isRecursiveSingleton() const;
339
340
  /** recursive single arguments
341
   *
342
   * Get recursive singleton argument types (uninterpreted sorts that the
343
   * cardinality of this datatype is dependent upon). For example, for :
344
   *   stream :=  cons( head1 : U1, head2 : U2, tail : stream )
345
   * Then, the recursive singleton argument types of stream are { U1, U2 },
346
   * since if U1 and U2 have cardinality one, then stream has cardinality
347
   * one as well.
348
   *
349
   * The versions of these methods that takes Type t is required
350
   * for parametric datatypes, where t is an instantiated
351
   * parametric datatype type whose datatype is this class.
352
   */
353
  unsigned getNumRecursiveSingletonArgTypes(TypeNode t) const;
354
  TypeNode getRecursiveSingletonArgType(TypeNode t, size_t i) const;
355
  unsigned getNumRecursiveSingletonArgTypes() const;
356
  TypeNode getRecursiveSingletonArgType(size_t i) const;
357
358
  /**
359
   * Construct and return a ground term of this DType.  The
360
   * DType must be both resolved and well-founded, or else an
361
   * exception is thrown.
362
   *
363
   * This method takes a type t, which is a datatype type whose
364
   * datatype is this class, which may be an instantiated datatype
365
   * type if this datatype is parametric.
366
   */
367
  Node mkGroundTerm(TypeNode t) const;
368
  /** Make ground value
369
   *
370
   * Same as above, but constructs a constant value instead of a ground term.
371
   * These two notions typically coincide. However, for uninterpreted sorts,
372
   * they do not: mkGroundTerm returns a fresh variable whereas mkValue returns
373
   * an uninterpreted constant. The motivation for mkGroundTerm is that
374
   * unintepreted constants should never appear in lemmas. The motivation for
375
   * mkGroundValue is for things like type enumeration and model construction.
376
   */
377
  Node mkGroundValue(TypeNode t) const;
378
379
  /**
380
   * Get the TypeNode associated to this DType.  Can only be
381
   * called post-resolution.
382
   */
383
  TypeNode getTypeNode() const;
384
385
  /**
386
   * Get the TypeNode associated to this (parameterized) DType.  Can only be
387
   * called post-resolution.
388
   */
389
  TypeNode getTypeNode(const std::vector<TypeNode>& params) const;
390
391
  /** Return true iff this DType has already been resolved. */
392
  bool isResolved() const;
393
394
  /** Get the ith DTypeConstructor. */
395
  const DTypeConstructor& operator[](size_t index) const;
396
397
  /** get sygus type
398
   * This gets the built-in type associated with
399
   * this sygus datatype, i.e. the type of the
400
   * term that this sygus datatype encodes.
401
   */
402
  TypeNode getSygusType() const;
403
404
  /** get sygus var list
405
   * This gets the variable list of the function
406
   * to synthesize using this sygus datatype.
407
   * For example, if we are synthesizing a binary
408
   * function f where solutions are of the form:
409
   *   f = (lambda (xy) t[x,y])
410
   * In this case, this method returns the
411
   * bound variable list containing x and y.
412
   */
413
  Node getSygusVarList() const;
414
  /** get sygus allow constants
415
   *
416
   * Does this sygus datatype allow constants?
417
   * Notice that this is not a property of the
418
   * constructors of this datatype. Instead, it is
419
   * an auxiliary flag (provided in the call
420
   * to setSygus).
421
   */
422
  bool getSygusAllowConst() const;
423
  /** get sygus allow all
424
   *
425
   * Does this sygus datatype allow all terms?
426
   * Notice that this is not a property of the
427
   * constructors of this datatype. Instead, it is
428
   * an auxiliary flag (provided in the call
429
   * to setSygus).
430
   */
431
  bool getSygusAllowAll() const;
432
433
  /** involves external type
434
   * Get whether this datatype has a subfield
435
   * in any constructor that is not a datatype type.
436
   */
437
  bool involvesExternalType() const;
438
  /** involves uninterpreted type
439
   * Get whether this datatype has a subfield
440
   * in any constructor that is an uninterpreted type.
441
   */
442
  bool involvesUninterpretedType() const;
443
444
  /**
445
   * Get the list of constructors.
446
   */
447
  const std::vector<std::shared_ptr<DTypeConstructor> >& getConstructors()
448
      const;
449
450
  /** prints this datatype to stream */
451
  void toStream(std::ostream& out) const;
452
453
 private:
454
  /**
455
   * DTypes refer to themselves, recursively, and we have a
456
   * chicken-and-egg problem.  The TypeNode around the DType
457
   * cannot exist until the DType is finalized, and the DType
458
   * cannot refer to the TypeNode representing itself until it
459
   * exists.  resolve() is called by the NodeManager when a type is
460
   * ultimately requested of the DType specification (that is, when
461
   * NodeManager::mkTypeNode() or NodeManager::mkMutualTypeNodes()
462
   * is called).  Has the effect of freezing the object, too; that is,
463
   * addConstructor() will fail after a call to resolve().
464
   *
465
   * The basic goal of resolution is to assign constructors, selectors,
466
   * and testers.  To do this, any UnresolvedType/SelfType references
467
   * must be cleared up.  This is the purpose of the "resolutions" map;
468
   * it includes any mutually-recursive datatypes that are currently
469
   * under resolution.  The four vectors come in two pairs (so, really
470
   * they are two maps).  placeholders->replacements give type variables
471
   * that should be resolved in the case of parametric datatypes.
472
   *
473
   * @param em the NodeManager at play
474
   * @param resolutions a map of strings to TypeNodes currently under
475
   * resolution
476
   * @param placeholders the types in these DTypes under resolution that must
477
   * be replaced
478
   * @param replacements the corresponding replacements
479
   * @param paramTypes the sort constructors in these DTypes under resolution
480
   * that must be replaced
481
   * @param paramReplacements the corresponding (parametric) TypeNodes
482
   */
483
  bool resolve(const std::map<std::string, TypeNode>& resolutions,
484
               const std::vector<TypeNode>& placeholders,
485
               const std::vector<TypeNode>& replacements,
486
               const std::vector<TypeNode>& paramTypes,
487
               const std::vector<TypeNode>& paramReplacements);
488
489
  /** compute the cardinality of this datatype */
490
  Cardinality computeCardinality(TypeNode t,
491
                                 std::vector<TypeNode>& processing) const;
492
  /** compute whether this datatype is a recursive singleton */
493
  bool computeCardinalityRecSingleton(TypeNode t,
494
                                      std::vector<TypeNode>& processing,
495
                                      std::vector<TypeNode>& u_assume) const;
496
  /** compute whether this datatype is well-founded */
497
  bool computeWellFounded(std::vector<TypeNode>& processing) const;
498
  /** compute ground term
499
   *
500
   * This method checks if there is a term of this datatype whose type is t
501
   * that is finitely constructable. As needed, it traverses its subfield types.
502
   *
503
   * The argument processing is the set of datatype types we are currently
504
   * traversing.
505
   *
506
   * The argument isValue is whether we are constructing a constant value. If
507
   * this flag is false, we are constructing a canonical ground term that is
508
   * not necessarily constant.
509
   */
510
  Node computeGroundTerm(TypeNode t,
511
                         std::vector<TypeNode>& processing,
512
                         bool isValue) const;
513
  /** Get the shared selector
514
   *
515
   * This returns the index^th (constructor-agnostic)
516
   * selector for type t. The type dtt is the datatype
517
   * type whose datatype is this class, where this may
518
   * be an instantiated parametric datatype.
519
   *
520
   * In the terminology of "DTypes with Shared Selectors",
521
   * this returns the term sel_{dtt}^{t,index}.
522
   */
523
  Node getSharedSelector(TypeNode dtt, TypeNode t, size_t index) const;
524
  /**
525
   * Helper for mkGroundTerm and mkGroundValue above.
526
   */
527
  Node mkGroundTermInternal(TypeNode t, bool isValue) const;
528
  /**
529
   * This method is used to get alien subfield types of this datatype.
530
   *
531
   * A subfield type T of a datatype type D is a type such that a value of
532
   * type T may appear as a subterm of a value of type D.
533
   *
534
   * An *alien* subfield type T of a datatype type D is a type such that a
535
   * value v of type T may appear as a subterm of a value of D, and moreover
536
   * v occurs as a strict subterm of a non-datatype term in that value.
537
   *
538
   * For example, the alien subfield types of T in:
539
   *   T -> Emp | Container(s : (Set List))
540
   *   List -> nil | cons( head : Int, tail: List)
541
   * are { List, Int }. Notice that Int is an alien subfield type since it
542
   * appears as a subfield type of List, and List is an alien subfield type
543
   * of T. In other words, Int is an alien subfield type due to the above
544
   * definition due to the term (Container (singleton (cons 0 nil))), where
545
   * 0 occurs as a subterm of (singleton (cons 0 nil)). The non-strict
546
   * subfield types of T in this example are { (Set List) }.
547
   *
548
   * For example, the alien subfield types of T in:
549
   *   T -> Emp | Container(s : List)
550
   *   List -> nil | cons( head : (Set T), tail: List)
551
   * are { T, List, (Set T) }. Notice that T is an alien subfield type of itself
552
   * since List is a subfield type of T and T is an alien subfield type of List.
553
   * Furthermore, List and (Set T) are also alien subfield types of T since
554
   * List is a subfield type of T and T is an alien subfield type of itself.
555
   *
556
   * For example, the alien subfield types of T in:
557
   *   T -> Emp | Container(s : (Array Int T))
558
   * are { T, Int }, where we assume that values of (Array U1 U2) are
559
   * constructed from values of U1 and U2, for all types U1, U2. The non-strict
560
   * subfield types of T in this example are { (Array Int T) }.
561
   *
562
   * @param types The set of types to append the alien subfield types to,
563
   * @param processed The datatypes (cached using d_self) we have processed. If
564
   * the range of this map is true, we have processed the datatype with
565
   * isAlienPos = true.
566
   * @param isAlienPos Whether we are in an alien subfield type position. This
567
   * flag is true if we have traversed beneath a non-datatype type constructor.
568
   */
569
  void getAlienSubfieldTypes(
570
      std::unordered_set<TypeNode, TypeNodeHashFunction>& types,
571
      std::map<TypeNode, bool>& processed,
572
      bool isAlienPos) const;
573
  /** name of this datatype */
574
  std::string d_name;
575
  /** the type parameters of this datatype (if this is a parametric datatype)
576
   */
577
  std::vector<TypeNode> d_params;
578
  /** whether the datatype is a codatatype. */
579
  bool d_isCo;
580
  /** whether the datatype is a tuple */
581
  bool d_isTuple;
582
  /** whether the datatype is a record */
583
  bool d_isRecord;
584
  /** the constructors of this datatype */
585
  std::vector<std::shared_ptr<DTypeConstructor> > d_constructors;
586
  /** whether this datatype has been resolved */
587
  bool d_resolved;
588
  /** self type */
589
  mutable TypeNode d_self;
590
  /** cache for involves external type */
591
  bool d_involvesExt;
592
  /** cache for involves uninterpreted type */
593
  bool d_involvesUt;
594
  /** the builtin type that this sygus type encodes */
595
  TypeNode d_sygusType;
596
  /** the variable list for the sygus function to synthesize */
597
  Node d_sygusBvl;
598
  /** whether all constants are allowed as solutions */
599
  bool d_sygusAllowConst;
600
  /** whether all terms are allowed as solutions */
601
  bool d_sygusAllowAll;
602
603
  /** the cardinality of this datatype
604
   * "mutable" because computing the cardinality can be expensive,
605
   * and so it's computed just once, on demand---this is the cache
606
   */
607
  mutable Cardinality d_card;
608
609
  /** is this type a recursive singleton type?
610
   * The range of this map stores
611
   * 0 if the field has not been computed,
612
   * 1 if this datatype is a recursive singleton type,
613
   * -1 if this datatype is not a recursive singleton type.
614
   * For definition of (co)recursive singleton, see
615
   * Section 2 of Reynolds et al. CADE 2015.
616
   */
617
  mutable std::map<TypeNode, int> d_cardRecSingleton;
618
  /** if d_cardRecSingleton is true,
619
   * This datatype has infinite cardinality if at least one of the
620
   * following uninterpreted sorts having cardinality > 1.
621
   */
622
  mutable std::map<TypeNode, std::vector<TypeNode> > d_cardUAssume;
623
  /**
624
   * Cache of whether this datatype is well-founded, where 0 means we have
625
   * not computed this information, 1 means it is well-founded, -1 means it is
626
   * not.
627
   */
628
  mutable int d_wellFounded;
629
  /**
630
   * Cache of whether this datatype has nested recursion, where 0 means we have
631
   * not computed this information, 1 means it has nested recursion, -1 means it
632
   * does not.
633
   */
634
  mutable int d_nestedRecursion;
635
  /** cache of ground term for this datatype */
636
  mutable std::map<TypeNode, Node> d_groundTerm;
637
  /** cache of ground values for this datatype */
638
  mutable std::map<TypeNode, Node> d_groundValue;
639
  /** cache of shared selectors for this datatype */
640
  mutable std::map<TypeNode, std::map<TypeNode, std::map<unsigned, Node> > >
641
      d_sharedSel;
642
}; /* class DType */
643
644
/**
645
 * A hash function for DTypes.  Needed to store them in hash sets
646
 * and hash maps.
647
 */
648
struct DTypeHashFunction
649
{
650
  size_t operator()(const DType& dt) const
651
  {
652
    return std::hash<std::string>()(dt.getName());
653
  }
654
  size_t operator()(const DType* dt) const
655
  {
656
    return std::hash<std::string>()(dt->getName());
657
  }
658
}; /* struct DTypeHashFunction */
659
660
/* stores an index to DType residing in NodeManager */
661
class DTypeIndexConstant
662
{
663
 public:
664
  DTypeIndexConstant(size_t index);
665
666
  size_t getIndex() const { return d_index; }
667
  bool operator==(const DTypeIndexConstant& uc) const
668
  {
669
    return d_index == uc.d_index;
670
  }
671
  bool operator!=(const DTypeIndexConstant& uc) const { return !(*this == uc); }
672
  bool operator<(const DTypeIndexConstant& uc) const
673
  {
674
    return d_index < uc.d_index;
675
  }
676
  bool operator<=(const DTypeIndexConstant& uc) const
677
  {
678
    return d_index <= uc.d_index;
679
  }
680
  bool operator>(const DTypeIndexConstant& uc) const { return !(*this <= uc); }
681
  bool operator>=(const DTypeIndexConstant& uc) const { return !(*this < uc); }
682
683
 private:
684
  const size_t d_index;
685
}; /* class DTypeIndexConstant */
686
687
std::ostream& operator<<(std::ostream& out, const DTypeIndexConstant& dic);
688
689
struct DTypeIndexConstantHashFunction
690
{
691
  size_t operator()(const DTypeIndexConstant& dic) const
692
  {
693
    return IntegerHashFunction()(dic.getIndex());
694
  }
695
}; /* struct DTypeIndexConstantHashFunction */
696
697
std::ostream& operator<<(std::ostream& os, const DType& dt);
698
699
}  // namespace CVC4
700
701
#endif