A Bitwuzla sort.

hash t compute the hash value for a sort.

• parameter t

  The sort.

• returns

  The hash value of the sort.

equal a b Syntactical equality operator.

• parameter a

  The first sort.

• parameter b

  The second sort.

• returns

  True if the given sorts are equal.

compare a b Syntactical comparison operator.

• parameter a

  The first sort.

• parameter b

  The second sort.

• returns

  Zero if the given sorts are equal, a positive number if a > b, a negative number otherwise.

pp formatter t print sort.

• parameter t

  The sort.

• parameter formatter

  The outpout formatter.

to_string t get string representation of this sort.

• returns

  String representation of this sort.

id t get the id of this sort.

• parameter t

  The sort.

• returns

  The id value of the sort.

bv_size t get the size of a bit-vector sort.

Requires that given sort is a bit-vector sort.

• parameter t

  The sort.

• returns

  The size of the bit-vector sort.

fp_exp_size sort get the exponent size of a floating-point sort.

Requires that given sort is a floating-point sort.

• parameter t

  The sort.

• returns

  The exponent size of the floating-point sort.

fp_sig_size t get the significand size of a floating-point sort.

Requires that given sort is a floating-point sort.

• parameter t

  The sort.

• returns

  The significand size of the floating-point sort.

array_index t get the index sort of an array sort.

Requires that given sort is an array sort.

• parameter t

  The sort.

• returns

  The index sort of the array sort.

array_element t get the element sort of an array sort.

Requires that given sort is an array sort.

• parameter t

  The sort.

• returns

  The element sort of the array sort.

fun_domain_sorts t get the domain sorts of a function sort.

Requires that given sort is a function sort.

• parameter t

  The sort.

• returns

  The domain sorts of the function sort as an array of sort.

fun_codomain t get the codomain sort of a function sort.

Requires that given sort is a function sort.

• parameter t

  The sort.

• returns

  The codomain sort of the function sort.

fun_arity t get the arity of a function sort.

• parameter t

  The sort.

• returns

  The number of arguments of the function sort.

uninterpreted_symbol t get the symbol of an uninterpreted sort.

• parameter t

  The sort.

• returns

  The symbol.

• raises Not_found

  if no symbol is defined.

is_array t determine if a sort is an array sort.

• parameter t

  The sort.

• returns

  true if t is an array sort.

is_bool t determine if a sort is a Boolean sort.

• parameter t

  The sort.

• returns

  true if t is a Boolean sort.

is_bv t determine if a sort is a bit-vector sort.

• parameter t

  The sort.

• returns

  true if t is a bit-vector sort.

is_fp t determine if a sort is a floating-point sort.

• parameter t

  The sort.

• returns

  true if t is a floating-point sort.

is_fun t determine if a sort is a function sort.

• parameter t

  The sort.

• returns

  true if t is a function sort.

is_rm t determine if a sort is a Roundingmode sort.

• parameter t

  The sort.

• returns

  true if t is a Roundingmode sort.

is_uninterpreted t determine if a sort is an uninterpreted sort.

• parameter t

  The sort.

• returns

  true if t is an uninterpreted sort.