Module Astral_internal.Sort

type t =
  1. | Bool
  2. | Int
  3. | Finite of Identifier.t * string list
  4. | Set of t
  5. | Sequence of t
  6. | Array of t * t
  7. | Bitvector of int
  8. | Tupple of t list
  9. | Sum of t list
  10. | Uninterpreted of Identifier.t
  11. | Loc of Identifier.t * Identifier.t list
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

val equal_mod_nil : t -> t -> bool

Equality modulo nil sort: each location sort is equal to the nil sort.

val is_builtin : t -> bool
val name : t -> string
val all_names : t -> string list

In case of location sort, return its name and all defined aliases. For other sorts, return a singleton list with a name.

val cardinality : t -> int option

For finite sorts, return their cardinality

Built-in locations sorts

val loc_ls : t
val loc_nil : t

Constructors

val int : t
val bool : t
val mk_finite : string -> string list -> t
val mk_loc : ?aliases:string list -> string -> t
val mk_set : t -> t
val mk_uninterpreted : string -> t
val mk_array : t -> t -> t
val mk_bitvector : int -> t
val mk_sum : t list -> t

Predicates

val is_bool : t -> bool
val is_loc : t -> bool
val is_set : t -> bool
val is_array : t -> bool
val is_bitvector : t -> bool
val is_nil : t -> bool
val get_dom_sort : t -> t

Get domain sort of either set, sequence or array sort.

val get_range_sort : t -> t

Get range sort of an array sort.

val get_width : t -> int

Get width of a bitvector sort.

val get_constant_names : t -> string list

Get names of constants of a finite sort.

val is_atomic : t -> bool

Atomic sorts are Bool, Int, Finite, Bitvector and Loc.

val show_kind : t -> string

Operations

val substitute : t -> t -> t -> t

substitute sort pattern target replaces all occurences of sort pattern by atomic sort target.

SMTLIB

val smt2_name : t -> string
val smt2_decl : t -> string