Module HoareDomain.MapBot

Parameters

module SpecD : Lattice.S
module R : SetDomain.S

Signature

include sig ... end
type key = SpecD.t
type value = R.t
val remove : key -> t -> t
val find : key -> t -> value
val find_opt : key -> t -> value option
val iter : (key -> value -> unit) -> t -> unit
val mapi : (key -> value -> value) -> t -> t
val add_list : (key * value) list -> t -> t
val add_list_set : key list -> value -> t -> t
val add_list_fun : key list -> (key -> value) -> t -> t
val for_all : (key -> value -> bool) -> t -> bool
val map2 : (value -> value -> value) -> t -> t -> t
val long_map2 : (value -> value -> value) -> t -> t -> t
val merge : (key -> value option -> value option -> value option) -> t -> t -> t
val cardinal : t -> int
val singleton : key -> value -> t
val empty : unit -> t
val is_empty : t -> bool
val bindings : t -> (key * value) list
val equal : t -> t -> bool
val hash : t -> int
val compare : t -> t -> int
val show : t -> string
val pretty : unit -> t -> Printable.Pretty.doc
val printXml : 'a BatInnerIO.output -> t -> unit
val name : unit -> string
val to_yojson : t -> Yojson.Safe.t
val tag : t -> int
val arbitrary : unit -> t QCheck.arbitrary
val relift : t -> t
val bot : unit -> t
val is_bot : t -> bool
val top : unit -> t
val is_top : t -> bool
val widen_with_fct : (value -> value -> value) -> t -> t -> t
val join_with_fct : (value -> value -> value) -> t -> t -> t
val leq_with_fct : (value -> value -> bool) -> t -> t -> bool
val choose' : t -> key * value
val choose : t -> SpecD.t
val filter' : (key -> value -> bool) -> t -> t
val filter : (key -> bool) -> t -> t
val iter' : (key -> value -> unit) -> t -> unit
val for_all' : (key -> value -> bool) -> t -> bool
val exists' : (key -> value -> bool) -> t -> bool
val exists : (key -> bool) -> t -> bool
val fold' : (key -> value -> 'a -> 'a) -> t -> 'a -> 'a
val fold : (key -> 'a -> 'a) -> t -> 'a -> 'a
val add : key -> R.t -> t -> t
val map : (key -> key) -> t -> t
val elements : t -> (key * R.t) list
val of_list : (key * R.t) list -> t
val union : t -> t -> t
val mem : SpecD.t -> R.t -> t -> bool
val leq : t -> t -> bool
val le : SpecD.t -> SpecD.t -> bool
val reduce : t -> t
val product_bot : (key -> key -> key) -> (R.t -> R.t -> R.t) -> t -> t -> t
val product_bot2 : ((key * R.t) -> (key * R.t) -> key * R.t) -> t -> t -> t
val product_widen : (key -> key -> key) -> (R.t -> R.t -> R.t) -> t -> t -> t
val product_widen2 : ((key * R.t) -> (key * R.t) -> key * R.t) -> t -> t -> t
val join : t -> t -> t
val meet : t -> t -> t
val narrow : t -> t -> t
val widen : t -> t -> t
val apply_list : ((key * R.t) list -> (key * R.t) list) -> t -> t
val pretty_diff : unit -> (t * t) -> Pretty.doc