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