Cvc5DatatypeConstructor

This struct represents a datatype constructor. Datatype constructors are specified by a datatype constructor declaration via cvc5_mk_dt_cons_decl() when constructing a datatype sort and can be retrieved from a Cvc5Datatype via cvc5_dt_get_constructor().

typedef struct cvc5_dt_cons_t *Cvc5DatatypeConstructor

A cvc5 datatype constructor.

Cvc5DatatypeConstructor cvc5_dt_cons_copy(Cvc5DatatypeConstructor cons)

Make copy of datatype constructor, increases reference counter of cons.

Note

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

Parameters:

cons – The datatype constructor to copy.

Returns:

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

void cvc5_dt_cons_release(Cvc5DatatypeConstructor cons)

Release copy of datatype constructor, decrements reference counter of cons.

Note

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

Parameters:

cons – The datatype constructor to release.

bool cvc5_dt_cons_is_equal(Cvc5DatatypeConstructor a, Cvc5DatatypeConstructor b)

Compare two datatype constructors for structural equality.

Parameters:

• a – The first datatype constructor.

• b – The second datatype constructor.

Returns:

True if the datatype constructors are equal.

const char *cvc5_dt_cons_get_name(Cvc5DatatypeConstructor cons)

Get the name of a given datatype constructor.

Note

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

Parameters:

cons – The datatype constructor.

Returns:

The name.

Cvc5Term cvc5_dt_cons_get_term(Cvc5DatatypeConstructor cons)

Get the constructor term of a given datatype constructor.

Datatype constructors are a special class of function-like terms whose sort is datatype constructor (cvc5_sort_is_dt_constructor()). All datatype constructors, including nullary ones, should be used as the first argument to Terms whose kind is CVC5_KIND_APPLY_CONSTRUCTOR. For example, the nil list can be constructed by cvc5_mk_term(CVC5_KIND_APPLY_CONSTRUCTOR, {t}), where t is the term returned by this function.

Note

This function should not be used for parametric datatypes. Instead, use the function cvc5_dt_cons_get_instantiated_term() below.

Parameters:

cons – The datatype constructor.

Returns:

The constructor term.

Cvc5Term cvc5_dt_cons_get_instantiated_term(Cvc5DatatypeConstructor cons, Cvc5Sort sort)

Get the constructor term of this datatype constructor whose return type is sort.

This function is intended to be used on constructors of parametric datatypes and can be seen as returning the constructor term that has been explicitly cast to the given sort.

This function is required for constructors of parametric datatypes whose return type cannot be determined by type inference. For example, given:

(declare-datatype List
    (par (T) ((nil) (cons (head T) (tail (List T))))))

The type of nil terms must be provided by the user. In SMT version 2.6, this is done via the syntax for qualified identifiers:

(as nil (List Int))

This function is equivalent of applying the above, where the datatype constructor is the one corresponding to nil, and sort is (List Int).

Note

The returned constructor term t is used to construct the above (nullary) application of nil with cvc5_mk_term(CVC5_KIND_APPLY_CONSTRUCTOR, {t}).

Warning

This function is experimental and may change in future versions.

Parameters:

• cons – The datatype constructor.

• sort – The desired return sort of the constructor.

Returns:

The constructor term.

Cvc5Term cvc5_dt_cons_get_tester_term(Cvc5DatatypeConstructor cons)

Get the tester term of a given datatype constructor.

Similar to constructors, testers are a class of function-like terms of tester sort (cvc5_sort_is_dt_constructor()) which should be used as the first argument of Terms of kind CVC5_KIND_APPLY_TESTER.

Parameters:

cons – The datatype constructor.

Returns:

The tester term.

size_t cvc5_dt_cons_get_num_selectors(Cvc5DatatypeConstructor cons)

Get the number of selectors of a given datatype constructor.

Parameters:

cons – The datatype constructor.

Returns:

The number of selectors.

Cvc5DatatypeSelector cvc5_dt_cons_get_selector(Cvc5DatatypeConstructor cons, size_t index)

Get the selector at index i of a given datatype constructor.

Parameters:

cons – The datatype constructor.

Returns:

The i^th DatatypeSelector.

Cvc5DatatypeSelector cvc5_dt_cons_get_selector_by_name(Cvc5DatatypeConstructor cons, const char *name)

Get the datatype selector with the given name.

Note

This is a linear search through the selectors, so in case of multiple, similarly-named selectors, the first is returned.

Parameters:

• cons – The datatype constructor.

• name – The name of the datatype selector.

Returns:

The first datatype selector with the given name.

const char *cvc5_dt_cons_to_string(Cvc5DatatypeConstructor cons)

Get a string representation of a given datatype constructor.

Note

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

Parameters:

cons – The datatype constructor.

Returns:

The string representation.

size_t cvc5_dt_cons_hash(Cvc5DatatypeConstructor cons)

Compute the hash value of a datatype constructor.

Parameters:

term – The datatype constructor.

Returns:

The hash value of the datatype constructor.