Datatype ¶

class Datatype ¶

A cvc5 datatype.

Public Functions

Datatype ( ) ¶

Constructor.

~Datatype ( ) ¶

Destructor.

DatatypeConstructor operator [] ( size_t idx ) const ¶

Get the datatype constructor at a given index.

Parameters :

idx – The index of the datatype constructor to return.

Returns :

The datatype constructor with the given index.

DatatypeConstructor operator [] ( const std :: string & name ) const ¶

Get the datatype constructor with the given name. This is a linear search through the constructors, so in case of multiple, similarly-named constructors, the first is returned.

Parameters :

name – The name of the datatype constructor.

Returns :

The datatype constructor with the given name.

DatatypeConstructor getConstructor ( const std :: string & name ) const ¶

DatatypeSelector getSelector ( const std :: string & name ) const ¶

Get the datatype constructor with the given name. This is a linear search through the constructors and their selectors, so in case of multiple, similarly-named selectors, the first is returned.

Parameters :

name – The name of the datatype selector.

Returns :

The datatype selector with the given name.

std :: string getName ( ) const ¶

Returns :

The name of this Datatype .

size_t getNumConstructors ( ) const ¶

Returns :

The number of constructors for this Datatype .

std :: vector < Sort > getParameters ( ) const ¶

Get the parameters of this datatype, if it is parametric.

Note

Asserts that this datatype is parametric.

Warning

This method is experimental and may change in future versions.

Returns :

The parameters of this datatype.

bool isParametric ( ) const ¶

Warning

This method is experimental and may change in future versions.

Returns :

True if this datatype is parametric.

bool isCodatatype ( ) const ¶

Returns :

True if this datatype corresponds to a co-datatype

bool isTuple ( ) const ¶

Returns :

True if this datatype corresponds to a tuple

bool isRecord ( ) const ¶

Warning

This method is experimental and may change in future versions.

Returns :

True if this datatype corresponds to a record.

bool isFinite ( ) const ¶

Returns :

True if this datatype is finite

bool isWellFounded ( ) const ¶

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.

bool isNull ( ) const ¶

Returns :

True if this Datatype is a null object.

std :: string toString ( ) const ¶

Returns :

A string representation of this datatype.

const_iterator begin ( ) const ¶

Returns :

An iterator to the first constructor of this datatype.

const_iterator end ( ) const ¶

Returns :

An iterator to one-off-the-last constructor of this datatype.

class const_iterator ¶

Iterator for the constructors of a datatype.

Public Types

using iterator_category = std :: forward_iterator_tag ¶

Iterator tag

using value_type = Datatype ¶

The type of the item

using pointer = const Datatype * ¶

The pointer type of the item

using reference = const Datatype & ¶

The reference type of the item

using difference_type = std :: ptrdiff_t ¶

The type returned when two iterators are subtracted

Public Functions

const_iterator ( ) ¶

Nullary constructor (required for Cython).

const_iterator & operator = ( const const_iterator & it ) ¶

Assignment operator.

Parameters :

it – The iterator to assign to.

Returns :

The reference to the iterator after assignment.

bool operator == ( const const_iterator & it ) const ¶

Equality operator.

Parameters :

it – The iterator to compare to for equality.

Returns :

True if the iterators are equal.

bool operator != ( const const_iterator & it ) const ¶

Disequality operator.

Parameters :

it – The iterator to compare to for disequality.

Returns :

True if the iterators are disequal.

const_iterator & operator ++ ( ) ¶

Increment operator (prefix).

Returns :

A reference to the iterator after incrementing by one.

const_iterator operator ++ ( int ) ¶

Increment operator (postfix).

Returns :

A reference to the iterator after incrementing by one.

const DatatypeConstructor & operator * ( ) const ¶

Dereference operator.

Returns :

A reference to the constructor this iterator points to.

const DatatypeConstructor * operator -> ( ) const ¶

Dereference operator.

Returns :

A pointer to the constructor this iterator points to.