Enum z3_sys::SortKind
[−]
[src]
#[repr(u32)]pub enum SortKind { Uninterpreted, Bool, Int, Real, BV, Array, Datatype, Relation, FiniteDomain, FloatingPoint, RoundingMode, Seq, RE, Unknown, }
The different kinds of Z3 types (See Z3_get_sort_kind
).
This corresponds to Z3_sort_kind
in the C API.
Variants
Uninterpreted
This corresponds to Z3_UINTERPRETED_SORT
in the C API.
Bool
This corresponds to Z3_BOOL_SORT
in the C API.
Int
This corresponds to Z3_INT_SORT
in the C API.
Real
This corresponds to Z3_REAL_SORT
in the C API.
BV
This corresponds to Z3_BV_SORT
in the C API.
Array
This corresponds to Z3_ARRAY_SORT
in the C API.
Datatype
This corresponds to Z3_DATATYPE_SORT
in the C API.
Relation
This corresponds to Z3_RELATION_SORT
in the C API.
FiniteDomain
This corresponds to Z3_FINITE_DOMAIN_SORT
in the C API.
FloatingPoint
This corresponds to Z3_FLOATING_POINT_SORT
in the C API.
RoundingMode
This corresponds to Z3_ROUNDING_MODE_SORT
in the C API.
Seq
This corresponds to Z3_SEQ_SORT
in the C API.
RE
This corresponds to Z3_RE_SORT
in the C API.
Unknown
This corresponds to Z3_UNKNOWN_SORT
in the C API.
Trait Implementations
impl Debug for SortKind
[src]
fn fmt(&self, __arg_0: &mut Formatter) -> Result
[src]
Formats the value using the given formatter. Read more
impl Copy for SortKind
[src]
impl Clone for SortKind
[src]
fn clone(&self) -> SortKind
[src]
Returns a copy of the value. Read more
fn clone_from(&mut self, source: &Self)
1.0.0[src]
Performs copy-assignment from source
. Read more
impl PartialEq for SortKind
[src]
fn eq(&self, __arg_0: &SortKind) -> bool
[src]
This method tests for self
and other
values to be equal, and is used by ==
. Read more
fn ne(&self, other: &Rhs) -> bool
1.0.0[src]
This method tests for !=
.