From 77df0b0f119fc70624e4b830320a2b3e1034f7b5 Mon Sep 17 00:00:00 2001 From: Alex AUVOLAT Date: Wed, 21 May 2014 18:07:37 +0200 Subject: Just retab (many lines changed for nothing) --- abstract/intervals_domain.ml | 230 +++++++++++++++++++++---------------------- 1 file changed, 115 insertions(+), 115 deletions(-) (limited to 'abstract/intervals_domain.ml') diff --git a/abstract/intervals_domain.ml b/abstract/intervals_domain.ml index 98f4daf..b63f8a9 100644 --- a/abstract/intervals_domain.ml +++ b/abstract/intervals_domain.ml @@ -1,122 +1,122 @@ 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 = + 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) ^ "]" + 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 -- cgit v1.2.3