DatatypeSelector

This class represents a datatype selector. Datatype selectors are specified via cvc5::DatatypeConstructorDecl::addSelector(), cvc5::DatatypeConstructorDecl::addSelectorSelf() and cvc5::DatatypeConstructorDecl::addSelectorUnresolved() when constructing a datatype sort and can be retrieved from a cvc5::DatatypeConstructor via cvc5::DatatypeConstructor::getSelector().

class DatatypeSelector

A cvc5 datatype selector.

Public Functions

DatatypeSelector()

Constructor.

~DatatypeSelector()

Destructor.

bool operator==(const DatatypeSelector &sel) const

Equality operator.

Parameters:

sel – The datatype selector to compare to for equality.

Returns:

True if the datatype selectors are equal.

std::string getName() const

Get the name of this datatype selector.

Returns:

The name of this Datatype selector.

Term getTerm() const

Get the selector term of this datatype selector.

Selector terms are a class of function-like terms of selector sort (Sort::isDatatypeSelector()), and should be used as the first argument of Terms of kind APPLY_SELECTOR.

Returns:

The selector term.

Term getUpdaterTerm() const

Get the updater term of this datatype selector.

Similar to selectors, updater terms are a class of function-like terms of updater Sort (Sort::isDatatypeUpdater()), and should be used as the first argument of Terms of kind APPLY_UPDATER.

Returns:

The updater term.

Sort getCodomainSort() const

Get the codomain sort of this selector.

Returns:

The codomain sort of this selector.

bool isNull() const
Returns:

True if this DatatypeSelector is a null object.

std::string toString() const

Get the string representation of this datatype selector.

Returns:

The string representation.

Friends

friend struct std::hash< DatatypeSelector >
std::ostream &cvc5::operator<<(std::ostream &out, const DatatypeSelector &stor)

Serialize a datatype selector to given stream.

Parameters:

  • out – The output stream.

  • stor – The datatype selector to be serialized to given stream.

Returns:

The output stream.