Sort (bitwuzla-cxx.Bitwuzla

Sort

type t

A Bitwuzla sort.

Util

val hash : t -> int

hash t compute the hash value for a sort.

parameter t
The sort.

returns
The hash value of the sort.

val equal : t -> t -> bool

equal a b Syntactical equality operator.

parameter a
The first sort.

parameter b
The second sort.

returns
True if the given sorts are equal.

val compare : t -> t -> int

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.

val pp : Stdlib.Format.formatter -> t -> unit

pp formatter t print sort.

parameter t
The sort.

parameter formatter
The outpout formatter.

val to_string : t -> string

to_string t get string representation of this sort.

returns
String representation of this sort.

Query

val id : t -> int64

id t get the id of this sort.

parameter t
The sort.

returns
The id value of the sort.

val bv_size : t -> int

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.

val fp_exp_size : t -> int

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.

val fp_sig_size : t -> int

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.

val array_index : t -> t

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.

val array_element : t -> t

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.

val fun_domain : t -> t array

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.

val fun_codomain : t -> t

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.

val fun_arity : t -> int

fun_arity t get the arity of a function sort.

parameter t
The sort.

returns
The number of arguments of the function sort.

val uninterpreted_symbol : t -> string

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.

val is_array : t -> bool

is_array t determine if a sort is an array sort.

parameter t
The sort.

returns
true if t is an array sort.

val is_bool : t -> bool

is_bool t determine if a sort is a Boolean sort.

parameter t
The sort.

returns
true if t is a Boolean sort.

val is_bv : t -> bool

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.

val is_fp : t -> bool

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.

val is_fun : t -> bool

is_fun t determine if a sort is a function sort.

parameter t
The sort.

returns
true if t is a function sort.

val is_rm : t -> bool

is_rm t determine if a sort is a Roundingmode sort.

parameter t
The sort.

returns
true if t is a Roundingmode sort.

val is_uninterpreted : t -> bool

is_uninterpreted t determine if a sort is an uninterpreted sort.

parameter t
The sort.

returns
true if t is an uninterpreted sort.