Datatype ¶
- class cvc5. Datatype ¶
-
A cvc5 datatype.
Wrapper class for the C++ class
cvc5::Datatype.- __getitem__ ( ) ¶
-
Get the datatype constructor with the given index, where index can be either a numeric id starting with zero, or the name of the constructor. In the latter case, this is a linear search through the constructors, so in case of multiple, similarly-named constructors, the first is returned.
- Parameters :
-
index – The id or name of the datatype constructor.
- Returns :
-
The matching datatype constructor.
- __iter__ ( ) ¶
-
Iterate over all constructors.
- getConstructor ( self , unicode name ) ¶
-
- Parameters :
-
name – The name of the constructor.
- Returns :
-
A constructor by name.
- getName ( self ) ¶
-
- Returns :
-
The name of the datatype.
- getNumConstructors ( self ) ¶
-
- Returns :
-
The number of constructors in this datatype.
- getParameters ( self ) ¶
-
- Returns :
-
The parameters of this datatype, if it is parametric. An exception is thrown if this datatype is not parametric.
- getSelector ( self , unicode name ) ¶
-
- Parameters :
-
name – The name of the selector..
- Returns :
-
A selector by name.
- isCodatatype ( self ) ¶
-
- Returns :
-
True if this datatype corresponds to a co-datatype.
- isFinite ( self ) ¶
-
- Returns :
-
True if this datatype is finite.
- isNull ( self ) ¶
-
- Returns :
-
True if this Datatype is a null object.
- isParametric ( self ) ¶
-
Warning
This method is experimental and may change in future versions.
- Returns :
-
True if this datatype is parametric.
- isRecord ( self ) ¶
-
Warning
This method is experimental and may change in future versions.
- Returns :
-
True if this datatype corresponds to a record.
- isTuple ( self ) ¶
-
- Returns :
-
True if this datatype corresponds to a tuple.
- isWellFounded ( self ) ¶
-
Determine if this datatype is well-founded.
If this datatype is not a codatatype, this returns false if there are no values of this datatype that are of finite size.
- Returns :
-
True if this datatype is well-founded