summaryrefslogtreecommitdiff
path: root/abstract/intervals_domain.ml
diff options
context:
space:
mode:
Diffstat (limited to 'abstract/intervals_domain.ml')
-rw-r--r--abstract/intervals_domain.ml230
1 files changed, 115 insertions, 115 deletions
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
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-21 20:18:33 +0000