Module Astral_internal.GlobalSID

val sid_original : SID.t Stdlib.ref
val sid_updated : SID.t Stdlib.ref
val cache : PredicateAbstraction.M.t Stdlib.ref
val show : unit -> string
val reset : unit -> unit
val reset_results : unit -> unit
val compute_graph : unit -> unit
val select : bool -> SID.t
val register_builtin : (module ID_sig.BUILTIN) -> unit
val register_user_defined : InductiveDefinition.t -> unit
val update_user_defined : InductiveDefinition.t -> unit
val is_builtin : string -> bool
val is_user_defined : string -> bool
val find : ?original:bool -> string -> SID.ID.t
val find_user_defined : ?original:bool -> string -> InductiveDefinition.t
val fold_user_defined : ?original:bool -> (InductiveDefinition.t -> 'a -> 'a) -> 'a -> 'a
val get_user_defined : ?original:bool -> unit -> InductiveDefinition.t list
val is_self_recursive : string -> bool
val dependencies : ?original:bool -> string -> InductiveDefinition.t list
val dependency_graph : unit -> DependencyGraph.t
val get : unit -> SID.t
val get_signatures : unit -> (string * Astral_internal.SL.Variable.Sort.t list) list
val unfold : string -> SL.Term.t list -> int -> SL.t

==== Context ====

module S : sig ... end
module M : sig ... end
val builtin_sorts : MemoryModel.StructDef.t M.t -> Sort.t M.t
val builtin_structs : unit -> MemoryModel.StructDef.t M.t
val builtin_heap_sort : unit -> HeapSort.t
val builtin_ids : unit -> S.t
val builtin_context : unit -> ParserContext.t

==== Preprocessing ====

val preprocess_user_definitions : (InductiveDefinition.t -> InductiveDefinition.t option) -> unit

Apply the function to each inductive definition

==== Syntactic queries ====

val get_structs : Stdlib.String.t list -> (Stdlib.String.t list -> SL.t -> MemoryModel.StructDef.t list) -> Stdlib.String.t -> MemoryModel.StructDef.t list

==== Semantics queries ====

val has_unique_footprint : string -> bool

==== BUILTINS: General ====

val instantiate : HeapSort.t -> string -> SL.Term.t list -> (SL.t, string) Stdlib.Result.t

==== BUILTINS: Model checking ====

val model_check : string -> (SL.Term.t list * MemoryModel.StructDef.t list) -> StackHeapModel.t -> bool
val compute_footprints : string -> (SL.Term.t list * MemoryModel.StructDef.t list) -> StackHeapModel.t -> StackHeapModel.Footprint.t

==== BUILTINS: Translation ====

module Translation (E : Translation_sig.ENCODING) : sig ... end

==== Abstraction of predicates ====

val is_computed : unit -> bool
val abstraction : string -> Astral_internal__PredicateAbstraction.t
val get_must_allocated : params:SL.Term.t list -> string -> SL.Term.t list
val get_may_dangling : params:SL.Term.t list -> string -> SL.Term.t list
val existentials : ?visited:InductiveDefinition.t list -> InductiveDefinition.t -> SL.Variable.t list

==== Location bound computation ====

val term_bound : SL.t -> SL_graph0.G.t -> HeapSort.t -> SL.Term.t -> float
val alloc : string -> SL.t -> SL_graph0.G.t -> HeapSort.t -> SL.Term.t list -> float
val additional_bounds : SL.t -> LocationBounds0.t
val sl_graph : string -> (SL.Term.t list * MemoryModel.StructDef.t list) -> SL_graph0.t

TODO: compute some must-relations

val unfolding_depth : 'a -> 'b -> string -> 'c -> int
val formula_preprocessing : SL.t -> SL.t
val formula_preprocessing_ctx : Context.t -> Context.t