Struct z3::Context
[−]
[src]
pub struct Context { /* fields omitted */ }
Methods
impl Context
[src]
fn new(cfg: &Config) -> Context
fn bool_sort(&self) -> Sort
fn int_sort(&self) -> Sort
fn real_sort(&self) -> Sort
fn bitvector_sort(&self, sz: u32) -> Sort
fn array_sort<'ctx>(
&'ctx self,
domain: &Sort<'ctx>,
range: &Sort<'ctx>
) -> Sort<'ctx>
&'ctx self,
domain: &Sort<'ctx>,
range: &Sort<'ctx>
) -> Sort<'ctx>