diff options
Diffstat (limited to 'abstract/intervals_domain.ml')
| -rw-r--r-- | abstract/intervals_domain.ml | 20 |
1 files changed, 8 insertions, 12 deletions
diff --git a/abstract/intervals_domain.ml b/abstract/intervals_domain.ml index 848f634..181266b 100644 --- a/abstract/intervals_domain.ml +++ b/abstract/intervals_domain.ml @@ -1,9 +1,7 @@ open Value_domain module VD : VALUE_DOMAIN = struct - type bound = Int of int | PInf | MInf - - type t = Itv of bound * bound | Bot + type t = itv (* utilities *) let bound_leq a b = (* a <= b ? *) @@ -64,14 +62,18 @@ module VD : VALUE_DOMAIN = struct | MInf -> PInf | Int i -> Int (- i) - let bound_abs a = bound_max a (bound_neg a) + let bound_abs a = bound_max a (bound_neg a) (* implementation *) let top = Itv(MInf, PInf) let bottom = Bot let const i = Itv(Int i, Int i) let rand i j = - if i <= j then Itv(Int i, Int j) else Bot + if i <= j then Itv(Int i, Int j) else Bot + let to_itv x = x + let as_const = function + | Itv(Int i, Int j) when i = j -> Some i + | _ -> None let subset a b = match a, b with | Bot, _ -> true @@ -147,12 +149,6 @@ module VD : VALUE_DOMAIN = struct 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 -> string_of_int i - let to_string = function - | Bot -> "bot" - | Itv(a, b) -> "[" ^ (bound_str a) ^ ";" ^ (bound_str b) ^ "]" + let to_string = string_of_itv end |