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 Bottom.Type.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 Bottom.Type.or_bottom
val neg : 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 Bottom.Type.or_bottom
val scale_rem : pos:bool -> Integer.t -> t -> t
val mul : t -> t -> t
val div : t -> t -> t Bottom.Type.or_bottom
val c_rem : t -> t -> t Bottom.Type.or_bottom
val cast : size:Integer.t -> signed:bool -> t -> t

Misc.


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