blob: 9cf6d768b5e816ea0cccf3f8a0d3b8ec40d6fab0 (
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
|
module type VALUE_DOMAIN = sig
type t
(* constructors *)
val top : t
val bottom : t
val const : Z.t -> t
val rand : Z.t -> Z.t -> t
(* 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
|
