Previous  Up  Next

Module Int_interval

module Int_interval: sig .. end

Integer intervals with congruence. An interval defined by min, max, rem, modu represents all integers between the bounds min and max and congruent to rem modulo modu. A value of None for min (resp. max) represents -infinity (resp. +infinity). modu is > 0, and 0 <= rem < modu.

include Datatype.S_with_collections
include Eva_lattice_type.Full_AI_Lattice_with_cardinality
val check : min:Integer.t option ->
       max:Integer.t option -> rem:Integer.t -> modu:Integer.t -> unit

Checks that the interval defined by min, max, rem, modu is well formed.

val make : min:Integer.t option ->
       max:Integer.t option -> rem:Integer.t -> modu:Integer.t -> t

Makes the interval of all integers between min and max and congruent to rem modulo modu. Fails if these conditions does not hold:

val inject_range : Integer.t option -> Integer.t option -> t

Makes the interval of all integers between min and max.

val min_and_max : t -> Integer.t option * Integer.t option

Returns the bounds of the given interval. None means infinity.

val min_max_rem_modu : t -> Integer.t option * Integer.t option * Integer.t * Integer.t

Returns the bounds and the modulo of the given interval.

val mem : Integer.t -> t -> bool

mem i t returns true iff the integer i is in the interval t.

val cardinal : t -> Integer.t option

Returns the number of integers represented by the given interval. Returns None if the interval represents an infinite number of integers.

val complement_under : min:Integer.t -> max:Integer.t -> t -> t Lattice_bounds.or_bottom

Returns an under-approximation of the integers between min and max that are *not* represented by the given interval.

Interval semantics.

See Int_val for more details.

val add_singleton_int : Integer.t -> t -> t
val add : t -> t -> t
val add_under : t -> t -> t Lattice_bounds.or_bottom
val neg : t -> t
val abs : t -> t
val scale : Integer.t -> t -> t
val scale_div : pos:bool -> Integer.t -> t -> t
val scale_div_under : pos:bool -> Integer.t -> t -> t Lattice_bounds.or_bottom
val scale_rem : pos:bool -> Integer.t -> t -> t
val mul : t -> t -> t
val div : t -> t -> t Lattice_bounds.or_bottom
val c_rem : t -> t -> t Lattice_bounds.or_bottom
val cast : size:Integer.t -> signed:bool -> t -> t

Misc.

val subdivide : t -> t * t
val reduce_sign : t -> bool -> t Lattice_bounds.or_bottom
val reduce_bit : int -> t -> bool -> t Lattice_bounds.or_bottom
val fold_int : ?increasing:bool -> (Integer.t -> 'a -> 'a) -> t -> 'a -> 'a