Sort

Bitwuzla supports 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 not tied to a specific Bitwuzla instance and can be shared across instances.

class bitwuzla::Sort
struct std::hash<bitwuzla::Sort>
bool bitwuzla::operator==(const Sort& a, const Sort& b)
bool bitwuzla::operator!=(const Sort& a, const Sort& b)
std::ostream& bitwuzla::operator<<(std::ostream& out, const Sort& term)

namespace bitwuzla {

class Sort

Public Functions

Sort(): Default constructor, creates null sort.

~Sort(): Destructor.

bool is_null() const

Determine if this sort is a null sort.

Returns:: True if this sort is a null sort.

uint64_t id() const

Get the id of this sort.

Returns:: The sort id.

uint64_t bv_size() const

Get the size of a bit-vector sort.

Requires that given sort is a bit-vector sort.

Returns:: The size of the bit-vector sort.

uint64_t fp_exp_size() const

Get the exponent size of a floating-point sort.

Requires that given sort is a floating-point sort.

Returns:: The exponent size of the floating-point sort.

uint64_t fp_sig_size() const

Get the significand size of a floating-point sort.

Requires that given sort is a floating-point sort.

Returns:: The significand size of the floating-point sort.

Sort array_index() const

Get the index sort of an array sort.

Requires that given sort is an array sort.

Returns:: The index sort of the array sort.

Sort array_element() const

Get the element sort of an array sort.

Requires that given sort is an array sort.

Returns:: The element sort of the array sort.

std::vector<Sort> fun_domain() const

Get the domain sorts of a function sort.

Requires that given sort is a function sort.

Returns:: The domain sorts of the function sort.

Sort fun_codomain() const

Get the codomain sort of a function sort.

Requires that given sort is a function sort.

Returns:: The codomain sort of the function sort.

size_t fun_arity() const

Get the arity of a function sort.

Returns:: The number of arguments of the function sort.

std::optional<std::string> uninterpreted_symbol() const

Get the symbol of an uninterpreted sort.

Returns:: The symbol.

bool is_array() const

Determine if this sort is an array sort.

Returns:: True if this sort is an array sort.

bool is_bool() const

Determine if this sort is a Boolean sort.

Returns:: True if this sort is a Boolean sort.

bool is_bv() const

Determine if this sort is a bit-vector sort.

Returns:: True if sort is a bit-vector sort.

bool is_fp() const

Determine if this sort is a floating-point sort.

Returns:: True if this sort is a floating-point sort.

bool is_fun() const

Determine if this sort is a function sort.

Returns:: True if this sort is a function sort.

bool is_rm() const

Determine if this sort is a Roundingmode sort.

Returns:: True if this sort is a Roundingmode sort.

bool is_uninterpreted() const

Determine if this sort is an uninterpreted sort.

Returns:: True if this sort is an uninterpreted sort.

std::string str() const

Get string representation of this sort.

Returns:: String representation of this sort.

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

Syntactical equality operator.

Parameters:

a – The first sort.
b – The second sort.

Returns:

True if the given sorts are equal.

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

Syntactical disequality operator.

Parameters:

a – The first sort.
b – The second sort.

Returns:

True if the given sorts are disequal.

std::ostream &bitwuzla::operator<<(std::ostream &out, const Sort &sort)

Print sort to output stream.

Parameters:

out – The output stream.
sort – The sort.

Returns:

The output stream.

}

namespace std {

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

Public Functions

size_t operator()(const bitwuzla::Sort &sort) const

Hash function for Sort.

Parameters:: sort – The sort.
Returns:: The hash value of the sort.

}