BitwuzlaSort

Bitwuzla supports array (SMT-LIB: Array), Boolean (SMT-LIB: Bool), bit-vector (SMT-LIB: (_ BitVec n)), floating-point (SMT-LIB: (_ FloatingPoint e s)), rounding mode (SMT-LIB: RoundingMode), and uninterpreted sorts (SMT-LIB: declare-sort). As for array sorts, this includes nested arrays, i.e., array sorts where the element sort is an array sort.

• typedef struct BitwuzlaSort

• bitwuzla_sort_hash()

• bitwuzla_sort_copy()

• bitwuzla_sort_release()

• bitwuzla_sort_bv_get_size()

• bitwuzla_sort_fp_get_exp_size()

• bitwuzla_sort_fp_get_sig_size()

• bitwuzla_sort_array_get_index()

• bitwuzla_sort_array_get_element()

• bitwuzla_sort_fun_get_domain_sorts()

• bitwuzla_sort_fun_get_codomain()

• bitwuzla_sort_fun_get_arity()

• bitwuzla_sort_get_uninterpreted_symbol()

• bitwuzla_sort_is_array()

• bitwuzla_sort_is_bool()

• bitwuzla_sort_is_bv()

• bitwuzla_sort_is_fp()

• bitwuzla_sort_is_fun()

• bitwuzla_sort_is_rm()

• bitwuzla_sort_is_uninterpreted()

• bitwuzla_sort_to_string()

• bitwuzla_sort_print()

typedef struct bitwuzla_sort_t *BitwuzlaSort

A Bitwuzla sort.

size_t bitwuzla_sort_hash(BitwuzlaSort sort)

Compute the hash value for a sort.

Parameters:

sort – The sort.

Returns:

The hash value of the sort.

BitwuzlaSort bitwuzla_sort_copy(BitwuzlaSort sort)

Make copy of sort.

Increments reference counter of sort.

See also

• bitwuzla_sort_release

Note

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

Parameters:

sort – The sort to copy.

Returns:

The same sort with its reference count increased by one.

void bitwuzla_sort_release(BitwuzlaSort sort)

Release copy of sort.

Decrements reference counter of `sort.

See also

• bitwuzla_sort_copy

• bitwuzla_term_manager_release

Note

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

Parameters:

sort – The sort to release.

uint64_t bitwuzla_sort_bv_get_size(BitwuzlaSort sort)

Get the size of a bit-vector sort.

Requires that given sort is a bit-vector sort.

Parameters:

sort – The sort.

Returns:

The size of the bit-vector sort.

uint64_t bitwuzla_sort_fp_get_exp_size(BitwuzlaSort sort)

Get the exponent size of a floating-point sort.

Requires that given sort is a floating-point sort.

Parameters:

sort – The sort.

Returns:

The exponent size of the floating-point sort.

uint64_t bitwuzla_sort_fp_get_sig_size(BitwuzlaSort sort)

Get the significand size of a floating-point sort.

Requires that given sort is a floating-point sort.

Parameters:

sort – The sort.

Returns:

The significand size of the floating-point sort.

BitwuzlaSort bitwuzla_sort_array_get_index(BitwuzlaSort sort)

Get the index sort of an array sort.

Requires that given sort is an array sort.

Parameters:

sort – The sort.

Returns:

The index sort of the array sort.

BitwuzlaSort bitwuzla_sort_array_get_element(BitwuzlaSort sort)

Get the element sort of an array sort.

Requires that given sort is an array sort.

Parameters:

sort – The sort.

Returns:

The element sort of the array sort.

BitwuzlaSort *bitwuzla_sort_fun_get_domain_sorts(BitwuzlaSort sort, size_t *size)

Get the domain sorts of a function sort.

The domain sorts are returned as an array of sorts of size size. Requires that given sort is a function sort.

Parameters:

• sort – The sort.

• size – The size of the returned array.

Returns:

The domain sorts of the function sort.

BitwuzlaSort bitwuzla_sort_fun_get_codomain(BitwuzlaSort sort)

Get the codomain sort of a function sort.

Requires that given sort is a function sort.

Parameters:

sort – The sort.

Returns:

The codomain sort of the function sort.

uint64_t bitwuzla_sort_fun_get_arity(BitwuzlaSort sort)

Get the arity of a function sort.

Parameters:

sort – The sort.

Returns:

The number of arguments of the function sort.

const char *bitwuzla_sort_get_uninterpreted_symbol(BitwuzlaSort sort)

Get the symbol of an uninterpreted sort.

Note

The returned char* pointer is only valid until the next bitwuzla_sort_uninterpreted_get_symbol call.

Parameters:

sort – The sort.

Returns:

The symbol; NULL if no symbol is defined.

bool bitwuzla_sort_is_array(BitwuzlaSort sort)

Determine if a sort is an array sort.

Parameters:

sort – The sort.

Returns:

True if sort is an array sort.

bool bitwuzla_sort_is_bool(BitwuzlaSort sort)

Determine if a sort is a Boolean sort.

Parameters:

sort – The sort.

Returns:

True if sort is a Boolean sort.

bool bitwuzla_sort_is_bv(BitwuzlaSort sort)

Determine if a sort is a bit-vector sort.

Parameters:

sort – The sort.

Returns:

True if sort is a bit-vector sort.

bool bitwuzla_sort_is_fp(BitwuzlaSort sort)

Determine if a sort is a floating-point sort.

Parameters:

sort – The sort.

Returns:

True if sort is a floating-point sort.

bool bitwuzla_sort_is_fun(BitwuzlaSort sort)

Determine if a sort is a function sort.

Parameters:

sort – The sort.

Returns:

True if sort is a function sort.

bool bitwuzla_sort_is_rm(BitwuzlaSort sort)

Determine if a sort is a Roundingmode sort.

Parameters:

sort – The sort.

Returns:

True if sort is a Roundingmode sort.

bool bitwuzla_sort_is_uninterpreted(BitwuzlaSort sort)

Determine if a sort is an uninterpreted sort.

Parameters:

sort – The sort.

Returns:

True if sort is a uninterpreted sort.

const char *bitwuzla_sort_to_string(BitwuzlaSort sort)

Get the SMT-LIBV v2 string representation of a sort.

Note

The returned char* pointer is only valid until the next bitwuzla_sort_to_string call.

Returns:

A string representation of the given sort.

void bitwuzla_sort_print(BitwuzlaSort sort, FILE *file)

Print sort to given file in SMT-LIB v2 format.

Parameters:

• sort – The sort.

• file – The file to print the sort to.