src/expr/type.h

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