Module Abstract_interp.Int

include module type of Integer with type t = Z.t

type t = Z.t

val equal : t -> t -> bool

val compare : t -> t -> int

val le : t -> t -> bool

val ge : t -> t -> bool

val lt : t -> t -> bool

val gt : t -> t -> bool

val add : t -> t -> t

val sub : t -> t -> t

val mul : t -> t -> t

val shift_left : t -> t -> t

• raises Invalid_argument

  if second argument (count) is negative

val shift_right : t -> t -> t

• raises Invalid_argument

  if second argument (count) is negative

val shift_right_logical : t -> t -> t

• raises Invalid_argument

  if any argument is negative

val logand : t -> t -> t

val logor : t -> t -> t

val logxor : t -> t -> t

val lognot : t -> t

val min : t -> t -> t

val max : t -> t -> t

val e_div : t -> t -> t

Euclidean division (that returns a positive rem). Implemented by Z.ediv

Equivalent to C division if both operands are positive. Equivalent to a floored division if b > 0 (rounds downwards), otherwise rounds upwards. Note: it is possible that e_div (-a) b <> e_div a (-b).

val e_rem : t -> t -> t

Remainder of the Euclidean division (always positive). Implemented by Z.erem

val e_div_rem : t -> t -> t * t

e_div_rem a b returns (e_div a b, e_rem a b). Implemented by Z.ediv_rem

val c_div : t -> t -> t

Truncated division towards 0 (like in C99). Implemented by Z.div

val c_rem : t -> t -> t

Remainder of the truncated division towards 0 (like in C99). Implemented by Z.rem

val c_div_rem : t -> t -> t * t

c_div_rem a b returns (c_div a b, c_rem a b). Implemented by Z.div_rem

val pgcd : t -> t -> t

pgcd v 0 == pgcd 0 v == abs v. Result is always positive

val ppcm : t -> t -> t

ppcm v 0 == ppcm 0 v == 0. Result is always positive

val cast : size:t -> signed:bool -> value:t -> t

val abs : t -> t

val neg : t -> t

val succ : t -> t

val pred : t -> t

val is_zero : t -> bool

val is_one : t -> bool

val is_even : t -> bool

val zero : t

val one : t

val two : t

val four : t

val eight : t

val sixteen : t

val thirtytwo : t

val onethousand : t

val billion_one : t

val minus_one : t

val max_int64 : t

val min_int64 : t

val two_power_32 : t

val two_power_64 : t

val length : t -> t -> t

b - a + 1

val of_int : int -> t

val of_int64 : Stdlib.Int64.t -> t

val of_int32 : Stdlib.Int32.t -> t

val to_int : t -> int

• raises Z.Overflow

  if too big

val to_int64 : t -> int64

• raises Z.Overflow

  if too big

• raises Z.Overflow

  if too big

val to_int32 : t -> int32

• raises Z.Overflow

  if too big

• raises Z.Overflow

  if too big

val to_float : t -> float

val of_float : float -> t

val round_up_to_r : min:t -> r:t -> modu:t -> t

round_up_to_r m r modu is the smallest number n such that n>=m and n = r modulo modu

val round_down_to_r : max:t -> r:t -> modu:t -> t

round_down_to_r m r modu is the largest number n such that n<=m and n = r modulo modu

val two_power : t -> t

Computes 2^n

• raises Z.Overflow

  for exponents greater than 1024

val two_power_of_int : int -> t

Computes 2^n

val power_int_positive_int : int -> int -> t

Exponentiation

val extract_bits : start:t -> stop:t -> t -> t

val popcount : t -> int

val hash : t -> int

val to_string : t -> string

val of_string : string -> t

• raises Invalid_argument

  when the string cannot be parsed.

val pp_bin : ?nbits:int -> ?sep:string -> t Pretty_utils.formatter

Print binary format. Digits are output by blocs of 4 bits separated by ~sep with at least ~nbits total bits. If nbits is non positive, it will be ignored.

Positive values are prefixed with "0b" and negative values are printed as their 2-complement (lnot) with prefix "1b".

val pp_hex : ?nbits:int -> ?sep:string -> t Pretty_utils.formatter

Print hexadecimal format. Digits are output by blocs of 16 bits (4 hex digits) separated by ~sep with at least ~nbits total bits. If nbits is non positive, it will be ignored.

Positive values are preffixed with "0x" and negative values are printed as their 2-complement (lnot) with prefix "1x".

module Set : sig ... end

val pretty : Stdlib.Format.formatter -> t -> unit

val fold : (t -> 'a -> 'a) -> inf:t -> sup:t -> step:t -> 'a -> 'a

Fold the function on the value between inf and sup at every step. If step is positive the first value is inf and values go increasing, if step is negative the first value is sup and values go decreasing