Commit 840640e0 authored by David Bühler's avatar David Bühler

[Ival] In int_val, fixes [min_max_rem_modu] on singletons.

parent 07b12648
......@@ -190,16 +190,15 @@ let inject_set_or_top_or_bottom = function
(* Computes [min], [max], [rem] and [modu] from an integer set. *)
let make_top_from_set s =
let min = Int_set.min s in
let modu =
Int_set.fold
(fun x acc ->
if Int.equal x min
then acc
else Int.pgcd (Int.sub x min) acc)
s
Int.zero
let rem, modu =
if Int_set.cardinal s = 1
then Int.zero, min
else
let modu =
Int_set.fold (fun x acc -> Int.pgcd (Int.sub x min) acc) s Int.zero
in
Int.e_rem min modu, modu
in
let rem = Int.e_rem min modu in
let max = Some (Int_set.max s) in
let min = Some min in
min, max, rem, modu
......
......@@ -86,8 +86,7 @@ val max_int: t -> Integer.t option
val min_and_max: t -> Integer.t option * Integer.t option
(** Returns [min, max, rem, modu] such that for all integers [i] represented by
the given abstraction, [i] satisfies min ≤ i ≤ max and i ≅ rem [modu].
The abstraction must not be a singleton. *)
the given abstraction, [i] satisfies min ≤ i ≤ max and i ≅ rem [modu]. *)
val min_max_rem_modu:
t -> Integer.t option * Integer.t option * Integer.t * Integer.t
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment