diff options
Diffstat (limited to 'abstract/value_domain.ml')
| -rw-r--r-- | abstract/value_domain.ml | 44 |
1 files changed, 29 insertions, 15 deletions
diff --git a/abstract/value_domain.ml b/abstract/value_domain.ml index fb01ac6..7b9d557 100644 --- a/abstract/value_domain.ml +++ b/abstract/value_domain.ml @@ -1,30 +1,44 @@ + +type bound = Int of int | PInf | MInf +type itv = Itv of bound * bound | Bot + +let string_of_bound = function + | MInf -> "-oo" + | PInf -> "+oo" + | Int i -> string_of_int i +let string_of_itv = function + | Bot -> "⊥" + | Itv(a, b) -> "[" ^ (string_of_bound a) ^ ";" ^ (string_of_bound b) ^ "]" + module type VALUE_DOMAIN = sig type t (* constructors *) - val top : t - val bottom : t - val const : int -> t - val rand : int -> int -> t + val top : t + val bottom : t + val const : int -> t + val rand : int -> int -> t + val to_itv : t -> itv + val as_const : t -> int option (* order *) - val subset : t -> t -> bool + val subset : t -> t -> bool (* set-theoretic operations *) - val join : t -> t -> t (* union *) - val meet : t -> t -> t (* intersection *) - val widen : t -> t -> t + val join : t -> t -> t (* union *) + val meet : t -> t -> t (* intersection *) + val widen : t -> t -> t (* arithmetic operations *) - val neg : t -> t - val add : t -> t -> t - val sub : t -> t -> t - val mul : t -> t -> t - val div : t -> t -> t - val rem : t -> t -> t + val neg : t -> t + val add : t -> t -> t + val sub : t -> t -> t + val mul : t -> t -> t + val div : t -> t -> t + val rem : t -> t -> t (* boolean test *) - val leq : t -> t -> t * t (* For intervals : [a, b] -> [c, d] -> ([a, min b d], [max a c, d]) *) + val leq : t -> t -> t * t (* For intervals : [a, b] -> [c, d] -> ([a, min b d], [max a c, d]) *) (* pretty-printing *) val to_string : t -> string |