BitwuzlaTermManager

• typedef struct BitwuzlaTermManager

• bitwuzla_term_manager_new()

• bitwuzla_term_manager_delete()

• bitwuzla_term_manager_release()

typedef struct BitwuzlaTermManager BitwuzlaTermManager

BitwuzlaTermManager *bitwuzla_term_manager_new()

Create a new BitwuzlaTermManager instance.

The returned instance must be deleted via bitwuzla_term_manager_delete().

See also

• bitwuzla_term_manager_release

• bitwuzla_term_manager_delete

void bitwuzla_term_manager_delete(BitwuzlaTermManager *tm)

Delete a BitwuzlaTermManager instance.

The given instance must have been created via bitwuzla_term_manager_new().

See also

• bitwuzla_term_manager_new

Note

This will also invalidate all sorts and terms created by this term manager.

Parameters:

tm – The BitwuzlaTermManager instance to delete.

void bitwuzla_term_manager_release(BitwuzlaTermManager *tm)

Release all sort and term references.

This will free all memory used by sorts and terms allocated by the term manager.

See also

• bitwuzla_term_release

• bitwuzla_term_copy

• bitwuzla_sort_release

• bitwuzla_sort_copy

Note

This will invalidate all sorts and terms created by the term manager.

Parameters:

tm – The BitwuzlaTermManager instance.

Term Creation

Terms of a given BitwuzlaKind are created via bitwuzla_mk_term() (and related bitwuzla_mk_term*() functions provided for convenience). a comprehensive documentation of supported term kinds can be found here. For creating terms that represent general and special values of a given sort, Bitwuzla provides additional functions, see below.

BitwuzlaTerm bitwuzla_mk_true(BitwuzlaTermManager *tm)

Create a true value.

Parameters:

tm – The term manager instance.

Returns:

A term representing true.

BitwuzlaTerm bitwuzla_mk_false(BitwuzlaTermManager *tm)

Create a false value.

Parameters:

tm – The term manager instance.

Returns:

A term representing false.

BitwuzlaTerm bitwuzla_mk_bv_zero(BitwuzlaTermManager *tm, BitwuzlaSort sort)

Create a bit-vector value zero.

See also

• bitwuzla_mk_bv_sort

Parameters:

• tm – The term manager instance.

• sort – The sort of the value.

Returns:

A term representing the bit-vector value 0 of given sort.

BitwuzlaTerm bitwuzla_mk_bv_one(BitwuzlaTermManager *tm, BitwuzlaSort sort)

Create a bit-vector value one.

See also

• bitwuzla_mk_bv_sort

Parameters:

• tm – The term manager instance.

• sort – The sort of the value.

Returns:

A term representing the bit-vector value 1 of given sort.

BitwuzlaTerm bitwuzla_mk_bv_ones(BitwuzlaTermManager *tm, BitwuzlaSort sort)

Create a bit-vector value where all bits are set to 1.

See also

• bitwuzla_mk_bv_sort

Parameters:

• tm – The term manager instance.

• sort – The sort of the value.

Returns:

A term representing the bit-vector value of given sort where all bits are set to 1.

BitwuzlaTerm bitwuzla_mk_bv_min_signed(BitwuzlaTermManager *tm, BitwuzlaSort sort)

Create a bit-vector minimum signed value.

See also

• bitwuzla_mk_bv_sort

Parameters:

• tm – The term manager instance.

• sort – The sort of the value.

Returns:

A term representing the bit-vector value of given sort where the MSB is set to 1 and all remaining bits are set to 0.

BitwuzlaTerm bitwuzla_mk_bv_max_signed(BitwuzlaTermManager *tm, BitwuzlaSort sort)

Create a bit-vector maximum signed value.

See also

• bitwuzla_mk_bv_sort

Parameters:

• tm – The term manager instance.

• sort – The sort of the value.

Returns:

A term representing the bit-vector value of given sort where the MSB is set to 0 and all remaining bits are set to 1.

BitwuzlaTerm bitwuzla_mk_fp_pos_zero(BitwuzlaTermManager *tm, BitwuzlaSort sort)

Create a floating-point positive zero value (SMT-LIB: +zero).

See also

• bitwuzla_mk_fp_sort

Parameters:

• tm – The term manager instance.

