Module StackHeapModel.Stack

type t
module M : Datatype_sig.MONO_MAP with type key := SL.Term.t and type data := Location.t

Stack is represented as a mapping from relevant terms to locations.

val empty : t
val mk : SMT.Model.t -> M.t -> t
val add : SL.Term.t -> Location.t -> t -> t
val eval : t -> SL.Term.t -> Location.t
val to_smtlib : t -> string