GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/dtype_cons.h Lines: 2 2 100.0 %
Date: 2021-03-22 Branches: 8 16 50.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file dtype_cons.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_CONS_H
18
#define CVC4__EXPR__DTYPE_CONS_H
19
20
#include <map>
21
#include <string>
22
#include <vector>
23
#include "expr/dtype_selector.h"
24
#include "expr/node.h"
25
#include "expr/type_node.h"
26
27
namespace CVC4 {
28
29
/**
30
 * The Node-level representation of a constructor for a datatype, which
31
 * currently resides in the Expr-level DatatypeConstructor class
32
 * (expr/datatype.h).
33
 */
34
5760
class DTypeConstructor
35
{
36
  friend class DType;
37
38
 public:
39
  /**
40
   * Create a new datatype constructor with the given name for the
41
   * constructor and the same name (prefixed with "is_") for the
42
   * tester.  The actual constructor and tester (meaning, the Nodes
43
   * representing operators for these entities) aren't created until
44
   * resolution time.
45
   *
46
   * weight is the value that this constructor carries when computing size
47
   * for SyGuS. For example, if A, B, C have weights 0, 1, and 3 respectively,
48
   * then C( B( A() ), B( A() ) ) has size 5.
49
   */
50
  DTypeConstructor(std::string name, unsigned weight = 1);
51
52
25026
  ~DTypeConstructor() {}
53
  /**
54
   * Add an argument (i.e., a data field) of the given name and type
55
   * to this constructor.  Selector names need not be unique;
56
   * they are for convenience and pretty-printing only.
57
   */
58
  void addArg(std::string selectorName, TypeNode selectorType);
59
  /**
60
   * Add an argument, given a pointer to a selector object.
61
   */
62
  void addArg(std::shared_ptr<DTypeSelector> a);
63
  /**
64
   * Add a self-referential (i.e., a data field) of the given name
65
   * to this Datatype constructor that refers to the enclosing
66
   * Datatype.  For example, using the familiar "nat" Datatype, to
67
   * create the "pred" field for "succ" constructor, one uses
68
   * succ::addArgSelf("pred")---the actual Type
69
   * cannot be passed because the Datatype is still under
70
   * construction.  Selector names need not be unique; they are for
71
   * convenience and pretty-printing only.
72
   *
73
   * This is a special case of
74
   * DTypeConstructor::addArg(std::string).
75
   */
76
  void addArgSelf(std::string selectorName);
77
78
  /** Get the name of this constructor. */
79
  const std::string& getName() const;
80
81
  /**
82
   * Get the constructor operator of this constructor.  The
83
   * DType must be resolved.
84
   */
85
  Node getConstructor() const;
86
87
  /**
88
   * Get the tester operator of this constructor.  The
89
   * DType must be resolved.
90
   */
91
  Node getTester() const;
92
  //-------------------------------------- sygus
93
  /** set sygus
94
   *
95
   * Set that this constructor is a sygus datatype constructor that encodes
96
   * operator op.
97
   */
98
  void setSygus(Node op);
99
  /** get sygus op
100
   *
101
   * This method returns the operator or term that this constructor represents
102
   * in the sygus encoding. This may be a builtin operator, defined function,
103
   * variable, or constant that this constructor encodes in this deep embedding.
104
   */
105
  Node getSygusOp() const;
106
  /** is this a sygus identity function?
107
   *
108
   * This returns true if the sygus operator of this datatype constructor is
109
   * of the form (lambda (x) x).
110
   */
111
  bool isSygusIdFunc() const;
112
  /** get weight
113
   *
114
   * Get the weight of this constructor. This value is used when computing the
115
   * size of datatype terms that involve this constructor.
116
   */
117
  unsigned getWeight() const;
118
  //-------------------------------------- end sygus
119
120
  /**
121
   * Get the number of arguments (so far) of this DType constructor.
122
   */
123
  size_t getNumArgs() const;
124
  /**
125
   * Get the list of arguments to this constructor.
126
   */
127
  const std::vector<std::shared_ptr<DTypeSelector> >& getArgs() const;
128
  /**
129
   * Get the specialized constructor type for a parametric
130
   * constructor; this call is only permitted after resolution.
131
   * Given a (concrete) returnType, the constructor's concrete
132
   * type in this parametric datatype is returned.
133
   *
134
   * For instance, if the datatype is list[T], with constructor
135
   * "cons[T]" of type "T -> list[T] -> list[T]", then calling
136
   * this function with "list[int]" will return the concrete
137
   * "cons" constructor type for lists of int---namely,
138
   * "int -> list[int] -> list[int]".
139
   */
140
  TypeNode getSpecializedConstructorType(TypeNode returnType) const;
141
142
  /**
143
   * Return the cardinality of this constructor (the product of the
144
   * cardinalities of its arguments).
145
   */
146
  Cardinality getCardinality(TypeNode t) const;
147
148
  /**
149
   * Return true iff this constructor is finite (it is nullary or
150
   * each of its argument types are finite).  This function can
151
   * only be called for resolved constructors.
152
   */
153
  bool isFinite(TypeNode t) const;
154
  /**
155
   * Return true iff this constructor is finite (it is nullary or
156
   * each of its argument types are finite) under assumption
157
   * uninterpreted sorts are finite.  This function can
158
   * only be called for resolved constructors.
159
   */
160
  bool isInterpretedFinite(TypeNode t) const;
161
  /**
162
   * Has finite external argument type. This returns true if this constructor
163
   * has an argument type that is not a datatype and is interpreted as a
164
   * finite type. This function can only be called for resolved constructors.
165
   *
166
   */
167
  bool hasFiniteExternalArgType(TypeNode t) const;
168
169
  /**
170
   * Returns true iff this constructor has already been
171
   * resolved.
172
   */
173
  bool isResolved() const;
174
175
  /** Get the ith DTypeConstructor arg. */
176
  const DTypeSelector& operator[](size_t index) const;
177
178
  /**
179
   * Get argument type. Returns the return type of the i^th selector of this
180
   * constructor.
181
   */
182
  TypeNode getArgType(size_t i) const;
183
184
  /** get selector internal
185
   *
186
   * This gets the selector for the index^th argument
187
   * of this constructor. The type dtt is the datatype
188
   * type whose datatype is the owner of this constructor,
189
   * where this type may be an instantiated parametric datatype.
190
   *
191
   * If shared selectors are enabled,
192
   * this returns a shared (constructor-agnotic) selector, which
193
   * in the terminology of "DTypes with Shared Selectors", is:
194
   *   sel_{dtt}^{T,atos(T,C,index)}
195
   * where C is this constructor, and T is the type
196
   * of the index^th field of this constructor.
197
   * The semantics of sel_{dtt}^{T,n}( t ) is the n^th field of
198
   * type T of constructor term t if one exists, or is
199
   * unconstrained otherwise.
200
   */
201
  Node getSelectorInternal(TypeNode dtt, size_t index) const;
202
203
  /** get selector index internal
204
   *
205
   * This gets the argument number of this constructor
206
   * that the selector sel accesses. It returns -1 if the
207
   * selector sel is not a selector for this constructor.
208
   *
209
   * In the terminology of "DTypes with Shared Selectors",
210
   * if sel is sel_{dtt}^{T,index} for some (T, index), where
211
   * dtt is the datatype type whose datatype is the owner
212
   * of this constructor, then this method returns
213
   *   stoa(T,C,index)
214
   */
215
  int getSelectorIndexInternal(Node sel) const;
216
  /** get selector index for name
217
   *
218
   * Returns the index of selector with the given name, or -1 if it
219
   * does not exist.
220
   */
221
  int getSelectorIndexForName(const std::string& name) const;
222
223
  /** involves external type
224
   *
225
   * Get whether this constructor has a subfield
226
   * in any constructor that is not a datatype type.
227
   */
228
  bool involvesExternalType() const;
229
  /** involves uninterpreted type
230
   *
231
   * Get whether this constructor has a subfield
232
   * in any constructor that is an uninterpreted type.
233
   */
234
  bool involvesUninterpretedType() const;
235
  /** prints this datatype constructor to stream */
236
  void toStream(std::ostream& out) const;
237
238
 private:
239
  /** Constructor cardinality type */
240
  enum class CardinalityType
241
  {
242
    // the constructor is finite
243
    FINITE,
244
    // the constructor is interpreted-finite (finite under the assumption that
245
    // uninterpreted sorts are finite)
246
    INTERPRETED_FINITE,
247
    // the constructor is infinte
248
    INFINITE
249
  };
250
  /** resolve
251
   *
252
   * This resolves (initializes) the constructor. For details
253
   * on how datatypes and their constructors are resolved, see
254
   * documentation for DType::resolve.
255
   */
256
  bool resolve(TypeNode self,
257
               const std::map<std::string, TypeNode>& resolutions,
258
               const std::vector<TypeNode>& placeholders,
259
               const std::vector<TypeNode>& replacements,
260
               const std::vector<TypeNode>& paramTypes,
261
               const std::vector<TypeNode>& paramReplacements,
262
               size_t cindex);
263
264
  /** Helper function for resolving parametric datatypes.
265
   *
266
   * This replaces instances of the TypeNode produced for unresolved
267
   * parametric datatypes, with the corresponding resolved TypeNode.  For
268
   * example, take the parametric definition of a list,
269
   *    list[T] = cons(car : T, cdr : list[T]) | null.
270
   * If "range" is the unresolved parametric datatype:
271
   *   DATATYPE list =
272
   *    cons(car: SORT_TAG_1,
273
   *         cdr: SORT_TAG_2(SORT_TAG_1)) | null END;,
274
   * this function will return the resolved type:
275
   *   DATATYPE list =
276
   *    cons(car: SORT_TAG_1,
277
   *         cdr: (list PARAMETERIC_DATATYPE SORT_TAG_1)) | null END;
278
   */
279
  TypeNode doParametricSubstitution(
280
      TypeNode range,
281
      const std::vector<TypeNode>& paramTypes,
282
      const std::vector<TypeNode>& paramReplacements);
283
284
  /** compute the cardinality of this datatype */
285
  Cardinality computeCardinality(TypeNode t,
286
                                 std::vector<TypeNode>& processing) const;
287
  /** compute whether this datatype is well-founded */
288
  bool computeWellFounded(std::vector<TypeNode>& processing) const;
289
  /** compute ground term
290
   *
291
   * This method is used for constructing a term that is an application
292
   * of this constructor whose type is t.
293
   *
294
   * The argument processing is the set of datatype types we are currently
295
   * traversing. This is used to avoid infinite loops.
296
   *
297
   * The argument gt caches the ground terms we have computed so far.
298
   *
299
   * The argument isValue is whether we are constructing a constant value. If
300
   * this flag is false, we are constructing a canonical ground term that is
301
   * not necessarily constant.
302
   */
303
  Node computeGroundTerm(TypeNode t,
304
                         std::vector<TypeNode>& processing,
305
                         std::map<TypeNode, Node>& gt,
306
                         bool isValue) const;
307
  /**
308
   * Compute cardinality info, returns a pair where its first component is
309
   * an identifier indicating the cardinality type of this constructor for
310
   * type t, and a Boolean indicating whether the constructor has any arguments
311
   * that have finite external type.
312
   */
313
  std::pair<CardinalityType, bool> computeCardinalityInfo(TypeNode t) const;
314
  /** compute shared selectors
315
   * This computes the maps d_sharedSelectors and d_sharedSelectorIndex.
316
   */
317
  void computeSharedSelectors(TypeNode domainType) const;
318
  /** the name of the constructor */
319
  std::string d_name;
320
  /** the name of the tester */
321
  std::string d_testerName;
322
  /** the constructor expression */
323
  Node d_constructor;
324
  /** the tester for this constructor */
325
  Node d_tester;
326
  /** the arguments of this constructor */
327
  std::vector<std::shared_ptr<DTypeSelector> > d_args;
328
  /** sygus operator */
329
  Node d_sygusOp;
330
  /** weight */
331
  unsigned d_weight;
332
  /** shared selectors for each type
333
   *
334
   * This stores the shared (constructor-agnotic)
335
   * selectors that access the fields of this datatype.
336
   * In the terminology of "DTypes with Shared Selectors",
337
   * this stores:
338
   *   sel_{dtt}^{T1,atos(T1,C,1)}, ...,
339
   *   sel_{dtt}^{Tn,atos(Tn,C,n)}
340
   * where C is this constructor, which has type
341
   * T1 x ... x Tn -> dtt above.
342
   * We store this information for (possibly multiple)
343
   * datatype types dtt, since this constructor may be
344
   * for a parametric datatype, where dtt is an instantiated
345
   * parametric datatype.
346
   */
347
  mutable std::map<TypeNode, std::vector<Node> > d_sharedSelectors;
348
  /** for each type, a cache mapping from shared selectors to
349
   * its argument index for this constructor.
350
   */
351
  mutable std::map<TypeNode, std::map<Node, unsigned> > d_sharedSelectorIndex;
352
  /**  A cache for computeCardinalityInfo. */
353
  mutable std::map<TypeNode, std::pair<CardinalityType, bool> > d_cardInfo;
354
}; /* class DTypeConstructor */
355
356
/**
357
 * A hash function for DTypeConstructors.  Needed to store them in hash sets
358
 * and hash maps.
359
 */
360
struct DTypeConstructorHashFunction
361
{
362
  size_t operator()(const DTypeConstructor& dtc) const
363
  {
364
    return std::hash<std::string>()(dtc.getName());
365
  }
366
  size_t operator()(const DTypeConstructor* dtc) const
367
  {
368
    return std::hash<std::string>()(dtc->getName());
369
  }
370
}; /* struct DTypeConstructorHashFunction */
371
372
std::ostream& operator<<(std::ostream& os, const DTypeConstructor& ctor);
373
374
}  // namespace CVC4
375
376
#endif