Skip to content

Commit fb3b89c

Browse files
committed
Simplify interval div
1 parent b5b4d8d commit fb3b89c

File tree

1 file changed

+16
-22
lines changed

1 file changed

+16
-22
lines changed

src/cdomain/value/cdomains/intDomain0.ml

Lines changed: 16 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -372,28 +372,22 @@ module IntervalArith (Ints_t : IntOps.IntOps) = struct
372372
let x2y2p = (Ints_t.div x2 y2) in
373373
(min4 x1y1n x1y2n x2y1n x2y2n, max4 x1y1p x1y2p x2y1p x2y2p)
374374

375-
let rec div (a, b) (c, d) =
376-
(* let open Ints_t in *)
377-
assert Ints_t.(compare c d <= 0);
378-
if Ints_t.(compare one c) <= 0 then
379-
(None, Some (Ints_t.(min (div a c) (div a d), max (div b c) (div b d))))
380-
else if Ints_t.(compare d zero) < 0 then
381-
(Some (Ints_t.(min (div b c) (div b d), max (div a c) (div a d))), None)
382-
else (
383-
let p =
384-
if Ints_t.(compare one d) <= 0 then
385-
snd (div (a, b) (Ints_t.one, d))
386-
else
387-
None
388-
in
389-
let n =
390-
if Ints_t.(compare c zero) < 0 then
391-
fst (div (a, b) (c, Ints_t.(neg one)))
392-
else
393-
None
394-
in
395-
(n, p)
396-
)
375+
let div (a, b) (c, d) =
376+
let pos =
377+
if Ints_t.(compare one d) <= 0 then
378+
let c = Ints_t.(max one c) in
379+
Some (Ints_t.(min (div a c) (div a d), max (div b c) (div b d)))
380+
else
381+
None
382+
in
383+
let neg =
384+
if Ints_t.(compare c zero) < 0 then
385+
let d = Ints_t.(min d (neg one)) in
386+
Some (Ints_t.(min (div b c) (div b d), max (div a c) (div a d)))
387+
else
388+
None
389+
in
390+
(neg, pos)
397391

398392
let add (x1, x2) (y1, y2) = (Ints_t.add x1 y1, Ints_t.add x2 y2)
399393
let sub (x1, x2) (y1, y2) = (Ints_t.sub x1 y2, Ints_t.sub x2 y1)

0 commit comments

Comments
 (0)