1 /********************* */
2 /*! \file datatype.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-2019 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 ** A class representing a Datatype definition for the theory of
15 ** inductive datatypes.
16 **/
17
18 #include "cvc4_public.h"
19
20 #ifndef __CVC4__DATATYPE_H
21 #define __CVC4__DATATYPE_H
22
23 #include <functional>
24 #include <iostream>
25 #include <string>
26 #include <vector>
27 #include <map>
28
29 namespace CVC4 {
30 // messy; Expr needs Datatype (because it's the payload of a
31 // CONSTANT-kinded expression), and Datatype needs Expr.
32 //class CVC4_PUBLIC Datatype;
33 class CVC4_PUBLIC DatatypeIndexConstant;
34 }/* CVC4 namespace */
35
36 #include "base/exception.h"
37 #include "expr/expr.h"
38 #include "expr/type.h"
39 #include "util/hash.h"
40
41
42 namespace CVC4 {
43
44 class CVC4_PUBLIC ExprManager;
45
46 class CVC4_PUBLIC DatatypeConstructor;
47 class CVC4_PUBLIC DatatypeConstructorArg;
48
49 class CVC4_PUBLIC DatatypeConstructorIterator {
50 const std::vector<DatatypeConstructor>* d_v;
51 size_t d_i;
52
53 friend class Datatype;
54
DatatypeConstructorIterator(const std::vector<DatatypeConstructor> & v,bool start)55 DatatypeConstructorIterator(const std::vector<DatatypeConstructor>& v, bool start) : d_v(&v), d_i(start ? 0 : v.size()) {
56 }
57
58 public:
59 typedef const DatatypeConstructor& value_type;
60 const DatatypeConstructor& operator*() const { return (*d_v)[d_i]; }
61 const DatatypeConstructor* operator->() const { return &(*d_v)[d_i]; }
62 DatatypeConstructorIterator& operator++() { ++d_i; return *this; }
63 DatatypeConstructorIterator operator++(int) { DatatypeConstructorIterator i(*this); ++d_i; return i; }
64 bool operator==(const DatatypeConstructorIterator& other) const { return d_v == other.d_v && d_i == other.d_i; }
65 bool operator!=(const DatatypeConstructorIterator& other) const { return d_v != other.d_v || d_i != other.d_i; }
66 };/* class DatatypeConstructorIterator */
67
68 class CVC4_PUBLIC DatatypeConstructorArgIterator {
69 const std::vector<DatatypeConstructorArg>* d_v;
70 size_t d_i;
71
72 friend class DatatypeConstructor;
73
DatatypeConstructorArgIterator(const std::vector<DatatypeConstructorArg> & v,bool start)74 DatatypeConstructorArgIterator(const std::vector<DatatypeConstructorArg>& v, bool start) : d_v(&v), d_i(start ? 0 : v.size()) {
75 }
76
77 public:
78 typedef const DatatypeConstructorArg& value_type;
79 const DatatypeConstructorArg& operator*() const { return (*d_v)[d_i]; }
80 const DatatypeConstructorArg* operator->() const { return &(*d_v)[d_i]; }
81 DatatypeConstructorArgIterator& operator++() { ++d_i; return *this; }
82 DatatypeConstructorArgIterator operator++(int) { DatatypeConstructorArgIterator i(*this); ++d_i; return i; }
83 bool operator==(const DatatypeConstructorArgIterator& other) const { return d_v == other.d_v && d_i == other.d_i; }
84 bool operator!=(const DatatypeConstructorArgIterator& other) const { return d_v != other.d_v || d_i != other.d_i; }
85 };/* class DatatypeConstructorArgIterator */
86
87 /**
88 * An exception that is thrown when a datatype resolution fails.
89 */
90 class CVC4_PUBLIC DatatypeResolutionException : public Exception {
91 public:
92 inline DatatypeResolutionException(std::string msg);
93 };/* class DatatypeResolutionException */
94
95 /**
96 * A holder type (used in calls to DatatypeConstructor::addArg())
97 * to allow a Datatype to refer to itself. Self-typed fields of
98 * Datatypes will be properly typed when a Type is created for the
99 * Datatype by the ExprManager (which calls Datatype::resolve()).
100 */
101 class CVC4_PUBLIC DatatypeSelfType {
102 };/* class DatatypeSelfType */
103
104 /**
105 * An unresolved type (used in calls to
106 * DatatypeConstructor::addArg()) to allow a Datatype to refer to
107 * itself or to other mutually-recursive Datatypes. Unresolved-type
108 * fields of Datatypes will be properly typed when a Type is created
109 * for the Datatype by the ExprManager (which calls
110 * Datatype::resolve()).
111 */
112 class CVC4_PUBLIC DatatypeUnresolvedType {
113 std::string d_name;
114 public:
115 inline DatatypeUnresolvedType(std::string name);
116 inline std::string getName() const;
117 };/* class DatatypeUnresolvedType */
118
119 /**
120 * A Datatype constructor argument (i.e., a Datatype field).
121 */
122 class CVC4_PUBLIC DatatypeConstructorArg {
123 friend class DatatypeConstructor;
124 friend class Datatype;
125
126 public:
127 /** Get the name of this constructor argument. */
128 std::string getName() const;
129
130 /**
131 * Get the selector for this constructor argument; this call is
132 * only permitted after resolution.
133 */
134 Expr getSelector() const;
135
136 /**
137 * Get the associated constructor for this constructor argument;
138 * this call is only permitted after resolution.
139 */
140 Expr getConstructor() const;
141
142 /**
143 * Get the type of the selector for this constructor argument;
144 * this call is only permitted after resolution.
145 */
146 SelectorType getType() const;
147
148 /**
149 * Get the range type of this argument.
150 */
151 Type getRangeType() const;
152
153 /**
154 * Returns true iff this constructor argument has been resolved.
155 */
156 bool isResolved() const;
157
158 /** prints this datatype constructor argument to stream */
159 void toStream(std::ostream& out) const;
160
161 private:
162 /** the name of this selector */
163 std::string d_name;
164 /** the selector expression */
165 Expr d_selector;
166 /** the constructor associated with this selector */
167 Expr d_constructor;
168 /** whether this class has been resolved */
169 bool d_resolved;
170 /** is this selector unresolved? */
171 bool isUnresolvedSelf() const;
172 /** constructor */
173 DatatypeConstructorArg(std::string name, Expr selector);
174 };/* class DatatypeConstructorArg */
175
176 class Printer;
177
178 /** sygus datatype constructor printer
179 *
180 * This is a virtual class that is used to specify
181 * a custom printing callback for sygus terms. This is
182 * useful for sygus grammars that include defined
183 * functions or let expressions.
184 */
185 class CVC4_PUBLIC SygusPrintCallback
186 {
187 public:
SygusPrintCallback()188 SygusPrintCallback() {}
~SygusPrintCallback()189 virtual ~SygusPrintCallback() {}
190 /**
191 * Writes the term that sygus datatype expression e
192 * encodes to stream out. p is the printer that
193 * requested that expression e be written on output
194 * stream out. Calls may be made to p to print
195 * subterms of e.
196 */
197 virtual void toStreamSygus(const Printer* p,
198 std::ostream& out,
199 Expr e) const = 0;
200 };
201
202 /**
203 * A constructor for a Datatype.
204 */
205 class CVC4_PUBLIC DatatypeConstructor {
206 friend class Datatype;
207
208 public:
209 /** The type for iterators over constructor arguments. */
210 typedef DatatypeConstructorArgIterator iterator;
211 /** The (const) type for iterators over constructor arguments. */
212 typedef DatatypeConstructorArgIterator const_iterator;
213
214 /**
215 * Create a new Datatype constructor with the given name for the
216 * constructor and the same name (prefixed with "is_") for the
217 * tester. The actual constructor and tester (meaning, the Exprs
218 * representing operators for these entities) aren't created until
219 * resolution time.
220 */
221 explicit DatatypeConstructor(std::string name);
222
223 /**
224 * Create a new Datatype constructor with the given name for the
225 * constructor and the given name for the tester. The actual
226 * constructor and tester aren't created until resolution time.
227 * weight is the value that this constructor carries when computing size.
228 * For example, if A, B, C have weights 0, 1, and 3 respectively, then
229 * C( B( A() ), B( A() ) ) has size 5.
230 */
231 DatatypeConstructor(std::string name,
232 std::string tester,
233 unsigned weight = 1);
234
~DatatypeConstructor()235 ~DatatypeConstructor() {}
236 /**
237 * Add an argument (i.e., a data field) of the given name and type
238 * to this Datatype constructor. Selector names need not be unique;
239 * they are for convenience and pretty-printing only.
240 */
241 void addArg(std::string selectorName, Type selectorType);
242
243 /**
244 * Add an argument (i.e., a data field) of the given name to this
245 * Datatype constructor that refers to an as-yet-unresolved
246 * Datatype (which may be mutually-recursive). Selector names need
247 * not be unique; they are for convenience and pretty-printing only.
248 */
249 void addArg(std::string selectorName, DatatypeUnresolvedType selectorType);
250
251 /**
252 * Add a self-referential (i.e., a data field) of the given name
253 * to this Datatype constructor that refers to the enclosing
254 * Datatype. For example, using the familiar "nat" Datatype, to
255 * create the "pred" field for "succ" constructor, one uses
256 * succ::addArg("pred", DatatypeSelfType())---the actual Type
257 * cannot be passed because the Datatype is still under
258 * construction. Selector names need not be unique; they are for
259 * convenience and pretty-printing only.
260 *
261 * This is a special case of
262 * DatatypeConstructor::addArg(std::string, DatatypeUnresolvedType).
263 */
264 void addArg(std::string selectorName, DatatypeSelfType);
265
266 /** Get the name of this Datatype constructor. */
267 std::string getName() const;
268
269 /**
270 * Get the constructor operator of this Datatype constructor. The
271 * Datatype must be resolved.
272 */
273 Expr getConstructor() const;
274
275 /**
276 * Get the tester operator of this Datatype constructor. The
277 * Datatype must be resolved.
278 */
279 Expr getTester() const;
280
281 /** get sygus op
282 *
283 * This method returns the operator or
284 * term that this constructor represents
285 * in the sygus encoding. This may be a
286 * builtin operator, defined function, variable,
287 * or constant that this constructor encodes in this
288 * deep embedding.
289 */
290 Expr getSygusOp() const;
291 /** is this a sygus identity function?
292 *
293 * This returns true if the sygus operator of this datatype constructor is
294 * of the form (lambda (x) x).
295 */
296 bool isSygusIdFunc() const;
297 /** get sygus print callback
298 *
299 * This class stores custom ways of printing
300 * sygus datatype constructors, for instance,
301 * to handle defined or let expressions that
302 * appear in user-provided grammars.
303 */
304 std::shared_ptr<SygusPrintCallback> getSygusPrintCallback() const;
305 /** get weight
306 *
307 * Get the weight of this constructor. This value is used when computing the
308 * size of datatype terms that involve this constructor.
309 */
310 unsigned getWeight() const;
311
312 /**
313 * Get the tester name for this Datatype constructor.
314 */
315 std::string getTesterName() const;
316
317 /**
318 * Get the number of arguments (so far) of this Datatype constructor.
319 */
320 inline size_t getNumArgs() const;
321
322 /**
323 * Get the specialized constructor type for a parametric
324 * constructor; this call is only permitted after resolution.
325 * Given a (concrete) returnType, the constructor's concrete
326 * type in this parametric datatype is returned.
327 *
328 * For instance, if the datatype is list[T], with constructor
329 * "cons[T]" of type "T -> list[T] -> list[T]", then calling
330 * this function with "list[int]" will return the concrete
331 * "cons" constructor type for lists of int---namely,
332 * "int -> list[int] -> list[int]".
333 */
334 Type getSpecializedConstructorType(Type returnType) const;
335
336 /**
337 * Return the cardinality of this constructor (the product of the
338 * cardinalities of its arguments).
339 */
340 Cardinality getCardinality(Type t) const;
341
342 /**
343 * Return true iff this constructor is finite (it is nullary or
344 * each of its argument types are finite). This function can
345 * only be called for resolved constructors.
346 */
347 bool isFinite(Type t) const;
348 /**
349 * Return true iff this constructor is finite (it is nullary or
350 * each of its argument types are finite) under assumption
351 * uninterpreted sorts are finite. This function can
352 * only be called for resolved constructors.
353 */
354 bool isInterpretedFinite(Type t) const;
355
356 /**
357 * Returns true iff this Datatype constructor has already been
358 * resolved.
359 */
360 inline bool isResolved() const;
361
362 /** Get the beginning iterator over DatatypeConstructor args. */
363 inline iterator begin();
364 /** Get the ending iterator over DatatypeConstructor args. */
365 inline iterator end();
366 /** Get the beginning const_iterator over DatatypeConstructor args. */
367 inline const_iterator begin() const;
368 /** Get the ending const_iterator over DatatypeConstructor args. */
369 inline const_iterator end() const;
370
371 /** Get the ith DatatypeConstructor arg. */
372 const DatatypeConstructorArg& operator[](size_t index) const;
373
374 /**
375 * Get the DatatypeConstructor arg named. This is a linear search
376 * through the arguments, so in the case of multiple,
377 * similarly-named arguments, the first is returned.
378 */
379 const DatatypeConstructorArg& operator[](std::string name) const;
380
381 /**
382 * Get the selector named. This is a linear search
383 * through the arguments, so in the case of multiple,
384 * similarly-named arguments, the selector for the first
385 * is returned.
386 */
387 Expr getSelector(std::string name) const;
388 /**
389 * Get argument type. Returns the return type of the i^th selector of this
390 * constructor.
391 */
392 Type getArgType(unsigned i) const;
393
394 /** get selector internal
395 *
396 * This gets selector for the index^th argument
397 * of this constructor. The type dtt is the datatype
398 * type whose datatype is the owner of this constructor,
399 * where this type may be an instantiated parametric datatype.
400 *
401 * If shared selectors are enabled,
402 * this returns a shared (constructor-agnotic) selector, which
403 * in the terminology of "Datatypes with Shared Selectors", is:
404 * sel_{dtt}^{T,atos(T,C,index)}
405 * where C is this constructor, and T is the type
406 * of the index^th field of this constructor.
407 * The semantics of sel_{dtt}^{T,n}( t ) is the n^th field of
408 * type T of constructor term t if one exists, or is
409 * unconstrained otherwise.
410 */
411 Expr getSelectorInternal(Type dtt, size_t index) const;
412
413 /** get selector index internal
414 *
415 * This gets the argument number of this constructor
416 * that the selector sel accesses. It returns -1 if the
417 * selector sel is not a selector for this constructor.
418 *
419 * In the terminology of "Datatypes with Shared Selectors",
420 * if sel is sel_{dtt}^{T,index} for some (T, index), where
421 * dtt is the datatype type whose datatype is the owner
422 * of this constructor, then this method returns
423 * stoa(T,C,index)
424 */
425 int getSelectorIndexInternal( Expr sel ) const;
426
427 /** involves external type
428 *
429 * Get whether this constructor has a subfield
430 * in any constructor that is not a datatype type.
431 */
432 bool involvesExternalType() const;
433 /** involves external type
434 *
435 * Get whether this constructor has a subfield
436 * in any constructor that is an uninterpreted type.
437 */
438 bool involvesUninterpretedType() const;
439
440 /** set sygus
441 *
442 * Set that this constructor is a sygus datatype constructor that encodes
443 * operator op. spc is the sygus callback of this datatype constructor,
444 * which is stored in a shared pointer.
445 */
446 void setSygus(Expr op, std::shared_ptr<SygusPrintCallback> spc);
447
448 /**
449 * Get the list of arguments to this constructor.
450 */
451 const std::vector<DatatypeConstructorArg>* getArgs() const;
452
453 /** prints this datatype constructor to stream */
454 void toStream(std::ostream& out) const;
455
456 private:
457 /** the name of the constructor */
458 std::string d_name;
459 /** the constructor expression */
460 Expr d_constructor;
461 /** the tester for this constructor */
462 Expr d_tester;
463 /** the arguments of this constructor */
464 std::vector<DatatypeConstructorArg> d_args;
465 /** sygus operator */
466 Expr d_sygus_op;
467 /** sygus print callback */
468 std::shared_ptr<SygusPrintCallback> d_sygus_pc;
469 /** weight */
470 unsigned d_weight;
471
472 /** shared selectors for each type
473 *
474 * This stores the shared (constructor-agnotic)
475 * selectors that access the fields of this datatype.
476 * In the terminology of "Datatypes with Shared Selectors",
477 * this stores:
478 * sel_{dtt}^{T1,atos(T1,C,1)}, ...,
479 * sel_{dtt}^{Tn,atos(Tn,C,n)}
480 * where C is this constructor, which has type
481 * T1 x ... x Tn -> dtt above.
482 * We store this information for (possibly multiple)
483 * datatype types dtt, since this constructor may be
484 * for a parametric datatype, where dtt is an instantiated
485 * parametric datatype.
486 */
487 mutable std::map<Type, std::vector<Expr> > d_shared_selectors;
488 /** for each type, a cache mapping from shared selectors to
489 * its argument index for this constructor.
490 */
491 mutable std::map<Type, std::map<Expr, unsigned> > d_shared_selector_index;
492 /** resolve
493 *
494 * This resolves (initializes) the constructor. For details
495 * on how datatypes and their constructors are resolved, see
496 * documentation for Datatype::resolve.
497 */
498 void resolve(ExprManager* em,
499 DatatypeType self,
500 const std::map<std::string, DatatypeType>& resolutions,
501 const std::vector<Type>& placeholders,
502 const std::vector<Type>& replacements,
503 const std::vector<SortConstructorType>& paramTypes,
504 const std::vector<DatatypeType>& paramReplacements,
505 size_t cindex);
506
507 /** Helper function for resolving parametric datatypes.
508 *
509 * This replaces instances of the SortConstructorType produced for unresolved
510 * parametric datatypes, with the corresponding resolved DatatypeType. For
511 * example, take the parametric definition of a list,
512 * list[T] = cons(car : T, cdr : list[T]) | null.
513 * If "range" is the unresolved parametric datatype:
514 * DATATYPE list =
515 * cons(car: SORT_TAG_1,
516 * cdr: SORT_TAG_2(SORT_TAG_1)) | null END;,
517 * this function will return the resolved type:
518 * DATATYPE list =
519 * cons(car: SORT_TAG_1,
520 * cdr: (list PARAMETERIC_DATATYPE SORT_TAG_1)) | null END;
521 */
522 Type doParametricSubstitution(
523 Type range,
524 const std::vector<SortConstructorType>& paramTypes,
525 const std::vector<DatatypeType>& paramReplacements);
526
527 /** compute the cardinality of this datatype */
528 Cardinality computeCardinality(Type t, std::vector<Type>& processing) const;
529 /** compute whether this datatype is well-founded */
530 bool computeWellFounded(std::vector<Type>& processing) const;
531 /** compute ground term */
532 Expr computeGroundTerm(Type t,
533 std::vector<Type>& processing,
534 std::map<Type, Expr>& gt) const;
535 /** compute shared selectors
536 * This computes the maps d_shared_selectors and d_shared_selector_index.
537 */
538 void computeSharedSelectors(Type domainType) const;
539 };/* class DatatypeConstructor */
540
541 /**
542 * The representation of an inductive datatype.
543 *
544 * This is far more complicated than it first seems. Consider this
545 * datatype definition:
546 *
547 * DATATYPE nat =
548 * succ(pred: nat)
549 * | zero
550 * END;
551 *
552 * You cannot define "nat" until you have a Type for it, but you
553 * cannot have a Type for it until you fill in the type of the "pred"
554 * selector, which needs the Type. So we have a chicken-and-egg
555 * problem. It's even more complicated when we have mutual recursion
556 * between datatypes, since the CVC presentation language does not
557 * require forward-declarations. Here, we define trees of lists that
558 * contain trees of lists (etc):
559 *
560 * DATATYPE
561 * tree = node(left: tree, right: tree) | leaf(list),
562 * list = cons(car: tree, cdr: list) | nil
563 * END;
564 *
565 * Note that while parsing the "tree" definition, we have to take it
566 * on faith that "list" is a valid type. We build Datatype objects to
567 * describe "tree" and "list", and their constructors and constructor
568 * arguments, but leave any unknown types (including self-references)
569 * in an "unresolved" state. After parsing the whole DATATYPE block,
570 * we create a DatatypeType through
571 * ExprManager::mkMutualDatatypeTypes(). The ExprManager creates a
572 * DatatypeType for each, but before "releasing" this type into the
573 * wild, it does a round of in-place "resolution" on each Datatype by
574 * calling Datatype::resolve() with a map of string -> DatatypeType to
575 * allow the datatype to construct the necessary testers and
576 * selectors.
577 *
578 * An additional point to make is that we want to ease the burden on
579 * both the parser AND the users of the CVC4 API, so this class takes
580 * on the task of generating its own selectors and testers, for
581 * instance. That means that, after reifying the Datatype with the
582 * ExprManager, the parser needs to go through the (now-resolved)
583 * Datatype and request the constructor, selector, and tester terms.
584 * See src/parser/parser.cpp for how this is done. For API usage
585 * ideas, see test/unit/util/datatype_black.h.
586 *
587 * Datatypes may also be defined parametrically, such as this example:
588 *
589 * DATATYPE
590 * list[T] = cons(car : T, cdr : list[T]) | null,
591 * tree = node(children : list[tree]) | leaf
592 * END;
593 *
594 * Here, the definition of the parametric datatype list, where T is a type variable.
595 * In other words, this defines a family of types list[C] where C is any concrete
596 * type. Datatypes can be parameterized over multiple type variables using the
597 * syntax sym[ T1, ..., Tn ] = ...,
598 *
599 */
600 class CVC4_PUBLIC Datatype {
601 friend class DatatypeConstructor;
602 public:
603 /**
604 * Get the datatype of a constructor, selector, or tester operator.
605 */
606 static const Datatype& datatypeOf(Expr item) CVC4_PUBLIC;
607
608 /**
609 * Get the index of a constructor or tester in its datatype, or the
610 * index of a selector in its constructor. (Zero is always the
611 * first index.)
612 */
613 static size_t indexOf(Expr item) CVC4_PUBLIC;
614
615 /**
616 * Get the index of constructor corresponding to selector. (Zero is
617 * always the first index.)
618 */
619 static size_t cindexOf(Expr item) CVC4_PUBLIC;
620
621 /**
622 * Same as above, but without checks. These methods should be used by
623 * internal (Node-level) code.
624 */
625 static size_t indexOfInternal(Expr item);
626 static size_t cindexOfInternal(Expr item);
627
628 /** The type for iterators over constructors. */
629 typedef DatatypeConstructorIterator iterator;
630 /** The (const) type for iterators over constructors. */
631 typedef DatatypeConstructorIterator const_iterator;
632
633 /** Create a new Datatype of the given name. */
634 inline explicit Datatype(std::string name, bool isCo = false);
635
636 /**
637 * Create a new Datatype of the given name, with the given
638 * parameterization.
639 */
640 inline Datatype(std::string name, const std::vector<Type>& params, bool isCo = false);
641
642 ~Datatype();
643
644 /** Add a constructor to this Datatype.
645 *
646 * Notice that constructor names need not
647 * be unique; they are for convenience and pretty-printing only.
648 */
649 void addConstructor(const DatatypeConstructor& c);
650
651 /** set sygus
652 *
653 * This marks this datatype as a sygus datatype.
654 * A sygus datatype is one that represents terms of type st
655 * via a deep embedding described in Section 4 of
656 * Reynolds et al. CAV 2015. We say that this sygus datatype
657 * "encodes" its sygus type st in the following.
658 *
659 * st : the type this datatype encodes (this can be Int, Bool, etc.),
660 * bvl : the list of arguments for the synth-fun
661 * allow_const : whether all constants are (implicitly) allowed by the
662 * datatype
663 * allow_all : whether all terms are (implicitly) allowed by the datatype
664 *
665 * Notice that allow_const/allow_all do not reflect the constructors
666 * for this datatype, and instead are used solely for relaxing constraints
667 * when doing solution reconstruction (Figure 5 of Reynolds et al.
668 * CAV 2015).
669 */
670 void setSygus( Type st, Expr bvl, bool allow_const, bool allow_all );
671 /** add sygus constructor
672 *
673 * This adds a sygus constructor to this datatype, where
674 * this datatype should be currently unresolved.
675 *
676 * op : the builtin operator, constant, or variable that
677 * this constructor encodes
678 * cname : the name of the constructor (for printing only)
679 * cargs : the arguments of the constructor
680 * spc : an (optional) callback that is used for custom printing. This is
681 * to accomodate user-provided grammars in the sygus format.
682 *
683 * It should be the case that cargs are sygus datatypes that
684 * encode the arguments of op. For example, a sygus constructor
685 * with op = PLUS should be such that cargs.size()>=2 and
686 * the sygus type of cargs[i] is Real/Int for each i.
687 *
688 * weight denotes the value added by the constructor when computing the size
689 * of datatype terms. Passing a value <0 denotes the default weight for the
690 * constructor, which is 0 for nullary constructors and 1 for non-nullary
691 * constructors.
692 */
693 void addSygusConstructor(Expr op,
694 const std::string& cname,
695 const std::vector<Type>& cargs,
696 std::shared_ptr<SygusPrintCallback> spc = nullptr,
697 int weight = -1);
698
699 /** set that this datatype is a tuple */
700 void setTuple();
701
702 /** set that this datatype is a record */
703 void setRecord();
704
705 /** Get the name of this Datatype. */
706 inline std::string getName() const;
707
708 /** Get the number of constructors (so far) for this Datatype. */
709 inline size_t getNumConstructors() const;
710
711 /** Is this datatype parametric? */
712 inline bool isParametric() const;
713
714 /** Get the nubmer of type parameters */
715 inline size_t getNumParameters() const;
716
717 /** Get parameter */
718 inline Type getParameter( unsigned int i ) const;
719
720 /** Get parameters */
721 inline std::vector<Type> getParameters() const;
722
723 /** is this a co-datatype? */
724 inline bool isCodatatype() const;
725
726 /** is this a sygus datatype? */
727 inline bool isSygus() const;
728
729 /** is this a tuple datatype? */
730 inline bool isTuple() const;
731
732 /** is this a record datatype? */
733 inline bool isRecord() const;
734
735 /** get the record representation for this datatype */
736 inline Record * getRecord() const;
737
738 /**
739 * Return the cardinality of this datatype.
740 * The Datatype must be resolved.
741 *
742 * The version of this method that takes Type t is required
743 * for parametric datatypes, where t is an instantiated
744 * parametric datatype type whose datatype is this class.
745 */
746 Cardinality getCardinality(Type t) const;
747 Cardinality getCardinality() const;
748
749 /**
750 * Return true iff this Datatype has finite cardinality. If the
751 * datatype is not well-founded, this method returns false. The
752 * Datatype must be resolved or an exception is thrown.
753 *
754 * The version of this method that takes Type t is required
755 * for parametric datatypes, where t is an instantiated
756 * parametric datatype type whose datatype is this class.
757 */
758 bool isFinite(Type t) const;
759 bool isFinite() const;
760
761 /**
762 * Return true iff this Datatype is finite (all constructors are
763 * finite, i.e., there are finitely many ground terms) under the
764 * assumption unintepreted sorts are finite. If the
765 * datatype is not well-founded, this method returns false. The
766 * Datatype must be resolved or an exception is thrown.
767 *
768 * The versions of these methods that takes Type t is required
769 * for parametric datatypes, where t is an instantiated
770 * parametric datatype type whose datatype is this class.
771 */
772 bool isInterpretedFinite(Type t) const;
773 bool isInterpretedFinite() const;
774
775 /** is well-founded
776 *
777 * Return true iff this datatype is well-founded (there exist finite
778 * values of this type).
779 * This datatype must be resolved or an exception is thrown.
780 */
781 bool isWellFounded() const;
782
783 /** is recursive singleton
784 *
785 * Return true iff this datatype is a recursive singleton
786 * (a recursive singleton is a recursive datatype with only
787 * one infinite value). For details, see Reynolds et al. CADE 2015.
788 *
789 * The versions of these methods that takes Type t is required
790 * for parametric datatypes, where t is an instantiated
791 * parametric datatype type whose datatype is this class.
792 */
793 bool isRecursiveSingleton(Type t) const;
794 bool isRecursiveSingleton() const;
795
796 /** recursive single arguments
797 *
798 * Get recursive singleton argument types (uninterpreted sorts that the
799 * cardinality of this datatype is dependent upon). For example, for :
800 * stream := cons( head1 : U1, head2 : U2, tail : stream )
801 * Then, the recursive singleton argument types of stream are { U1, U2 },
802 * since if U1 and U2 have cardinality one, then stream has cardinality
803 * one as well.
804 *
805 * The versions of these methods that takes Type t is required
806 * for parametric datatypes, where t is an instantiated
807 * parametric datatype type whose datatype is this class.
808 */
809 unsigned getNumRecursiveSingletonArgTypes(Type t) const;
810 Type getRecursiveSingletonArgType(Type t, unsigned i) const;
811 unsigned getNumRecursiveSingletonArgTypes() const;
812 Type getRecursiveSingletonArgType(unsigned i) const;
813
814 /**
815 * Construct and return a ground term of this Datatype. The
816 * Datatype must be both resolved and well-founded, or else an
817 * exception is thrown.
818 *
819 * This method takes a Type t, which is a datatype type whose
820 * datatype is this class, which may be an instantiated datatype
821 * type if this datatype is parametric.
822 */
823 Expr mkGroundTerm(Type t) const;
824
825 /**
826 * Get the DatatypeType associated to this Datatype. Can only be
827 * called post-resolution.
828 */
829 DatatypeType getDatatypeType() const;
830
831 /**
832 * Get the DatatypeType associated to this (parameterized) Datatype. Can only be
833 * called post-resolution.
834 */
835 DatatypeType getDatatypeType(const std::vector<Type>& params) const;
836
837 /**
838 * Return true iff the two Datatypes are the same.
839 *
840 * We need == for mkConst(Datatype) to properly work---since if the
841 * Datatype Expr requested is the same as an already-existing one,
842 * we need to return that one. For that, we have a hash and
843 * operator==. We provide != for symmetry. We don't provide
844 * operator<() etc. because given two Datatype Exprs, you could
845 * simply compare those rather than the (bare) Datatypes. This
846 * means, though, that Datatype cannot be stored in a sorted list or
847 * RB tree directly, so maybe we can consider adding these
848 * comparison operators later on.
849 */
850 bool operator==(const Datatype& other) const;
851 /** Return true iff the two Datatypes are not the same. */
852 inline bool operator!=(const Datatype& other) const;
853
854 /** Return true iff this Datatype has already been resolved. */
855 inline bool isResolved() const;
856
857 /** Get the beginning iterator over DatatypeConstructors. */
858 inline iterator begin();
859 /** Get the ending iterator over DatatypeConstructors. */
860 inline iterator end();
861 /** Get the beginning const_iterator over DatatypeConstructors. */
862 inline const_iterator begin() const;
863 /** Get the ending const_iterator over DatatypeConstructors. */
864 inline const_iterator end() const;
865
866 /** Get the ith DatatypeConstructor. */
867 const DatatypeConstructor& operator[](size_t index) const;
868
869 /**
870 * Get the DatatypeConstructor named. This is a linear search
871 * through the constructors, so in the case of multiple,
872 * similarly-named constructors, the first is returned.
873 */
874 const DatatypeConstructor& operator[](std::string name) const;
875
876 /**
877 * Get the constructor operator for the named constructor.
878 * This is a linear search through the constructors, so in
879 * the case of multiple, similarly-named constructors, the
880 * first is returned.
881 *
882 * This Datatype must be resolved.
883 */
884 Expr getConstructor(std::string name) const;
885
886 /** get sygus type
887 * This gets the built-in type associated with
888 * this sygus datatype, i.e. the type of the
889 * term that this sygus datatype encodes.
890 */
891 Type getSygusType() const;
892
893 /** get sygus var list
894 * This gets the variable list of the function
895 * to synthesize using this sygus datatype.
896 * For example, if we are synthesizing a binary
897 * function f where solutions are of the form:
898 * f = (lambda (xy) t[x,y])
899 * In this case, this method returns the
900 * bound variable list containing x and y.
901 */
902 Expr getSygusVarList() const;
903 /** get sygus allow constants
904 *
905 * Does this sygus datatype allow constants?
906 * Notice that this is not a property of the
907 * constructors of this datatype. Instead, it is
908 * an auxiliary flag (provided in the call
909 * to setSygus).
910 */
911 bool getSygusAllowConst() const;
912 /** get sygus allow all
913 *
914 * Does this sygus datatype allow all terms?
915 * Notice that this is not a property of the
916 * constructors of this datatype. Instead, it is
917 * an auxiliary flag (provided in the call
918 * to setSygus).
919 */
920 bool getSygusAllowAll() const;
921
922 /** involves external type
923 * Get whether this datatype has a subfield
924 * in any constructor that is not a datatype type.
925 */
926 bool involvesExternalType() const;
927 /** involves uninterpreted type
928 * Get whether this datatype has a subfield
929 * in any constructor that is an uninterpreted type.
930 */
931 bool involvesUninterpretedType() const;
932
933 /**
934 * Get the list of constructors.
935 */
936 const std::vector<DatatypeConstructor>* getConstructors() const;
937
938 /** prints this datatype to stream */
939 void toStream(std::ostream& out) const;
940
941 private:
942 /** name of this datatype */
943 std::string d_name;
944 /** the type parameters of this datatype (if this is a parametric datatype)
945 */
946 std::vector<Type> d_params;
947 /** whether the datatype is a codatatype. */
948 bool d_isCo;
949 /** whether the datatype is a tuple */
950 bool d_isTuple;
951 /** whether the datatype is a record */
952 bool d_isRecord;
953 /** the data of the record for this datatype (if applicable) */
954 Record* d_record;
955 /** the constructors of this datatype */
956 std::vector<DatatypeConstructor> d_constructors;
957 /** whether this datatype has been resolved */
958 bool d_resolved;
959 Type d_self;
960 /** cache for involves external type */
961 bool d_involvesExt;
962 /** cache for involves uninterpreted type */
963 bool d_involvesUt;
964 /** the builtin type that this sygus type encodes */
965 Type d_sygus_type;
966 /** the variable list for the sygus function to synthesize */
967 Expr d_sygus_bvl;
968 /** whether all constants are allowed as solutions */
969 bool d_sygus_allow_const;
970 /** whether all terms are allowed as solutions */
971 bool d_sygus_allow_all;
972
973 /** the cardinality of this datatype
974 * "mutable" because computing the cardinality can be expensive,
975 * and so it's computed just once, on demand---this is the cache
976 */
977 mutable Cardinality d_card;
978
979 /** is this type a recursive singleton type?
980 * The range of this map stores
981 * 0 if the field has not been computed,
982 * 1 if this datatype is a recursive singleton type,
983 * -1 if this datatype is not a recursive singleton type.
984 * For definition of (co)recursive singleton, see
985 * Section 2 of Reynolds et al. CADE 2015.
986 */
987 mutable std::map<Type, int> d_card_rec_singleton;
988 /** if d_card_rec_singleton is true,
989 * This datatype has infinite cardinality if at least one of the
990 * following uninterpreted sorts having cardinality > 1.
991 */
992 mutable std::map<Type, std::vector<Type> > d_card_u_assume;
993 /** cache of whether this datatype is well-founded */
994 mutable int d_well_founded;
995 /** cache of ground term for this datatype */
996 mutable std::map<Type, Expr> d_ground_term;
997 /** cache of shared selectors for this datatype */
998 mutable std::map<Type, std::map<Type, std::map<unsigned, Expr> > >
999 d_shared_sel;
1000
1001 /**
1002 * Datatypes refer to themselves, recursively, and we have a
1003 * chicken-and-egg problem. The DatatypeType around the Datatype
1004 * cannot exist until the Datatype is finalized, and the Datatype
1005 * cannot refer to the DatatypeType representing itself until it
1006 * exists. resolve() is called by the ExprManager when a Type is
1007 * ultimately requested of the Datatype specification (that is, when
1008 * ExprManager::mkDatatypeType() or ExprManager::mkMutualDatatypeTypes()
1009 * is called). Has the effect of freezing the object, too; that is,
1010 * addConstructor() will fail after a call to resolve().
1011 *
1012 * The basic goal of resolution is to assign constructors, selectors,
1013 * and testers. To do this, any UnresolvedType/SelfType references
1014 * must be cleared up. This is the purpose of the "resolutions" map;
1015 * it includes any mutually-recursive datatypes that are currently
1016 * under resolution. The four vectors come in two pairs (so, really
1017 * they are two maps). placeholders->replacements give type variables
1018 * that should be resolved in the case of parametric datatypes.
1019 *
1020 * @param em the ExprManager at play
1021 * @param resolutions a map of strings to DatatypeTypes currently under
1022 * resolution
1023 * @param placeholders the types in these Datatypes under resolution that must
1024 * be replaced
1025 * @param replacements the corresponding replacements
1026 * @param paramTypes the sort constructors in these Datatypes under resolution
1027 * that must be replaced
1028 * @param paramReplacements the corresponding (parametric) DatatypeTypes
1029 */
1030 void resolve(ExprManager* em,
1031 const std::map<std::string, DatatypeType>& resolutions,
1032 const std::vector<Type>& placeholders,
1033 const std::vector<Type>& replacements,
1034 const std::vector<SortConstructorType>& paramTypes,
1035 const std::vector<DatatypeType>& paramReplacements);
1036 friend class ExprManager; // for access to resolve()
1037
1038 /** compute the cardinality of this datatype */
1039 Cardinality computeCardinality(Type t, std::vector<Type>& processing) const;
1040 /** compute whether this datatype is a recursive singleton */
1041 bool computeCardinalityRecSingleton(Type t,
1042 std::vector<Type>& processing,
1043 std::vector<Type>& u_assume) const;
1044 /** compute whether this datatype is well-founded */
1045 bool computeWellFounded(std::vector<Type>& processing) const;
1046 /** compute ground term */
1047 Expr computeGroundTerm(Type t, std::vector<Type>& processing) const;
1048 /** Get the shared selector
1049 *
1050 * This returns the index^th (constructor-agnostic)
1051 * selector for type t. The type dtt is the datatype
1052 * type whose datatype is this class, where this may
1053 * be an instantiated parametric datatype.
1054 *
1055 * In the terminology of "Datatypes with Shared Selectors",
1056 * this returns the term sel_{dtt}^{t,index}.
1057 */
1058 Expr getSharedSelector(Type dtt, Type t, unsigned index) const;
1059 };/* class Datatype */
1060
1061 /**
1062 * A hash function for Datatypes. Needed to store them in hash sets
1063 * and hash maps.
1064 */
1065 struct CVC4_PUBLIC DatatypeHashFunction {
operatorDatatypeHashFunction1066 inline size_t operator()(const Datatype& dt) const {
1067 return std::hash<std::string>()(dt.getName());
1068 }
operatorDatatypeHashFunction1069 inline size_t operator()(const Datatype* dt) const {
1070 return std::hash<std::string>()(dt->getName());
1071 }
operatorDatatypeHashFunction1072 inline size_t operator()(const DatatypeConstructor& dtc) const {
1073 return std::hash<std::string>()(dtc.getName());
1074 }
operatorDatatypeHashFunction1075 inline size_t operator()(const DatatypeConstructor* dtc) const {
1076 return std::hash<std::string>()(dtc->getName());
1077 }
1078 };/* struct DatatypeHashFunction */
1079
1080
1081
1082 /* stores an index to Datatype residing in NodeManager */
1083 class CVC4_PUBLIC DatatypeIndexConstant {
1084 public:
1085 DatatypeIndexConstant(unsigned index);
1086
getIndex()1087 const unsigned getIndex() const { return d_index; }
1088 bool operator==(const DatatypeIndexConstant& uc) const
1089 {
1090 return d_index == uc.d_index;
1091 }
1092 bool operator!=(const DatatypeIndexConstant& uc) const
1093 {
1094 return !(*this == uc);
1095 }
1096 bool operator<(const DatatypeIndexConstant& uc) const
1097 {
1098 return d_index < uc.d_index;
1099 }
1100 bool operator<=(const DatatypeIndexConstant& uc) const
1101 {
1102 return d_index <= uc.d_index;
1103 }
1104 bool operator>(const DatatypeIndexConstant& uc) const
1105 {
1106 return !(*this <= uc);
1107 }
1108 bool operator>=(const DatatypeIndexConstant& uc) const
1109 {
1110 return !(*this < uc);
1111 }
1112 private:
1113 const unsigned d_index;
1114 };/* class DatatypeIndexConstant */
1115
1116 std::ostream& operator<<(std::ostream& out, const DatatypeIndexConstant& dic) CVC4_PUBLIC;
1117
1118 struct CVC4_PUBLIC DatatypeIndexConstantHashFunction {
operatorDatatypeIndexConstantHashFunction1119 inline size_t operator()(const DatatypeIndexConstant& dic) const {
1120 return IntegerHashFunction()(dic.getIndex());
1121 }
1122 };/* struct DatatypeIndexConstantHashFunction */
1123
1124
1125
1126 // FUNCTION DECLARATIONS FOR OUTPUT STREAMS
1127
1128 std::ostream& operator<<(std::ostream& os, const Datatype& dt) CVC4_PUBLIC;
1129 std::ostream& operator<<(std::ostream& os, const DatatypeConstructor& ctor) CVC4_PUBLIC;
1130 std::ostream& operator<<(std::ostream& os, const DatatypeConstructorArg& arg) CVC4_PUBLIC;
1131
1132 // INLINE FUNCTIONS
1133
DatatypeResolutionException(std::string msg)1134 inline DatatypeResolutionException::DatatypeResolutionException(std::string msg) :
1135 Exception(msg) {
1136 }
1137
DatatypeUnresolvedType(std::string name)1138 inline DatatypeUnresolvedType::DatatypeUnresolvedType(std::string name) :
1139 d_name(name) {
1140 }
1141
getName()1142 inline std::string DatatypeUnresolvedType::getName() const { return d_name; }
Datatype(std::string name,bool isCo)1143 inline Datatype::Datatype(std::string name, bool isCo)
1144 : d_name(name),
1145 d_params(),
1146 d_isCo(isCo),
1147 d_isTuple(false),
1148 d_isRecord(false),
1149 d_record(NULL),
1150 d_constructors(),
1151 d_resolved(false),
1152 d_self(),
1153 d_involvesExt(false),
1154 d_involvesUt(false),
1155 d_sygus_allow_const(false),
1156 d_sygus_allow_all(false),
1157 d_card(CardinalityUnknown()),
1158 d_well_founded(0) {}
1159
Datatype(std::string name,const std::vector<Type> & params,bool isCo)1160 inline Datatype::Datatype(std::string name, const std::vector<Type>& params,
1161 bool isCo)
1162 : d_name(name),
1163 d_params(params),
1164 d_isCo(isCo),
1165 d_isTuple(false),
1166 d_isRecord(false),
1167 d_record(NULL),
1168 d_constructors(),
1169 d_resolved(false),
1170 d_self(),
1171 d_involvesExt(false),
1172 d_involvesUt(false),
1173 d_sygus_allow_const(false),
1174 d_sygus_allow_all(false),
1175 d_card(CardinalityUnknown()),
1176 d_well_founded(0) {}
1177
getName()1178 inline std::string Datatype::getName() const { return d_name; }
getNumConstructors()1179 inline size_t Datatype::getNumConstructors() const
1180 {
1181 return d_constructors.size();
1182 }
1183
isParametric()1184 inline bool Datatype::isParametric() const { return d_params.size() > 0; }
getNumParameters()1185 inline size_t Datatype::getNumParameters() const { return d_params.size(); }
getParameter(unsigned int i)1186 inline Type Datatype::getParameter( unsigned int i ) const {
1187 CheckArgument(isParametric(), this,
1188 "Cannot get type parameter of a non-parametric datatype.");
1189 CheckArgument(i < d_params.size(), i,
1190 "Type parameter index out of range for datatype.");
1191 return d_params[i];
1192 }
1193
getParameters()1194 inline std::vector<Type> Datatype::getParameters() const {
1195 CheckArgument(isParametric(), this,
1196 "Cannot get type parameters of a non-parametric datatype.");
1197 return d_params;
1198 }
1199
isCodatatype()1200 inline bool Datatype::isCodatatype() const {
1201 return d_isCo;
1202 }
1203
isSygus()1204 inline bool Datatype::isSygus() const {
1205 return !d_sygus_type.isNull();
1206 }
1207
isTuple()1208 inline bool Datatype::isTuple() const {
1209 return d_isTuple;
1210 }
1211
isRecord()1212 inline bool Datatype::isRecord() const {
1213 return d_isRecord;
1214 }
1215
getRecord()1216 inline Record * Datatype::getRecord() const {
1217 return d_record;
1218 }
1219 inline bool Datatype::operator!=(const Datatype& other) const
1220 {
1221 return !(*this == other);
1222 }
1223
isResolved()1224 inline bool Datatype::isResolved() const { return d_resolved; }
begin()1225 inline Datatype::iterator Datatype::begin()
1226 {
1227 return iterator(d_constructors, true);
1228 }
1229
end()1230 inline Datatype::iterator Datatype::end()
1231 {
1232 return iterator(d_constructors, false);
1233 }
1234
begin()1235 inline Datatype::const_iterator Datatype::begin() const
1236 {
1237 return const_iterator(d_constructors, true);
1238 }
1239
end()1240 inline Datatype::const_iterator Datatype::end() const
1241 {
1242 return const_iterator(d_constructors, false);
1243 }
1244
isResolved()1245 inline bool DatatypeConstructor::isResolved() const
1246 {
1247 return !d_tester.isNull();
1248 }
1249
getNumArgs()1250 inline size_t DatatypeConstructor::getNumArgs() const { return d_args.size(); }
isResolved()1251 inline bool DatatypeConstructorArg::isResolved() const
1252 {
1253 // We could just write:
1254 //
1255 // return !d_selector.isNull() && d_selector.getType().isSelector();
1256 //
1257 // HOWEVER, this causes problems in ExprManager tear-down, because
1258 // the attributes are removed before the pool is purged. When the
1259 // pool is purged, this triggers an equality test between Datatypes,
1260 // and this triggers a call to isResolved(), which breaks because
1261 // d_selector has no type after attributes are stripped.
1262 //
1263 // This problem, coupled with the fact that this function is called
1264 // _often_, means we should just use a boolean flag.
1265 //
1266 return d_resolved;
1267 }
1268
begin()1269 inline DatatypeConstructor::iterator DatatypeConstructor::begin()
1270 {
1271 return iterator(d_args, true);
1272 }
1273
end()1274 inline DatatypeConstructor::iterator DatatypeConstructor::end()
1275 {
1276 return iterator(d_args, false);
1277 }
1278
begin()1279 inline DatatypeConstructor::const_iterator DatatypeConstructor::begin() const
1280 {
1281 return const_iterator(d_args, true);
1282 }
1283
end()1284 inline DatatypeConstructor::const_iterator DatatypeConstructor::end() const
1285 {
1286 return const_iterator(d_args, false);
1287 }
1288
1289 }/* CVC4 namespace */
1290
1291 #endif /* __CVC4__DATATYPE_H */
1292