Module Symbolic.Pure_context

GIL pure formulae

type t
val to_yojson : t -> Yojson.Safe.t
val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or
val init : unit -> t

init () returns a fresh empty collection of pure formulae

val equal : t -> t -> bool

equal pfs_a pfs_b returns true iff pfs_a = pfs_b

val to_list : t -> Gil_syntax.Formula.t list

to_list pfs serialises the pure formulae pfs into a list

val of_list : Gil_syntax.Formula.t list -> t

of_list fs deserialises a list of formulae fs into pure formulae

val to_set : t -> Gil_syntax.Formula.Set.t
val mem : t -> Gil_syntax.Formula.t -> bool

mem pfs f return true iff the formula f is part of the pure formulae pfs

val extend : t -> Gil_syntax.Formula.t -> unit

extend pfs f extends the pure formulae pfs with the formula f

val clear : t -> unit

clear pfs empties the pure formulae pfs

val length : t -> int

length pfs returns the length of the pure formulae pfs

val copy : t -> t

copy pfs Returns a copy of the pure formulae pfs

val merge_into_left : t -> t -> unit

merge_into_left pfsl pfsr merges the pure formulae pfsr with the pure formulae pfsl

val set : t -> Gil_syntax.Formula.t list -> unit

set pfs fs sets the pure formulae pfs to fs

val iter : (Gil_syntax.Formula.t -> unit) -> t -> unit

iter f pfs iterates over the pure formulae pfs using the function f

val fold_left : ('a -> Gil_syntax.Formula.t -> 'a) -> 'a -> t -> 'a

fold_left f ac pfs folds over the pure formulae pfs using the function f and initial accumulator ac

val map_inplace : (Gil_syntax.Formula.t -> Gil_syntax.Formula.t) -> t -> unit

map_inplace f pfs is like a map operation, but performing in place

val substitution : Symbolic.Subst.t -> t -> unit

substitution subst pfs substitutes the substutition subst in the pure formulae pfs in-place

val subst_expr_for_expr : Gil_syntax.Expr.t -> Gil_syntax.Expr.t -> t -> unit

subst_expr_for_expr e_to_subst e_subst pfs substitutes the expression e_to_subst with the expression e_subst in the pure formulae pfs in-place

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

lvars pfs returns the set containing all the lvars occurring in pfs

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

Returns the set containing all the alocs occurring in --pfs--

alocs pfs returns the set containing all the abstract locations occurring in pfs

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

clocs pfs returns the set containing all the concrete locations occurring in pfs

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

pp fmt pfs prints the pure formulae pfs

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

pp pvars lvars locs fmt pfs prints the pure formulae pfs relevnt to pvars, lvars and locs

filter_with_info pvars lvars locs pfs returns only the pfs relevant to pvars, lvars, and locs

val sort : t -> unit

sort pfs sorts the pure formulae pfs

val remove_duplicates : t -> unit
val clean_up : t -> unit
val filter_map_stop : (Gil_syntax.Formula.t -> [ `Stop | `Filter | `Replace of Gil_syntax.Formula.t ]) -> t -> bool
val filter_stop_cond : keep:(Gil_syntax.Formula.t -> bool) -> cond:(Gil_syntax.Formula.t -> bool) -> t -> bool

See Gillian.Utils.Ext_list.filter_stop_cond

val filter : (Gil_syntax.Formula.t -> bool) -> t -> unit
val filter_map : (Gil_syntax.Formula.t -> Gil_syntax.Formula.t option) -> t -> unit
val exists : (Gil_syntax.Formula.t -> bool) -> t -> bool
val get_nth : int -> t -> Gil_syntax.Formula.t option

Gets the nths formula. There are very few good use cases for this function, and uses should generaly use iterators instead. O(n)