Struct z3::Sort

pub struct Sort<'ctx> { /* fields omitted */ }

Methods

impl<'ctx> Sort<'ctx>

fn uninterpretd(ctx: &'ctx Context, sym: &Symbol<'ctx>) -> Sort<'ctx>

fn bool(ctx: &Context) -> Sort

fn int(ctx: &Context) -> Sort

fn real(ctx: &Context) -> Sort

fn bitvector(ctx: &Context, sz: u32) -> Sort

fn array(
    ctx: &'ctx Context,
    domain: &Sort<'ctx>,
    range: &Sort<'ctx>
) -> Sort<'ctx>

fn set(ctx: &'ctx Context, elt: &Sort<'ctx>) -> Sort<'ctx>