Cvc5DatatypeConstructorDecl 

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

typedef struct cvc5_dt_cons_decl_t * Cvc5DatatypeConstructorDecl 

A cvc5 datatype constructor declaration. A datatype constructor declaration is a specification used for creating a datatype constructor.

Cvc5DatatypeConstructorDecl cvc5_dt_cons_decl_copy ( Cvc5DatatypeConstructorDecl decl ) 

Make copy of datatype constructor 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 constructor declaration to copy.

Returns :

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

void cvc5_dt_cons_decl_release ( Cvc5DatatypeConstructorDecl decl ) 

Release copy of datatype constructor 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 Cvc5DatatypeConstructorDecl returns a copy that is owned by the callee of the function and thus, can be released.

Parameters :

decl – The datatype constructor declaration to release.

bool cvc5_dt_cons_decl_is_equal ( Cvc5DatatypeConstructorDecl a , Cvc5DatatypeConstructorDecl b ) 

Compare two datatype constructor declarations for structural equality.

Parameters :

• a – The first datatype constructor declaration.

• b – The second datatype constructor declaration.

Returns :

True if the datatype constructor declarations are equal.

void cvc5_dt_cons_decl_add_selector ( Cvc5DatatypeConstructorDecl decl , const char * name , Cvc5Sort sort ) 

Add datatype selector declaration to a given constructor declaration.

Parameters :

• decl – The datatype constructor declaration.

• name – The name of the datatype selector declaration to add.

• sort – The codomain sort of the datatype selector declaration to add.

void cvc5_dt_cons_decl_add_selector_self ( Cvc5DatatypeConstructorDecl decl , const char * name ) 

Add datatype selector declaration whose codomain type is the datatype itself to a given constructor declaration.

Parameters :

• decl – The datatype constructor declaration.

• name – The name of the datatype selector declaration to add.

void cvc5_dt_cons_decl_add_selector_unresolved ( Cvc5DatatypeConstructorDecl decl , const char * name , const char * unres_name ) 

Add datatype selector declaration whose codomain sort is an unresolved datatype with the given name to a given constructor declaration.

Parameters :

• decl – The datatype constructor declaration.

• name – The name of the datatype selector declaration to add.

• unres_name – The name of the unresolved datatype. The codomain of the selector will be the resolved datatype with the given name.

const char * cvc5_dt_cons_decl_to_string ( Cvc5DatatypeConstructorDecl decl ) 

Get a string representation of a given constructor declaration.

Note

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

Parameters :

decl – The datatype constructor declaration.

Returns :

The string representation.

size_t cvc5_dt_cons_decl_hash ( Cvc5DatatypeConstructorDecl decl ) 

Compute the hash value of a datatype constructor declaration.

Parameters :

decl – The datatype constructor declaration.

Returns :

The hash value of the datatype constructor declaration.