• sort – The sort of the value.

Returns:

A term representing the floating-point positive zero value of given floating-point sort.

BitwuzlaTerm bitwuzla_mk_fp_neg_zero(BitwuzlaTermManager *tm, BitwuzlaSort sort)

Create a floating-point negative zero value (SMT-LIB: -zero).

See also

• bitwuzla_mk_fp_sort

Parameters:

• tm – The term manager instance.

• sort – The sort of the value.

Returns:

A term representing the floating-point negative zero value of given floating-point sort.

BitwuzlaTerm bitwuzla_mk_fp_pos_inf(BitwuzlaTermManager *tm, BitwuzlaSort sort)

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

See also

• bitwuzla_mk_fp_sort

Parameters:

• tm – The term manager instance.

• sort – The sort of the value.

Returns:

A term representing the floating-point positive infinity value of given floating-point sort.

BitwuzlaTerm bitwuzla_mk_fp_neg_inf(BitwuzlaTermManager *tm, BitwuzlaSort sort)

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

See also

• bitwuzla_mk_fp_sort

Parameters:

• tm – The term manager instance.

• sort – The sort of the value.

Returns:

A term representing the floating-point negative infinity value of given floating-point sort.

BitwuzlaTerm bitwuzla_mk_fp_nan(BitwuzlaTermManager *tm, BitwuzlaSort sort)

Create a floating-point NaN value.

See also

• bitwuzla_mk_fp_sort

Parameters:

• tm – The term manager instance.

• sort – The sort of the value.

Returns:

A term representing the floating-point NaN value of given floating-point sort.

BitwuzlaTerm bitwuzla_mk_bv_value(BitwuzlaTermManager *tm, BitwuzlaSort sort, const char *value, uint8_t base)

Create a bit-vector value from its string representation.

Parameter base determines the base of the string representation.

See also

• bitwuzla_mk_bv_sort

Note

Given value must fit into a bit-vector of given size (sort).

Parameters:

• tm – The term manager instance.

• sort – The sort of the value.

• value – A string representing the value.

• base – The base in which the string is given; 2 for binary, 10 for decimal, and 16 for hexadecimal.

Returns:

A term of kind BITWUZLA_KIND_VAL, representing the bit-vector value of given sort.

BitwuzlaTerm bitwuzla_mk_bv_value_uint64(BitwuzlaTermManager *tm, BitwuzlaSort sort, uint64_t value)

Create a bit-vector value from its unsigned integer representation.

See also

• bitwuzla_mk_bv_sort

Note

Given value must fit into a bit-vector of given size (sort).

Parameters:

• tm – The term manager instance.

• sort – The sort of the value.

• value – The unsigned integer representation of the bit-vector value.

Returns:

A term of kind BITWUZLA_KIND_VAL, representing the bit-vector value of given sort.

BitwuzlaTerm bitwuzla_mk_bv_value_int64(BitwuzlaTermManager *tm, BitwuzlaSort sort, int64_t value)

Create a bit-vector value from its signed integer representation.

See also

• bitwuzla_mk_bv_sort

Note

Given value must fit into a bit-vector of given size (sort).

Parameters:

• tm – The term manager instance.

• sort – The sort of the value.

• value – The unsigned integer representation of the bit-vector value.

Returns:

A term of kind BITWUZLA_KIND_VAL, representing the bit-vector value of given sort.

BitwuzlaTerm bitwuzla_mk_fp_value(BitwuzlaTermManager *tm, BitwuzlaTerm bv_sign, BitwuzlaTerm bv_exponent, BitwuzlaTerm bv_significand)

Create a floating-point value from its IEEE 754 standard representation given as three bit-vector values representing the sign bit, the exponent and the significand.

Parameters:

• tm – The term manager instance.

• bv_sign – The sign bit.

• bv_exponent – The exponent bit-vector value.

• bv_significand – The significand bit-vector value.

Returns:

A term of kind BITWUZLA_KIND_VAL, representing the floating-point value.

BitwuzlaTerm bitwuzla_mk_fp_from_real(BitwuzlaTermManager *tm, BitwuzlaSort sort, BitwuzlaTerm rm, const char *real)

Create a floating-point value from its real representation, given as a decimal string, with respect to given rounding mode.

See also

