Struct Z3Sort 

pub struct Z3Sort {
    pub id: SortId,
    /* private fields */
}

Analogue of z3::Sort.

A lightweight handle pairing a SortId with the owning context’s TermManager, so that the sort can be introspected (kind, bit-width, array domain/range, name) after the fact.

Fields

id: SortId

The underlying sort identifier.

Implementations

impl Z3Sort

pub fn new(ctx: &Z3Context, id: SortId) -> Self

Wrap a raw SortId together with the context it belongs to.

pub fn kind(&self) -> Z3SortKind

Return the high-level Z3SortKind of this sort.

pub fn bv_size(&self) -> Option<u32>

If this is a bit-vector sort, return its width in bits.

Returns None for every other sort kind.

pub fn array_domain(&self) -> Option<Z3Sort>

If this is an array sort, return its domain (index) sort.

Returns None for every other sort kind.

pub fn array_range(&self) -> Option<Z3Sort>

If this is an array sort, return its range (element) sort.

Returns None for every other sort kind.

pub fn name(&self) -> String

Return a human-readable name for this sort.

Mirrors Z3’s Sort::to_string, e.g. "Bool", "Int", "Real", "BitVec(32)", "Array", or the declared name of an uninterpreted / datatype sort.

Trait Implementations

impl Clone for Z3Sort

fn clone(&self) -> Z3Sort

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Z3Sort

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Display for Z3Sort

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.