BitwuzlaTerm

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.

• typedef struct BitwuzlaTerm

• bitwuzla_term_hash()

• bitwuzla_term_copy()

• bitwuzla_term_release()

• bitwuzla_term_get_kind()

• bitwuzla_term_get_children()

• bitwuzla_term_get_indices()

• bitwuzla_term_is_indexed()

• bitwuzla_term_get_sort()

• bitwuzla_term_array_get_index_sort()

• bitwuzla_term_array_get_element_sort()

• bitwuzla_term_fun_get_domain_sorts()

• bitwuzla_term_fun_get_codomain_sort()

• bitwuzla_term_bv_get_size()

• bitwuzla_term_fp_get_exp_size()

• bitwuzla_term_fp_get_sig_size()

• bitwuzla_term_fun_get_arity()

• bitwuzla_term_get_symbol()

• bitwuzla_term_is_array()

• bitwuzla_term_is_const()

• bitwuzla_term_is_fun()

• bitwuzla_term_is_var()

• bitwuzla_term_is_value()

• bitwuzla_term_is_bv_value()

• bitwuzla_term_is_fp_value()

• bitwuzla_term_is_rm_value()

• bitwuzla_term_is_bool()

• bitwuzla_term_is_bv()

• bitwuzla_term_is_fp()

• bitwuzla_term_is_rm()

• bitwuzla_term_is_uninterpreted()

• bitwuzla_term_is_bv_value_zero()

• bitwuzla_term_is_bv_value_one()

• bitwuzla_term_is_bv_value_ones()

• bitwuzla_term_is_bv_value_min_signed()

• bitwuzla_term_is_bv_value_max_signed()

• bitwuzla_term_is_fp_value_pos_zero()

• bitwuzla_term_is_fp_value_neg_zero()

• bitwuzla_term_is_fp_value_pos_inf()

• bitwuzla_term_is_fp_value_neg_inf()

• bitwuzla_term_is_fp_value_nan()

• bitwuzla_term_is_rm_value_rna()

• bitwuzla_term_is_rm_value_rne()

• bitwuzla_term_is_rm_value_rtn()

• bitwuzla_term_is_rm_value_rtp()

• bitwuzla_term_is_rm_value_rtz()

• bitwuzla_term_value_get_bool()

• bitwuzla_term_value_get_str()

• bitwuzla_term_value_get_fp_ieee()

• bitwuzla_term_value_get_rm()

• bitwuzla_term_to_string()

• bitwuzla_term_print()

typedef struct bitwuzla_term_t *BitwuzlaTerm

A Bitwuzla term.

size_t bitwuzla_term_hash(BitwuzlaTerm term)

Compute the hash value for a term.

Parameters:

term – The term.

Returns:

The hash value of the term.

BitwuzlaTerm bitwuzla_term_copy(BitwuzlaTerm term)

Make copy of term.

Increase reference counter of term.

See also

• bitwuzla_term_release

Note

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

Parameters:

term – The term to copy.

Returns:

The same term with its reference count increased by one.

void bitwuzla_term_release(BitwuzlaTerm term)

Release copy of term.

Decrements reference counter of term.

See also

• bitwuzla_term_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 BitwuzlaTerm returns a copy that is owned by the callee of the function and thus, can be released.

Parameters:

term – The term to release.

BitwuzlaKind bitwuzla_term_get_kind(BitwuzlaTerm term)

Get the kind of a term.

See also

BitwuzlaKind

Parameters:

term – The term.

Returns:

The kind of the given term.

BitwuzlaTerm *bitwuzla_term_get_children(BitwuzlaTerm term, size_t *size)

Get the child terms of a term.

Returns NULL if given term does not have children.

Parameters:

• term – The term.

• size – Output parameter, stores the number of children of term.

Returns:

The children of term as an array of terms.

uint64_t *bitwuzla_term_get_indices(BitwuzlaTerm term, size_t *size)

Get the indices of an indexed term.

Requires that given term is an indexed term.

Parameters:

• term – The term.

• size – Output parameter, stores the number of indices of term.

Returns:

The indices of term as an array of indices.

bool bitwuzla_term_is_indexed(BitwuzlaTerm term)

Determine if a term is an indexed term.

Parameters:

term – The term.

Returns:

True if term is an indexed term.

BitwuzlaSort bitwuzla_term_get_sort(BitwuzlaTerm term)

Get the sort of a term.

Parameters:

