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