DatatypeSelector

class cvc5.DatatypeSelector

A cvc5 datatype selector.

Wrapper class for cvc5::DatatypeSelector.

getCodomainSort()

Returns:

The codomain sort of this selector.

getName()

Returns:

The name of this datatype selector.

getTerm()

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 of this datatype selector.

getUpdaterTerm()

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 of this datatype selector.

isNull()

Returns:

True if this DatatypeSelector is a null object.