Module InferModules__Absarray

Abstraction for Arrays

val abstract_array_check : InferIR.Tenv.t ‑> InferModules.Prop.normal InferModules.Prop.t ‑> InferModules.Prop.normal InferModules.Prop.t

Apply array abstraction and check the result

val array_abstraction_performed : bool InferStdlib.IStd.ref

Remember whether array abstraction was performed (to be reset before calling Abs.abstract)

val remove_redundant_elements : InferIR.Tenv.t ‑> InferModules.Prop.normal InferModules.Prop.t ‑> InferModules.Prop.normal InferModules.Prop.t

remove redundant elements in an array