#[repr(u32)]pub enum SortKind {
Show 16 variants
Uninterpreted = 0,
Bool = 1,
Int = 2,
Real = 3,
Bv = 4,
Array = 5,
Datatype = 6,
Relation = 7,
FiniteDomain = 8,
FloatingPoint = 9,
RoundingMode = 10,
Seq = 11,
Re = 12,
Char = 13,
TypeVar = 14,
Unknown = 1_000,
}Expand description
The different kinds of Z3 types (See Z3_get_sort_kind).
Variants§
Uninterpreted = 0
Corresponds to Z3_UNINTERPRETED_SORT in the C API.
Bool = 1
Corresponds to Z3_BOOL_SORT in the C API.
Int = 2
Corresponds to Z3_INT_SORT in the C API.
Real = 3
Corresponds to Z3_REAL_SORT in the C API.
Bv = 4
Corresponds to Z3_BV_SORT in the C API.
Array = 5
Corresponds to Z3_ARRAY_SORT in the C API.
Datatype = 6
Corresponds to Z3_DATATYPE_SORT in the C API.
Relation = 7
Corresponds to Z3_RELATION_SORT in the C API.
FiniteDomain = 8
Corresponds to Z3_FINITE_DOMAIN_SORT in the C API.
FloatingPoint = 9
Corresponds to Z3_FLOATING_POINT_SORT in the C API.
RoundingMode = 10
Corresponds to Z3_ROUNDING_MODE_SORT in the C API.
Seq = 11
Corresponds to Z3_SEQ_SORT in the C API.
Re = 12
Corresponds to Z3_RE_SORT in the C API.
Char = 13
Corresponds to Z3_CHAR_SORT in the C API.
TypeVar = 14
Corresponds to Z3_TYPE_VAR in the C API.
Unknown = 1_000
Corresponds to Z3_UNKNOWN_SORT in the C API.