Term (bitwuzla-cxx.Bitwuzla

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

raises Not_found
if no symbol is defined.

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 =

| Bool : bool cast
(*
for Boolean values
*)
| RoundingMode : RoundingMode.t cast
(*
for rounding mode values
*)
| String : {
1. base : int;
} -> string cast
(*
for any value (Boolean, RoundingMode, bit-vector and floating-point)
*)
| IEEE_754 : (string * string * string) cast
(*
for floating-point values as strings for sign bit, exponent and significand
*)
| 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.