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

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

class Datatype 

A cvc5 datatype.

Public Functions

Datatype ( ) 

Constructor.

~Datatype ( ) 

Destructor.

bool operator == ( const Datatype & dt ) const 

Equality operator.

Parameters :

dt – The datatype to compare to for equality.

Returns :

True if the datatypes are equal.

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.

Friends

friend struct std::hash< 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.