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 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 DatatypeType;
  53 class ConstructorType;
  54 class SelectorType;
  55 class TesterType;
  56 class FunctionType;
  57 class TupleType;
  58 class RecordType;
  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 bit-vector type?
 262    * @return true if the type is a bit-vector type
 263    */
 264   bool isBitVector() const;
 265
 266   /**
 267    * Is this a function type?
 268    * @return true if the type is a function type
 269    */
 270   bool isFunction() const;
 271
 272   /**
 273    * Is this a predicate type, i.e. if it's a function type mapping to Boolean.
 274    * All predicate types are also function types.
 275    * @return true if the type is a predicate type
 276    */
 277   bool isPredicate() const;
 278
 279   /**
 280    * Is this a tuple type?
 281    * @return true if the type is a tuple type
 282    */
 283   bool isTuple() const;
 284
 285   /**
 286    * Is this a record type?
 287    * @return true if the type is a record type
 288    */
 289   bool isRecord() const;
 290
 291   /**
 292    * Is this a symbolic expression type?
 293    * @return true if the type is a symbolic expression type
 294    */
 295   bool isSExpr() const;
 296
 297   /**
 298    * Is this an array type?
 299    * @return true if the type is a array type
 300    */
 301   bool isArray() const;
 302
 303   /**
 304    * Is this a datatype type?
 305    * @return true if the type is a datatype type
 306    */
 307   bool isDatatype() const;
 308
 309   /**
 310    * Is this a constructor type?
 311    * @return true if the type is a constructor type
 312    */
 313   bool isConstructor() const;
 314
 315   /**
 316    * Is this a selector type?
 317    * @return true if the type is a selector type
 318    */
 319   bool isSelector() const;
 320
 321   /**
 322    * Is this a tester type?
 323    * @return true if the type is a tester type
 324    */
 325   bool isTester() const;
 326
 327   /**
 328    * Is this a sort kind?
 329    * @return true if this is a sort kind
 330    */
 331   bool isSort() const;
 332
 333   /**
 334    * Is this a sort constructor kind?
 335    * @return true if this is a sort constructor kind
 336    */
 337   bool isSortConstructor() const;
 338
 339   /**
 340    * Is this a predicate subtype?
 341    * @return true if this is a predicate subtype
 342    */
 343   // not in release 1.0
 344   //bool isPredicateSubtype() const;
 345
 346   /**
 347    * Is this an integer subrange type?
 348    * @return true if this is an integer subrange type
 349    */
 350   bool isSubrange() const;
 351
 352   /**
 353    * Outputs a string representation of this type to the stream.
 354    * @param out the stream to output to
 355    */
 356   void toStream(std::ostream& out) const;
 357
 358   /**
 359    * Constructs a string representation of this type.
 360    */
 361   std::string toString() const;
 362 };/* class Type */
 363
 364 /**
 365  * Singleton class encapsulating the Boolean type.
 366  */
 367 class CVC4_PUBLIC BooleanType : public Type {
 368
 369 public:
 370
 371   /** Construct from the base type */
 372   BooleanType(const Type& type = Type()) throw(IllegalArgumentException);
 373 };/* class BooleanType */
 374
 375 /**
 376  * Singleton class encapsulating the integer type.
 377  */
 378 class CVC4_PUBLIC IntegerType : public Type {
 379
 380 public:
 381
 382   /** Construct from the base type */
 383   IntegerType(const Type& type = Type()) throw(IllegalArgumentException);
 384 };/* class IntegerType */
 385
 386 /**
 387  * Singleton class encapsulating the real type.
 388  */
 389 class CVC4_PUBLIC RealType : public Type {
 390
 391 public:
 392
 393   /** Construct from the base type */
 394   RealType(const Type& type = Type()) throw(IllegalArgumentException);
 395 };/* class RealType */
 396
 397 /**
 398  * Singleton class encapsulating the string type.
 399  */
 400 class CVC4_PUBLIC StringType : public Type {
 401
 402 public:
 403
 404   /** Construct from the base type */
 405   StringType(const Type& type) throw(IllegalArgumentException);
 406 };/* class StringType */
 407
 408 /**
 409  * Class encapsulating a function type.
 410  */
 411 class CVC4_PUBLIC FunctionType : public Type {
 412
 413 public:
 414
 415   /** Construct from the base type */
 416   FunctionType(const Type& type = Type()) throw(IllegalArgumentException);
 417
 418   /** Get the argument types */
 419   std::vector<Type> getArgTypes() const;
 420
 421   /** Get the range type (i.e., the type of the result). */
 422   Type getRangeType() const;
 423 };/* class FunctionType */
 424
 425 /**
 426  * Class encapsulating a tuple type.
 427  */
 428 class CVC4_PUBLIC TupleType : public Type {
 429
 430 public:
 431
 432   /** Construct from the base type */
 433   TupleType(const Type& type = Type()) throw(IllegalArgumentException);
 434
 435   /** Get the length of the tuple.  The same as getTypes().size(). */
 436   size_t getLength() const;
 437
 438   /** Get the constituent types */
 439   std::vector<Type> getTypes() const;
 440
 441 };/* class TupleType */
 442
 443 /**
 444  * Class encapsulating a record type.
 445  */
 446 class CVC4_PUBLIC RecordType : public Type {
 447
 448 public:
 449
 450   /** Construct from the base type */
 451   RecordType(const Type& type = Type()) throw(IllegalArgumentException);
 452
 453   /** Get the constituent types */
 454   const Record& getRecord() const;
 455 };/* class RecordType */
 456
 457 /**
 458  * Class encapsulating a tuple type.
 459  */
 460 class CVC4_PUBLIC SExprType : public Type {
 461
 462 public:
 463
 464   /** Construct from the base type */
 465   SExprType(const Type& type = Type()) throw(IllegalArgumentException);
 466
 467   /** Get the constituent types */
 468   std::vector<Type> getTypes() const;
 469 };/* class SExprType */
 470
 471 /**
 472  * Class encapsulating an array type.
 473  */
 474 class CVC4_PUBLIC ArrayType : public Type {
 475
 476 public:
 477
 478   /** Construct from the base type */
 479   ArrayType(const Type& type = Type()) throw(IllegalArgumentException);
 480
 481   /** Get the index type */
 482   Type getIndexType() const;
 483
 484   /** Get the constituent type */
 485   Type getConstituentType() const;
 486 };/* class ArrayType */
 487
 488 /**
 489  * Class encapsulating a user-defined sort.
 490  */
 491 class CVC4_PUBLIC SortType : public Type {
 492
 493 public:
 494
 495   /** Construct from the base type */
 496   SortType(const Type& type = Type()) throw(IllegalArgumentException);
 497
 498   /** Get the name of the sort */
 499   std::string getName() const;
 500
 501   /** Is this type parameterized? */
 502   bool isParameterized() const;
 503
 504   /** Get the parameter types */
 505   std::vector<Type> getParamTypes() const;
 506
 507 };/* class SortType */
 508
 509 /**
 510  * Class encapsulating a user-defined sort constructor.
 511  */
 512 class CVC4_PUBLIC SortConstructorType : public Type {
 513
 514 public:
 515
 516   /** Construct from the base type */
 517   SortConstructorType(const Type& type = Type()) throw(IllegalArgumentException);
 518
 519   /** Get the name of the sort constructor */
 520   std::string getName() const;
 521
 522   /** Get the arity of the sort constructor */
 523   size_t getArity() const;
 524
 525   /** Instantiate a sort using this sort constructor */
 526   SortType instantiate(const std::vector<Type>& params) const;
 527
 528 };/* class SortConstructorType */
 529
 530 // not in release 1.0
 531 #if 0
 532 /**
 533  * Class encapsulating a predicate subtype.
 534  */
 535 class CVC4_PUBLIC PredicateSubtype : public Type {
 536
 537 public:
 538
 539   /** Construct from the base type */
 540   PredicateSubtype(const Type& type = Type()) throw(IllegalArgumentException);
 541
 542   /** Get the LAMBDA defining this predicate subtype */
 543   Expr getPredicate() const;
 544
 545   /**
 546    * Get the parent type of this predicate subtype; note that this
 547    * could be another predicate subtype.
 548    */
 549   Type getParentType() const;
 550
 551 };/* class PredicateSubtype */
 552 #endif /* 0 */
 553
 554 /**
 555  * Class encapsulating an integer subrange type.
 556  */
 557 class CVC4_PUBLIC SubrangeType : public Type {
 558
 559 public:
 560
 561   /** Construct from the base type */
 562   SubrangeType(const Type& type = Type()) throw(IllegalArgumentException);
 563
 564   /** Get the bounds defining this integer subrange */
 565   SubrangeBounds getSubrangeBounds() const;
 566
 567 };/* class SubrangeType */
 568
 569 /**
 570  * Class encapsulating the bit-vector type.
 571  */
 572 class CVC4_PUBLIC BitVectorType : public Type {
 573
 574 public:
 575
 576   /** Construct from the base type */
 577   BitVectorType(const Type& type = Type()) throw(IllegalArgumentException);
 578
 579   /**
 580    * Returns the size of the bit-vector type.
 581    * @return the width of the bit-vector type (> 0)
 582    */
 583   unsigned getSize() const;
 584
 585 };/* class BitVectorType */
 586
 587
 588 /**
 589  * Class encapsulating the datatype type
 590  */
 591 class CVC4_PUBLIC DatatypeType : public Type {
 592
 593 public:
 594
 595   /** Construct from the base type */
 596   DatatypeType(const Type& type = Type()) throw(IllegalArgumentException);
 597
 598   /** Get the underlying datatype */
 599   const Datatype& getDatatype() const;
 600
 601   /** Is this datatype parametric? */
 602   bool isParametric() const;
 603
 604   /**
 605    * Get the constructor operator associated to the given constructor
 606    * name in this datatype.
 607    */
 608   Expr getConstructor(std::string name) const;
 609
 610   /**
 611    * Has this datatype been fully instantiated ?
 612    *
 613    * @return true if this datatype is not parametric or, if it is, it
 614    * has been fully instantiated
 615    */
 616   bool isInstantiated() const;
 617
 618   /**
 619    * Has this datatype been instantiated for parameter N ?
 620    */
 621   bool isParameterInstantiated(unsigned n) const;
 622
 623   /** Get the parameter types */
 624   std::vector<Type> getParamTypes() const;
 625
 626   /** Get the arity of the datatype constructor */
 627   size_t getArity() const;
 628
 629   /** Instantiate a datatype using this datatype constructor */
 630   DatatypeType instantiate(const std::vector<Type>& params) const;
 631
 632 };/* class DatatypeType */
 633
 634 /**
 635  * Class encapsulating the constructor type
 636  */
 637 class CVC4_PUBLIC ConstructorType : public Type {
 638
 639 public:
 640
 641   /** Construct from the base type */
 642   ConstructorType(const Type& type = Type()) throw(IllegalArgumentException);
 643
 644   /** Get the range type */
 645   DatatypeType getRangeType() const;
 646
 647   /** Get the argument types */
 648   std::vector<Type> getArgTypes() const;
 649
 650   /** Get the number of constructor arguments */
 651   size_t getArity() const;
 652
 653 };/* class ConstructorType */
 654
 655
 656 /**
 657  * Class encapsulating the Selector type
 658  */
 659 class CVC4_PUBLIC SelectorType : public Type {
 660
 661 public:
 662
 663   /** Construct from the base type */
 664   SelectorType(const Type& type = Type()) throw(IllegalArgumentException);
 665
 666   /** Get the domain type for this selector (the datatype type) */
 667   DatatypeType getDomain() const;
 668
 669   /** Get the range type for this selector (the field type) */
 670   Type getRangeType() const;
 671
 672 };/* class SelectorType */
 673
 674 /**
 675  * Class encapsulating the Tester type
 676  */
 677 class CVC4_PUBLIC TesterType : public Type {
 678
 679 public:
 680
 681   /** Construct from the base type */
 682   TesterType(const Type& type = Type()) throw(IllegalArgumentException);
 683
 684   /** Get the type that this tester tests (the datatype type) */
 685   DatatypeType getDomain() const;
 686
 687   /**
 688    * Get the range type for this tester (included for sake of
 689    * interface completeness), but doesn't give useful information).
 690    */
 691   BooleanType getRangeType() const;
 692
 693 };/* class TesterType */
 694
 695 }/* CVC4 namespace */
 696
 697 #endif /* __CVC4__TYPE_H */