Bitv32 (docs.other.smtml.Smtml.Typed.Bitv32)

include Bitv.S with type w = bitv32

type w = bitv32

type t = w expr

val ty : w ty

val zero : t

The bitvector value 0.

val one : t

The bitvector value 1.

val v : Bitvector.t -> t

val of_int : int -> t

of_int i creates a bitvector term from an integer i.

val symbol : Symbol.t -> t

val clz : t -> t

clz t counts the leading zeros in t.

val ctz : t -> t

ctz t counts the trailing zeros in t.

val popcnt : t -> t

popcnt t counts the number of set bits (population count) in t.

val neg : t -> t

neg t computes the two's complement negation of t.

val lognot : t -> t

lognot t computes the bitwise NOT of t.

val to_int : signed:bool -> int expr -> t

to_int ~signed t converts the bitvector t to an integer term. If signed is true, t is treated as a 2's complement signed value.

val add : t -> t -> t

add t1 t2 computes the bitwise addition t1 + t2.

val sub : t -> t -> t

sub t1 t2 computes the bitwise subtraction t1 - t2.

val mul : t -> t -> t

mul t1 t2 computes the bitwise multiplication t1 * t2.

val div : t -> t -> t

div t1 t2 is integer division.

val unsigned_div : t -> t -> t

unsigned_div t1 t2 is explicitly unsigned integer division.

val logor : t -> t -> t

val logand : t -> t -> t

val logxor : t -> t -> t

val shl : t -> t -> t

shl t amount shifts t left by amount bits.

val ashr : t -> t -> t

ashr t amount performs an arithmetic shift right (preserving sign).

val lshr : t -> t -> t

lshr t amount performs a logical shift right (inserting zeros).

val rem : t -> t -> t

rem t1 t2 computes the signed remainder of t1 / t2.

val unsigned_rem : t -> t -> t

unsigned_rem t1 t2 computes the unsigned remainder of t1 / t2.

val rotate_left : t -> t -> t

rotate_left t amount rotates the bits of t to the left by amount.

val rotate_right : t -> t -> t

rotate_right t amount rotates the bits of t to the right by amount.

val eq : t -> t -> bool expr

Alias for Bool.eq.

val ne : t -> t -> bool expr

Negation of eq.

val lt : t -> t -> bool expr

lt t1 t2 is signed less-than.

val lt_u : t -> t -> bool expr

lt_u t1 t2 is unsigned less-than.

val le : t -> t -> bool expr

le t1 t2 is signed less-than-or-equal.

val le_u : t -> t -> bool expr

le t1 t2 is unsigned less-than-or-equal.

val concat : 'a expr -> 'b expr -> 'c expr

concat t1 t2 concatenates t1 (high bits) and t2 (low bits).

Example: concat (v8 0xAA) (v8 0xBB) results in 0xAABB (16-bit).

val extract : t -> high:int -> low:int -> 'a expr

extract t ~high ~low extracts the bits from index high down tolow (inclusive).

Example:extract (i32 0xAABBCCDD) ~high:15 ~low:8 results in 0xCC (8-bit).

val zero_extend : int -> t -> 'a expr

zero_extend n t extends t to a width of width(t) + n by padding with zeros.

val sign_extend : int -> t -> 'a expr

sign_extend n t extends t to a width of width(t) + n by replicating the sign bit.

val to_bool : t -> bool expr

to_bool t returns true if t is non-zero, false otherwise.

val of_bool : bool expr -> t

of_bool b converts true to 1 and false to 0.

val pp : t Fmt.t

val of_int32 : Smtml_prelude.Int32.t -> t

of_int32 i creates a 32-bit vector from an OCaml Int32.t.

val of_int8_s : bitv8 expr -> t

of_int8_s t sign-extends an 8-bit vector to 32 bits.

val of_int8_u : bitv8 expr -> t

of_int8_u t zero-extends an 8-bit vector to 32 bits.

val of_int16_s : bitv16 expr -> t

of_int16_s t sign-extends a 16-bit vector to 32 bits.

val of_int16_u : bitv16 expr -> t

of_int16_u t zero-extends a 16-bit vector to 32 bits.

val to_bytes : t -> bitv8 expr list

to_bytes t splits the 32-bit vector into 4 bytes (little-endian).

Truncate float to signed integer (raises exception on overflow/NaN).

val trunc_f32_s_exn : float32 expr -> t

trunc_f32_s_exn f truncates a float32 to a signed integer. Raises Eval.Eval_error exception on failure.

val trunc_f32_u_exn : float32 expr -> t

trunc_f32_u_exn f truncates a float32 to an unsigned integer. Raises Eval.Eval_error exception on failure.

val trunc_f64_s_exn : float64 expr -> t

trunc_f64_s_exn f truncates a float64 to a signed integer. Raises Eval.Eval_error exception on failure.

val trunc_f64_u_exn : float64 expr -> t

trunc_f64_u_exn f truncates a float64 to an unsigned integer. Raises Eval.Eval_error exception on failure.

Truncate float to signed integer (returns result/error).

val trunc_f32_s : 
  float32 expr ->
  (t, [> `Integer_overflow | `Conversion_to_integer ]) Smtml_prelude.result

trunc_f32_s f attempts to truncate a float32 to a signed integer.

val trunc_f32_u : 
  float32 expr ->
  (t, [> `Integer_overflow | `Conversion_to_integer ]) Smtml_prelude.result

trunc_f32_u f attempts to truncate a float32 to an unsigned integer.

val trunc_f64_s : 
  float64 expr ->
  (t, [> `Integer_overflow | `Conversion_to_integer ]) Smtml_prelude.result

trunc_f64_s f attempts to truncate a float64 to a signed integer.

val trunc_f64_u : 
  float64 expr ->
  (t, [> `Integer_overflow | `Conversion_to_integer ]) Smtml_prelude.result

trunc_f64_u f attempts to truncate a float64 to an unsigned integer.

Truncate with saturation (clamps to min/max on overflow, 0 on NaN).

val trunc_sat_f32_s : float32 expr -> t

trunc_sat_f32_s f truncates a float32 to signed integer with saturation. (Clamps to min/max on overflow, 0 on NaN).

val trunc_sat_f32_u : float32 expr -> t

trunc_sat_f32_u f truncates a float32 to unsigned integer with saturation. (Clamps to min/max on overflow, 0 on NaN).

val trunc_sat_f64_s : float64 expr -> t

trunc_sat_f64_s f truncates a float64 to signed integer with saturation. (Clamps to min/max on overflow, 0 on NaN).

val trunc_sat_f64_u : float64 expr -> t

trunc_sat_f64_u f truncates a float64 to unsigned integer with saturation. (Clamps to min/max on overflow, 0 on NaN).

val reinterpret_f32 : float32 expr -> t

reinterpret_f32 t interprets the bits of a float32 as a bitv32.

val wrap_i64 : bitv64 expr -> t

wrap_i64 t discards the upper 32 bits of a 64-bit integer t.

val extend_s : int -> t -> t

extend_s n t sign-extends t by n bits.