• bitwuzla_mk_fp_sort

Note

Given rounding mode may be an arbitrary, non-value rounding mode term. If it is a value, the returned term will be a floating-point value, else a non-value floating-point term.

Parameters:

• tm – The term manager instance.

• sort – The sort of the value.

• rm – The rounding mode.

• real – The decimal string representing a real value.

Returns:

A floating-point representation of the given real string. If rm is of kind BITWUZLA_KIND_VALUE the floating-point will be of kind BITWUZLA_KIND_VALUE, else it will be a non-value term.

BitwuzlaTerm bitwuzla_mk_fp_from_rational(BitwuzlaTermManager *tm, BitwuzlaSort sort, BitwuzlaTerm rm, const char *num, const char *den)

Create a floating-point value from its rational representation, given as a two decimal strings representing the numerator and denominator, with respect to given rounding mode.

See also

• bitwuzla_mk_fp_sort

Note

Given rounding mode may be an arbitrary, non-value rounding mode term. If it is a value, the returned term will be a floating-point value, else a non-value floating-point term.

Parameters:

• tm – The term manager instance.

• sort – The sort of the value.

• rm – The rounding mode.

• num – The decimal string representing the numerator.

• den – The decimal string representing the denominator.

Returns:

A floating-point representation of the given rational string. If rm is of kind BITWUZLA_KIND_VALUE the floating-point will be of kind BITWUZLA_KIND_VALUE, else it will be a non-value term.

BitwuzlaTerm bitwuzla_mk_rm_value(BitwuzlaTermManager *tm, BitwuzlaRoundingMode rm)

Create a rounding mode value.

See also

• BitwuzlaRoundingMode

Parameters:

• rm – The rounding mode value.

• tm – The term manager instance.

Returns:

A term of kind BITWUZLA_KIND_VAL, representing the rounding mode value.

BitwuzlaTerm bitwuzla_mk_term1(BitwuzlaTermManager *tm, BitwuzlaKind kind, BitwuzlaTerm arg)

Create a term of given kind with one argument term.

See also

• BitwuzlaKind

Parameters:

• tm – The term manager instance.

• kind – The operator kind.

• arg – The argument to the operator.

Returns:

A term representing an operation of given kind.

BitwuzlaTerm bitwuzla_mk_term2(BitwuzlaTermManager *tm, BitwuzlaKind kind, BitwuzlaTerm arg0, BitwuzlaTerm arg1)

Create a term of given kind with two argument terms.

See also

• BitwuzlaKind

Parameters:

• tm – The term manager instance.

• kind – The operator kind.

• arg0 – The first argument to the operator.

• arg1 – The second argument to the operator.

Returns:

A term representing an operation of given kind.

BitwuzlaTerm bitwuzla_mk_term3(BitwuzlaTermManager *tm, BitwuzlaKind kind, BitwuzlaTerm arg0, BitwuzlaTerm arg1, BitwuzlaTerm arg2)

Create a term of given kind with three argument terms.

See also

• BitwuzlaKind

Parameters:

• tm – The term manager instance.

• kind – The operator kind.

• arg0 – The first argument to the operator.

• arg1 – The second argument to the operator.

• arg2 – The third argument to the operator.

Returns:

A term representing an operation of given kind.

BitwuzlaTerm bitwuzla_mk_term(BitwuzlaTermManager *tm, BitwuzlaKind kind, uint32_t argc, BitwuzlaTerm args[])

Create a term of given kind with the given argument terms.

See also

• BitwuzlaKind

Parameters:

• tm – The term manager instance.

• kind – The operator kind.

• argc – The number of argument terms.

• args – The argument terms.

Returns:

A term representing an operation of given kind.

BitwuzlaTerm bitwuzla_mk_term1_indexed1(BitwuzlaTermManager *tm, BitwuzlaKind kind, BitwuzlaTerm arg, uint64_t idx)

Create an indexed term of given kind with one argument term and one index.

See also

• BitwuzlaKind

Parameters:

• tm – The term manager instance.

• kind – The operator kind.

• arg – The argument term.

• idx – The index.

Returns:

A term representing an indexed operation of given kind.

BitwuzlaTerm bitwuzla_mk_term1_indexed2(BitwuzlaTermManager *tm, BitwuzlaKind kind, BitwuzlaTerm arg, uint64_t idx0, uint64_t idx1)

