Module SVal.SSubst

Type of GIL values

type t

Type of GIL substitutions

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

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

val is_empty : t -> bool

Is the substitution empty?

val clear : t -> unit

Reset substitution

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

Domain of the substitution

val range : t -> vt list

Range of the substitution

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

Substitution lookup

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

Substitution incremental update

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

Substitution update

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

Substitution membership

val copy : t -> t

Substitution copy

val extend : t -> (Gillian.Gil_syntax.Var.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.Var.t -> vt -> bool) -> t

Substitution filter

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

Substitution variable filter

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

Substitution iterator

val fold : t -> (Gillian.Gil_syntax.Var.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 filter_in_place : t -> (Gillian.Gil_syntax.Var.t -> vt -> vt option) -> unit
val to_list : t -> (Gillian.Gil_syntax.Var.t * vt) list

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