SStore (gillian.Engine.SStore)

type vt = Gillian.Gil_syntax.Expr.t

type t

val to_yojson : t -> Yojson.Safe.t

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

val copy : t -> t

val domain : t -> Utils.Containers.SS.t

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

val assertions : t -> Gillian.Gil_syntax.Formula.t list

val substitution_in_place : 
  ?subst_all:bool ->
  Gillian.Symbolic.Subst.t ->
  t ->
  unit

val is_well_formed : t -> bool

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

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