DatatypeSelector ¶

class DatatypeSelector ¶

A cvc5 datatype selector.

Public Functions

DatatypeSelector ( ) ¶

Constructor.

~DatatypeSelector ( ) ¶

Destructor.

std :: string getName ( ) const ¶

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 ¶

Returns :

The codomain sort of this selector.

bool isNull ( ) const ¶

Returns :

True if this DatatypeSelector is a null object.

std :: string toString ( ) const ¶

Returns :

A string representation of this datatype selector.