Module MemoryModel.StructDef

type t = private {
  1. name : Identifier.t;
  2. cons : Identifier.t;
  3. fields : Field.t list;
}
val mk : string -> ?cons:string -> Field.t list -> t

mk struct_name constructor_name fields creates a structure consisting of given fields. Constructor name is used only for pretty-printing of pointer assertions and, by default, is the same as structure name.

val mk_tuple : int -> t

mk_tuple n creates a structure consisting of fields f_1, f_2, ..., f_n; each of them of sort "tuple_n".

For internal usage only.

val lift_sort : Sort.t -> t

Creates a structure consisting of single "next" field of provided sort.

For internal usage only.

val ls : t
val get_name : t -> string
val get_constructor : t -> string
val get_fields : t -> Field.t list
val signature : t -> Sort.t list

Get list of sorts of all fields in the structure.

val get_sorts : t -> Sort.t list

Same as signature, but removes duplicates.

val field_index : t -> Field.t -> int

Return index of the field in the structure.

val field_value : t -> Field.t -> 'a list -> 'a
val find_field : (Field.t -> bool) -> t -> Field.t
val smt2_decl : t -> string
val smt2_decl_group : t list -> string
val show_cons : t -> string
include Datatype_sig.PRINTABLE with type t := t
include Datatype_sig.SHOW with type t := 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
include Datatype_sig.COMPARABLE with type t := t
include Datatype_sig.COMPARISON with type t := t
val show : t -> string
val compare : t -> t -> int
val equal : t -> t -> bool
include Datatype_sig.COLLECTIONS with type t := t
module Set : Datatype_sig.SET with type elt = t

Set over type t

module MonoList : Datatype_sig.MONO_LIST with type key = t and type t = t list

Monomorphic list over type t

module Map : Datatype_sig.MAP with type key = t

Polymorphic map from t to 'a

module MonoMap (Data : Datatype_sig.SHOW) : Datatype_sig.MONO_MAP with type key = t and type data = Data.t

Monomorphic map from t to Data.t