term – The term.

Returns:

The sort of the term.

BitwuzlaSort bitwuzla_term_array_get_index_sort(BitwuzlaTerm term)

Get the index sort of an array term.

Requires that given term is an array or an array store term.

Parameters:

term – The term.

Returns:

The index sort of the array term.

BitwuzlaSort bitwuzla_term_array_get_element_sort(BitwuzlaTerm term)

Get the element sort of an array term.

Requires that given term is an array or an array store term.

Parameters:

term – The term.

Returns:

The element sort of the array term.

BitwuzlaSort *bitwuzla_term_fun_get_domain_sorts(BitwuzlaTerm term, size_t *size)

Get the domain sorts of a function term.

The domain sorts are returned as an array of sorts of size `size. Requires that given term is an uninterpreted function, a lambda term, an array store term, or an ite term over function terms.

Parameters:

• term – The term.

• size – The size of the returned array. Optional, NULL is allowed.

Returns:

The domain sorts of the function term.

BitwuzlaSort bitwuzla_term_fun_get_codomain_sort(BitwuzlaTerm term)

Get the codomain sort of a function term.

Requires that given term is an uninterpreted function, a lambda term, an array store term, or an ite term over function terms.

Parameters:

term – The term.

Returns:

The codomain sort of the function term.

uint64_t bitwuzla_term_bv_get_size(BitwuzlaTerm term)

Get the bit-width of a bit-vector term.

Requires that given term is a bit-vector term.

Parameters:

term – The term.

Returns:

The bit-width of the bit-vector term.

uint64_t bitwuzla_term_fp_get_exp_size(BitwuzlaTerm term)

Get the bit-width of the exponent of a floating-point term.

Requires that given term is a floating-point term.

Parameters:

term – The term.

Returns:

The bit-width of the exponent of the floating-point term.

uint64_t bitwuzla_term_fp_get_sig_size(BitwuzlaTerm term)

Get the bit-width of the significand of a floating-point term.

Requires that given term is a floating-point term.

Parameters:

term – The term.

Returns:

The bit-width of the significand of the floating-point term.

uint64_t bitwuzla_term_fun_get_arity(BitwuzlaTerm term)

Get the arity of a function term.

Requires that given term is a function term.

Parameters:

term – The term.

Returns:

The arity of the function term.

const char *bitwuzla_term_get_symbol(BitwuzlaTerm term)

Get the symbol of a term.

Parameters:

term – The term.

Returns:

The symbol of term. NULL if no symbol is defined.

bool bitwuzla_term_is_equal_sort(BitwuzlaTerm term0, BitwuzlaTerm term1)

Determine if the sorts of two terms are equal.

Parameters:

• term0 – The first term.

• term1 – The second term.

Returns:

True if the sorts of term0 and term1 are equal.

bool bitwuzla_term_is_array(BitwuzlaTerm term)

Determine if a term is an array term.

Parameters:

term – The term.

Returns:

True if term is an array term.

bool bitwuzla_term_is_const(BitwuzlaTerm term)

Determine if a term is a constant.

Parameters:

term – The term.

Returns:

True if term is a constant.

bool bitwuzla_term_is_fun(BitwuzlaTerm term)

Determine if a term is a function.

Parameters:

term – The term.

Returns:

True if term is a function.

bool bitwuzla_term_is_var(BitwuzlaTerm term)

Determine if a term is a variable.

Parameters:

term – The term.

Returns:

True if term is a variable.

bool bitwuzla_term_is_value(BitwuzlaTerm term)

Determine if a term is a value.

Parameters:

term – The term.

Returns:

True if term is a value.

bool bitwuzla_term_is_bv_value(BitwuzlaTerm term)

Determine if a term is a bit-vector value.

Parameters:

term – The term.

Returns:

True if term is a bit-vector value.

bool bitwuzla_term_is_fp_value(BitwuzlaTerm term)

Determine if a term is a floating-point value.

Parameters:

term – The term.

Returns:

True if term is a floating-point value.

bool bitwuzla_term_is_rm_value(BitwuzlaTerm term)

Determine if a term is a rounding mode value.

Parameters:

term – The term.

Returns:

True if term is a rounding mode value.

bool bitwuzla_term_is_bool(BitwuzlaTerm term)

Determine if a term is a Boolean term.

Parameters:

term – The term.

Returns:

True if term is a Boolean term.

bool bitwuzla_term_is_bv(BitwuzlaTerm term)

Determine if a term is a bit-vector term.

Parameters:

term – The term.

Returns:

True if term is a bit-vector term.

bool bitwuzla_term_is_fp(BitwuzlaTerm term)

Determine if a term is a floating-point term.

Parameters:

term – The term.

Returns:

True if term is a floating-point term.

bool bitwuzla_term_is_rm(BitwuzlaTerm term)

Determine if a term is a rounding mode term.

Parameters:

term – The term.

Returns:

True if term is a rounding mode term.

bool bitwuzla_term_is_uninterpreted(BitwuzlaTerm term)

Determine if a term is a term of uninterpreted sort.

Parameters:

term – The term.

Returns:

True if term is a term of uninterpreted sort.

bool bitwuzla_term_is_true(BitwuzlaTerm term)

Determine if a term is Boolean value true.

Parameters:

term – The term.

Returns:

True if term is a Boolean value true.

bool bitwuzla_term_is_false(BitwuzlaTerm term)

Determine if a term is Boolean value false.

Parameters:

term – The term.

Returns:

false if term is a Boolean value false.

bool bitwuzla_term_is_bv_value_zero(BitwuzlaTerm term)

Determine if a term is a bit-vector value representing zero.

Parameters:

term – The term.

Returns:

True if term is a bit-vector zero value.

bool bitwuzla_term_is_bv_value_one(BitwuzlaTerm term)

Determine if a term is a bit-vector value representing one.

Parameters:

term – The term.

Returns:

True if term is a bit-vector one value.

bool bitwuzla_term_is_bv_value_ones(BitwuzlaTerm term)

Determine if a term is a bit-vector value with all bits set to one.

Parameters:

term – The term.

Returns:

True if term is a bit-vector value with all bits set to one.

bool bitwuzla_term_is_bv_value_min_signed(BitwuzlaTerm term)

Determine if a term is a bit-vector minimum signed value.

Parameters:

term – The term.

Returns:

True if term is a bit-vector value with the most significant bit set to 1 and all other bits set to 0.

bool bitwuzla_term_is_bv_value_max_signed(BitwuzlaTerm term)

Determine if a term is a bit-vector maximum signed value.

Parameters:

term – The term.

Returns:

True if term is a bit-vector value with the most significant bit set to 0 and all other bits set to 1.

bool bitwuzla_term_is_fp_value_pos_zero(BitwuzlaTerm term)

Determine if a term is a floating-point positive zero (+zero) value.

Parameters:

term – The term.

Returns:

True if term is a floating-point +zero value.

bool bitwuzla_term_is_fp_value_neg_zero(BitwuzlaTerm term)

Determine if a term is a floating-point value negative zero (-zero).

Parameters:

term – The term.

Returns:

True if term is a floating-point value negative zero.

bool bitwuzla_term_is_fp_value_pos_inf(BitwuzlaTerm term)

Determine if a term is a floating-point positive infinity (+oo) value.

Parameters:

term – The term.

Returns:

True if term is a floating-point +oo value.

bool bitwuzla_term_is_fp_value_neg_inf(BitwuzlaTerm term)

Determine if a term is a floating-point negative infinity (-oo) value.

Parameters:

term – The term.

Returns:

True if term is a floating-point -oo value.

bool bitwuzla_term_is_fp_value_nan(BitwuzlaTerm term)

Determine if a term is a floating-point NaN value.

Parameters:

term – The term.

Returns:

True if term is a floating-point NaN value.

bool bitwuzla_term_is_rm_value_rna(BitwuzlaTerm term)

Determine if a term is a rounding mode RNA value.

Parameters:

term – The term.

Returns:

True if term is a roundindg mode RNA value.

bool bitwuzla_term_is_rm_value_rne(BitwuzlaTerm term)

Determine if a term is a rounding mode RNE value.

Parameters:

term – The term.

Returns:

True if term is a rounding mode RNE value.

bool bitwuzla_term_is_rm_value_rtn(BitwuzlaTerm term)

Determine if a term is a rounding mode RTN value.

Parameters:

term – The term.

Returns:

True if term is a rounding mode RTN value.

bool bitwuzla_term_is_rm_value_rtp(BitwuzlaTerm term)

Determine if a term is a rounding mode RTP value.

Parameters:

term – The term.

Returns:

True if term is a rounding mode RTP value.

bool bitwuzla_term_is_rm_value_rtz(BitwuzlaTerm term)

Determine if a term is a rounding mode RTZ value.

Parameters:

term – The term.

Returns:

True if term is a rounding mode RTZ value.

bool bitwuzla_term_value_get_bool(BitwuzlaTerm term)

Get Boolean representation of given Boolean value term.

Parameters:

term – The Boolean value term.

Returns:

Boolean representation of value term.

const char *bitwuzla_term_value_get_str(BitwuzlaTerm term)

Get string representation of Boolean, bit-vector, floating-point, or rounding mode value term.

This returns the raw value string (as opposed to bitwuzla_term_to_string(), which returns the SMT-LIB v2 representation of a term). For example, this function returns “010” for a bit-vector value 2 of size 3, while bitwuzla_term_to_string() returns “#b010”.

Note

This uses default binary format for bit-vector value strings.

Note

Return value is valid until next bitwuzla_term_value_get_str call.

Parameters:

term – The value term.

Returns:

The string representation of the value term.

const char *bitwuzla_term_value_get_str_fmt(BitwuzlaTerm term, uint8_t base)

Get string representation of Boolean, bit-vector, floating-point, or rounding mode value term. String representations of bit-vector values are printed in the given base.

This returns the raw value string (as opposed to bitwuzla_term_to_string(), which returns the SMT-LIB v2 representation of a term). For example, this function returns “010” for a bit-vector value 2 of size 3, while bitwuzla_term_to_string() returns “#b010”.

Note

The returned string for floating-point values is always the binary IEEE-754 representation of the value (parameter base is ignored). Parameter base always configures the numeric base for bit-vector values, and for floating-point values in case of the tuple of strings instantiation. It is always ignored for Boolean and RoundingMode values.

Note

Return value is valid until next bitwuzla_term_value_get_str_fmt call.

Parameters:

• term – The value term.

• base – The base of the string representation of bit-vector values; 2 for binary, 10 for decimal, and 16 for hexadecimal. Always ignored for Boolean and RoundingMode values.

Returns:

String representation of the value term.

void bitwuzla_term_value_get_fp_ieee(BitwuzlaTerm term, const char **sign, const char **exponent, const char **significand, uint8_t base)

Get (the raw) string representation of a given floating-point value term in IEEE 754 standard representation.

Note

Return values sign, exponent and significand are valid until next bitwuzla_term_value_get_fp_ieee call.

Parameters:

• term – The floating-point value term.

• sign – Output parameter. String representation of the sign bit.

• exponent – Output parameter. String representation of the exponent bit-vector value.

• significand – Output parameter. String representation of the significand bit-vector value.

• base – The base in which the component bit-vector strings are given; 2 for binary, 10 for decimal, and 16 for hexadecimal.

BitwuzlaRoundingMode bitwuzla_term_value_get_rm(BitwuzlaTerm term)

Get representation of given rounding mode value term.

Parameters:

term – The rounding mode value term.

Returns:

The BitwuzlaRoundingMode representation of the given rounding mode value.

const char *bitwuzla_term_to_string(BitwuzlaTerm term)

Get the SMT-LIB v2 string representation of a term.

Note

This uses default binary format for bit-vector value strings.

Note

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

Returns:

A string representation of the given term.

const char *bitwuzla_term_to_string_fmt(BitwuzlaTerm term, uint8_t base)

Get the SMT-LIB v2 string representation of a term. String representations of bit-vector values are printed in the given base.

Note

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

Parameters:

• term – The term.

• base – The base of the string representation of bit-vector values; 2 for binary, 10 for decimal, and 16 for hexadecimal. Always ignored for Boolean and RoundingMode values.

Returns:

A string representation of the given term.

void bitwuzla_term_print(BitwuzlaTerm term, FILE *file)

Print term in SMT-LIB v2 format.

Note

This uses default binary format for bit-vector value strings.

Parameters:

• term – The term.

• file – The file to print the term to.

void bitwuzla_term_print_fmt(BitwuzlaTerm term, FILE *file, uint8_t base)

Print term in SMT-LIB v2 format.

Note

Floating-point values are printed in terms of operator fp. Their component bit-vector values can only be printed in binary or decimal format. If base 16 is configured, the format for floating-point component bit-vector values defaults to binary format.

Parameters:

• term – The term.

• file – The file to print the term to.

• base – The base of the string representation of bit-vector values; 2 for binary, 10 for decimal, and 16 for hexadecimal.