path: root/abstract/value_domain.ml

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