Module Astral_internal.PreciseToImprecise

val is_imprecise_sh : SL.t -> bool
val as_imprecise_sh : SL.t -> SL.Variable.t list * SL.t list * SL.t list
val as_imprecise_query : SL.t -> SL.query
val to_precise : SL.t -> SL.t

Converts input in precise semantics to equivalent formula in imprecise semantics.

If input represents satisfiability/entailment of symbolic heaps, then result do as well.

val to_imprecise : SL.t -> SL.t

Converts input in imprecise semantics to equivalent formula in precise semantics.

If input represents satisfiability/entailment of symbolic heaps, then result do as well.