Cvc5DatatypeSelector 

This struct represents a datatype selector. A Cvc5DatatypeSelector is specified via cvc5_dt_cons_decl_add_selector() , cvc5_dt_cons_decl_add_selector_self() and cvc5_dt_cons_decl_add_selector_unresolved() , when constructing a datatype sort and can be retrieved from a Cvc5DatatypeConstructor via cvc5_dt_cons_get_selector() .

typedef struct cvc5_dt_sel_t * Cvc5DatatypeSelector 

A cvc5 datatype selector.

Cvc5DatatypeSelector cvc5_dt_sel_copy ( Cvc5DatatypeSelector sel ) 

Make copy of datatype selector, increases reference counter of sel .

Note

This step is optional and allows users to manage resources in a more fine-grained manner.

Parameters :

sel – The datatype selector to copy.

Returns :

The same datatype selector with its reference count increased by one.

void cvc5_dt_sel_release ( Cvc5DatatypeSelector sel ) 

Release copy of datatype selector, decrements reference counter of sel .

Note

This step is optional and allows users to release resources in a more fine-grained manner. Further, any API function that returns a Cvc5DatatypeSelector returns a copy that is owned by the callee of the function and thus, can be released.

Parameters :

sel – The datatype selector to release.

bool cvc5_dt_sel_is_equal ( Cvc5DatatypeSelector a , Cvc5DatatypeSelector b ) 

Compare two datatype selectors for structural equality.

Parameters :

• a – The first datatype selector.

• b – The second datatype selector.

Returns :

True if the datatype selectors are equal.

const char * cvc5_dt_sel_get_name ( Cvc5DatatypeSelector sel ) 

Get the name of a given datatype selector.

Note

The returned char* pointer is only valid until the next call to this function.

Parameters :

sel – The datatype selector.

Returns :

The name of the Datatype selector.

Cvc5Term cvc5_dt_sel_get_term ( Cvc5DatatypeSelector sel ) 

Get the selector term of a given datatype selector.

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

Parameters :

sel – The datatype selector.

Returns :

The selector term.

Cvc5Term cvc5_dt_sel_get_updater_term ( Cvc5DatatypeSelector sel ) 

Get the updater term of a given datatype selector.

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

Parameters :

sel – The datatype selector.

Returns :

The updater term.

Cvc5Sort cvc5_dt_sel_get_codomain_sort ( Cvc5DatatypeSelector sel ) 

Get the codomain sort of a given datatype selector.

Parameters :

sel – The datatype selector.

Returns :

The codomain sort of the selector.

const char * cvc5_dt_sel_to_string ( Cvc5DatatypeSelector sel ) 

Get the string representation of a given datatype selector.

Note

The returned char* pointer is only valid until the next call to this function.

Parameters :

sel – The datatype selector.

Returns :

The string representation.

size_t cvc5_dt_sel_hash ( Cvc5DatatypeSelector sel ) 

Compute the hash value of a datatype selector.

Parameters :

term – The datatype selector.

Returns :

The hash value of the datatype selector.