Module S.ESubst

type vt = Val.t

Type of GIL values

type t = Val.et

Type of GIL e-substitutions

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

E-substitution constructor, with a list of bindings of the form (variable, value)

val of_seq : (Gillian.Gil_syntax.Expr.t * vt) Stdlib.Seq.t -> t
val is_empty : t -> bool

Is the e-substitution empty?

val clear : t -> unit

Reset e-substitution

val domain : t -> (Gillian.Gil_syntax.Expr.t -> bool) option -> Gil_syntax.Expr.Set.t

Domain of the e-substitution

val range : t -> vt list

Range of the e-substitution

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

Substitution lookup

val add : t -> Gillian.Gil_syntax.Expr.t -> vt -> unit

Substitution incremental update

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

Substitution update

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

Substitution membership

val copy : t -> t

Substitution copy

val extend : t -> (Gillian.Gil_syntax.Expr.t * vt) list -> unit

Substitution extension with a list of bindings

val merge_left : t -> t -> unit

Substution merge into left

val filter : t -> (Gillian.Gil_syntax.Expr.t -> vt -> bool) -> t

Substitution filter

val projection : t -> Gil_syntax.Expr.Set.t -> t

Substitution variable filter

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

Substitution iterator

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

Substitution fold

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

Pretty Printer

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

Full pretty Printer

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

Selective Pretty Printer

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

Convert substitution to 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

Substitution inside a logical expression

val subst_in_expr_opt : t -> Gillian.Gil_syntax.Expr.t -> Gillian.Gil_syntax.Expr.t option

Optional substitution inside a logical expression

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