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