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.