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.