Term

Terms of a given bitwuzla::Kind are created via bitwuzla::mk_term(). 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.

• class bitwuzla::Term

• struct std::hash<bitwuzla::Term>

• bool bitwuzla::operator==(const Term& a, const Term& b)

• bool bitwuzla::operator!=(const Term& a, const Term& b)

• std::ostream& bitwuzla::operator<<(std::ostream& out, const Term& term)

namespace bitwuzla {

class Term

Public Functions

Term()

Default constructor, creates null term.

~Term()

Destructor.

bool is_null() const

Determine if this term is a null term.

Returns:

True if this term is a null term.

uint64_t id() const

Get the id of this term.

Returns:

The term id.

Kind kind() const

Get the kind of this term.

Returns:

The kind.

Sort sort() const

Get the sort of this term.

Returns:

The sort of the term.

size_t num_children() const

Get the number of child terms of this term.

Returns:

The number of children of this term.

std::vector<Term> children() const

Get the child terms of this term.

Returns:

The children of this term as a vector of terms.

Term operator[](size_t index) const

Get child at position index.

Note

Only valid to call if num_children() > 0.

Parameters:

index – The position of the child.

Returns:

The child node at position index.

size_t num_indices() const

Get the number of indices of this term.

Returns:

The number of indices of this term.

std::vector<uint64_t> indices() const

Get the indices of an indexed term.

Requires that given term is an indexed term.

Returns:

The indices of this term as a vector of indices.

std::optional<std::reference_wrapper<const std::string>> symbol() const

Get the symbol of this term.

Returns:

The symbol of this term.

bool is_const() const

Determine if this term is a constant.

Returns:

True if this term is a constant.

bool is_variable() const

Determine if this term is a variable.

Returns:

True if this term is a variable.

bool is_value() const

Determine if this term is a value.

Returns:

True if this term is a value.

bool is_true() const

Determine if this term is Boolean value true.

Returns:

True if this term is Boolean value true.

bool is_false() const

Determine if this term is Boolean value false.

Returns:

True if this term is Boolean value false.

bool is_bv_value_zero() const

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

Returns:

True if this term is a bit-vector zero value.

bool is_bv_value_one() const

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

Returns:

True if this term is a bit-vector one value.

bool is_bv_value_ones() const

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

Returns:

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

bool is_bv_value_min_signed() const

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

Returns:

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

bool is_bv_value_max_signed() const

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

Returns:

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

bool is_fp_value_pos_zero() const

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

Returns:

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

bool is_fp_value_neg_zero() const

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

Returns:

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

bool is_fp_value_pos_inf() const

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

Returns:

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

bool is_fp_value_neg_inf() const

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

Returns:

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

bool is_fp_value_nan() const

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

Returns:

True if this term is a floating-point NaN value.

bool is_rm_value_rna() const

Determine if this term is a rounding mode RNA value.

Returns:

True if this term is a roundindg mode RNA value.

bool is_rm_value_rne() const

Determine if this term is a rounding mode RNE value.

Returns:

True if this term is a rounding mode RNE value.

bool is_rm_value_rtn() const

Determine if this term is a rounding mode RTN value.

Returns:

True if this term is a rounding mode RTN value.

bool is_rm_value_rtp() const

Determine if this term is a rounding mode RTP value.

Returns:

True if this term is a rounding mode RTP value.

bool is_rm_value_rtz() const

Determine if this term is a rounding mode RTZ value.

Returns:

True if this term is a rounding mode RTZ value.

std::string str(uint8_t base = 2) const

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

Note

Floating-point values are represented 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:

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

Returns:

A string representation of this term.

template<class T>
T value(uint8_t base = 2) const

Get value from value term.

This function is instantiated for types

• bool for Boolean values

• RoundingMode for rounding mode values

• std::string for any value (Boolean, RoundingMode, bit-vector and floating-point)

• std::tuple<std::string, std::string, std::string> for floating-point values

In case of string representations of values (the std::string and std::tuple<std::string, std::string, std::string> instantions of this function), this returns the raw value string (as opposed to str(), 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 str() returns “#b010”.

Note

For the general std::string instantiation case, 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.

Template Parameters:

T – The type of the value representation. bool for Boolean values; RoundingMode for rounding mode values; std::tuple<std::string, std::string, std::string> for floating-point values (IEEE-754 representation as strings for sign bit, exponent and significand); and, generally, std::string for any value type.

Parameters:

base – The numeric base for bit-vector values; 2 for binary, 10 for decimal, and 16 for hexadecimal. Always ignored for Boolean and RoundingMode values.

bool bitwuzla::operator==(const Term &a, const Term &b)

Syntactical equality operator.

Parameters:

• a – The first term.

• b – The second term.

Returns:

True if the given terms are equal.

bool bitwuzla::operator!=(const Term &a, const Term &b)

Syntactical disequality operator.

Parameters:

• a – The first term.

• b – The second term.

Returns:

True if the given terms are disequal.

std::ostream &bitwuzla::operator<<(std::ostream &out, const Term &term)

Print term to output stream.

Parameters:

• out – The output stream.

• term – The term.

Returns:

The output stream.

}

namespace std {

template<>
struct hash<bitwuzla::Term>

Public Functions

size_t operator()(const bitwuzla::Term &term) const

Hash function for Term.

Parameters:

term – The term.

Returns:

The hash value of the term.

}