cvc4-1.4
type.h
Go to the documentation of this file.
1 /********************* */
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;
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>
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;
63 // not in release 1.0
64 //class PredicateSubtype;
65 class SubrangeType;
66 class Type;
67 
71  size_t operator()(const CVC4::Type& t) const;
72 };/* struct TypeHashFunction */
73 
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 
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 
101  TypeNode* d_typeNode;
102 
104  NodeManager* d_nodeManager;
105 
111  Type makeType(const TypeNode& typeNode) const;
112 
118  Type(NodeManager* em, TypeNode* typeNode);
119 
121  static TypeNode* getTypeNode(const Type& t) throw() { return t.d_typeNode; }
122 
123 public:
124 
126  virtual ~Type();
127 
129  Type();
130 
135  Type(const Type& t);
136 
141  bool isNull() const;
142 
146  Cardinality getCardinality() const;
147 
151  bool isWellFounded() const;
152 
157  Expr mkGroundTerm() const;
158 
162  bool isSubtypeOf(Type t) const;
163 
168  bool isComparableTo(Type t) const;
169 
173  Type getBaseType() const;
174 
178  Type substitute(const Type& type, const Type& replacement) const;
179 
183  Type substitute(const std::vector<Type>& types,
184  const std::vector<Type>& replacements) const;
185 
189  ExprManager* getExprManager() const;
190 
194  Type exportTo(ExprManager* exprManager, ExprManagerMapCollection& vmap) const;
195 
201  Type& operator=(const Type& t);
202 
208  bool operator==(const Type& t) const;
209 
215  bool operator!=(const Type& t) const;
216 
220  bool operator<(const Type& t) const;
221 
225  bool operator<=(const Type& t) const;
226 
230  bool operator>(const Type& t) const;
231 
235  bool operator>=(const Type& t) const;
236 
241  bool isBoolean() const;
242 
247  bool isInteger() const;
248 
253  bool isReal() const;
254 
259  bool isString() const;
260 
265  bool isBitVector() const;
266 
271  bool isFunction() const;
272 
278  bool isPredicate() const;
279 
284  bool isTuple() const;
285 
290  bool isRecord() const;
291 
296  bool isSExpr() const;
297 
302  bool isArray() const;
303 
308  bool isSet() const;
309 
314  bool isDatatype() const;
315 
320  bool isConstructor() const;
321 
326  bool isSelector() const;
327 
332  bool isTester() const;
333 
338  bool isSort() const;
339 
344  bool isSortConstructor() const;
345 
350  // not in release 1.0
351  //bool isPredicateSubtype() const;
352 
357  bool isSubrange() const;
358 
363  void toStream(std::ostream& out) const;
364 
368  std::string toString() const;
369 };/* class Type */
370 
374 class CVC4_PUBLIC BooleanType : public Type {
375 
376 public:
377 
379  BooleanType(const Type& type = Type()) throw(IllegalArgumentException);
380 };/* class BooleanType */
381 
385 class CVC4_PUBLIC IntegerType : public Type {
386 
387 public:
388 
390  IntegerType(const Type& type = Type()) throw(IllegalArgumentException);
391 };/* class IntegerType */
392 
396 class CVC4_PUBLIC RealType : public Type {
397 
398 public:
399 
401  RealType(const Type& type = Type()) throw(IllegalArgumentException);
402 };/* class RealType */
403 
407 class CVC4_PUBLIC StringType : public Type {
408 
409 public:
410 
412  StringType(const Type& type) throw(IllegalArgumentException);
413 };/* class StringType */
414 
418 class CVC4_PUBLIC FunctionType : public Type {
419 
420 public:
421 
423  FunctionType(const Type& type = Type()) throw(IllegalArgumentException);
424 
426  size_t getArity() const;
427 
429  std::vector<Type> getArgTypes() const;
430 
432  Type getRangeType() const;
433 };/* class FunctionType */
434 
438 class CVC4_PUBLIC TupleType : public Type {
439 
440 public:
441 
443  TupleType(const Type& type = Type()) throw(IllegalArgumentException);
444 
446  size_t getLength() const;
447 
449  std::vector<Type> getTypes() const;
450 
451 };/* class TupleType */
452 
456 class CVC4_PUBLIC RecordType : public Type {
457 
458 public:
459 
461  RecordType(const Type& type = Type()) throw(IllegalArgumentException);
462 
464  const Record& getRecord() const;
465 };/* class RecordType */
466 
470 class CVC4_PUBLIC SExprType : public Type {
471 
472 public:
473 
475  SExprType(const Type& type = Type()) throw(IllegalArgumentException);
476 
478  std::vector<Type> getTypes() const;
479 };/* class SExprType */
480 
484 class CVC4_PUBLIC ArrayType : public Type {
485 
486 public:
487 
489  ArrayType(const Type& type = Type()) throw(IllegalArgumentException);
490 
492  Type getIndexType() const;
493 
495  Type getConstituentType() const;
496 };/* class ArrayType */
497 
501 class CVC4_PUBLIC SetType : public Type {
502 
503 public:
504 
506  SetType(const Type& type = Type()) throw(IllegalArgumentException);
507 
509  Type getElementType() const;
510 };/* class SetType */
511 
515 class CVC4_PUBLIC SortType : public Type {
516 
517 public:
518 
520  SortType(const Type& type = Type()) throw(IllegalArgumentException);
521 
523  std::string getName() const;
524 
526  bool isParameterized() const;
527 
529  std::vector<Type> getParamTypes() const;
530 
531 };/* class SortType */
532 
536 class CVC4_PUBLIC SortConstructorType : public Type {
537 
538 public:
539 
541  SortConstructorType(const Type& type = Type()) throw(IllegalArgumentException);
542 
544  std::string getName() const;
545 
547  size_t getArity() const;
548 
550  SortType instantiate(const std::vector<Type>& params) const;
551 
552 };/* class SortConstructorType */
553 
554 // not in release 1.0
555 #if 0
556 
559 class CVC4_PUBLIC PredicateSubtype : public Type {
560 
561 public:
562 
564  PredicateSubtype(const Type& type = Type()) throw(IllegalArgumentException);
565 
567  Expr getPredicate() const;
568 
573  Type getParentType() const;
574 
575 };/* class PredicateSubtype */
576 #endif /* 0 */
577 
581 class CVC4_PUBLIC SubrangeType : public Type {
582 
583 public:
584 
586  SubrangeType(const Type& type = Type()) throw(IllegalArgumentException);
587 
589  SubrangeBounds getSubrangeBounds() const;
590 
591 };/* class SubrangeType */
592 
596 class CVC4_PUBLIC BitVectorType : public Type {
597 
598 public:
599 
601  BitVectorType(const Type& type = Type()) throw(IllegalArgumentException);
602 
607  unsigned getSize() const;
608 
609 };/* class BitVectorType */
610 
611 
615 class CVC4_PUBLIC DatatypeType : public Type {
616 
617 public:
618 
620  DatatypeType(const Type& type = Type()) throw(IllegalArgumentException);
621 
623  const Datatype& getDatatype() const;
624 
626  bool isParametric() const;
627 
632  Expr getConstructor(std::string name) const;
633 
640  bool isInstantiated() const;
641 
645  bool isParameterInstantiated(unsigned n) const;
646 
648  std::vector<Type> getParamTypes() const;
649 
651  size_t getArity() const;
652 
654  DatatypeType instantiate(const std::vector<Type>& params) const;
655 
656 };/* class DatatypeType */
657 
661 class CVC4_PUBLIC ConstructorType : public Type {
662 
663 public:
664 
666  ConstructorType(const Type& type = Type()) throw(IllegalArgumentException);
667 
669  DatatypeType getRangeType() const;
670 
672  std::vector<Type> getArgTypes() const;
673 
675  size_t getArity() const;
676 
677 };/* class ConstructorType */
678 
679 
683 class CVC4_PUBLIC SelectorType : public Type {
684 
685 public:
686 
688  SelectorType(const Type& type = Type()) throw(IllegalArgumentException);
689 
691  DatatypeType getDomain() const;
692 
694  Type getRangeType() const;
695 
696 };/* class SelectorType */
697 
701 class CVC4_PUBLIC TesterType : public Type {
702 
703 public:
704 
706  TesterType(const Type& type = Type()) throw(IllegalArgumentException);
707 
709  DatatypeType getDomain() const;
710 
715  BooleanType getRangeType() const;
716 
717 };/* class TesterType */
718 
719 }/* CVC4 namespace */
720 
721 #endif /* __CVC4__TYPE_H */
Singleton class encapsulating the real type.
Definition: type.h:396
Class encapsulating the Selector type.
Definition: type.h:683
void * Expr
Class encapsulating CVC4 expressions and methods for constructing new expressions.
Definition: expr.h:227
Singleton class encapsulating the integer type.
Definition: type.h:385
Class encapsulating a user-defined sort.
Definition: type.h:515
Class encapsulating an set type.
Definition: type.h:501
void * ExprManager
Hash function for Types.
Definition: type.h:69
Class encapsulating a tuple type.
Definition: type.h:470
The representation of an inductive datatype.
Definition: datatype.h:423
A simple representation of a cardinality.
Definition: cardinality.h:65
Class encapsulating CVC4 expression types.
Definition: type.h:89
std::ostream & operator<<(std::ostream &out, const UninterpretedConstant &uc)
static TypeNode * getTypeNode(const Type &t)
Accessor for derived classes.
Definition: type.h:121
TypeNode * d_typeNode
The internal expression representation.
Definition: type.h:101
Class encapsulating the Tester type.
Definition: type.h:701
Singleton class encapsulating the Boolean type.
Definition: type.h:374
Representation of subrange bounds.
Representation of cardinality.
Class encapsulating an array type.
Definition: type.h:484
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
Class encapsulating a function type.
Definition: type.h:418
Class encapsulating a user-defined sort constructor.
Definition: type.h:536
Class encapsulating the datatype type.
Definition: type.h:615
Macros that should be defined everywhere during the building of the libraries and driver binary...
Class encapsulating a record type.
Definition: type.h:456
NodeManager * d_nodeManager
The responsible expression manager.
Definition: type.h:104
TypeNode exportTypeInternal(TypeNode n, NodeManager *from, NodeManager *nm, ExprManagerMapCollection &vmap)
Class encapsulating a tuple type.
Definition: type.h:438
Singleton class encapsulating the string type.
Definition: type.h:407
struct CVC4::options::out__option_t out
Class encapsulating an integer subrange type.
Definition: type.h:581
void * Type
Class encapsulating the constructor type.
Definition: type.h:661
Class encapsulating the bit-vector type.
Definition: type.h:596
bool operator!=(enum Result::Sat s, const Result &r)
bool operator==(enum Result::Sat s, const Result &r)