Module Jsil_syntax.Pred

module SSubst = Gillian.Symbolic.Subst
module L = Logging
type t = {
  1. name : string;
    (*

    Name of the predicate

    *)
  2. num_params : int;
    (*

    Number of parameters

    *)
  3. params : (string * Type.t option) list;
    (*

    Actual parameters

    *)
  4. ins : int list;
    (*

    Ins

    *)
  5. definitions : ((string * string list) option * Asrt.t) list;
    (*

    Predicate definitions

    *)
  6. facts : Expr.t list;
    (*

    Facts about the predicate

    *)
  7. pure : bool;
    (*

    Is the predicate pure

    *)
  8. abstract : bool;
    (*

    Is the predicate abstract

    *)
  9. nounfold : bool;
    (*

    Should the predicate be unfolded?

    *)
  10. normalised : bool;
    (*

    If the predicate has been previously normalised

    *)
}

JSIL logic predicate.

val init : t list -> (string, t) Stdlib.Hashtbl.t

Creates/populates a Hashtbl from the predicate list pred_defs

val pp : Stdlib.Format.formatter -> t -> unit
val empty_pred_tbl : unit -> ('a, 'b) Stdlib.Hashtbl.t