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()

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