src/expr/type.h

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