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