Datatype
This class represents a datatype. A
cvc5.Datatype
is encapsulated
by a datatype
Sort
and can be retrieved from a
datatype sort via
cvc5.Sort.getDatatype()
.
Datatypes are specified by a
cvc5.DatatypeDecl
via
cvc5.TermManager.mkDatatypeDecl()
when constructing a datatype
sort.
- 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 ( )
-
- Parameters :
-
name – The name of the constructor.
- Returns :
-
A constructor by name.
- getName ( )
-
- Returns :
-
The name of the datatype.
- getNumConstructors ( )
-
- Returns :
-
The number of constructors in this datatype.
- getParameters ( )
-
- Returns :
-
The parameters of this datatype, if it is parametric. An exception is thrown if this datatype is not parametric.
- getSelector ( )
-
- Parameters :
-
name – The name of the selector..
- Returns :
-
A selector by name.
- isCodatatype ( )
-
- Returns :
-
True if this datatype corresponds to a co-datatype.
- isFinite ( )
-
- Returns :
-
True if this datatype is finite.
- isNull ( )
-
- Returns :
-
True if this Datatype is a null object.
- isParametric ( )
-
Warning
This function is experimental and may change in future versions.
- Returns :
-
True if this datatype is parametric.
- isRecord ( )
-
Warning
This function is experimental and may change in future versions.
- Returns :
-
True if this datatype corresponds to a record.
- isTuple ( )
-
- Returns :
-
True if this datatype corresponds to a tuple.
- isWellFounded ( )
-
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