Create an indexed term of given kind with one argument term and two indices.

See also

• BitwuzlaKind

Parameters:

• tm – The term manager instance.

• kind – The operator kind.

• arg – The argument term.

• idx0 – The first index.

• idx1 – The second index.

Returns:

A term representing an indexed operation of given kind.

BitwuzlaTerm bitwuzla_mk_term2_indexed1(BitwuzlaTermManager *tm, BitwuzlaKind kind, BitwuzlaTerm arg0, BitwuzlaTerm arg1, uint64_t idx)

Create an indexed term of given kind with two argument terms and one index.

See also

• BitwuzlaKind

Parameters:

• tm – The term manager instance.

• kind – The operator kind.

• arg0 – The first argument term.

• arg1 – The second argument term.

• idx – The index.

Returns:

A term representing an indexed operation of given kind.

BitwuzlaTerm bitwuzla_mk_term2_indexed2(BitwuzlaTermManager *tm, BitwuzlaKind kind, BitwuzlaTerm arg0, BitwuzlaTerm arg1, uint64_t idx0, uint64_t idx1)

Create an indexed term of given kind with two argument terms and two indices.

See also

• BitwuzlaKind

Parameters:

• tm – The term manager instance.

• kind – The operator kind.

• arg0 – The first argument term.

• arg1 – The second argument term.

• idx0 – The first index.

• idx1 – The second index.

Returns:

A term representing an indexed operation of given kind.

BitwuzlaTerm bitwuzla_mk_term_indexed(BitwuzlaTermManager *tm, BitwuzlaKind kind, uint32_t argc, BitwuzlaTerm args[], uint32_t idxc, const uint64_t idxs[])

Create an indexed term of given kind with the given argument terms and indices.

See also

• BitwuzlaKind

Parameters:

• tm – The term manager instance.

• kind – The operator kind.

• argc – The number of argument terms.

• args – The argument terms.

• idxc – The number of indices.

• idxs – The indices.

Returns:

A term representing an indexed operation of given kind.

BitwuzlaTerm bitwuzla_mk_const(BitwuzlaTermManager *tm, BitwuzlaSort sort, const char *symbol)

Create a (first-order) constant of given sort with given symbol.

See also

• bitwuzla_mk_array_sort

• bitwuzla_mk_bool_sort

• bitwuzla_mk_bv_sort

• bitwuzla_mk_fp_sort

• bitwuzla_mk_fun_sort

• bitwuzla_mk_rm_sort

Parameters:

• tm – The term manager instance.

• sort – The sort of the constant.

• symbol – The symbol of the constant.

Returns:

A term of kind BITWUZLA_KIND_CONST, representing the constant.

BitwuzlaTerm bitwuzla_mk_const_array(BitwuzlaTermManager *tm, BitwuzlaSort sort, BitwuzlaTerm value)

Create a one-dimensional constant array of given sort, initialized with given value.

See also

• bitwuzla_mk_array_sort

Parameters:

• tm – The term manager instance.

• sort – The sort of the array.

• value – The term to initialize the elements of the array with.

Returns:

A term of kind BITWUZLA_KIND_CONST_ARRAY, representing a constant array of given sort.

BitwuzlaTerm bitwuzla_mk_var(BitwuzlaTermManager *tm, BitwuzlaSort sort, const char *symbol)

Create a variable of given sort with given symbol.

See also

• bitwuzla_mk_bool_sort

• bitwuzla_mk_bv_sort

• bitwuzla_mk_fp_sort

• bitwuzla_mk_fun_sort

• bitwuzla_mk_rm_sort

Note

This creates a variable to be bound by quantifiers or lambdas.

Parameters:

• tm – The term manager instance.

• sort – The sort of the variable.

• symbol – The symbol of the variable.

Returns:

A term of kind BITWUZLA_KIND_VAR, representing the variable.

Term Substitution

BitwuzlaTerm bitwuzla_substitute_term(BitwuzlaTerm term, size_t map_size, BitwuzlaTerm map_keys[], BitwuzlaTerm map_values[])

Substitute a set of keys with their corresponding values in the given term.

Parameters:

• term – The term in which the keys are to be substituted.

