Module SmallModels.Derivation

module HS : sig ... end
module GS : sig ... end
type t = {
  1. id : InductiveDefinition.t;
  2. stable : int option;
  3. graphs : GS.t;
    (*

    Derived graphs

    *)
  4. worklist : HS.t;
    (*

    Worklist of hypergraphs to be unfolded

    *)
  5. finished : HS.t;
    (*

    Set of already (fully) unfolded hypergraphs

    *)
}
val empty : InductiveDefinition.t -> t
val add_to_worklist : t -> HS.elt -> t
val leafs : t -> GS.elt list
val worklist : t -> HS.elt list
val unfold_step : ?base_only:bool -> int -> t -> t

Single step of unfolding:

val close : t -> t
val unfold : int -> t -> t
val initial : InductiveDefinition.t -> t
val get_pure : t -> SL_graph.Set.t
val is_stable : t -> t -> bool
val negated : SL.t -> InductiveDefinition.t -> SL.t list
val is_fixpoint : 'a -> SID_checks.distinguisher SID_checks.M.t -> SL.t -> t -> bool
val size : t -> Stdlib.Float.t

TODO: Is root a variable allocated in all models?

val find_allocated : InductiveDefinition.t -> SL_graph.G.t list -> SL.Variable.t list
val find_never_allocated : InductiveDefinition.t -> Astral_internal.SL_graph.G.t list -> SL.Variable.t list
val compute_skeleton_fields : SL_graph.G.t list -> MemoryModel.Field.t list
val abstraction : InductiveDefinition.t -> t -> Abstraction.t
val cardinal : t -> int
val show : ?indent:int -> t -> unit
val debug : 'a -> 'b -> unit