blob: 7b9d55764fa0717f9d3f185b6913aa12decbadb3 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
|
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 to_itv : t -> itv
val as_const : t -> int option
(* order *)
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
(* 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
(* boolean test *)
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
end
|
