src/expr/type.h

   1 /*********************                                                        */
   2 /*! \file type.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Dejan Jovanovic, 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 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 datatype type?
 378    * @return true if the type is a datatype type
 379    */
 380   bool isDatatype() const;
 381
 382   /**
 383    * Is this a constructor type?
 384    * @return true if the type is a constructor type
 385    */
 386   bool isConstructor() const;
 387
 388   /**
 389    * Is this a selector type?
 390    * @return true if the type is a selector type
 391    */
 392   bool isSelector() const;
 393
 394   /**
 395    * Is this a tester type?
 396    * @return true if the type is a tester type
 397    */
 398   bool isTester() const;
 399
 400   /**
 401    * Is this a sort kind?
 402    * @return true if this is a sort kind
 403    */
 404   bool isSort() const;
 405
 406   /**
 407    * Is this a sort constructor kind?
 408    * @return true if this is a sort constructor kind
 409    */
 410   bool isSortConstructor() const;
 411
 412   /**
 413    * Is this a predicate subtype?
 414    * @return true if this is a predicate subtype
 415    */
 416   // not in release 1.0
 417   //bool isPredicateSubtype() const;
 418
 419   /**
 420    * Is this an integer subrange type?
 421    * @return true if this is an integer subrange type
 422    */
 423   //bool isSubrange() const;
 424
 425   /**
 426    * Outputs a string representation of this type to the stream.
 427    * @param out the stream to output to
 428    */
 429   void toStream(std::ostream& out) const;
 430
 431   /**
 432    * Constructs a string representation of this type.
 433    */
 434   std::string toString() const;
 435 };/* class Type */
 436
 437 /** Singleton class encapsulating the Boolean type. */
 438 class CVC4_PUBLIC BooleanType : public Type {
 439  public:
 440   /** Construct from the base type */
 441   BooleanType(const Type& type = Type());
 442 };/* class BooleanType */
 443
 444 /** Singleton class encapsulating the integer type. */
 445 class CVC4_PUBLIC IntegerType : public Type {
 446  public:
 447   /** Construct from the base type */
 448   IntegerType(const Type& type = Type());
 449 };/* class IntegerType */
 450
 451 /** Singleton class encapsulating the real type. */
 452 class CVC4_PUBLIC RealType : public Type {
 453  public:
 454   /** Construct from the base type */
 455   RealType(const Type& type = Type());
 456 };/* class RealType */
 457
 458 /** Singleton class encapsulating the string type. */
 459 class CVC4_PUBLIC StringType : public Type {
 460  public:
 461   /** Construct from the base type */
 462   StringType(const Type& type);
 463 };/* class StringType */
 464
 465 /** Singleton class encapsulating the string type. */
 466 class CVC4_PUBLIC RegExpType : public Type {
 467  public:
 468   /** Construct from the base type */
 469   RegExpType(const Type& type);
 470 };/* class RegExpType */
 471
 472 /** Singleton class encapsulating the rounding mode type. */
 473 class CVC4_PUBLIC RoundingModeType : public Type {
 474  public:
 475   /** Construct from the base type */
 476   RoundingModeType(const Type& type = Type());
 477 };/* class RoundingModeType */
 478
 479 /** Class encapsulating a function type. */
 480 class CVC4_PUBLIC FunctionType : public Type {
 481  public:
 482   /** Construct from the base type */
 483   FunctionType(const Type& type = Type());
 484
 485   /** Get the arity of the function type */
 486   size_t getArity() const;
 487
 488   /** Get the argument types */
 489   std::vector<Type> getArgTypes() const;
 490
 491   /** Get the range type (i.e., the type of the result). */
 492   Type getRangeType() const;
 493 };/* class FunctionType */
 494
 495 /** Class encapsulating a sexpr type. */
 496 class CVC4_PUBLIC SExprType : public Type {
 497  public:
 498   /** Construct from the base type */
 499   SExprType(const Type& type = Type());
 500
 501   /** Get the constituent types */
 502   std::vector<Type> getTypes() const;
 503 };/* class SExprType */
 504
 505 /** Class encapsulating an array type. */
 506 class CVC4_PUBLIC ArrayType : public Type {
 507  public:
 508   /** Construct from the base type */
 509   ArrayType(const Type& type = Type());
 510
 511   /** Get the index type */
 512   Type getIndexType() const;
 513
 514   /** Get the constituent type */
 515   Type getConstituentType() const;
 516 };/* class ArrayType */
 517
 518 /** Class encapsulating an set type. */
 519 class CVC4_PUBLIC SetType : public Type {
 520  public:
 521   /** Construct from the base type */
 522   SetType(const Type& type = Type());
 523
 524   /** Get the index type */
 525   Type getElementType() const;
 526 };/* class SetType */
 527
 528 /** Class encapsulating a user-defined sort. */
 529 class CVC4_PUBLIC SortType : public Type {
 530  public:
 531   /** Construct from the base type */
 532   SortType(const Type& type = Type());
 533
 534   /** Get the name of the sort */
 535   std::string getName() const;
 536
 537   /** Is this type parameterized? */
 538   bool isParameterized() const;
 539
 540   /** Get the parameter types */
 541   std::vector<Type> getParamTypes() const;
 542
 543 };/* class SortType */
 544
 545 /** Class encapsulating a user-defined sort constructor. */
 546 class CVC4_PUBLIC SortConstructorType : public Type {
 547  public:
 548   /** Construct from the base type */
 549   SortConstructorType(const Type& type = Type());
 550
 551   /** Get the name of the sort constructor */
 552   std::string getName() const;
 553
 554   /** Get the arity of the sort constructor */
 555   size_t getArity() const;
 556
 557   /** Instantiate a sort using this sort constructor */
 558   SortType instantiate(const std::vector<Type>& params) const;
 559
 560 };/* class SortConstructorType */
 561
 562 /** Class encapsulating the bit-vector type. */
 563 class CVC4_PUBLIC BitVectorType : public Type {
 564  public:
 565   /** Construct from the base type */
 566   BitVectorType(const Type& type = Type());
 567
 568   /**
 569    * Returns the size of the bit-vector type.
 570    * @return the width of the bit-vector type (> 0)
 571    */
 572   unsigned getSize() const;
 573
 574 };/* class BitVectorType */
 575
 576 /** Class encapsulating the floating point type. */
 577 class CVC4_PUBLIC FloatingPointType : public Type {
 578  public:
 579   /** Construct from the base type */
 580   FloatingPointType(const Type& type = Type());
 581
 582   /**
 583    * Returns the size of the floating-point exponent type.
 584    * @return the width of the floating-point exponent type (> 0)
 585    */
 586   unsigned getExponentSize() const;
 587
 588   /**
 589    * Returns the size of the floating-point significand type.
 590    * @return the width of the floating-point significand type (> 0)
 591    */
 592   unsigned getSignificandSize() const;
 593
 594 };/* class FloatingPointType */
 595
 596 /** Class encapsulating the datatype type */
 597 class CVC4_PUBLIC DatatypeType : public Type {
 598  public:
 599   /** Construct from the base type */
 600   DatatypeType(const Type& type = Type());
 601
 602   /** Get the underlying datatype */
 603   const Datatype& getDatatype() const;
 604
 605   /** Is this datatype parametric? */
 606   bool isParametric() const;
 607
 608   /**
 609    * Get the constructor operator associated to the given constructor
 610    * name in this datatype.
 611    */
 612   Expr getConstructor(std::string name) const;
 613
 614   /**
 615    * Has this datatype been fully instantiated ?
 616    *
 617    * @return true if this datatype is not parametric or, if it is, it
 618    * has been fully instantiated
 619    */
 620   bool isInstantiated() const;
 621
 622   /** Has this datatype been instantiated for parameter `n` ? */
 623   bool isParameterInstantiated(unsigned n) const;
 624
 625   /** Get the parameter types */
 626   std::vector<Type> getParamTypes() const;
 627
 628   /** Get the arity of the datatype constructor */
 629   size_t getArity() const;
 630
 631   /** Instantiate a datatype using this datatype constructor */
 632   DatatypeType instantiate(const std::vector<Type>& params) const;
 633
 634   /** Get the length of a tuple type */
 635   size_t getTupleLength() const;
 636
 637   /** Get the constituent types of a tuple type */
 638   std::vector<Type> getTupleTypes() const;
 639
 640   /** Get the description of the record type */
 641   const Record& getRecord() const;
 642
 643 };/* class DatatypeType */
 644
 645 /** Class encapsulating the constructor type. */
 646 class CVC4_PUBLIC ConstructorType : public Type {
 647  public:
 648   /** Construct from the base type */
 649   ConstructorType(const Type& type = Type());
 650
 651   /** Get the range type */
 652   DatatypeType getRangeType() const;
 653
 654   /** Get the argument types */
 655   std::vector<Type> getArgTypes() const;
 656
 657   /** Get the number of constructor arguments */
 658   size_t getArity() const;
 659
 660 };/* class ConstructorType */
 661
 662 /** Class encapsulating the Selector type. */
 663 class CVC4_PUBLIC SelectorType : public Type {
 664  public:
 665   /** Construct from the base type */
 666   SelectorType(const Type& type = Type());
 667
 668   /** Get the domain type for this selector (the datatype type) */
 669   DatatypeType getDomain() const;
 670
 671   /** Get the range type for this selector (the field type) */
 672   Type getRangeType() const;
 673
 674 };/* class SelectorType */
 675
 676 /** Class encapsulating the Tester type. */
 677 class CVC4_PUBLIC TesterType : public Type {
 678  public:
 679   /** Construct from the base type */
 680   TesterType(const Type& type = Type());
 681
 682   /** Get the type that this tester tests (the datatype type) */
 683   DatatypeType getDomain() const;
 684
 685   /**
 686    * Get the range type for this tester (included for sake of
 687    * interface completeness), but doesn't give useful information).
 688    */
 689   BooleanType getRangeType() const;
 690
 691 };/* class TesterType */
 692
 693 }/* CVC4 namespace */
 694
 695 #endif /* CVC4__TYPE_H */