#[repr(u32)]pub enum SortKind {
Show 14 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,
Unknown = 1_000,
}Expand description
The different kinds of Z3 types.
This corresponds to Z3_sort_kind in the C API.
Variants§
Uninterpreted = 0
This corresponds to Z3_UNINTERPRETED_SORT in the C API.
Bool = 1
This corresponds to Z3_BOOL_SORT in the C API.
Int = 2
This corresponds to Z3_INT_SORT in the C API.
Real = 3
This corresponds to Z3_REAL_SORT in the C API.
BV = 4
This corresponds to Z3_BV_SORT in the C API.
Array = 5
This corresponds to Z3_ARRAY_SORT in the C API.
Datatype = 6
This corresponds to Z3_DATATYPE_SORT in the C API.
Relation = 7
This corresponds to Z3_RELATION_SORT in the C API.
FiniteDomain = 8
This corresponds to Z3_FINITE_DOMAIN_SORT in the C API.
FloatingPoint = 9
This corresponds to Z3_FLOATING_POINT_SORT in the C API.
RoundingMode = 10
This corresponds to Z3_ROUNDING_MODE_SORT in the C API.
Seq = 11
This corresponds to Z3_SEQ_SORT in the C API.
RE = 12
This corresponds to Z3_RE_SORT in the C API.
Unknown = 1_000
This corresponds to Z3_UNKNOWN_SORT in the C API.