Module Astral_internal.UnfoldIDs

val must_allocate_lhs : SL.t -> HeapSort.t -> SL.t -> SL_graph0.G.t -> 'a -> int
val max_unfold_bound_lhs : 'a -> 'b -> 'b

Bound on unfolding of lhs when rhs is atomic.

val max_unfold_bound_rhs : 'a -> 'b -> 'b

Bound on unfolding of rhs when lhs is atomic.

val unfold_predicate_lhs : SID.t -> 'a -> 'b -> int -> string -> SL.Term.t list -> SL.t
val unfold_lhs : SID.t -> SL_graph0.G.t -> HeapSort.t -> LocationBounds.t -> SL.t -> SL.t -> 'a -> SL.t
val unfold_sat : SID.t -> SL.t -> SL.t
val unfold_rhs : 'a -> Context.t -> SL.t -> SL.t -> SL.t
val unfold_default : Context.t -> SL.t -> Context.t
val apply : ?bound_map:'a -> Context.t -> SL.t -> Context.t
val apply_ctx : ?bound_map:'a -> Context.t -> Context.t