Cvc5TermManager

This struct represents a cvc5 term manager instance.

Terms, Sorts and Ops are not tied to a Cvc5 but associated with a Cvc5TermManager instance, which can be shared between solver instances (and thus allows sharing of terms and sorts between solver instances).

Term kinds are defined via enum Cvc5Kind, and sort kinds via enum Cvc5SortKind.

Solver options are configured via cvc5_set_option() and queried via cvc5_get_option() (for more information on configuration options, see Options). Information about a specific option can be retrieved via cvc5_get_option_info() (see Cvc5OptionInfo).

typedef struct Cvc5TermManager Cvc5TermManager: A cvc5 term (and sort) manager.

Cvc5TermManager *cvc5_term_manager_new()

Construct a new instance of a cvc5 term manager.

Returns:: The cvc5 term manager.

void cvc5_term_manager_delete(Cvc5TermManager *tm)

Delete a cvc5 term manager instance.

Parameters:: tm – The term manager instance.

void cvc5_term_manager_release(Cvc5TermManager *tm)

Release all managed references.

This will free all memory used by any managed objects allocated by the term manager.

Note

This invalidates all managed objects created by the term manager.

Parameters:: tm – The term manager instance.

void cvc5_term_manager_print_stats_safe(Cvc5TermManager *tm, int fd)

Print the term manager statistics to the given file descriptor, suitable for usage in signal handlers.

Parameters:

tm – The term manager instance.
fd – The file descriptor.

Cvc5Statistics cvc5_term_manager_get_statistics(Cvc5TermManager *tm)

Get a snapshot of the current state of the statistic values of this term manager. The returned object is completely decoupled from the term manager and will not change when the term manager is used again.

Parameters:: tm – The term manager instance.
Returns:: A snapshot of the current state of the statistic values.

Sort Creation

Cvc5Sort cvc5_get_boolean_sort(Cvc5TermManager *tm)

Get the Boolean sort.

Parameters:: cvc5 – The solver instance.
Returns:: Sort Boolean.

Cvc5Sort cvc5_get_integer_sort(Cvc5TermManager *tm)

Get the Integer sort.

Parameters:: tm – The term manager instance.
Returns:: Sort Integer.

Cvc5Sort cvc5_get_real_sort(Cvc5TermManager *tm)

Get the Real sort.

Parameters:: tm – The term manager instance.
Returns:: Sort Real.

Cvc5Sort cvc5_get_regexp_sort(Cvc5TermManager *tm)

Get the regular expression sort.

Parameters:: tm – The term manager instance.
Returns:: Sort RegExp.

Cvc5Sort cvc5_get_rm_sort(Cvc5TermManager *tm)

Get the rounding mode sort.

Parameters:: tm – The term manager instance.
Returns:: The rounding mode sort.

Cvc5Sort cvc5_get_string_sort(Cvc5TermManager *tm)

Get the string sort.

Parameters:: tm – The term manager instance.
Returns:: Sort String.

Cvc5Sort cvc5_mk_array_sort(Cvc5TermManager *tm, Cvc5Sort index, Cvc5Sort elem)

Create an array sort.

Parameters:

tm – The term manager instance.
index – The array index sort.
elem – The array element sort.

Returns:

The array sort.

Cvc5Sort cvc5_mk_bv_sort(Cvc5TermManager *tm, uint32_t size)

Create a bit-vector sort.

Parameters:

tm – The term manager instance.
size – The bit-width of the bit-vector sort.

Returns:

The bit-vector sort.

Cvc5Sort cvc5_mk_fp_sort(Cvc5TermManager *tm, uint32_t exp, uint32_t sig)

Create a floating-point sort.

Parameters:

tm – The term manager instance.
exp – The bit-width of the exponent of the floating-point sort.
sig – The bit-width of the significand of the floating-point sort.

Cvc5Sort cvc5_mk_ff_sort(Cvc5TermManager *tm, const char *size, uint32_t base)

Create a finite-field sort from a given string of base n.

Parameters:

size – The modulus of the field. Must be prime.
base – The base of the string representation of size.

Returns:

The finite-field sort.

Cvc5Sort cvc5_mk_dt_sort(Cvc5TermManager *tm, Cvc5DatatypeDecl decl)

Create a datatype sort.

Parameters:

tm – The term manager instance.
decl – The datatype declaration from which the sort is created.

Returns:

The datatype sort.

const Cvc5Sort *cvc5_mk_dt_sorts(Cvc5TermManager *tm, size_t size, const Cvc5DatatypeDecl decls[])

