sig
type t
val pretty : Format.formatter -> State_set.t -> unit
val empty : State_set.t
val singleton : Cvalue.Model.t * Trace.t -> State_set.t
val of_list : (Cvalue.Model.t * Trace.t) list -> State_set.t
val of_list_forget_history : Cvalue.Model.t list -> State_set.t
val is_empty : State_set.t -> bool
val length : State_set.t -> int
val add : Cvalue.Model.t * Trace.t -> State_set.t -> State_set.t
exception Unchanged
val merge_into : State_set.t -> into:State_set.t -> State_set.t
val merge : State_set.t -> State_set.t -> State_set.t
val add_statement : State_set.t -> Cil_types.stmt -> State_set.t
val fold :
('a -> Cvalue.Model.t * Trace.t -> 'a) -> 'a -> State_set.t -> 'a
val iter : (Cvalue.Model.t * Trace.t -> unit) -> State_set.t -> unit
val exists : (Cvalue.Model.t -> bool) -> State_set.t -> bool
val map :
(Cvalue.Model.t * Trace.t -> Cvalue.Model.t * Trace.t) ->
State_set.t -> State_set.t
val reorder : State_set.t -> State_set.t
val join : State_set.t -> Cvalue.Model.t * Trace.t
val narrow : State_set.t -> State_set.t -> State_set.t
val narrow_list : State_set.t list -> State_set.t
val to_list : State_set.t -> Cvalue.Model.t list
end