TermManager

Terms of a given bitwuzla::Kind are created via TermManager::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, the term manager provides additional functions, see below.

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

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

namespace bitwuzla {

class TermManager

Public Functions

TermManager(const TermManager &tm) = delete

Disallow copy construction.

TermManager &operator=(const TermManager &tm) = delete

Disallow copy assignment.

Term mk_true()

Create a true value.

Returns:

A term representing true.

Term mk_false()

Create a false value.

Returns:

A term representing false.

Term mk_bv_zero(const Sort &sort)

Create a bit-vector value zero.

See also

  • TermManager::mk_bv_sort()

Parameters:

sort – The sort of the value.

Returns:

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

Term mk_bv_one(const Sort &sort)

Create a bit-vector value one.

See also

  • TermManager::mk_bv_sort()

Parameters:

sort – The sort of the value.

Returns:

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

Term mk_bv_ones(const Sort &sort)

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

See also

  • TermManager::mk_bv_sort()

Parameters:

sort – The sort of the value.

Returns:

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

Term mk_bv_min_signed(const Sort &sort)

Create a bit-vector minimum signed value.

See also

  • TermManager::mk_bv_sort()

Parameters:

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.

Term mk_bv_max_signed(const Sort &sort)

Create a bit-vector maximum signed value.

See also

  • TermManager::mk_bv_sort()

Parameters:

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.

Term mk_bv_value(const Sort &sort, const std::string &value, uint8_t base = 2)

Create a bit-vector value from its string representation.

Parameter base determines the base of the string representation.

See also

  • TermManager::mk_bv_sort()

Note

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

Parameters:

  • 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 Kind::VALUE, representing the bit-vector value of given sort.

Term mk_bv_value_uint64(const Sort &sort, uint64_t value)

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

See also

  • TermManager::mk_bv_sort()

Note

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

Parameters:

  • sort – The sort of the value.

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

Returns:

A term of kind Kind::VALUE, representing the bit-vector value of given sort.

Term mk_bv_value_int64(const Sort &sort, int64_t value)

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

See also

  • TermManager::mk_bv_sort()

Note

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

Parameters:

  • sort – The sort of the value.

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

Returns:

A term of kind Kind::VALUE, representing the bit-vector value of given sort.

Term mk_fp_pos_zero(const Sort &sort)

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

See also

  • TermManager::mk_fp_sort()

Parameters:

sort – The sort of the value.

Returns:

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

Term mk_fp_neg_zero(const Sort &sort)

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

See also

  • TermManager::mk_fp_sort()

Parameters:

sort – The sort of the value.

Returns:

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

Term mk_fp_pos_inf(const Sort &sort)

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

See also

  • TermManager::mk_fp_sort()

Parameters:

sort – The sort of the value.

Returns:

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

Term mk_fp_neg_inf(const Sort &sort)

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

See also

  • TermManager::mk_fp_sort()

Parameters:

sort – The sort of the value.

Returns:

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

Term mk_fp_nan(const Sort &sort)

Create a floating-point NaN value.

See also

  • TermManager::mk_fp_sort()

Parameters:

sort – The sort of the value.

Returns:

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

Term mk_fp_value(const Term &bv_sign, const Term &bv_exponent, const Term &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:

  • bv_sign – The sign bit.

  • bv_exponent – The exponent bit-vector value.

  • bv_significand – The significand bit-vector value.

Returns:

A term of kind Kind::VALUE, representing the floating-point value.

Term mk_fp_value(const Sort &sort, const Term &rm, const std::string &real)

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

See also

  • TermManager::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:

  • 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 Kind::VALUE the floating-point will be of kind Kind::VALUE, else it will be a non-value term.

Term mk_fp_value(const Sort &sort, const Term &rm, const std::string &num, const std::string &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

  • TermManager::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:

  • 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 Kind::VALUE the floating-point will be of kind Kind::VALUE, else it will be a non-value term.

Term mk_const_array(const Sort &sort, const Term &term)

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

See also

  • TermManager::mk_array_sort()

Parameters:

  • sort – The sort of the array.

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

Returns:

A term of kind Kind::CONST_ARRAY, representing a constant array of given sort.

Term mk_rm_value(RoundingMode rm)

Create a rounding mode value.

See also

Parameters:

rm – The rounding mode value.

Returns:

A term of kind Kind::VALUE, representing the rounding mode value.

Term mk_term(Kind kind, const std::vector<Term> &args, const std::vector<uint64_t> &indices = {})

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

See also

Parameters:

  • kind – The operator kind.

  • args – The argument terms.

  • indices – The indices of this term, empty if not indexed.

Returns:

A term representing an operation of given kind.

Term mk_const(const Sort &sort, const std::optional<std::string> &symbol = std::nullopt)

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

See also

  • TermManager::mk_array_sort()

  • TermManager::mk_bool_sort()

  • TermManager::mk_bv_sort()

  • TermManager::mk_fp_sort()

  • TermManager::mk_fun_sort()

  • TermManager::mk_rm_sort()

Parameters:

  • sort – The sort of the constant.

  • symbol – The symbol of the constant.

Returns:

A term of Kind::CONSTANT, representing the constant.

Term mk_var(const Sort &sort, const std::optional<std::string> &symbol = std::nullopt)

Create a variable of given sort with given symbol.

See also

  • TermManager::mk_bool_sort()

  • TermManager::mk_bv_sort()

  • TermManager::mk_fp_sort()

  • TermManager::mk_fun_sort()

  • TermManager::mk_rm_sort()

Note

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

Parameters:

  • sort – The sort of the variable.

  • symbol – The symbol of the variable.

Returns:

A term of Kind::VARIABLE, representing the variable.

Term substitute_term(const Term &term, const std::unordered_map<Term, Term> &map)

Substitute a set terms in a given term. The substitutions to perform are represented as map from keys to be substituted with their corresponding values in the given term.

Parameters:

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

  • map – The substitution map.

Returns:

The resulting term from this substitution.

void substitute_terms(std::vector<Term> &terms, const std::unordered_map<Term, Term> &map)

Substitute a set of terms in a set of given terms. The substitutions to perform are represented as map from keys to be substituted with their corresponding values in the given terms.

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

Parameters:

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

  • map – The substitution map.

}