package bitwuzla-cxx

  1. Overview
  2. Docs

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 : 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.

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.

OCaml

Innovation. Community. Security.