package smtml

  1. Overview
  2. Docs
An SMT solver frontend for OCaml

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (18)

Authors

  1. J
    João Pereira <joaomhmpereira@tecnico.ulisboa.pt>
  2. F
    Filipe Marques <filipe.s.marques@tecnico.ulisboa.pt>
  3. H
    Hichem Rami Ait El Hara <hra@ocamlpro.com>
  4. R
    redianthus <redopam@pm.me>
  5. A
    Arthur Carcano <arthur.carcano@ocamlpro.com>
  6. P
    Pierre Chambart <pierre.chambart@ocamlpro.com>
  7. J
    José Fragoso Santos <jose.fragoso@tecnico.ulisboa.pt>

Maintainers

  1. F
    Filipe Marques <filipe.s.marques@tecnico.ulisboa.pt>

Sources

v0.22.0.tar.gz
md5=2ec822c82786736b275c31e850f7d292
sha512=335a1595b0652ca0d5aa50177e47a66467935d586433ad26329d6fa7d9ff6fd3eda51d630c2002278eb6565e8de83e0750b000c0a0f5b453b7ed11ffca3519a2

doc/smtml/Smtml/Typed/Bitv32/index.html

Module Typed.Bitv32Source

include Bitv.S with type w = bitv32
Sourcetype w = bitv32
Sourcetype t = w expr
Sourceval ty : w ty
Sourceval zero : t

The bitvector value 0.

Sourceval one : t

The bitvector value 1.

Sourceval v : Bitvector.t -> t
Sourceval of_int : int -> t

of_int i creates a bitvector term from an integer i.

Sourceval symbol : Symbol.t -> t
Sourceval clz : t -> t

clz t counts the leading zeros in t.

Sourceval ctz : t -> t

ctz t counts the trailing zeros in t.

Sourceval popcnt : t -> t

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

Sourceval neg : t -> t

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

Sourceval lognot : t -> t

lognot t computes the bitwise NOT of t.

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

Sourceval add : t -> t -> t

add t1 t2 computes the bitwise addition t1 + t2.

Sourceval sub : t -> t -> t

sub t1 t2 computes the bitwise subtraction t1 - t2.

Sourceval mul : t -> t -> t

mul t1 t2 computes the bitwise multiplication t1 * t2.

Sourceval div : t -> t -> t

div t1 t2 is integer division.

Sourceval unsigned_div : t -> t -> t

unsigned_div t1 t2 is explicitly unsigned integer division.

Sourceval logor : t -> t -> t
Sourceval logand : t -> t -> t
Sourceval logxor : t -> t -> t
Sourceval shl : t -> t -> t

shl t amount shifts t left by amount bits.

Sourceval ashr : t -> t -> t

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

Sourceval lshr : t -> t -> t

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

Sourceval rem : t -> t -> t

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

Sourceval unsigned_rem : t -> t -> t

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

Sourceval rotate_left : t -> t -> t

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

Sourceval rotate_right : t -> t -> t

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

Sourceval eq : t -> t -> bool expr

Alias for Bool.eq.

Sourceval ne : t -> t -> bool expr

Negation of eq.

Sourceval lt : t -> t -> bool expr

lt t1 t2 is signed less-than.

Sourceval lt_u : t -> t -> bool expr

lt_u t1 t2 is unsigned less-than.

Sourceval le : t -> t -> bool expr

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

Sourceval le_u : t -> t -> bool expr

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

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

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

extract t ~high ~low extracts the bytes from index high down to low (inclusive).

Example: extract (i32 0xAABBCCDD) ~high:2 ~low:1 results in 0xCC (1-byte).

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

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

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

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

Sourceval to_bool : t -> bool expr

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

Sourceval of_bool : bool expr -> t

of_bool b converts true to 1 and false to 0.

Sourceval pp : t Fmt.t
Sourceval of_int32 : Smtml_prelude.Int32.t -> t

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

Sourceval of_int8_s : bitv8 expr -> t

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

Sourceval of_int8_u : bitv8 expr -> t

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

Sourceval of_int16_s : bitv16 expr -> t

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

Sourceval of_int16_u : bitv16 expr -> t

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Sourceval reinterpret_f32 : float32 expr -> t

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

Sourceval wrap_i64 : bitv64 expr -> t

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

Sourceval extend_s : int -> t -> t

extend_s n t sign-extends t by n bits.