src/expr/type.h

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