Module Astral_internal.BitvectorLocations

include Location_sig.LOCATIONS
include Location_sig.LOCATIONS_BASE
val name : string

Name of the encoding. Used only for debugging.

type internal
val init : SL.t -> HeapSort.t -> LocationBounds0.t -> t
val var_axiom : t -> SMT.Variable.t -> SMT.t
val heap_axioms : t -> SMT.t -> SMT.t
val lemmas : t -> SMT.t
val show : t -> string

Declaration

val mk_var : t -> string -> SMT.t

Create location variable.

val mk_fresh_var : t -> string -> SMT.t

Create fresh location variable.

val mk_set_var : t -> string -> SMT.t

Create location set variable.

val mk_fresh_set_var : t -> string -> SMT.t

Create fresh location set variable.

Accessors

val null : t -> SMT.t

Translation

val translate_var : t -> SL.Variable.t -> SMT.Variable.t
val translate_smt_term : t -> SMT.t -> SMT.t
val inverse_translate : t -> SMT.Model.t -> Constant.t -> StackHeapModel.Location.t

Translate an interpretation of a location to its representation in stack-heap model.

Typing

val mk_of_type : t -> SMT.t -> Sort.t -> SMT.t
val mk_set_of_type : t -> SMT.t -> Sort.t -> SMT.t

Quantifiers

val mk_exists : t -> (SMT.t -> SMT.t) -> SMT.t
val mk_forall : t -> (SMT.t -> SMT.t) -> SMT.t
val mk_exists' : t -> int -> (SMT.t list -> SMT.t) -> SMT.t
val mk_forall' : t -> int -> (SMT.t list -> SMT.t) -> SMT.t

Axioms

val axioms : t -> SL.t -> (SL.Term.t -> SMT.t) -> SMT.t
val set_sort : t -> Sort.t

Sort of location sets.

val powerset : t -> SMT.t list list