Module State_imp

module State_imp: sig .. end

Sets of Cvalue.Model.t implemented imperatively. Current implementation is optimized to detect similarities in the memory states

module Sindexed: Hashtbl.Make(sig
type t = Cvalue.Model.subtree 


val hash : Cvalue.Model.subtree -> int
val equal : Cvalue.Model.subtree -> Cvalue.Model.subtree -> bool
end)

val sentinel : Cvalue.Model.t Sindexed.t

type t = {

	`mutable t : Cvalue.Model.t Sindexed.t;`
	`mutable p : Hptmap.prefix;`
	`mutable o : Cvalue.Model.t list;`

}

val fold : (Cvalue.Model.t -> 'a -> 'a) -> t -> 'a -> 'a

Iterators

val iter : (Cvalue.Model.t -> unit) -> t -> unit

exception Found

val empty : unit -> t

Creation

val is_empty : t -> bool

Information

val exists : (Cvalue.Model.t -> bool) -> t -> bool

val length : t -> int

exception Unchanged

Adding elements.

The three next functions raise Unchanged if the element(s) was already present.

val pretty : Format.formatter -> t -> unit

val add_to_list : Cvalue.Model.t -> Cvalue.Model.t list -> Cvalue.Model.t list

val add_exn : Cvalue.Model.t -> t -> unit

val merge_set_return_new : State_set.t -> t -> State_set.t

val add : Cvalue.Model.t -> t -> unit

val singleton : Cvalue.Model.t -> t

val join : t -> Cvalue.Model.t

Export

val fold : (Cvalue.Model.t -> 'a -> 'a) -> t -> 'a -> 'a

Iterators

val to_list : t -> Cvalue.Model.t list

val to_set : t -> State_set.t