Create a vector of datatype sorts.

Note

The names of the datatype declarations must be distinct.

Parameters:

tm – The term manager instance.
size – The number of datatype declarations.
decls – The datatype declarations from which the sort is created.

Returns:

The datatype sorts.

Cvc5Sort cvc5_mk_fun_sort(Cvc5TermManager *tm, size_t size, const Cvc5Sort sorts[], Cvc5Sort codomain)

Create function sort.

Parameters:

tm – The term manager instance.
size – The number of domain sorts.
sorts – The sort of the function arguments (the domain sorts).
codomain – The sort of the function return value.

Returns:

The function sort.

Cvc5Sort cvc5_mk_param_sort(Cvc5TermManager *tm, const char *symbol)

Create a sort parameter.

Warning

This function is experimental and may change in future versions.

Parameters:

tm – The term manager instance.
symbol – The name of the sort, may be NULL.

Returns:

The sort parameter.

Cvc5Sort cvc5_mk_predicate_sort(Cvc5TermManager *tm, size_t size, const Cvc5Sort sorts[])

Create a predicate sort.

Note

This is equivalent to calling mkFunctionSort() with the Boolean sort as the codomain.

Parameters:

cvc5 – The solver instance.
size – The number of sorts.
sorts – The list of sorts of the predicate.

Returns:

The predicate sort.

Cvc5Sort cvc5_mk_record_sort(Cvc5TermManager *tm, size_t size, const char *names[], const Cvc5Sort sorts[])

Create a record sort

Warning

This function is experimental and may change in future versions.

Parameters:

tm – The term manager instance.
names – The names of the fields of the record.
sorts – The sorts of the fields of the record.

Returns:

The record sort.

Cvc5Sort cvc5_mk_set_sort(Cvc5TermManager *tm, Cvc5Sort sort)

Create a set sort.

Parameters:

tm – The term manager instance.
sort – The sort of the set elements.

Returns:

The set sort.

Cvc5Sort cvc5_mk_bag_sort(Cvc5TermManager *tm, Cvc5Sort sort)

Create a bag sort.

Parameters:

tm – The term manager instance.
sort – The sort of the bag elements.

Returns:

The bag sort.

Cvc5Sort cvc5_mk_sequence_sort(Cvc5TermManager *tm, Cvc5Sort sort)

Create a sequence sort.

Parameters:

tm – The term manager instance.
elemSort – The sort of the sequence elements.

Returns:

The sequence sort.

Cvc5Sort cvc5_mk_abstract_sort(Cvc5TermManager *tm, Cvc5SortKind k)

Create an abstract sort. An abstract sort represents a sort for a given kind whose parameters and arguments are unspecified.

The kind k must be the kind of a sort that can be abstracted, i.e., a sort that has indices or argument sorts. For example, #CVC5_KIND_ARRAY_SORT and CVC5_SORT_KIND_BITVECTOR_SORT can be passed as the kind k to this function, while CVC5_SORT_KIND_INTEGER_SORT and CVC5_SORT_KIND_STRING_SORT cannot.

Note

Providing the kind CVC5_SORT_KIND_ABSTRACT_SORT as an argument to this function returns the (fully) unspecified sort, denoted ?.

Note

Providing a kind k that has no indices and a fixed arity of argument sorts will return the sort of kind k whose arguments are the unspecified sort. For example, cvc5_mk_abstract_sort(tm, CVC5_SORT_KIND_ARRAY_SORT) will return the sort (ARRAY_SORT ? ?) instead of the abstract sort whose abstract kind is CVC5_SORT_KIND_ARRAY_SORT.

Warning

This function is experimental and may change in future versions.

Parameters:

tm – The term manager instance.
k – The kind of the abstract sort

Returns:

The abstract sort.

Cvc5Sort cvc5_mk_uninterpreted_sort(Cvc5TermManager *tm, const char *symbol)

Create an uninterpreted sort.

Parameters:

tm – The term manager instance.
symbol – The name of the sort, may be NULL.

Returns:

The uninterpreted sort.

Cvc5Sort cvc5_mk_unresolved_dt_sort(Cvc5TermManager *tm, const char *symbol, size_t arity)

Create an unresolved datatype sort.

This is for creating yet unresolved sort placeholders for mutually recursive parametric datatypes.

Warning

This function is experimental and may change in future versions.

Parameters:

tm – The term manager instance.
symbol – The symbol of the sort.
arity – The number of sort parameters of the sort.

