src/expr/datatype.h

   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
  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
  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 class DTypeSelector;
 105
 106 /**
 107  * An unresolved type (used in calls to
 108  * DatatypeConstructor::addArg()) to allow a Datatype to refer to
 109  * itself or to other mutually-recursive Datatypes.  Unresolved-type
 110  * fields of Datatypes will be properly typed when a Type is created
 111  * for the Datatype by the ExprManager (which calls
 112  * Datatype::resolve()).
 113  */
 114 class CVC4_PUBLIC DatatypeUnresolvedType {
 115   std::string d_name;
 116 public:
 117   inline DatatypeUnresolvedType(std::string name);
 118   inline std::string getName() const;
 119 };/* class DatatypeUnresolvedType */
 120
 121 /**
 122  * A Datatype constructor argument (i.e., a Datatype field).
 123  */
 124 class CVC4_PUBLIC DatatypeConstructorArg {
 125   friend class DatatypeConstructor;
 126   friend class Datatype;
 127
 128  public:
 129   /** Get the name of this constructor argument. */
 130   std::string getName() const;
 131
 132   /**
 133    * Get the selector for this constructor argument; this call is
 134    * only permitted after resolution.
 135    */
 136   Expr getSelector() const;
 137
 138   /**
 139    * Get the associated constructor for this constructor argument;
 140    * this call is only permitted after resolution.
 141    */
 142   Expr getConstructor() const;
 143
 144   /**
 145    * Get the type of the selector for this constructor argument;
 146    * this call is only permitted after resolution.
 147    */
 148   SelectorType getType() const;
 149
 150   /**
 151    * Get the range type of this argument.
 152    */
 153   Type getRangeType() const;
 154
 155   /**
 156    * Returns true iff this constructor argument has been resolved.
 157    */
 158   bool isResolved() const;
 159
 160   /** prints this datatype constructor argument to stream */
 161   void toStream(std::ostream& out) const;
 162
 163  private:
 164   /** The internal representation */
 165   std::shared_ptr<DTypeSelector> d_internal;
 166   /** The selector */
 167   Expr d_selector;
 168   /** is this selector unresolved? */
 169   bool isUnresolvedSelf() const;
 170   /** constructor */
 171   DatatypeConstructorArg(std::string name, Expr selector);
 172 };/* class DatatypeConstructorArg */
 173
 174 class Printer;
 175
 176 /** sygus datatype constructor printer
 177  *
 178  * This is a virtual class that is used to specify
 179  * a custom printing callback for sygus terms. This is
 180  * useful for sygus grammars that include defined
 181  * functions or let expressions.
 182  */
 183 class CVC4_PUBLIC SygusPrintCallback
 184 {
 185  public:
 186   SygusPrintCallback() {}
 187   virtual ~SygusPrintCallback() {}
 188   /**
 189    * Writes the term that sygus datatype expression e
 190    * encodes to stream out. p is the printer that
 191    * requested that expression e be written on output
 192    * stream out. Calls may be made to p to print
 193    * subterms of e.
 194    */
 195   virtual void toStreamSygus(const Printer* p,
 196                              std::ostream& out,
 197                              Expr e) const = 0;
 198 };
 199
 200 class DTypeConstructor;
 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
 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   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   bool isResolved() const;
 361
 362   /** Get the beginning iterator over DatatypeConstructor args. */
 363   iterator begin();
 364   /** Get the ending iterator over DatatypeConstructor args. */
 365   iterator end();
 366   /** Get the beginning const_iterator over DatatypeConstructor args. */
 367   const_iterator begin() const;
 368   /** Get the ending const_iterator over DatatypeConstructor args. */
 369   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 internal representation */
 458   std::shared_ptr<DTypeConstructor> d_internal;
 459   /** the name of the tester */
 460   std::string d_testerName;
 461   /** The constructor */
 462   Expr d_constructor;
 463   /** the arguments of this constructor */
 464   std::vector<DatatypeConstructorArg> d_args;
 465   /** sygus print callback */
 466   std::shared_ptr<SygusPrintCallback> d_sygus_pc;
 467 };/* class DatatypeConstructor */
 468
 469 class DType;
 470
 471 /**
 472  * The representation of an inductive datatype.
 473  *
 474  * This is far more complicated than it first seems.  Consider this
 475  * datatype definition:
 476  *
 477  *   DATATYPE nat =
 478  *     succ(pred: nat)
 479  *   | zero
 480  *   END;
 481  *
 482  * You cannot define "nat" until you have a Type for it, but you
 483  * cannot have a Type for it until you fill in the type of the "pred"
 484  * selector, which needs the Type.  So we have a chicken-and-egg
 485  * problem.  It's even more complicated when we have mutual recursion
 486  * between datatypes, since the CVC presentation language does not
 487  * require forward-declarations.  Here, we define trees of lists that
 488  * contain trees of lists (etc):
 489  *
 490  *   DATATYPE
 491  *     tree = node(left: tree, right: tree) | leaf(list),
 492  *     list = cons(car: tree, cdr: list) | nil
 493  *   END;
 494  *
 495  * Note that while parsing the "tree" definition, we have to take it
 496  * on faith that "list" is a valid type.  We build Datatype objects to
 497  * describe "tree" and "list", and their constructors and constructor
 498  * arguments, but leave any unknown types (including self-references)
 499  * in an "unresolved" state.  After parsing the whole DATATYPE block,
 500  * we create a DatatypeType through
 501  * ExprManager::mkMutualDatatypeTypes().  The ExprManager creates a
 502  * DatatypeType for each, but before "releasing" this type into the
 503  * wild, it does a round of in-place "resolution" on each Datatype by
 504  * calling Datatype::resolve() with a map of string -> DatatypeType to
 505  * allow the datatype to construct the necessary testers and
 506  * selectors.
 507  *
 508  * An additional point to make is that we want to ease the burden on
 509  * both the parser AND the users of the CVC4 API, so this class takes
 510  * on the task of generating its own selectors and testers, for
 511  * instance.  That means that, after reifying the Datatype with the
 512  * ExprManager, the parser needs to go through the (now-resolved)
 513  * Datatype and request the constructor, selector, and tester terms.
 514  * See src/parser/parser.cpp for how this is done.  For API usage
 515  * ideas, see test/unit/util/datatype_black.h.
 516  *
 517  * Datatypes may also be defined parametrically, such as this example:
 518  *
 519  *  DATATYPE
 520  *    list[T] = cons(car : T, cdr : list[T]) | null,
 521  *    tree = node(children : list[tree]) | leaf
 522  *  END;
 523  *
 524  * Here, the definition of the parametric datatype list, where T is a type variable.
 525  * In other words, this defines a family of types list[C] where C is any concrete
 526  * type.  Datatypes can be parameterized over multiple type variables using the
 527  * syntax sym[ T1, ..., Tn ] = ...,
 528  *
 529  */
 530 class CVC4_PUBLIC Datatype {
 531   friend class DatatypeConstructor;
 532   friend class ExprManager;  // for access to resolve()
 533   friend class NodeManager;  // temporary, for access to d_internal
 534  public:
 535   /**
 536    * Get the datatype of a constructor, selector, or tester operator.
 537    */
 538   static const Datatype& datatypeOf(Expr item) CVC4_PUBLIC;
 539
 540   /**
 541    * Get the index of a constructor or tester in its datatype, or the
 542    * index of a selector in its constructor.  (Zero is always the
 543    * first index.)
 544    */
 545   static size_t indexOf(Expr item) CVC4_PUBLIC;
 546
 547   /**
 548    * Get the index of constructor corresponding to selector.  (Zero is
 549    * always the first index.)
 550    */
 551   static size_t cindexOf(Expr item) CVC4_PUBLIC;
 552
 553   /**
 554    * Same as above, but without checks. These methods should be used by
 555    * internal (Node-level) code.
 556    */
 557   static size_t indexOfInternal(Expr item);
 558   static size_t cindexOfInternal(Expr item);
 559
 560   /** The type for iterators over constructors. */
 561   typedef DatatypeConstructorIterator iterator;
 562   /** The (const) type for iterators over constructors. */
 563   typedef DatatypeConstructorIterator const_iterator;
 564
 565   /** Create a new Datatype of the given name. */
 566   explicit Datatype(ExprManager* em, std::string name, bool isCo = false);
 567
 568   /**
 569    * Create a new Datatype of the given name, with the given
 570    * parameterization.
 571    */
 572   Datatype(ExprManager* em,
 573            std::string name,
 574            const std::vector<Type>& params,
 575            bool isCo = false);
 576
 577   ~Datatype();
 578
 579   /** Add a constructor to this Datatype.
 580    *
 581    * Notice that constructor names need not
 582    * be unique; they are for convenience and pretty-printing only.
 583    */
 584   void addConstructor(const DatatypeConstructor& c);
 585
 586   /** set sygus
 587    *
 588    * This marks this datatype as a sygus datatype.
 589    * A sygus datatype is one that represents terms of type st
 590    * via a deep embedding described in Section 4 of
 591    * Reynolds et al. CAV 2015. We say that this sygus datatype
 592    * "encodes" its sygus type st in the following.
 593    *
 594    * st : the type this datatype encodes (this can be Int, Bool, etc.),
 595    * bvl : the list of arguments for the synth-fun
 596    * allow_const : whether all constants are (implicitly) allowed by the
 597    * datatype
 598    * allow_all : whether all terms are (implicitly) allowed by the datatype
 599    *
 600    * Notice that allow_const/allow_all do not reflect the constructors
 601    * for this datatype, and instead are used solely for relaxing constraints
 602    * when doing solution reconstruction (Figure 5 of Reynolds et al.
 603    * CAV 2015).
 604    */
 605   void setSygus( Type st, Expr bvl, bool allow_const, bool allow_all );
 606   /** add sygus constructor
 607    *
 608    * This adds a sygus constructor to this datatype, where
 609    * this datatype should be currently unresolved.
 610    *
 611    * op : the builtin operator, constant, or variable that
 612    *      this constructor encodes
 613    * cname : the name of the constructor (for printing only)
 614    * cargs : the arguments of the constructor
 615    * spc : an (optional) callback that is used for custom printing. This is
 616    *       to accomodate user-provided grammars in the sygus format.
 617    *
 618    * It should be the case that cargs are sygus datatypes that
 619    * encode the arguments of op. For example, a sygus constructor
 620    * with op = PLUS should be such that cargs.size()>=2 and
 621    * the sygus type of cargs[i] is Real/Int for each i.
 622    *
 623    * weight denotes the value added by the constructor when computing the size
 624    * of datatype terms. Passing a value <0 denotes the default weight for the
 625    * constructor, which is 0 for nullary constructors and 1 for non-nullary
 626    * constructors.
 627    */
 628   void addSygusConstructor(Expr op,
 629                            const std::string& cname,
 630                            const std::vector<Type>& cargs,
 631                            std::shared_ptr<SygusPrintCallback> spc = nullptr,
 632                            int weight = -1);
 633
 634   /** set that this datatype is a tuple */
 635   void setTuple();
 636
 637   /** set that this datatype is a record */
 638   void setRecord();
 639
 640   /** Get the name of this Datatype. */
 641   std::string getName() const;
 642
 643   /** Get the number of constructors (so far) for this Datatype. */
 644   size_t getNumConstructors() const;
 645
 646   /** Is this datatype parametric? */
 647   bool isParametric() const;
 648
 649   /** Get the nubmer of type parameters */
 650   size_t getNumParameters() const;
 651
 652   /** Get parameter */
 653   Type getParameter(unsigned int i) const;
 654
 655   /** Get parameters */
 656   std::vector<Type> getParameters() const;
 657
 658   /** is this a co-datatype? */
 659   bool isCodatatype() const;
 660
 661   /** is this a sygus datatype? */
 662   bool isSygus() const;
 663
 664   /** is this a tuple datatype? */
 665   bool isTuple() const;
 666
 667   /** is this a record datatype? */
 668   bool isRecord() const;
 669
 670   /** get the record representation for this datatype */
 671   Record* getRecord() const;
 672
 673   /**
 674    * Return the cardinality of this datatype.
 675    * The Datatype must be resolved.
 676    *
 677    * The version of this method that takes Type t is required
 678    * for parametric datatypes, where t is an instantiated
 679    * parametric datatype type whose datatype is this class.
 680    */
 681   Cardinality getCardinality(Type t) const;
 682   Cardinality getCardinality() const;
 683
 684   /**
 685    * Return true iff this Datatype has finite cardinality. If the
 686    * datatype is not well-founded, this method returns false. The
 687    * Datatype must be resolved or an exception is thrown.
 688    *
 689    * The version of this method that takes Type t is required
 690    * for parametric datatypes, where t is an instantiated
 691    * parametric datatype type whose datatype is this class.
 692    */
 693   bool isFinite(Type t) const;
 694   bool isFinite() const;
 695
 696   /**
 697    * Return true iff this  Datatype is finite (all constructors are
 698    * finite, i.e., there  are finitely  many ground terms) under the
 699    * assumption unintepreted sorts are finite. If the
 700    * datatype is  not well-founded, this method returns false.  The
 701    * Datatype must be resolved or an exception is thrown.
 702    *
 703    * The versions of these methods that takes Type t is required
 704    * for parametric datatypes, where t is an instantiated
 705    * parametric datatype type whose datatype is this class.
 706    */
 707   bool isInterpretedFinite(Type t) const;
 708   bool isInterpretedFinite() const;
 709
 710   /** is well-founded
 711    *
 712    * Return true iff this datatype is well-founded (there exist finite
 713    * values of this type).
 714    * This datatype must be resolved or an exception is thrown.
 715    */
 716   bool isWellFounded() const;
 717
 718   /** is recursive singleton
 719    *
 720    * Return true iff this datatype is a recursive singleton
 721    * (a recursive singleton is a recursive datatype with only
 722    * one infinite value). For details, see Reynolds et al. CADE 2015.
 723    *
 724    * The versions of these methods that takes Type t is required
 725    * for parametric datatypes, where t is an instantiated
 726    * parametric datatype type whose datatype is this class.
 727    */
 728   bool isRecursiveSingleton(Type t) const;
 729   bool isRecursiveSingleton() const;
 730
 731   /** recursive single arguments
 732    *
 733    * Get recursive singleton argument types (uninterpreted sorts that the
 734    * cardinality of this datatype is dependent upon). For example, for :
 735    *   stream :=  cons( head1 : U1, head2 : U2, tail : stream )
 736    * Then, the recursive singleton argument types of stream are { U1, U2 },
 737    * since if U1 and U2 have cardinality one, then stream has cardinality
 738    * one as well.
 739    *
 740    * The versions of these methods that takes Type t is required
 741    * for parametric datatypes, where t is an instantiated
 742    * parametric datatype type whose datatype is this class.
 743   */
 744   unsigned getNumRecursiveSingletonArgTypes(Type t) const;
 745   Type getRecursiveSingletonArgType(Type t, unsigned i) const;
 746   unsigned getNumRecursiveSingletonArgTypes() const;
 747   Type getRecursiveSingletonArgType(unsigned i) const;
 748
 749   /**
 750    * Construct and return a ground term of this Datatype.  The
 751    * Datatype must be both resolved and well-founded, or else an
 752    * exception is thrown.
 753    *
 754    * This method takes a Type t, which is a datatype type whose
 755    * datatype is this class, which may be an instantiated datatype
 756    * type if this datatype is parametric.
 757    */
 758   Expr mkGroundTerm(Type t) const;
 759   /** Make ground value
 760    *
 761    * Same as above, but constructs a constant value instead of a ground term.
 762    * These two notions typically coincide. However, for uninterpreted sorts,
 763    * they do not: mkGroundTerm returns a fresh variable whereas mkValue returns
 764    * an uninterpreted constant. The motivation for mkGroundTerm is that
 765    * unintepreted constants should never appear in lemmas. The motivation for
 766    * mkGroundValue is for things like type enumeration and model construction.
 767    */
 768   Expr mkGroundValue(Type t) const;
 769
 770   /**
 771    * Get the DatatypeType associated to this Datatype.  Can only be
 772    * called post-resolution.
 773    */
 774   DatatypeType getDatatypeType() const;
 775
 776   /**
 777    * Get the DatatypeType associated to this (parameterized) Datatype.  Can only be
 778    * called post-resolution.
 779    */
 780   DatatypeType getDatatypeType(const std::vector<Type>& params) const;
 781
 782   /**
 783    * Return true iff the two Datatypes are the same.
 784    *
 785    * We need == for mkConst(Datatype) to properly work---since if the
 786    * Datatype Expr requested is the same as an already-existing one,
 787    * we need to return that one.  For that, we have a hash and
 788    * operator==.  We provide != for symmetry.  We don't provide
 789    * operator<() etc. because given two Datatype Exprs, you could
 790    * simply compare those rather than the (bare) Datatypes.  This
 791    * means, though, that Datatype cannot be stored in a sorted list or
 792    * RB tree directly, so maybe we can consider adding these
 793    * comparison operators later on.
 794    */
 795   bool operator==(const Datatype& other) const;
 796   /** Return true iff the two Datatypes are not the same. */
 797   bool operator!=(const Datatype& other) const;
 798
 799   /** Return true iff this Datatype has already been resolved. */
 800   bool isResolved() const;
 801
 802   /** Get the beginning iterator over DatatypeConstructors. */
 803   iterator begin();
 804   /** Get the ending iterator over DatatypeConstructors. */
 805   iterator end();
 806   /** Get the beginning const_iterator over DatatypeConstructors. */
 807   const_iterator begin() const;
 808   /** Get the ending const_iterator over DatatypeConstructors. */
 809   const_iterator end() const;
 810
 811   /** Get the ith DatatypeConstructor. */
 812   const DatatypeConstructor& operator[](size_t index) const;
 813
 814   /**
 815    * Get the DatatypeConstructor named.  This is a linear search
 816    * through the constructors, so in the case of multiple,
 817    * similarly-named constructors, the first is returned.
 818    */
 819   const DatatypeConstructor& operator[](std::string name) const;
 820
 821   /**
 822    * Get the constructor operator for the named constructor.
 823    * This is a linear search through the constructors, so in
 824    * the case of multiple, similarly-named constructors, the
 825    * first is returned.
 826    *
 827    * This Datatype must be resolved.
 828    */
 829   Expr getConstructor(std::string name) const;
 830
 831   /** get sygus type
 832    * This gets the built-in type associated with
 833    * this sygus datatype, i.e. the type of the
 834    * term that this sygus datatype encodes.
 835    */
 836   Type getSygusType() const;
 837
 838   /** get sygus var list
 839    * This gets the variable list of the function
 840    * to synthesize using this sygus datatype.
 841    * For example, if we are synthesizing a binary
 842    * function f where solutions are of the form:
 843    *   f = (lambda (xy) t[x,y])
 844    * In this case, this method returns the
 845    * bound variable list containing x and y.
 846    */
 847   Expr getSygusVarList() const;
 848   /** get sygus allow constants
 849    *
 850    * Does this sygus datatype allow constants?
 851    * Notice that this is not a property of the
 852    * constructors of this datatype. Instead, it is
 853    * an auxiliary flag (provided in the call
 854    * to setSygus).
 855    */
 856   bool getSygusAllowConst() const;
 857   /** get sygus allow all
 858    *
 859    * Does this sygus datatype allow all terms?
 860    * Notice that this is not a property of the
 861    * constructors of this datatype. Instead, it is
 862    * an auxiliary flag (provided in the call
 863    * to setSygus).
 864    */
 865   bool getSygusAllowAll() const;
 866
 867   /** involves external type
 868    * Get whether this datatype has a subfield
 869    * in any constructor that is not a datatype type.
 870    */
 871   bool involvesExternalType() const;
 872   /** involves uninterpreted type
 873    * Get whether this datatype has a subfield
 874    * in any constructor that is an uninterpreted type.
 875    */
 876   bool involvesUninterpretedType() const;
 877
 878   /**
 879    * Get the list of constructors.
 880    */
 881   const std::vector<DatatypeConstructor>* getConstructors() const;
 882
 883   /** prints this datatype to stream */
 884   void toStream(std::ostream& out) const;
 885
 886  private:
 887   /** The expression manager that created this datatype */
 888   ExprManager* d_em;
 889   /** The internal representation */
 890   std::shared_ptr<DType> d_internal;
 891   /** self type */
 892   Type d_self;
 893   /** the data of the record for this datatype (if applicable) */
 894   Record* d_record;
 895   /** whether the datatype is a record */
 896   bool d_isRecord;
 897   /** the constructors of this datatype */
 898   std::vector<DatatypeConstructor> d_constructors;
 899   /**
 900    * Datatypes refer to themselves, recursively, and we have a
 901    * chicken-and-egg problem.  The DatatypeType around the Datatype
 902    * cannot exist until the Datatype is finalized, and the Datatype
 903    * cannot refer to the DatatypeType representing itself until it
 904    * exists.  resolve() is called by the ExprManager when a Type is
 905    * ultimately requested of the Datatype specification (that is, when
 906    * ExprManager::mkDatatypeType() or ExprManager::mkMutualDatatypeTypes()
 907    * is called).  Has the effect of freezing the object, too; that is,
 908    * addConstructor() will fail after a call to resolve().
 909    *
 910    * The basic goal of resolution is to assign constructors, selectors,
 911    * and testers.  To do this, any UnresolvedType/SelfType references
 912    * must be cleared up.  This is the purpose of the "resolutions" map;
 913    * it includes any mutually-recursive datatypes that are currently
 914    * under resolution.  The four vectors come in two pairs (so, really
 915    * they are two maps).  placeholders->replacements give type variables
 916    * that should be resolved in the case of parametric datatypes.
 917    *
 918    * @param resolutions a map of strings to DatatypeTypes currently under
 919    * resolution
 920    * @param placeholders the types in these Datatypes under resolution that must
 921    * be replaced
 922    * @param replacements the corresponding replacements
 923    * @param paramTypes the sort constructors in these Datatypes under resolution
 924    * that must be replaced
 925    * @param paramReplacements the corresponding (parametric) DatatypeTypes
 926    */
 927   void resolve(const std::map<std::string, DatatypeType>& resolutions,
 928                const std::vector<Type>& placeholders,
 929                const std::vector<Type>& replacements,
 930                const std::vector<SortConstructorType>& paramTypes,
 931                const std::vector<DatatypeType>& paramReplacements);
 932 };/* class Datatype */
 933
 934 /**
 935  * A hash function for Datatypes.  Needed to store them in hash sets
 936  * and hash maps.
 937  */
 938 struct CVC4_PUBLIC DatatypeHashFunction {
 939   inline size_t operator()(const Datatype& dt) const {
 940     return std::hash<std::string>()(dt.getName());
 941   }
 942   inline size_t operator()(const Datatype* dt) const {
 943     return std::hash<std::string>()(dt->getName());
 944   }
 945   inline size_t operator()(const DatatypeConstructor& dtc) const {
 946     return std::hash<std::string>()(dtc.getName());
 947   }
 948   inline size_t operator()(const DatatypeConstructor* dtc) const {
 949     return std::hash<std::string>()(dtc->getName());
 950   }
 951 };/* struct DatatypeHashFunction */
 952
 953
 954
 955 /* stores an index to Datatype residing in NodeManager */
 956 class CVC4_PUBLIC DatatypeIndexConstant {
 957  public:
 958   DatatypeIndexConstant(unsigned index);
 959
 960   unsigned getIndex() const { return d_index; }
 961   bool operator==(const DatatypeIndexConstant& uc) const
 962   {
 963     return d_index == uc.d_index;
 964   }
 965   bool operator!=(const DatatypeIndexConstant& uc) const
 966   {
 967     return !(*this == uc);
 968   }
 969   bool operator<(const DatatypeIndexConstant& uc) const
 970   {
 971     return d_index < uc.d_index;
 972   }
 973   bool operator<=(const DatatypeIndexConstant& uc) const
 974   {
 975     return d_index <= uc.d_index;
 976   }
 977   bool operator>(const DatatypeIndexConstant& uc) const
 978   {
 979     return !(*this <= uc);
 980   }
 981   bool operator>=(const DatatypeIndexConstant& uc) const
 982   {
 983     return !(*this < uc);
 984   }
 985 private:
 986   const unsigned d_index;
 987 };/* class DatatypeIndexConstant */
 988
 989 std::ostream& operator<<(std::ostream& out, const DatatypeIndexConstant& dic) CVC4_PUBLIC;
 990
 991 struct CVC4_PUBLIC DatatypeIndexConstantHashFunction {
 992   inline size_t operator()(const DatatypeIndexConstant& dic) const {
 993     return IntegerHashFunction()(dic.getIndex());
 994   }
 995 };/* struct DatatypeIndexConstantHashFunction */
 996
 997
 998
 999 // FUNCTION DECLARATIONS FOR OUTPUT STREAMS
1000
1001 std::ostream& operator<<(std::ostream& os, const Datatype& dt) CVC4_PUBLIC;
1002 std::ostream& operator<<(std::ostream& os, const DatatypeConstructor& ctor) CVC4_PUBLIC;
1003 std::ostream& operator<<(std::ostream& os, const DatatypeConstructorArg& arg) CVC4_PUBLIC;
1004
1005 // INLINE FUNCTIONS
1006
1007 inline DatatypeResolutionException::DatatypeResolutionException(std::string msg) :
1008   Exception(msg) {
1009 }
1010
1011 inline DatatypeUnresolvedType::DatatypeUnresolvedType(std::string name) :
1012   d_name(name) {
1013 }
1014
1015 inline std::string DatatypeUnresolvedType::getName() const { return d_name; }
1016
1017
1018 }/* CVC4 namespace */
1019
1020 #endif /* CVC4__DATATYPE_H */