• map_size – The size of the substitution map.

• map_keys – The keys.

• map_values – The mapped values.

Returns:

The resulting term from this substitution.

void bitwuzla_substitute_terms(size_t terms_size, BitwuzlaTerm terms[], size_t map_size, BitwuzlaTerm map_keys[], BitwuzlaTerm map_values[])

Substitute a set of keys with their corresponding values in the set of given terms.

The terms in terms are replaced with the terms resulting from these substitutions.

Parameters:

• terms_size – The size of the set of terms.

• terms – The terms in which the keys are to be substituted.

• map_size – The size of the substitution map.

• map_keys – The keys.

• map_values – The mapped values.

Sort Creation

Bitwuzla supports creating 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.

BitwuzlaSort bitwuzla_mk_array_sort(BitwuzlaTermManager *tm, BitwuzlaSort index, BitwuzlaSort element)

Create an array sort.

See also

• bitwuzla_sort_is_array

• bitwuzla_sort_array_get_index

• bitwuzla_sort_array_get_element

• bitwuzla_term_is_array

• bitwuzla_term_array_get_index_sort

• bitwuzla_term_array_get_element_sort

Parameters:

• tm – The term manager instance.

• index – The index sort of the array sort.

• element – The element sort of the array sort.

Returns:

An array sort which maps sort index to sort element.

BitwuzlaSort bitwuzla_mk_bool_sort(BitwuzlaTermManager *tm)

Create a Boolean sort.

Parameters:

tm – The term manager instance.

Returns:

A Boolean sort.

BitwuzlaSort bitwuzla_mk_bv_sort(BitwuzlaTermManager *tm, uint64_t size)

Create a bit-vector sort of given size.

See also

• bitwuzla_sort_is_bv

• bitwuzla_sort_bv_get_size

• bitwuzla_term_is_bv

• bitwuzla_term_bv_get_size

Parameters:

• tm – The term manager instance.

• size – The size of the bit-vector sort.

Returns:

A bit-vector sort of given size.

BitwuzlaSort bitwuzla_mk_fp_sort(BitwuzlaTermManager *tm, uint64_t exp_size, uint64_t sig_size)

Create a floating-point sort of given exponent and significand size.

See also

• bitwuzla_sort_is_fp

• bitwuzla_sort_fp_get_exp_size

• bitwuzla_sort_fp_get_sig_size

• bitwuzla_term_is_fp

• bitwuzla_term_fp_get_exp_size

• bitwuzla_term_fp_get_sig_size

Parameters:

• tm – The term manager instance.

• exp_size – The size of the exponent.

• sig_size – The size of the significand (including sign bit).

Returns:

A floating-point sort of given format.

BitwuzlaSort bitwuzla_mk_fun_sort(BitwuzlaTermManager *tm, uint64_t arity, BitwuzlaSort domain[], BitwuzlaSort codomain)

Create a function sort.

See also

• bitwuzla_sort_is_fun

• bitwuzla_sort_fun_get_arity

• bitwuzla_sort_fun_get_domain_sorts

• bitwuzla_sort_fun_get_codomain

• bitwuzla_term_is_fun

• bitwuzla_term_fun_get_arity

• bitwuzla_term_fun_get_domain_sorts

• bitwuzla_term_fun_get_codomain_sort

Parameters:

• tm – The term manager instance.

• arity – The number of arguments to the function.

• domain – The domain sorts (the sorts of the arguments). The number of sorts in this vector must match arity.

• codomain – The codomain sort (the sort of the return value).

Returns:

A function sort of given domain and codomain sorts.

BitwuzlaSort bitwuzla_mk_rm_sort(BitwuzlaTermManager *tm)

Create a Roundingmode sort.

See also

• bitwuzla_sort_is_rm

• bitwuzla_term_is_rm

Parameters:

tm – The term manager instance.

Returns:

A Roundingmode sort.

BitwuzlaSort bitwuzla_mk_uninterpreted_sort(BitwuzlaTermManager *tm, const char *symbol)

Create an uninterpreted sort.

See also

• bitwuzla_sort_is_uninterpreted

• bitwuzla_term_is_uninterpreted

Parameters:

• tm – The term manager instance.

• symbol – The symbol of the sort. May be NULL.

Returns:

A uninterpreted sort.