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