Struct seer_z3::Sort [−][src]
pub struct Sort<'ctx> { /* fields omitted */ }Methods
impl<'ctx> Sort<'ctx>[src]
impl<'ctx> Sort<'ctx>pub fn uninterpretd(ctx: &'ctx Context, sym: &Symbol<'ctx>) -> Sort<'ctx>[src]
pub fn uninterpretd(ctx: &'ctx Context, sym: &Symbol<'ctx>) -> Sort<'ctx>pub fn bool(ctx: &Context) -> Sort[src]
pub fn bool(ctx: &Context) -> Sortpub fn int(ctx: &Context) -> Sort[src]
pub fn int(ctx: &Context) -> Sortpub fn real(ctx: &Context) -> Sort[src]
pub fn real(ctx: &Context) -> Sortpub fn bitvector(ctx: &Context, sz: u32) -> Sort[src]
pub fn bitvector(ctx: &Context, sz: u32) -> Sortpub fn array(
ctx: &'ctx Context,
domain: &Sort<'ctx>,
range: &Sort<'ctx>
) -> Sort<'ctx>[src]
pub fn array(
ctx: &'ctx Context,
domain: &Sort<'ctx>,
range: &Sort<'ctx>
) -> Sort<'ctx>pub fn set(ctx: &'ctx Context, elt: &Sort<'ctx>) -> Sort<'ctx>[src]
pub fn set(ctx: &'ctx Context, elt: &Sort<'ctx>) -> Sort<'ctx>