diff options
| author | Alex AUVOLAT <alex.auvolat@ens.fr> | 2014-06-01 10:06:35 +0200 |
|---|---|---|
| committer | Alex AUVOLAT <alex.auvolat@ens.fr> | 2014-06-01 10:06:35 +0200 |
| commit | 652d04c5476fdfb9cc7a2d93de3df4d76a6882ce (patch) | |
| tree | 128e3af9f8c23d9edf8ceb949565ead5840fd46a /abstract/intervals_domain.ml | |
| parent | 1038c28dab7775278c67e941a5e29d6e128eb09d (diff) | |
| download | SemVerif-Projet-652d04c5476fdfb9cc7a2d93de3df4d76a6882ce.tar.gz SemVerif-Projet-652d04c5476fdfb9cc7a2d93de3df4d76a6882ce.zip | |
Implémentation des intervalles ; début rédaction du rapport.
Diffstat (limited to 'abstract/intervals_domain.ml')
| -rw-r--r-- | abstract/intervals_domain.ml | 41 |
1 files changed, 39 insertions, 2 deletions
diff --git a/abstract/intervals_domain.ml b/abstract/intervals_domain.ml index b63f8a9..d95a938 100644 --- a/abstract/intervals_domain.ml +++ b/abstract/intervals_domain.ml @@ -33,6 +33,21 @@ module Intervals : VALUE_DOMAIN = struct | Int(x), Int(y) -> Int(Z.mul x y) | MInf, PInf | PInf, MInf -> MInf | MInf, MInf | PInf, PInf -> PInf + let bound_div a b = + match a, b with + | _, PInf | _, MInf -> Int Z.zero + | PInf, Int i -> + if i < Z.zero then MInf + else PInf + | MInf, Int i -> + if i < Z.zero then PInf + else MInf + | Int i, Int j -> + if j = Z.zero then + if i < Z.zero then MInf + else PInf + else Int (Z.div i j) + let bound_min a b = match a, b with | MInf, _ | _, MInf -> MInf @@ -50,6 +65,8 @@ module Intervals : VALUE_DOMAIN = struct | PInf -> MInf | MInf -> PInf | Int i -> Int (Z.neg i) + + let bound_abs a = bound_max a (bound_neg a) (* implementation *) let top = Itv(MInf, PInf) @@ -101,8 +118,28 @@ module Intervals : VALUE_DOMAIN = struct (bound_max (bound_mul b c) (bound_mul b d)))) - let div a b = top (* TODO *) - let rem a b = top (* TODO *) + let div a b = match a, b with + | Bot, _ -> Bot + | Itv(a, b), q -> + let p1 = match meet q (Itv(Int (Z.of_int 1), PInf)) with + | Bot -> Bot + | Itv(c, d) -> + Itv(min (bound_div a c) (bound_div a d), max (bound_div b c) (bound_div b d)) + in + let p2 = match meet q (Itv(MInf, Int (Z.of_int (-1)))) with + | Bot -> Bot + | Itv(c, d) -> + Itv(min (bound_div b c) (bound_div b d), max (bound_div a c) (bound_div a d)) + in + join p1 p2 + + let rem a b = match a, b with + | Bot, _ | _, Bot -> Bot + | Itv(a, b), Itv(c, d) -> + Itv( + Int Z.zero, + bound_max (bound_abs c) (bound_abs d) + ) let leq a b = match a, b with | Bot, _ | _, Bot -> Bot, Bot |