BitwuzlaTermManager

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

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

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

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.

Note

Terms are tied to a specific BitwuzlaTermManager instance and can be shared across Bitwuzla instances that have the same term manager.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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.

Note

Sorts are tied to a specific BitwuzlaTermManager instance and can be shared across Bitwuzla instances that have the same term manager.

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

Create an array sort.

See also

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

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

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

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

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

Parameters:

  • tm – The term manager instance.

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

Returns:

A uninterpreted sort.