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:
- min ≤ max
- 0 ≤ rem < modu
- min ≅ rem
modu
∧ max ≅ rem modu
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