Store (gillian.Bulk.Outcome.S.Store)

type vt = Val.t

Type of GIL values

type t

Type of GIL stores

val to_yojson : t -> Yojson.Safe.t

val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or

val bindings : t -> (Gillian.Gil_syntax.Var.t * vt) list

Return the set of bindings in a given store

val copy : t -> t

Store copy

val domain : t -> Gillian.Gil_syntax.Var.Set.t

Store domain

val filter_map_inplace : 
  t ->
  (Gillian.Gil_syntax.Var.t -> vt -> vt option) ->
  unit

Store filtering

val fold : t -> (Gillian.Gil_syntax.Var.t -> vt -> 'a -> 'a) -> 'a -> 'a

Store fold

val get : t -> Gillian.Gil_syntax.Var.t -> vt option

Return value of a given variable, if possible

val get_unsafe : t -> Gillian.Gil_syntax.Var.t -> vt

Return value of a given variable or throw

val init : (Gillian.Gil_syntax.Var.t * vt) list -> t

Store constructor, with a list of bindings of the form (variable, value)

val iter : t -> (Gillian.Gil_syntax.Var.t -> vt -> unit) -> unit

Store iterator

val mem : t -> Gillian.Gil_syntax.Var.t -> bool

Store membership

val partition : 
  t ->
  (vt -> bool) ->
  Gillian.Gil_syntax.Var.Set.t * Gillian.Gil_syntax.Var.Set.t

Partition store domain

val projection : t -> Gillian.Gil_syntax.Var.t list -> t

Store projection (returns new store)

val put : t -> Gillian.Gil_syntax.Var.t -> vt -> unit

Update value of variable in store

val remove : t -> Gillian.Gil_syntax.Var.t -> unit

Remove value of variable in store

val pp : Stdlib.Format.formatter -> t -> unit

Store printer

val pp_by_need : Utils.Containers.SS.t -> Stdlib.Format.formatter -> t -> unit

Store printer by need

val to_ssubst : t -> Gillian.Symbolic.Subst.t

Converts the store into an ssubst

val lvars : t -> Gillian.Gil_syntax.Var.Set.t

Logical variables