Cvc5Datatype

This struct represents a datatype. A Cvc5Datatype is encapsulated by a datatype sort and can be retrieved from a datatype sort via cvc5_sort_get_datatype(). Datatypes are specified by a Cvc5DatatypeDecl via cvc5_mk_dt_decl() when constructing a datatype sort.

typedef struct cvc5_dt_t *Cvc5Datatype

A cvc5 datatype.

Cvc5Datatype cvc5_dt_copy(Cvc5Datatype dt)

Make copy of datatype, increases reference counter of dt.

Note

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

Parameters:

dt – The datatype to copy.

Returns:

The same datatype with its reference count increased by one.

void cvc5_dt_release(Cvc5Datatype dt)

Release copy of datatype, decrements reference counter of dt.

Note

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

Parameters:

dt – The datatype to release.

bool cvc5_dt_is_equal(Cvc5Datatype a, Cvc5Datatype b)

Compare two datatypes for structural equality.

Parameters:

• a – The first datatype.

• b – The second datatype.

Returns:

True if the datatypes are equal.

Cvc5DatatypeConstructor cvc5_dt_get_constructor(Cvc5Datatype dt, size_t idx)

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

Parameters:

• dt – The datatype.

• idx – The index of the datatype constructor to return.

Returns:

The datatype constructor with the given index.

Cvc5DatatypeConstructor cvc5_dt_get_constructor_by_name(Cvc5Datatype dt, const char *name)

Get the datatype constructor of a given datatype with the given name.

Note

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

Parameters:

• dt – The datatype.

• name – The name of the datatype constructor.

Returns:

The datatype constructor with the given name.

Cvc5DatatypeSelector cvc5_dt_get_selector(Cvc5Datatype dt, const char *name)

Get the datatype selector of a given datatype with the given name.

Note

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

Parameters:

• dt – The datatype.

• name – The name of the datatype selector.

Returns:

The datatype selector with the given name.

const char *cvc5_dt_get_name(Cvc5Datatype dt)

Get the name of a given datatype.

Note

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

Parameters:

dt – The datatype.

Returns:

The name.

size_t cvc5_dt_get_num_constructors(Cvc5Datatype dt)

Get the number of constructors of a given datatype.

Parameters:

dt – The datatype.

Returns:

The number of constructors.

const Cvc5Sort *cvc5_dt_get_parameters(Cvc5Datatype dt, size_t *size)

Get the parameters of a given datatype, if it is parametric.

Note

Asserts that this datatype is parametric.

Warning

This function is experimental and may change in future versions.

Parameters:

• dt – The datatype.

• size – The size of the resulting array.

Returns:

The parameters of this datatype.

bool cvc5_dt_is_parametric(Cvc5Datatype dt)

Determine if a given datatype is parametric.

Warning

This function is experimental and may change in future versions.

Parameters:

dt – The datatype.

Returns:

True if the datatype is parametric.

bool cvc5_dt_is_codatatype(Cvc5Datatype dt)

Determine if a given datatype corresponds to a co-datatype.

Parameters:

dt – The datatype.

Returns:

True if the datatype corresponds to a co-datatype.

bool cvc5_dt_is_tuple(Cvc5Datatype dt)

Determine if a given datatype corresponds to a tuple.

Parameters:

dt – The datatype.

Returns:

True if this datatype corresponds to a tuple.

bool cvc5_dt_is_record(Cvc5Datatype dt)

Determine if a given datatype corresponds to a record.

Warning

This function is experimental and may change in future versions.

Parameters:

dt – The datatype.

Returns:

True if the datatype corresponds to a record.

bool cvc5_dt_is_finite(Cvc5Datatype dt)

Determine if a given datatype is finite.

Parameters:

dt – The datatype.

Returns:

True if the datatype is finite.

bool cvc5_dt_is_well_founded(Cvc5Datatype dt)

Determine if a given datatype is well-founded.

If the datatype is not a codatatype, this returns false if there are no values of the datatype that are of finite size.

Parameters:

dt – The datatype.

Returns:

True if the datatype is well-founded.

const char *cvc5_dt_to_string(Cvc5Datatype dt)

Get a string representation of a given datatype.

Note

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

Returns:

The string representation.

size_t cvc5_dt_hash(Cvc5Datatype dt)

Compute the hash value of a datatype.

Parameters:

term – The datatype.

Returns:

The hash value of the datatype.