Returns:

The unresolved sort.

Cvc5Sort cvc5_mk_uninterpreted_sort_constructor_sort(Cvc5TermManager *tm, size_t arity, const char *symbol)

Create an uninterpreted sort constructor sort.

An uninterpreted sort constructor is an uninterpreted sort with arity > 0.

Parameters:

tm – The term manager instance.
symbol – The symbol of the sort.
arity – The arity of the sort (must be > 0)

Returns:

The uninterpreted sort constructor sort.

Cvc5Sort cvc5_mk_tuple_sort(Cvc5TermManager *tm, size_t size, const Cvc5Sort sorts[])

Create a tuple sort.

Parameters:

tm – The term manager instance.
size – The number of sorts.
sorts – The sorts of f the elements of the tuple.

Returns:

The tuple sort.

Cvc5Sort cvc5_mk_nullable_sort(Cvc5TermManager *tm, Cvc5Sort sort)

Create a nullable sort.

Parameters:

tm – The term manager instance.
sort – The sort of the element of the nullable.

Returns:

The nullable sort.

Operator Creation

Cvc5Op cvc5_mk_op(Cvc5TermManager *tm, Cvc5Kind kind, size_t size, const uint32_t idxs[])

Create operator of Kind:

See Cvc5Kind for a description of the parameters.

Note

If idxs is empty, the Cvc5Op simply wraps the Cvc5Kind. The Cvc5Kind can be used in cvc5_mk_term directly without creating a Cvc5Op first.

Parameters:

tm – The term manager instance.
kind – The kind of the operator.
size – The number of indices of the operator.
idxs – The indices.

Cvc5Op cvc5_mk_op_from_str(Cvc5TermManager *tm, Cvc5Kind kind, const char *arg)

Create operator of kind:

CVC5_KIND_DIVISIBLE (to support arbitrary precision integers)

See CKind for a description of the parameters.

Parameters:

tm – The term manager instance.
kind – The kind of the operator.
arg – The string argument to this operator.

Term Creation

Cvc5Term cvc5_mk_term(Cvc5TermManager *tm, Cvc5Kind kind, size_t size, const Cvc5Term children[])

Create n-ary term of given kind.

Parameters:

tm – The term manager instance.
kind – The kind of the term.
size – The number of childrens.
children – The children of the term.

Returns:

The Term

Cvc5Term cvc5_mk_term_from_op(Cvc5TermManager *tm, Cvc5Op op, size_t size, const Cvc5Term children[])

Create n-ary term of given kind from a given operator. Create operators with cvc5_mk_op() and cvc5_mk_op_from_str().

Parameters:

tm – The term manager instance.
op – The operator.
size – The number of children.
children – The children of the term.

Returns:

The Term.

Cvc5Term cvc5_mk_tuple(Cvc5TermManager *tm, size_t size, const Cvc5Term terms[])

Create a tuple term.

Parameters:

tm – The term manager instance.
size – The number of elements in the tuple.
terms – The elements.

Returns:

The tuple Term.

Cvc5Term cvc5_mk_nullable_some(Cvc5TermManager *tm, Cvc5Term term)

Create a nullable some term.

Parameters:

tm – The term manager instance.
term – The element value.

Returns:

the Element value wrapped in some constructor.

Cvc5Term cvc5_mk_nullable_val(Cvc5TermManager *tm, Cvc5Term term)

Create a selector for nullable term.

Parameters:

tm – The term manager instance.
term – A nullable term.

Returns:

The element value of the nullable term.

Cvc5Term cvc5_mk_nullable_is_null(Cvc5TermManager *tm, Cvc5Term term)

Create a null tester for a nullable term.

Parameters:

tm – The term manager instance.
term – A nullable term.

Returns:

A tester whether term is null.

Cvc5Term cvc5_mk_nullable_is_some(Cvc5TermManager *tm, Cvc5Term term)

Create a some tester for a nullable term.

Parameters:

tm – The term manager instance.
term – A nullable term.

Returns:

A tester whether term is some.

Cvc5Term cvc5_mk_nullable_null(Cvc5TermManager *tm, Cvc5Sort sort)

Create a constant representing an null of the given sort.

Parameters:

tm – The term manager instance.
sort – The sort of the Nullable element.

Returns:

The null constant.

Cvc5Term cvc5_mk_nullable_lift(Cvc5TermManager *tm, Cvc5Kind kind, size_t size, const Cvc5Term args[])

