path: root/abstract/intervals_domain.ml

open Value_domain

module Intervals : VALUE_DOMAIN = struct
    type bound = Int of Z.t | PInf | MInf

    type t = Itv of bound * bound | Bot

    (* utilities *)
    let bound_leq a b =   (* a <= b ? *)
        match a, b with
        | MInf, _ | _, PInf -> true
        | Int a, Int b -> Z.leq a b
        | x, y -> x = y

    let bound_add a b =
        match a, b with
        | MInf, Int a | Int a, MInf -> MInf
        | PInf, Int a | Int a, PInf -> PInf
        | MInf, MInf -> MInf
        | PInf, PInf -> PInf
        | Int a, Int b -> Int (Z.add a b)
        | _ -> assert false
    let bound_mul a b =
        match a, b with
        | PInf, Int(x) | Int(x), PInf ->
            if x > Z.zero then PInf
            else if x < Z.zero then MInf
            else Int Z.zero
        | MInf, Int(x) | Int(x), MInf ->
            if x < Z.zero then PInf
            else if x > Z.zero then MInf
            else Int Z.zero
        | Int(x), Int(y) -> Int(Z.mul x y)
        | MInf, PInf | PInf, MInf -> MInf
        | MInf, MInf | PInf, PInf -> PInf

    let bound_min a b = match a, b with
        | MInf, _ | _, MInf -> MInf
        | Int a, Int b -> Int (min a b)
        | Int a, PInf -> Int a
        | PInf, Int a -> Int a
        | PInf, PInf -> PInf
    let bound_max a b = match a, b with
        | PInf, _ | _, PInf -> PInf
        | Int a, Int b -> Int (max a b)
        | Int a, MInf | MInf, Int a -> Int a
        | MInf, MInf -> MInf

    let bound_neg = function
        | PInf -> MInf
        | MInf -> PInf
        | Int i -> Int (Z.neg i)

    (* implementation *)
    let top = Itv(MInf, PInf)
    let bottom = Bot
    let const i = Itv(Int i, Int i)
    let rand i j =
    if Z.leq i j then Itv(Int i, Int j) else Bot

    let subset a b = match a, b with
        | Bot, _ -> true
        | _, Bot -> false
        | Itv(a, b), Itv(c, d) -> bound_leq a c && bound_leq d b

    let join a b = match a, b with
        | Bot, x | x, Bot -> x
        | Itv(a, b), Itv(c, d) -> Itv(bound_min a c, bound_max b d)

    let meet a b = match a, b with
        | Bot, x | x, Bot -> Bot
        | Itv(a, b), Itv(c, d) ->
            let u, v = bound_max a c, bound_min b d in
            if bound_leq u v
            then Itv(u, v)
            else Bot

    let widen a b = match a, b with
        | x, Bot | Bot, x -> x
        | Itv(a, b), Itv(c, d) ->
            Itv(
            (if not (bound_leq a c) then MInf else a),
            (if not (bound_leq d b) then PInf else b))

    let neg = function
        | Bot -> Bot
        | Itv(a, b) -> Itv(bound_neg b, bound_neg a)
    let add a b = match a, b with
        | Bot, _ | _, Bot -> Bot
        | Itv(a, b), Itv(c, d) -> Itv(bound_add a c, bound_add b d)
    let sub a b = match a, b with
        | Bot, _ | _, Bot -> Bot
        | Itv(a, b), Itv(c, d) -> Itv(bound_add a (bound_neg d), bound_add b (bound_neg c))
    let mul a b = match a, b with
        | Bot, _ | _, Bot -> Bot
        | Itv(a, b), Itv(c, d) ->
            Itv(
                (bound_min (bound_min (bound_mul a c) (bound_mul a d))
                            (bound_min (bound_mul b c) (bound_mul b d))),
                (bound_max (bound_max (bound_mul a c) (bound_mul a d))
                            (bound_max (bound_mul b c) (bound_mul b d))))
        

    let div a b = top (* TODO *)
    let rem a b = top (* TODO *)

    let leq a b = match a, b with
        | Bot, _ | _, Bot -> Bot, Bot
        | Itv(a, b), Itv(c, d) ->
            if not (bound_leq a d)
            then Bot, Bot
            else Itv(a, bound_min b d), Itv(bound_max a c, d)

    let bound_str = function
        | MInf -> "-oo"
        | PInf -> "+oo"
        | Int i -> Z.to_string i
    let to_string = function
        | Bot -> "bot"
        | Itv(a, b) -> "[" ^ (bound_str a) ^ ";" ^ (bound_str b) ^ "]"

end