src/expr/type.h

   1 /*********************                                                        */
   2 /*! \file type.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Dejan Jovanovic, Andrew Reynolds
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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 Interface for expression types.
  13  **
  14  ** Interface for expression types
  15  **/
  16
  17 #include "cvc4_public.h"
  18
  19 #ifndef CVC4__TYPE_H
  20 #define CVC4__TYPE_H
  21
  22 #include <climits>
  23 #include <cstdint>
  24 #include <string>
  25 #include <vector>
  26
  27 #include "util/cardinality.h"
  28
  29 namespace CVC4 {
  30
  31 class NodeManager;
  32 class CVC4_PUBLIC ExprManager;
  33 class CVC4_PUBLIC Expr;
  34 class TypeNode;
  35 struct CVC4_PUBLIC ExprManagerMapCollection;
  36
  37 class CVC4_PUBLIC SmtEngine;
  38
  39 class CVC4_PUBLIC Datatype;
  40 class Record;
  41
  42 template <bool ref_count>
  43 class NodeTemplate;
  44
  45 class BooleanType;
  46 class IntegerType;
  47 class RealType;
  48 class StringType;
  49 class RegExpType;
  50 class RoundingModeType;
  51 class BitVectorType;
  52 class ArrayType;
  53 class SetType;
  54 class DatatypeType;
  55 class ConstructorType;
  56 class SelectorType;
  57 class TesterType;
  58 class FunctionType;
  59 class SExprType;
  60 class SortType;
  61 class SortConstructorType;
  62 class Type;
  63
  64 /** Hash function for Types */
  65 struct CVC4_PUBLIC TypeHashFunction {
  66   /** Return a hash code for type t */
  67   size_t operator()(const CVC4::Type& t) const;
  68 };/* struct TypeHashFunction */
  69
  70 /**
  71  * Output operator for types
  72  * @param out the stream to output to
  73  * @param t the type to output
  74  * @return the stream
  75  */
  76 std::ostream& operator<<(std::ostream& out, const Type& t) CVC4_PUBLIC;
  77
  78 namespace expr {
  79   TypeNode exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* nm, ExprManagerMapCollection& vmap);
  80 }/* CVC4::expr namespace */
  81
  82 /**
  83  * Class encapsulating CVC4 expression types.
  84  */
  85 class CVC4_PUBLIC Type {
  86
  87   friend class SmtEngine;
  88   friend class ExprManager;
  89   friend class NodeManager;
  90   friend class TypeNode;
  91   friend std::ostream& CVC4::operator<<(std::ostream& out, const Type& t);
  92   friend TypeNode expr::exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* nm, ExprManagerMapCollection& vmap);
  93
  94 protected:
  95
  96   /** The internal expression representation */
  97   TypeNode* d_typeNode;
  98
  99   /** The responsible expression manager */
 100   NodeManager* d_nodeManager;
 101
 102   /**
 103    * Construct a new type given the typeNode, for internal use only.
 104    * @param typeNode the TypeNode to use
 105    * @return the Type corresponding to the TypeNode
 106    */
 107   Type makeType(const TypeNode& typeNode) const;
 108
 109   /**
 110    * Constructor for internal purposes.
 111    * @param em the expression manager that handles this expression
 112    * @param typeNode the actual TypeNode pointer for this type
 113    */
 114   Type(NodeManager* em, TypeNode* typeNode);
 115
 116   /** Accessor for derived classes */
 117   static TypeNode* getTypeNode(const Type& t) { return t.d_typeNode; }
 118  public:
 119   /** Force a virtual destructor for safety. */
 120   virtual ~Type();
 121
 122   /** Default constructor */
 123   Type();
 124
 125   /**
 126    * Copy constructor.
 127    * @param t the type to make a copy of
 128    */
 129   Type(const Type& t);
 130
 131   /**
 132    * Check whether this is a null type
 133    * @return true if type is null
 134    */
 135   bool isNull() const;
 136
 137   /**
 138    * Return the cardinality of this type.
 139    */
 140   Cardinality getCardinality() const;
 141
 142   /**
 143    * Is this type finite? This assumes uninterpreted sorts have infinite
 144    * cardinality.
 145    */
 146   bool isFinite() const;
 147
 148   /**
 149    * Is this type interpreted as being finite.
 150    * If finite model finding is enabled, this assumes all uninterpreted sorts
 151    *   are interpreted as finite.
 152    */
 153   bool isInterpretedFinite() const;
 154
 155   /**
 156    * Is this a well-founded type?
 157    */
 158   bool isWellFounded() const;
 159
 160   /**
 161    * Is this a first-class type?
 162    *
 163    * First-class types are types for which:
 164    * (1) we handle equalities between terms of that type, and
 165    * (2) they are allowed to be parameters of parametric types (e.g. index or
 166    * element types of arrays).
 167    *
 168    * Examples of types that are not first-class include constructor types,
 169    * selector types, tester types, regular expressions and SExprs.
 170    */
 171   bool isFirstClass() const;
 172
 173   /**
 174    * Is this a function-LIKE type?
 175    *
 176    * Anything function-like except arrays (e.g., datatype selectors) is
 177    * considered a function here. Function-like terms can not be the argument
 178    * or return value for any term that is function-like.
 179    * This is mainly to avoid higher order.
 180    *
 181    * Note that arrays are explicitly not considered function-like here.
 182    *
 183    * @return true if this is a function-like type
 184    */
 185   bool isFunctionLike() const;
 186
 187   /**
 188    * Construct and return a ground term for this Type.  Throws an
 189    * exception if this type is not well-founded.
 190    */
 191   Expr mkGroundTerm() const;
 192
 193   /**
 194    * Construct and return a ground value for this Type.  Throws an
 195    * exception if this type is not well-founded.
 196    *
 197    * This is the same as mkGroundTerm, but constructs a constant value instead
 198    * of a canonical ground term. These two notions typically coincide. However,
 199    * for uninterpreted sorts, they do not: mkGroundTerm returns a fresh variable
 200    * whereas mkValue returns an uninterpreted constant. The motivation for
 201    * mkGroundTerm is that unintepreted constants should never appear in lemmas.
 202    * The motivation for mkGroundValue is for e.g. type enumeration and model
 203    * construction.
 204    */
 205   Expr mkGroundValue() const;
 206
 207   /**
 208    * Is this type a subtype of the given type?
 209    */
 210   bool isSubtypeOf(Type t) const;
 211
 212   /**
 213    * Is this type comparable to the given type (i.e., do they share
 214    * a common ancestor in the subtype tree)?
 215    */
 216   bool isComparableTo(Type t) const;
 217
 218   /**
 219    * Get the most general base type of this type.
 220    */
 221   Type getBaseType() const;
 222
 223   /**
 224    * Substitution of Types.
 225    */
 226   Type substitute(const Type& type, const Type& replacement) const;
 227
 228   /**
 229    * Simultaneous substitution of Types.
 230    */
 231   Type substitute(const std::vector<Type>& types,
 232                   const std::vector<Type>& replacements) const;
 233
 234   /**
 235    * Get this type's ExprManager.
 236    */
 237   ExprManager* getExprManager() const;
 238
 239   /**
 240    * Exports this type into a different ExprManager.
 241    */
 242   Type exportTo(ExprManager* exprManager, ExprManagerMapCollection& vmap) const;
 243
 244   /**
 245    * Assignment operator.
 246    * @param t the type to assign to this type
 247    * @return this type after assignment.
 248    */
 249   Type& operator=(const Type& t);
 250
 251   /**
 252    * Comparison for structural equality.
 253    * @param t the type to compare to
 254    * @returns true if the types are equal
 255    */
 256   bool operator==(const Type& t) const;
 257
 258   /**
 259    * Comparison for structural disequality.
 260    * @param t the type to compare to
 261    * @returns true if the types are not equal
 262    */
 263   bool operator!=(const Type& t) const;
 264
 265   /**
 266    * An ordering on Types so they can be stored in maps, etc.
 267    */
 268   bool operator<(const Type& t) const;
 269
 270   /**
 271    * An ordering on Types so they can be stored in maps, etc.
 272    */
 273   bool operator<=(const Type& t) const;
 274
 275   /**
 276    * An ordering on Types so they can be stored in maps, etc.
 277    */
 278   bool operator>(const Type& t) const;
 279
 280   /**
 281    * An ordering on Types so they can be stored in maps, etc.
 282    */
 283   bool operator>=(const Type& t) const;
 284
 285   /**
 286    * Is this the Boolean type?
 287    * @return true if the type is a Boolean type
 288    */
 289   bool isBoolean() const;
 290
 291   /**
 292    * Is this the integer type?
 293    * @return true if the type is a integer type
 294    */
 295   bool isInteger() const;
 296
 297   /**
 298    * Is this the real type?
 299    * @return true if the type is a real type
 300    */
 301   bool isReal() const;
 302
 303   /**
 304    * Is this the string type?
 305    * @return true if the type is the string type
 306    */
 307   bool isString() const;
 308
 309   /**
 310    * Is this the regexp type?
 311    * @return true if the type is the regexp type
 312    */
 313   bool isRegExp() const;
 314
 315   /**
 316    * Is this the rounding mode type?
 317    * @return true if the type is the rounding mode type
 318    */
 319   bool isRoundingMode() const;
 320
 321   /**
 322    * Is this the bit-vector type?
 323    * @return true if the type is a bit-vector type
 324    */
 325   bool isBitVector() const;
 326
 327   /**
 328    * Is this the floating-point type?
 329    * @return true if the type is a floating-point type
 330    */
 331   bool isFloatingPoint() const;
 332
 333   /**
 334    * Is this a function type?
 335    * @return true if the type is a function type
 336    */
 337   bool isFunction() const;
 338
 339   /**
 340    * Is this a predicate type, i.e. if it's a function type mapping to Boolean.
 341    * All predicate types are also function types.
 342    * @return true if the type is a predicate type
 343    */
 344   bool isPredicate() const;
 345
 346   /**
 347    * Is this a tuple type?
 348    * @return true if the type is a tuple type
 349    */
 350   bool isTuple() const;
 351
 352   /**
 353    * Is this a record type?
 354    * @return true if the type is a record type
 355    */
 356   bool isRecord() const;
 357
 358   /**
 359    * Is this a symbolic expression type?
 360    * @return true if the type is a symbolic expression type
 361    */
 362   bool isSExpr() const;
 363
 364   /**
 365    * Is this an array type?
 366    * @return true if the type is a array type
 367    */
 368   bool isArray() const;
 369
 370   /**
 371    * Is this a Set type?
 372    * @return true if the type is a Set type
 373    */
 374   bool isSet() const;
 375
 376   /**
 377    * Is this a Sequence type?
 378    * @return true if the type is a Sequence type
 379    */
 380   bool isSequence() const;
 381
 382   /**
 383    * Is this a datatype type?
 384    * @return true if the type is a datatype type
 385    */
 386   bool isDatatype() const;
 387
 388   /**
 389    * Is this a constructor type?
 390    * @return true if the type is a constructor type
 391    */
 392   bool isConstructor() const;
 393
 394   /**
 395    * Is this a selector type?
 396    * @return true if the type is a selector type
 397    */
 398   bool isSelector() const;
 399
 400   /**
 401    * Is this a tester type?
 402    * @return true if the type is a tester type
 403    */
 404   bool isTester() const;
 405
 406   /**
 407    * Is this a sort kind?
 408    * @return true if this is a sort kind
 409    */
 410   bool isSort() const;
 411
 412   /**
 413    * Is this a sort constructor kind?
 414    * @return true if this is a sort constructor kind
 415    */
 416   bool isSortConstructor() const;
 417
 418   /**
 419    * Is this a predicate subtype?
 420    * @return true if this is a predicate subtype
 421    */
 422   // not in release 1.0
 423   //bool isPredicateSubtype() const;
 424
 425   /**
 426    * Is this an integer subrange type?
 427    * @return true if this is an integer subrange type
 428    */
 429   //bool isSubrange() const;
 430
 431   /**
 432    * Outputs a string representation of this type to the stream.
 433    * @param out the stream to output to
 434    */
 435   void toStream(std::ostream& out) const;
 436
 437   /**
 438    * Constructs a string representation of this type.
 439    */
 440   std::string toString() const;
 441 };/* class Type */
 442
 443 /** Singleton class encapsulating the Boolean type. */
 444 class CVC4_PUBLIC BooleanType : public Type {
 445  public:
 446   /** Construct from the base type */
 447   BooleanType(const Type& type = Type());
 448 };/* class BooleanType */
 449
 450 /** Singleton class encapsulating the integer type. */
 451 class CVC4_PUBLIC IntegerType : public Type {
 452  public:
 453   /** Construct from the base type */
 454   IntegerType(const Type& type = Type());
 455 };/* class IntegerType */
 456
 457 /** Singleton class encapsulating the real type. */
 458 class CVC4_PUBLIC RealType : public Type {
 459  public:
 460   /** Construct from the base type */
 461   RealType(const Type& type = Type());
 462 };/* class RealType */
 463
 464 /** Singleton class encapsulating the string type. */
 465 class CVC4_PUBLIC StringType : public Type {
 466  public:
 467   /** Construct from the base type */
 468   StringType(const Type& type);
 469 };/* class StringType */
 470
 471 /** Singleton class encapsulating the string type. */
 472 class CVC4_PUBLIC RegExpType : public Type {
 473  public:
 474   /** Construct from the base type */
 475   RegExpType(const Type& type);
 476 };/* class RegExpType */
 477
 478 /** Singleton class encapsulating the rounding mode type. */
 479 class CVC4_PUBLIC RoundingModeType : public Type {
 480  public:
 481   /** Construct from the base type */
 482   RoundingModeType(const Type& type = Type());
 483 };/* class RoundingModeType */
 484
 485 /** Class encapsulating a function type. */
 486 class CVC4_PUBLIC FunctionType : public Type {
 487  public:
 488   /** Construct from the base type */
 489   FunctionType(const Type& type = Type());
 490
 491   /** Get the arity of the function type */
 492   size_t getArity() const;
 493
 494   /** Get the argument types */
 495   std::vector<Type> getArgTypes() const;
 496
 497   /** Get the range type (i.e., the type of the result). */
 498   Type getRangeType() const;
 499 };/* class FunctionType */
 500
 501 /** Class encapsulating a sexpr type. */
 502 class CVC4_PUBLIC SExprType : public Type {
 503  public:
 504   /** Construct from the base type */
 505   SExprType(const Type& type = Type());
 506
 507   /** Get the constituent types */
 508   std::vector<Type> getTypes() const;
 509 };/* class SExprType */
 510
 511 /** Class encapsulating an array type. */
 512 class CVC4_PUBLIC ArrayType : public Type {
 513  public:
 514   /** Construct from the base type */
 515   ArrayType(const Type& type = Type());
 516
 517   /** Get the index type */
 518   Type getIndexType() const;
 519
 520   /** Get the constituent type */
 521   Type getConstituentType() const;
 522 };/* class ArrayType */
 523
 524 /** Class encapsulating a set type. */
 525 class CVC4_PUBLIC SetType : public Type {
 526  public:
 527   /** Construct from the base type */
 528   SetType(const Type& type = Type());
 529
 530   /** Get the element type */
 531   Type getElementType() const;
 532 }; /* class SetType */
 533
 534 /** Class encapsulating a sequence type. */
 535 class CVC4_PUBLIC SequenceType : public Type
 536 {
 537  public:
 538   /** Construct from the base type */
 539   SequenceType(const Type& type = Type());
 540
 541   /** Get the element type */
 542   Type getElementType() const;
 543 }; /* class SetType */
 544
 545 /** Class encapsulating a user-defined sort. */
 546 class CVC4_PUBLIC SortType : public Type {
 547  public:
 548   /** Construct from the base type */
 549   SortType(const Type& type = Type());
 550
 551   /** Get the name of the sort */
 552   std::string getName() const;
 553
 554   /** Is this type parameterized? */
 555   bool isParameterized() const;
 556
 557   /** Get the parameter types */
 558   std::vector<Type> getParamTypes() const;
 559
 560 };/* class SortType */
 561
 562 /** Class encapsulating a user-defined sort constructor. */
 563 class CVC4_PUBLIC SortConstructorType : public Type {
 564  public:
 565   /** Construct from the base type */
 566   SortConstructorType(const Type& type = Type());
 567
 568   /** Get the name of the sort constructor */
 569   std::string getName() const;
 570
 571   /** Get the arity of the sort constructor */
 572   size_t getArity() const;
 573
 574   /** Instantiate a sort using this sort constructor */
 575   SortType instantiate(const std::vector<Type>& params) const;
 576
 577 };/* class SortConstructorType */
 578
 579 /** Class encapsulating the bit-vector type. */
 580 class CVC4_PUBLIC BitVectorType : public Type {
 581  public:
 582   /** Construct from the base type */
 583   BitVectorType(const Type& type = Type());
 584
 585   /**
 586    * Returns the size of the bit-vector type.
 587    * @return the width of the bit-vector type (> 0)
 588    */
 589   unsigned getSize() const;
 590
 591 };/* class BitVectorType */
 592
 593 /** Class encapsulating the floating point type. */
 594 class CVC4_PUBLIC FloatingPointType : public Type {
 595  public:
 596   /** Construct from the base type */
 597   FloatingPointType(const Type& type = Type());
 598
 599   /**
 600    * Returns the size of the floating-point exponent type.
 601    * @return the width of the floating-point exponent type (> 0)
 602    */
 603   unsigned getExponentSize() const;
 604
 605   /**
 606    * Returns the size of the floating-point significand type.
 607    * @return the width of the floating-point significand type (> 0)
 608    */
 609   unsigned getSignificandSize() const;
 610
 611 };/* class FloatingPointType */
 612
 613 /** Class encapsulating the datatype type */
 614 class CVC4_PUBLIC DatatypeType : public Type {
 615  public:
 616   /** Construct from the base type */
 617   DatatypeType(const Type& type = Type());
 618
 619   /** Get the underlying datatype */
 620   const Datatype& getDatatype() const;
 621
 622   /** Is this datatype parametric? */
 623   bool isParametric() const;
 624   /**
 625    * Has this datatype been fully instantiated ?
 626    *
 627    * @return true if this datatype is not parametric or, if it is, it
 628    * has been fully instantiated
 629    */
 630   bool isInstantiated() const;
 631
 632   /** Has this datatype been instantiated for parameter `n` ? */
 633   bool isParameterInstantiated(unsigned n) const;
 634
 635   /** Get the parameter types */
 636   std::vector<Type> getParamTypes() const;
 637
 638   /** Get the arity of the datatype constructor */
 639   size_t getArity() const;
 640
 641   /** Instantiate a datatype using this datatype constructor */
 642   DatatypeType instantiate(const std::vector<Type>& params) const;
 643
 644   /** Get the length of a tuple type */
 645   size_t getTupleLength() const;
 646
 647   /** Get the constituent types of a tuple type */
 648   std::vector<Type> getTupleTypes() const;
 649
 650 };/* class DatatypeType */
 651
 652 /** Class encapsulating the constructor type. */
 653 class CVC4_PUBLIC ConstructorType : public Type {
 654  public:
 655   /** Construct from the base type */
 656   ConstructorType(const Type& type = Type());
 657
 658   /** Get the range type */
 659   DatatypeType getRangeType() const;
 660
 661   /** Get the argument types */
 662   std::vector<Type> getArgTypes() const;
 663
 664   /** Get the number of constructor arguments */
 665   size_t getArity() const;
 666
 667 };/* class ConstructorType */
 668
 669 /** Class encapsulating the Selector type. */
 670 class CVC4_PUBLIC SelectorType : public Type {
 671  public:
 672   /** Construct from the base type */
 673   SelectorType(const Type& type = Type());
 674
 675   /** Get the domain type for this selector (the datatype type) */
 676   DatatypeType getDomain() const;
 677
 678   /** Get the range type for this selector (the field type) */
 679   Type getRangeType() const;
 680
 681 };/* class SelectorType */
 682
 683 /** Class encapsulating the Tester type. */
 684 class CVC4_PUBLIC TesterType : public Type {
 685  public:
 686   /** Construct from the base type */
 687   TesterType(const Type& type = Type());
 688
 689   /** Get the type that this tester tests (the datatype type) */
 690   DatatypeType getDomain() const;
 691
 692   /**
 693    * Get the range type for this tester (included for sake of
 694    * interface completeness), but doesn't give useful information).
 695    */
 696   BooleanType getRangeType() const;
 697
 698 };/* class TesterType */
 699
 700 }/* CVC4 namespace */
 701
 702 #endif /* CVC4__TYPE_H */