package bitwuzla-cxx

  1. Overview
  2. Docs

Term

type t

A Bitwuzla term.

Util

val hash : t -> int

hash t compute the hash value for a term.

  • parameter t

    The term.

  • returns

    The hash value of the term.

val equal : t -> t -> bool

equal a b Syntactical equality operator.

  • parameter a

    The first term.

  • parameter b

    The second term.

  • returns

    True if the given terms are equal.

val compare : t -> t -> int

compare a b Syntactical comparison operator.

  • parameter a

    The first term.

  • parameter b

    The second term.

  • returns

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

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

pp formatter t print term.

(alias for pp_smt2 2)

  • parameter formatter

    The outpout formatter.

  • parameter t

    The term.

val pp_smt2 : bv_format:int -> Format.formatter -> t -> unit

pp_smt2 base formatter t print term in SMTlib format.

  • parameter bv_format

    The bit-vector number format: 2 for binary, 10 for decimal and 16 for hexadecimal.

  • parameter formatter

    The output formatter.

  • parameter t

    The term.

val to_string : ?bv_format:int -> t -> string

to_string t ~bv_format get string representation of this term.

  • parameter t

    The term.

  • parameter bv_format

    The bit-vector number format: 2 for binary [default], 10 for decimal and 16 for hexadecimal.

  • returns

    String representation of this term.

Query

val id : t -> int64

id t get the id of this term.

  • parameter t

    The term.

  • returns

    The id value of the term.

val kind : t -> Kind.t

kind t get the kind of a term.

  • parameter t

    The term.

  • returns

    The kind of the given term.

val sort : t -> Sort.t

sort t get the sort of a term.

  • parameter t

    The term.

  • returns

    The sort of the term.

val num_children : t -> int

num_children t get the number of child terms of a term.

  • parameter t

    The term.

  • returns

    The number children of t.

val children : t -> t array

children t get the child terms of a term.

  • parameter t

    The term.

  • returns

    The children of t as an array of terms.

val get : t -> int -> t

get t i return child at position i.

Only valid to call if num_children t > 0.

  • parameter i

    The position of the child.

  • returns

    The child node at position i.

val num_indices : t -> int

num_indices t get the number of indices of an indexed term.

Requires that given term is an indexed term.

  • parameter t

    The term.

  • returns

    The number of indices of t.

val indices : t -> int array

indices t get the indices of an indexed term.

Requires that given term is an indexed term.

  • parameter t

    The term.

  • returns

    The children of t as an array of terms.

val symbol : t -> string

symbol t get the symbol of a term.

  • parameter t

    The term.

  • returns

    The symbol of t.

val is_const : t -> bool

is_const t determine if a term is a constant.

  • parameter t

    The term.

  • returns

    true if t is a constant.

val is_variable : t -> bool

is_variable t determine if a term is a variable.

  • parameter t

    The term.

  • returns

    true if t is a variable.

val is_value : t -> bool

is_value t determine if a term is a value.

  • parameter t

    The term.

  • returns

    true if t is a value.

val is_bv_value_zero : t -> bool

is_bv_value_zero t determine if a term is a bit-vector value representing zero.

  • parameter t

    The term.

  • returns

    true if t is a bit-vector zero value.

val is_bv_value_one : t -> bool

is_bv_value_one t determine if a term is a bit-vector value representing one.

  • parameter t

    The term.

  • returns

    true if t is a bit-vector one value.

val is_bv_value_ones : t -> bool

is_bv_value_ones t determine if a term is a bit-vector value with all bits set to one.

  • parameter t

    The term.

  • returns

    true if t is a bit-vector value with all bits set to one.

val is_bv_value_min_signed : t -> bool

is_bv_value_min_signed t determine if a term is a bit-vector minimum signed value.

  • parameter t

    The term.

  • returns

    true if t is a bit-vector value with the most significant bit set to 1 and all other bits set to 0.

val is_bv_value_max_signed : t -> bool

is_bv_value_max_signed t determine if a term is a bit-vector maximum signed value.

  • parameter t

    The term.

  • returns

    true if t is a bit-vector value with the most significant bit set to 0 and all other bits set to 1.

val is_fp_value_pos_zero : t -> bool

is_fp_value_pos_zero t determine if a term is a floating-point positive zero (+zero) value.

  • parameter t

    The term.

  • returns

    true if t is a floating-point +zero value.

val is_fp_value_neg_zero : t -> bool

is_fp_value_neg_zero t determine if a term is a floating-point value negative zero (-zero).

  • parameter t

    The term.

  • returns

    true if t is a floating-point value negative zero.

val is_fp_value_pos_inf : t -> bool

is_fp_value_pos_inf t determine if a term is a floating-point positive infinity (+oo) value.

  • parameter t

    The term.

  • returns

    true if t is a floating-point +oo value.

val is_fp_value_neg_inf : t -> bool

is_fp_value_neg_inf t determine if a term is a floating-point negative infinity (-oo) value.

  • parameter t

    The term.

  • returns

    true if t is a floating-point -oo value.

val is_fp_value_nan : t -> bool

is_fp_value_nan t determine if a term is a floating-point NaN value.

  • parameter t

    The term.

  • returns

    true if t is a floating-point NaN value.

val is_rm_value_rna : t -> bool

is_rm_value_rna t determine if a term is a rounding mode RNA value.

  • parameter t

    The term.

  • returns

    true if t is a rounding mode RNA value.

val is_rm_value_rne : t -> bool

is_rm_value_rna t determine if a term is a rounding mode RNE value.

  • parameter t

    The term.

  • returns

    true if t is a rounding mode RNE value.

val is_rm_value_rtn : t -> bool

is_rm_value_rna t determine if a term is a rounding mode RTN value.

  • parameter t

    The term.

  • returns

    true if t is a rounding mode RTN value.

val is_rm_value_rtp : t -> bool

is_rm_value_rna t determine if a term is a rounding mode RTP value.

  • parameter t

    The term.

  • returns

    true if t is a rounding mode RTP value.

val is_rm_value_rtz : t -> bool

is_rm_value_rna t determine if a term is a rounding mode RTZ value.

  • parameter t

    The term.

  • returns

    true if t is a rounding mode RTZ value.

type _ cast =
  1. | Bool : bool cast
    (*

    for Boolean values

    *)
  2. | RoundingMode : RoundingMode.t cast
    (*

    for rounding mode values

    *)
  3. | String : {
    1. base : int;
    } -> string cast
    (*

    for any value (Boolean, RoundingMode, bit-vector and floating-point)

    *)
  4. | IEEE_754 : (string * string * string) cast
    (*

    for floating-point values as strings for sign bit, exponent and significand

    *)
  5. | Z : Z.t cast
    (*

    for bit-vector

    *)
val value : 'a cast -> t -> 'a

value kind t get value from value term.

  • parameter kind

    The type of the value representation.

  • returns

    The value of t in a given representation.

OCaml

Innovation. Community. Security.