Module Astral_internal.HeapSort

type t
include Datatype_sig.PRINTABLE with type t := t
include Datatype_sig.SHOW with type t := t
val show : t -> string

String representation of type t

val pp : Stdlib.Format.formatter -> t -> unit

Output to formatter

val print : ?prefix:string -> t -> unit

Output to stdout.

val show_option : t option -> string
val print_option : ?prefix:string -> t option -> unit
val dump : string -> t -> unit

Dump to file given by filename

Lists of printable values

val show_list : ?separator:string -> t list -> string
val pp_list : Stdlib.Format.formatter -> t list -> unit
val print_list : ?separator:string -> ?prefix:string -> t list -> unit
val empty : t

Create an empty heap sort.

val is_empty : t -> bool
val union : t list -> t
val restriction : Sort.t list -> t -> t
val of_list : (Sort.t * MemoryModel.StructDef.t) list -> t
val to_list : t -> (Sort.t * MemoryModel.StructDef.t) list
val find_target : Sort.t -> t -> MemoryModel.StructDef.t

Find target struct for a location sort.

val find_target_unwrapped : Sort.t -> t -> Sort.t

Find target sort for a classical sort wrapped into struct.

val is_loc_sort : t -> Sort.t -> bool
val get_loc_sorts : t -> Sort.t list
val get_structures : t -> MemoryModel.StructDef.t list
val get_fields : t -> MemoryModel.Field.t list

Get all fields in all target structures.

val to_smt2 : t -> string
val to_smt2_decl : t -> string
val is_bitvector_model : t -> bool

True iff the given heap sort represents mappings from bitvectors to bitvectors, i.e., corresponds to low-level memory model.