Create a term that lifts kind to nullable terms.

Example: If we have the term ((_ nullable.lift +) x y), where x, y of type (Nullable Int), then kind would be ADD, and args would be [x, y]. This function would return (nullable.lift (lambda ((a Int) (b Int)) (+ a b)) x y)

Parameters:

tm – The term manager instance.
kind – The lifted operator.
size – The number of arguments of the lifted operator.
args – The arguments of the lifted operator.

Returns:

A term of kind CVC5_KIND_NULLABLE_LIFT where the first child is a lambda expression, and the remaining children are the original arguments.

Cvc5Term cvc5_mk_skolem(Cvc5TermManager *tm, Cvc5SkolemId id, size_t size, const Cvc5Term indices[])

Create a skolem.

Parameters:

tm – The term manager instance.
id – The skolem identifier.
size – The number of arguments of the lifted operator.
indices – The indices of the skolem.

Returns:

The skolem.

size_t cvc5_get_num_idxs_for_skolem_id(Cvc5TermManager *tm, Cvc5SkolemId id)

Get the number of indices for a skolem id.

Parameters:: id – The skolem id.
Returns:: The number of indices for the skolem id.

Cvc5Term cvc5_mk_true(Cvc5TermManager *tm)

Create a Boolean true constant.

Parameters:: tm – The term manager instance.
Returns:: The true constant.

Cvc5Term cvc5_mk_false(Cvc5TermManager *tm)

Create a Boolean false constant.

Parameters:: tm – The term manager instance.
Returns:: The false constant.

Cvc5Term cvc5_mk_boolean(Cvc5TermManager *tm, bool val)

Create a Boolean constant.

Parameters:

tm – The term manager instance.
val – The value of the constant.

Returns:

The Boolean constant.

Cvc5Term cvc5_mk_pi(Cvc5TermManager *tm)

Create a constant representing the number Pi.

Parameters:: tm – The term manager instance.
Returns:: A constant representing Pi.

Cvc5Term cvc5_mk_integer(Cvc5TermManager *tm, const char *s)

Create an integer constant from a string.

Parameters:

tm – The term manager instance.
s – The string representation of the constant, may represent an integer (e.g., “123”).

Returns:

A constant of sort Integer assuming s represents an integer)

Cvc5Term cvc5_mk_integer_int64(Cvc5TermManager *tm, int64_t val)

Create an integer constant from a c++ int.

Parameters:

tm – The term manager instance.
val – The value of the constant.

Returns:

A constant of sort Integer.

Cvc5Term cvc5_mk_real(Cvc5TermManager *tm, const char *s)

Create a real constant from a string.

Parameters:

tm – The term manager instance.
s – The string representation of the constant, may represent an integer (e.g., “123”) or real constant (e.g., “12.34” or “12/34”).

Returns:

A constant of sort Real.

Cvc5Term cvc5_mk_real_int64(Cvc5TermManager *tm, int64_t val)

Create a real constant from an integer.

Parameters:

tm – The term manager instance.
val – The value of the constant.

Returns:

A constant of sort Integer.

Cvc5Term cvc5_mk_real_num_den(Cvc5TermManager *tm, int64_t num, int64_t den)

Create a real constant from a rational.

Parameters:

tm – The term manager instance.
num – The value of the numerator.
den – The value of the denominator.

Returns:

A constant of sort Real.

Cvc5Term cvc5_mk_regexp_all(Cvc5TermManager *tm)

Create a regular expression all (re.all) term.

Parameters:: tm – The term manager instance.
Returns:: The all term.

Cvc5Term cvc5_mk_regexp_allchar(Cvc5TermManager *tm)

Create a regular expression allchar (re.allchar) term.

Parameters:: tm – The term manager instance.
Returns:: The allchar term.

Cvc5Term cvc5_mk_regexp_none(Cvc5TermManager *tm)

Create a regular expression none (re.none) term.

Parameters:: tm – The term manager instance.
Returns:: The none term.

Cvc5Term cvc5_mk_empty_set(Cvc5TermManager *tm, Cvc5Sort sort)

Create a constant representing an empty set of the given sort.

Parameters:

tm – The term manager instance.
sort – The sort of the set elements.

Returns:

The empty set constant.

Cvc5Term cvc5_mk_empty_bag(Cvc5TermManager *tm, Cvc5Sort sort)

Create a constant representing an empty bag of the given sort.

Parameters:

tm – The term manager instance.
sort – The sort of the bag elements.

Returns:

