Module Engine.Preds

type t
val to_yojson : t -> Yojson.Safe.t
val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or
type abs_t = string * Gillian.Gil_syntax.Expr.t list
val length : t -> int
val init : abs_t list -> t
val to_list : t -> abs_t list
val copy : t -> t
val is_empty : t -> bool
val extend : ?pure:bool -> t -> abs_t -> unit
val pop : t -> (abs_t -> bool) -> abs_t option
val strategic_choice : consume:bool -> t -> (abs_t -> int) -> abs_t option

Given a strategy finds a predicate best matching it (int is non-null and highest possible). If consume is true, and the function returns Some _, the predicate is also removed from the preds.

val remove_by_name : t -> string -> abs_t option
val find_pabs_by_name : t -> string -> abs_t list
val get_lvars : t -> Utils.Prelude.SS.t
val get_alocs : t -> Utils.Prelude.SS.t
val pp : Stdlib.Format.formatter -> t -> unit
val pp_pabs : Stdlib.Format.formatter -> abs_t -> unit
val consume_pred : maintain:bool -> t -> string -> Gillian.Gil_syntax.Expr.t option list -> Utils.Containers.SI.t -> (Gillian.Gil_syntax.Expr.t -> Gillian.Gil_syntax.Expr.t -> bool) -> abs_t option

consume_pred ~maintain pred_state name args_opt ins f_eq removes the predicate best matching the triple (name, args_opt, ins) using an equality function on values f_eq. It does so in place, and if maintain is true, the predicate is matched but not actually removed from the state.

val find : t -> (abs_t -> bool) -> abs_t option
val get_all : maintain:bool -> (abs_t -> bool) -> t -> abs_t list
val substitution_in_place : Gillian.Symbolic.Subst.t -> t -> unit
val to_assertions : t -> Gillian.Gil_syntax.Asrt.t list

Turns a predicate set into a list of assertions