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:

term – The datatype constructor declaration.

Returns:

The hash value of the datatype constructor declaration.