blob: a0f082f3c3d6d67a7f246bc8dbaad725af81fb90 (
plain) (
tree)
|
|
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]) *)
end
|
