Module Encoding.HeapEncoding

module Locations = Locations

The encoding of locations.

val name : string
type t

Type of encoded heap.

val show : t -> string
val mk : ?suffix:string -> SL.t -> HeapSort.t -> Locations.t -> t
val get_fields : t -> MemoryModel.Field.t list
val inverse_translate : t -> SMT.Model.t -> (SMT.t * StackHeapModel.Location.t) list -> StackHeapModel.Heap.t

inverse_translate t model domain

val axioms : t -> SMT.t
val field_encoding : t -> MemoryModel.Field.t -> SMT.t

Auxiliary function

val mk_succ : t -> MemoryModel.Field.t -> SMT.t -> SMT.t

Create a term representing a successor over the given field.

val mk_image : t -> SMT.t -> SMT.t

Term representing image of heap over given domain.

val mk_locs : t -> SMT.t -> SMT.t

Term representing all locations of heap.

val mk_eq_on_domain : t -> t -> SMT.t -> SMT.t

Term representing equality of two heaps on the given domain.

val mk_strongly_disjoint : t -> SMT.t list -> SMT.t list -> SMT.t