Module Astral_internal.PredicateAbstraction

type t = {
  1. id : InductiveDefinition.t;
  2. root : SL.Variable.t;
  3. allocated : SL.Variable.t list;
    (*

    Variables allocated in all non-empty models

    *)
  4. never_allocated : SL.Variable.t list;
  5. skeleton_fields : MemoryModel.Field.t list;
  6. stable_size : int;
  7. fixpoint_size : float;
  8. unfolding_depth : int;
}
val show : t -> string
val get_root : ?params:SL.Term.t list -> t -> SL.Term.t

Return the root of the inductive definition. If params is not provided, result corresponds to the formal variables.

val get_holes : ?params:SL.Term.t list -> t -> SL.Term.t list
val get_must_allocated : ?params:SL.Term.t list -> t -> SL.Term.t list
val get_may_dangling : ?params:SL.Term.t list -> t -> SL.Term.t list
val may_allocated : ?params:SL.Term.t list -> t -> SL.Term.t list
module M : Datatype_sig.MONO_MAP with type key := InductiveDefinition.t and type data := t