DatatypeSelector 

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

• class cvc5::DatatypeSelector

• std::ostream& cvc5::operator<< (std::ostream& out, const DatatypeSelector& sel)

class DatatypeSelector 

A cvc5 datatype selector.

Public Functions

DatatypeSelector ( ) 

Constructor.

~DatatypeSelector ( ) 

Destructor.

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.

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.