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.