path: root/abstract/value_domain.ml

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