External.ESubst
type vt = Val.t
type t = Val.et
val to_yojson : t -> Yojson.Safe.t
val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or
val init : (Gillian.Gil_syntax.Expr.t * vt) list -> t
val of_seq : (Gillian.Gil_syntax.Expr.t * vt) Stdlib.Seq.t -> t
val is_empty : t -> bool
val clear : t -> unit
val domain :
t ->
(Gillian.Gil_syntax.Expr.t -> bool) option ->
Gil_syntax.Expr.Set.t
val get : t -> Gillian.Gil_syntax.Expr.t -> vt option
val add : t -> Gillian.Gil_syntax.Expr.t -> vt -> unit
val put : t -> Gillian.Gil_syntax.Expr.t -> vt -> unit
val mem : t -> Gillian.Gil_syntax.Expr.t -> bool
val extend : t -> (Gillian.Gil_syntax.Expr.t * vt) list -> unit
val filter : t -> (Gillian.Gil_syntax.Expr.t -> vt -> bool) -> t
val iter : t -> (Gillian.Gil_syntax.Expr.t -> vt -> unit) -> unit
val fold : t -> (Gillian.Gil_syntax.Expr.t -> vt -> 'a -> 'a) -> 'a -> 'a
val pp : Stdlib.Format.formatter -> t -> unit
val full_pp : Stdlib.Format.formatter -> t -> unit
val pp_by_need : Utils.Containers.SS.t -> Stdlib.Format.formatter -> t -> unit
val filter_in_place :
t ->
(Gillian.Gil_syntax.Expr.t -> vt -> vt option) ->
unit
val to_list : t -> (Gillian.Gil_syntax.Expr.t * vt) list
val to_list_pp : t -> (string * string) list
val subst_in_expr :
t ->
partial:bool ->
Gillian.Gil_syntax.Expr.t ->
Gillian.Gil_syntax.Expr.t
val subst_in_expr_opt :
t ->
Gillian.Gil_syntax.Expr.t ->
Gillian.Gil_syntax.Expr.t option
val substitute_formula :
t ->
partial:bool ->
Gillian.Gil_syntax.Formula.t ->
Gillian.Gil_syntax.Formula.t
val substitute_in_formula_opt :
t ->
Gillian.Gil_syntax.Formula.t ->
Gillian.Gil_syntax.Formula.t option
val substitute_asrt :
t ->
partial:bool ->
Gillian.Gil_syntax.Asrt.t ->
Gillian.Gil_syntax.Asrt.t
val substitute_slcmd :
t ->
partial:bool ->
Gillian.Gil_syntax.SLCmd.t ->
Gillian.Gil_syntax.SLCmd.t
val substitute_lcmd :
t ->
partial:bool ->
Gillian.Gil_syntax.LCmd.t ->
Gillian.Gil_syntax.LCmd.t