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



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.

Note

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 selector with the given name.

Note

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

Get the name of this datatype.

Returns :

The name.

size_t getNumConstructors ( ) const

Get the number of constructors of this datatype.

Returns :

The number of constructors.

std :: vector < Sort > getParameters ( ) const

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

Note

Asserts that this datatype is parametric.

Warning

This function is experimental and may change in future versions.

Returns :

The parameters of this datatype.

bool isParametric ( ) const

Determine if this datatype is parametric.

Warning

This function is experimental and may change in future versions.

Returns :

True if this datatype is parametric.

bool isCodatatype ( ) const

Determine if this datatype corresponds to a co-datatype.

Returns :

True if this datatype corresponds to a co-datatype.

bool isTuple ( ) const

Determine if this datatype corresponds to a tuple.

Returns :

True if this datatype corresponds to a tuple.

bool isRecord ( ) const

Determine if this datatype corresponds to a record.

Warning

This function is experimental and may change in future versions.

Returns :

True if this datatype corresponds to a record.

bool isFinite ( ) const

Determine if a given datatype is finite.

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.


std :: ostream & cvc5 :: operator << ( std :: ostream & out , const Datatype & dtype )

Serialize a datatype to given stream.

Parameters :
  • out – The output stream.

  • dtype – The datatype to be serialized to given stream.

Returns :

The output stream.