Module Z3.Sort

module Sort: sig .. end

The Sort module implements type information for ASTs

type sort

val equal : sort -> sort -> bool

Comparison operator.

Returns True if the two sorts are from the same context and represent the same sort; false otherwise.

val get_id : sort -> int

Returns a unique identifier for the sort.

val get_sort_kind : sort -> Z3enums.sort_kind

The kind of the sort.

val get_name : sort -> Symbol.symbol

The name of the sort

val to_string : sort -> string

A string representation of the sort.

val mk_uninterpreted : context -> Symbol.symbol -> sort

Create a new uninterpreted sort.

val mk_uninterpreted_s : context -> string -> sort

Create a new uninterpreted sort.