let intersect ({ints=l1; expl=e1; is_int=is_int} as uints1)
{ints=l2; expl=e2} =
let rec step (l1,l2) acc expl =
match l1, l2 with
| (lo1,up1)::r1, (lo2,up2)::r2 ->
let (lo1,up1), (lo2,up2) =
if is_int then (int_bornes lo1 up1), (int_bornes lo2 up2)
else (lo1,up1), (lo2,up2) in
let cll = compare_bl_bl lo1 lo2 in
let cuu = compare_bu_bu up1 up2 in
let clu = compare_bl_bu lo1 up2 in
let cul = compare_bu_bl up1 lo2 in
if cul < 0 then
let nexpl = Ex.union (explain_borne up1) (explain_borne lo2) in
match r1 with
| [] -> step (r1, l2) acc (Ex.union nexpl expl)
| (lor1,upr1)::rr1 ->
let lor1 = add_expl_to_borne lor1 nexpl in
let r1 = (lor1,upr1)::rr1 in
step (r1, l2) acc expl
else if clu > 0 then
let nexpl = Ex.union (explain_borne up2) (explain_borne lo1) in
match r2 with
| [] -> step (l1, r2) acc (Ex.union nexpl expl)
| (lor2,upr2)::rr2 ->
let lor2 = add_expl_to_borne lor2 nexpl in
let r2 = (lor2,upr2)::rr2 in
step (l1, r2) acc expl
else if cll = 0 && cuu = 0 then
step (r1, r2) ((lo1,up1)::acc) expl
else if cll <= 0 && cuu >= 0 then
step (l1, r2) ((lo2,up2)::acc) expl
else if cll >= 0 && cuu <= 0 then
step (r1, l2) ((lo1,up1)::acc) expl
else if cll <= 0 && cuu <= 0 && cul >= 0 then
step (r1, l2) ((lo2,up1)::acc) expl
else if cll >= 0 && cuu >= 0 && clu <= 0 then
step (l1, r2) ((lo1,up2)::acc) expl
else assert false
| [], _ | _, [] -> List.rev acc, expl
in
let l, expl = step (l1,l2) [] (Ex.union e1 e2) in
if l = [] then raise (NotConsistent expl)
else { uints1 with ints = l; expl = expl }