package bitwuzla-cxx

  1. Overview
  2. Docs

Module Bitwuzla_cxx.SortSource

Sort

Sourcetype t

A Bitwuzla sort.

Util

Sourceval hash : t -> int

hash t compute the hash value for a sort.

  • parameter t

    The sort.

  • returns

    The hash value of the sort.

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

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

Sourceval pp : Format.formatter -> t -> unit

pp formatter t print sort.

  • parameter t

    The sort.

  • parameter formatter

    The outpout formatter.

Sourceval to_string : t -> string

to_string t get string representation of this sort.

  • returns

    String representation of this sort.

Query

Sourceval id : t -> int64

id t get the id of this sort.

  • parameter t

    The sort.

  • returns

    The id value of the sort.

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

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

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

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

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

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

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

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

Sourceval uninterpreted_symbol : t -> string

uninterpreted_symbol t get the symbol of an uninterpreted sort.

  • parameter t

    The sort.

  • returns

    The symbol.

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

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

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

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

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

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

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