gillian » Gillian » Symbolic » Pure_context

Module Symbolic.Pure_context

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.Expr.t list

to_list pfs serialises the pure formulae pfs into a list

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

of_list fs deserialises a list of formulae fs into pure formulae

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

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

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

val extend : t -> Gil_syntax.Expr.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.Expr.t list -> unit

set pfs fs sets the pure formulae pfs to fs

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

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

val fold_left : ('a -> Gil_syntax.Expr.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.Expr.t -> Gil_syntax.Expr.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

val filter_with_info :
  (Utils.Containers.SS.t * Utils.Containers.SS.t * Utils.Containers.SS.t) ->
  t ->
  t

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 get_relevant_info :
  Utils.Containers.SS.t ->
  Utils.Containers.SS.t ->
  Utils.Containers.SS.t ->
  t ->
  Utils.Containers.SS.t * Utils.Containers.SS.t * Utils.Containers.SS.t

val filter_map_stop :
  (Gil_syntax.Expr.t -> [ `Stop | `Filter | `Replace of Gil_syntax.Expr.t ]) ->
  t ->
  bool

val filter_stop_cond :
  keep:(Gil_syntax.Expr.t -> bool) ->
  cond:(Gil_syntax.Expr.t -> bool) ->
  t ->
  bool

See Gillian.Utils.Ext_list.filter_stop_cond

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

val filter_map : (Gil_syntax.Expr.t -> Gil_syntax.Expr.t option) -> t -> unit

val exists : (Gil_syntax.Expr.t -> bool) -> t -> bool

val get_nth : int -> t -> Gil_syntax.Expr.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)