ESubstP (gillian.Bulk.Outcome.Make.ESubstP)

type vt = ValP.t

Type of GIL values

type t = ValP.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