The empty bag constant.

Cvc5Term cvc5_mk_sep_emp(Cvc5TermManager *tm)

Create a separation logic empty term.

Warning

This function is experimental and may change in future versions.

Parameters:: tm – The term manager instance.
Returns:: The separation logic empty term.

Cvc5Term cvc5_mk_sep_nil(Cvc5TermManager *tm, Cvc5Sort sort)

Create a separation logic nil term.

Warning

This function is experimental and may change in future versions.

Parameters:

tm – The term manager instance.
sort – The sort of the nil term.

Returns:

The separation logic nil term.

Cvc5Term cvc5_mk_string(Cvc5TermManager *tm, const char *s, bool use_esc_seq)

Create a String constant from a regular character string which may contain SMT-LIB compatible escape sequences like \u1234 to encode unicode characters.

Parameters:

tm – The term manager instance.
s – The string this constant represents.
use_esc_seq – Determines whether escape sequences in s should. be converted to the corresponding unicode character

Returns:

The String constant.

Cvc5Term cvc5_mk_string_from_wchar(Cvc5TermManager *tm, const wchar_t *s)

Create a String constant from a wide character string. This function does not support escape sequences as wide character already supports unicode characters.

Parameters:

tm – The term manager instance.
s – The string this constant represents.

Returns:

The String constant.

Cvc5Term cvc5_mk_empty_sequence(Cvc5TermManager *tm, Cvc5Sort sort)

Create an empty sequence of the given element sort.

Parameters:

tm – The term manager instance.
sort – The element sort of the sequence.

Returns:

The empty sequence with given element sort.

Cvc5Term cvc5_mk_universe_set(Cvc5TermManager *tm, Cvc5Sort sort)

Create a universe set of the given sort.

Parameters:

tm – The term manager instance.
sort – The sort of the set elements.

Returns:

The universe set constant.

Cvc5Term cvc5_mk_bv_uint64(Cvc5TermManager *tm, uint32_t size, uint64_t val)

Create a bit-vector constant of given size and value.

Note

The given value must fit into a bit-vector of the given size.

Parameters:

tm – The term manager instance.
size – The bit-width of the bit-vector sort.
val – The value of the constant.

Returns:

The bit-vector constant.

Cvc5Term cvc5_mk_bv(Cvc5TermManager *tm, uint32_t size, const char *s, uint32_t base)

Create a bit-vector constant of a given bit-width from a given string of base 2, 10 or 16.

Note

The given value must fit into a bit-vector of the given size.

Parameters:

tm – The term manager instance.
size – The bit-width of the constant.
s – The string representation of the constant.
base – The base of the string representation (2 for binary, 10 for decimal, and 16 for hexadecimal).

Returns:

The bit-vector constant.

Cvc5Term cvc5_mk_ff_elem(Cvc5TermManager *tm, const char *value, Cvc5Sort sort, uint32_t base)

Create a finite field constant in a given field from a given string of base n.

If size is the field size, the constant needs not be in the range [0,size). If it is outside this range, it will be reduced modulo size before being constructed.

Parameters:

value – The string representation of the constant.
sort – The field sort.
base – The base of the string representation of value.

Cvc5Term cvc5_mk_const_array(Cvc5TermManager *tm, Cvc5Sort sort, Cvc5Term val)

Create a constant array with the provided constant value stored at every index.

Parameters:

tm – The term manager instance.
sort – The sort of the constant array (must be an array sort).
val – The constant value to store (must match the sort’s element sort).

Returns:

The constant array term.

Cvc5Term cvc5_mk_fp_pos_inf(Cvc5TermManager *tm, uint32_t exp, uint32_t sig)

Create a positive infinity floating-point constant (SMT-LIB: +oo).

Parameters:

tm – The term manager instance.
exp – Number of bits in the exponent.
sig – Number of bits in the significand.

Returns:

The floating-point constant.

Cvc5Term cvc5_mk_fp_neg_inf(Cvc5TermManager *tm, uint32_t exp, uint32_t sig)

Create a negative infinity floating-point constant (SMT-LIB: -oo).

Parameters:

tm – The term manager instance.
exp – Number of bits in the exponent.
sig – Number of bits in the significand.

Returns:

The floating-point constant.

Cvc5Term cvc5_mk_fp_nan(Cvc5TermManager *tm, uint32_t exp, uint32_t sig)

Create a not-a-number floating-point constant (Cvc5TermManager* tm, SMT-LIB: NaN).

Parameters:

