sig
module type StateSet =
sig
type state
type t
val empty : Partitioning.StateSet.t
val is_empty : Partitioning.StateSet.t -> bool
val singleton : Partitioning.StateSet.state -> Partitioning.StateSet.t
val singleton' :
Partitioning.StateSet.state Eval.or_bottom -> Partitioning.StateSet.t
val uncheck_add :
Partitioning.StateSet.state ->
Partitioning.StateSet.t -> Partitioning.StateSet.t
val add :
Partitioning.StateSet.state ->
Partitioning.StateSet.t -> Partitioning.StateSet.t
val add' :
Partitioning.StateSet.state Eval.or_bottom ->
Partitioning.StateSet.t -> Partitioning.StateSet.t
val length : Partitioning.StateSet.t -> int
val merge :
into:Partitioning.StateSet.t ->
Partitioning.StateSet.t -> Partitioning.StateSet.t * bool
val join :
?into:Partitioning.StateSet.state Eval.or_bottom ->
Partitioning.StateSet.t -> Partitioning.StateSet.state Eval.or_bottom
val fold :
(Partitioning.StateSet.state -> 'a -> 'a) ->
Partitioning.StateSet.t -> 'a -> 'a
val iter :
(Partitioning.StateSet.state -> unit) ->
Partitioning.StateSet.t -> unit
val map :
(Partitioning.StateSet.state -> Partitioning.StateSet.state) ->
Partitioning.StateSet.t -> Partitioning.StateSet.t
val reorder : Partitioning.StateSet.t -> Partitioning.StateSet.t
val of_list :
Partitioning.StateSet.state list -> Partitioning.StateSet.t
val to_list :
Partitioning.StateSet.t -> Partitioning.StateSet.state list
val pretty : Format.formatter -> Partitioning.StateSet.t -> unit
end
module Make_Set :
functor (Domain : Abstract_domain.S) ->
sig
type state = Domain.t
type t
val empty : t
val is_empty : t -> bool
val singleton : state -> t
val singleton' : state Eval.or_bottom -> t
val uncheck_add : state -> t -> t
val add : state -> t -> t
val add' : state Eval.or_bottom -> t -> t
val length : t -> int
val merge : into:t -> t -> t * bool
val join : ?into:state Eval.or_bottom -> t -> state Eval.or_bottom
val fold : (state -> 'a -> 'a) -> t -> 'a -> 'a
val iter : (state -> unit) -> t -> unit
val map : (state -> state) -> t -> t
val reorder : t -> t
val of_list : state list -> t
val to_list : t -> state list
val pretty : Format.formatter -> t -> unit
end
module type Partition =
sig
type state
type state_set
type t
val empty : unit -> Partitioning.Partition.t
val fold :
(Partitioning.Partition.state -> 'a -> 'a) ->
Partitioning.Partition.t -> 'a -> 'a
val merge_set_return_new :
Partitioning.Partition.state_set ->
Partitioning.Partition.t -> Partitioning.Partition.state_set
val join :
Partitioning.Partition.t ->
Partitioning.Partition.state Eval.or_bottom
val to_set :
Partitioning.Partition.t -> Partitioning.Partition.state_set
val to_list :
Partitioning.Partition.t -> Partitioning.Partition.state list
val pretty : Format.formatter -> Partitioning.Partition.t -> unit
end
module Make_Partition :
functor
(Domain : Abstract_domain.External) (States : sig
type state = Domain.t
type t
val empty : t
val is_empty :
t -> bool
val singleton :
state -> t
val singleton' :
state Eval.or_bottom ->
t
val uncheck_add :
state -> t -> t
val add :
state -> t -> t
val add' :
state Eval.or_bottom ->
t -> t
val length : t -> int
val merge :
into:t ->
t -> t * bool
val join :
?into:state
Eval.or_bottom ->
t ->
state Eval.or_bottom
val fold :
(state -> 'a -> 'a) ->
t -> 'a -> 'a
val iter :
(state -> unit) ->
t -> unit
val map :
(state -> state) ->
t -> t
val reorder : t -> t
val of_list :
state list -> t
val to_list :
t -> state list
val pretty :
Format.formatter ->
t -> unit
end) ->
sig
type state = Domain.t
type state_set = States.t
type t
val empty : unit -> t
val fold : (state -> 'a -> 'a) -> t -> 'a -> 'a
val merge_set_return_new : state_set -> t -> state_set
val join : t -> state Eval.or_bottom
val to_set : t -> state_set
val to_list : t -> state list
val pretty : Format.formatter -> t -> unit
end
end