Cvc5DatatypeDecl 

This struct encapsulates a datatype declaration. A Cvc5DatatypeDecl is constructed via cvc5_mk_dt_decl() . This is not a datatype itself, but the representation of the specification for creating a datatype sort via cvc5_mk_dt_sort() and cvc5_mk_dt_sorts() .

typedef struct cvc5_dt_decl_t * Cvc5DatatypeDecl 

A cvc5 datatype declaration. A datatype declaration is not itself a datatype (see Datatype), but a specification for creating a datatype sort.

The interface for a datatype declaration coincides with the syntax for the SMT-LIB 2.6 command declare-datatype , or a single datatype within the declare-datatypes command.

Datatype sorts can be constructed from a Cvc5DatatypeDecl using:

• cvc5_mk_datatype_sort()

• cvc5_mk_datatype_sorts()

Cvc5DatatypeDecl cvc5_dt_decl_copy ( Cvc5DatatypeDecl decl ) 

Make copy of datatype declaration, increases reference counter of decl .

Note

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

Parameters :

decl – The datatype declaration to copy.

Returns :

The same datatype declarationwith its reference count increased by one.

void cvc5_dt_decl_release ( Cvc5DatatypeDecl decl ) 

Release copy of datatype declaration, decrements reference counter of decl .

Note

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

Parameters :

decl – The datatype declaration to release.

bool cvc5_dt_decl_is_equal ( Cvc5DatatypeDecl a , Cvc5DatatypeDecl b ) 

Compare two datatype declarations for structural equality.

Parameters :

• a – The first datatype declaration.

• b – The second datatype declaration.

Returns :

True if the datatype declarations are equal.

void cvc5_dt_decl_add_constructor ( Cvc5DatatypeDecl decl , Cvc5DatatypeConstructorDecl ctor ) 

Add datatype constructor declaration.

Parameters :

• decl – The datatype declaration.

• ctor – The datatype constructor declaration to add.

size_t cvc5_dt_decl_get_num_constructors ( Cvc5DatatypeDecl decl ) 

Get the number of constructors for a given Datatype declaration.

Parameters :

decl – The datatype declaration.

Returns :

The number of constructors.

bool cvc5_dt_decl_is_parametric ( Cvc5DatatypeDecl decl ) 

Determine if a given Datatype declaration is parametric.

Warning

This function is experimental and may change in future versions.

Parameters :

decl – The datatype declaration.

Returns :

True if the datatype declaration is parametric.

bool cvc5_dt_decl_is_resolved ( Cvc5DatatypeDecl decl ) 

Determine if a given datatype declaration is resolved (has already been used to declare a datatype).

Parameters :

decl – The datatype declaration.

Returns :

True if the datatype declaration is resolved.

const char * cvc5_dt_decl_to_string ( Cvc5DatatypeDecl decl ) 

Get a string representation of a given datatype declaration.

Note

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

Parameters :

decl – The datatype declaration.

Returns :

A string representation of the datatype declaration.

const char * cvc5_dt_decl_get_name ( Cvc5DatatypeDecl decl ) 

Get the name of a given datatype declaration.

Note

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

Parameters :

decl – The datatype declaration.

Returns :

The name of the datatype declaration.

size_t cvc5_dt_decl_hash ( Cvc5DatatypeDecl decl ) 

Compute the hash value of a datatype declaration.

Parameters :

term – The datatype declaration.

Returns :

The hash value of the datatype declaration.