tm – The term manager instance.
exp – Number of bits in the exponent.
sig – Number of bits in the significand.

Returns:

The floating-point constant.

Cvc5Term cvc5_mk_fp_pos_zero(Cvc5TermManager *tm, uint32_t exp, uint32_t sig)

Create a positive zero floating-point constant (Cvc5TermManager* tm, SMT-LIB: +zero).

Parameters:

tm – The term manager instance.
exp – Number of bits in the exponent.
sig – Number of bits in the significand.

Returns:

The floating-point constant.

Cvc5Term cvc5_mk_fp_neg_zero(Cvc5TermManager *tm, uint32_t exp, uint32_t sig)

Create a negative zero floating-point constant (Cvc5TermManager* tm, SMT-LIB: -zero).

Parameters:

tm – The term manager instance.
exp – Number of bits in the exponent.
sig – Number of bits in the significand.

Returns:

The floating-point constant.

Cvc5Term cvc5_mk_rm(Cvc5TermManager *tm, Cvc5RoundingMode rm)

Create a rounding mode value.

Parameters:

tm – The term manager instance.
rm – The floating point rounding mode this constant represents.

Returns:

The rounding mode value.

Cvc5Term cvc5_mk_fp(Cvc5TermManager *tm, uint32_t exp, uint32_t sig, Cvc5Term val)

Create a floating-point value from a bit-vector given in IEEE-754 format.

Parameters:

tm – The term manager instance.
exp – Size of the exponent.
sig – Size of the significand.
val – Value of the floating-point constant as a bit-vector term.

Returns:

The floating-point value.

Cvc5Term cvc5_mk_fp_from_ieee(Cvc5TermManager *tm, Cvc5Term sign, Cvc5Term exp, Cvc5Term sig)

Create a floating-point value from its three IEEE-754 bit-vector value components (sign bit, exponent, significand).

Parameters:

tm – The term manager instance.
sign – The sign bit.
exp – The bit-vector representing the exponent.
sig – The bit-vector representing the significand.

Returns:

The floating-point value.

Cvc5Term cvc5_mk_cardinality_constraint(Cvc5TermManager *tm, Cvc5Sort sort, uint32_t upperBound)

Create a cardinality constraint for an uninterpreted sort.

Warning

This function is experimental and may change in future versions.

Parameters:

tm – The term manager instance.
sort – The sort the cardinality constraint is for.
upperBound – The upper bound on the cardinality of the sort.

Returns:

The cardinality constraint.

Cvc5Term cvc5_mk_const(Cvc5TermManager *tm, Cvc5Sort sort, const char *symbol)

Create a free constant.

SMT-LIB:

(declare-const <symbol> <sort>)
(declare-fun <symbol> () <sort>)

Parameters:

tm – The term manager instance.
sort – The sort of the constant.
symbol – The name of the constant, may be NULL.

Returns:

The constant.

Cvc5Term cvc5_mk_var(Cvc5TermManager *tm, Cvc5Sort sort, const char *symbol)

Create a bound variable to be used in a binder (i.e., a quantifier, a lambda, or a witness binder).

Parameters:

tm – The term manager instance.
sort – The sort of the variable.
symbol – The name of the variable, may be NULL.

Returns:

The variable.

Datatype Declaration Creation

Cvc5DatatypeDecl cvc5_mk_dt_decl(Cvc5TermManager *tm, const char *name, bool is_codt)

Create a datatype declaration.

Parameters:

tm – The term manager instance.
name – The name of the datatype.
is_codt – True if a codatatype is to be constructed.

Returns:

The Cvc5DatatypeDecl.

Cvc5DatatypeDecl cvc5_mk_dt_decl_with_params(Cvc5TermManager *tm, const char *name, size_t size, const Cvc5Sort params[], bool is_codt)

Create a datatype declaration. Create sorts parameter with cvc5_mk_param_sort().

Warning

This function is experimental and may change in future versions.

Parameters:

tm – The term manager instance.
name – The name of the datatype.
size – The number of sort parameters.
params – A list of sort parameters.
is_codt – True if a codatatype is to be constructed.

Returns:

The Cvc5DatatypeDecl.

Datatype Constructor Declaration Creation

Cvc5DatatypeConstructorDecl cvc5_mk_dt_cons_decl(Cvc5TermManager *tm, const char *name)

Create a datatype constructor declaration.

Parameters:

tm – The term manager instance.
name – The name of the datatype constructor.

Returns:

The DatatypeConstructorDecl.