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