#[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.