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.