Struct z3::Context

pub struct Context { /* private fields */ }

Manager of all other Z3 objects, global configuration options, etc.

Implementations

impl Context

pub fn new(cfg: &Config) -> Context

pub fn bool_sort(&self) -> Sort<'_>

pub fn int_sort(&self) -> Sort<'_>

pub fn real_sort(&self) -> Sort<'_>

pub fn bitvector_sort(&self, sz: u32) -> Sort<'_>

pub fn array_sort<'ctx>(
    &'ctx self,
    domain: &Sort<'ctx>,
    range: &Sort<'ctx>
) -> Sort<'ctx>

pub fn set_sort<'ctx>(&'ctx self, elt: &Sort<'ctx>) -> Sort<'ctx>

pub fn int_sym(&self, i: u32) -> Symbol<'_>

pub fn str_sym(&self, s: &str) -> Symbol<'_>

pub fn named_const<'ctx>(&'ctx self, s: &str, sort: &'ctx Sort<'_>) -> Ast<'ctx>

pub fn numbered_const<'ctx>(&'ctx self, i: u32, sort: &'ctx Sort<'_>) -> Ast<'ctx>

pub fn fresh_const<'ctx>(
    &'ctx self,
    prefix: &str,
    sort: &'ctx Sort<'_>
) -> Ast<'ctx>

pub fn named_bool_const(&self, s: &str) -> Ast<'_>

pub fn numbered_bool_const(&self, i: u32) -> Ast<'_>

pub fn fresh_bool_const<'ctx>(&'ctx self, prefix: &str) -> Ast<'ctx>

pub fn named_int_const(&self, s: &str) -> Ast<'_>

pub fn numbered_int_const(&self, i: u32) -> Ast<'_>

pub fn fresh_int_const<'ctx>(&'ctx self, prefix: &str) -> Ast<'ctx>

pub fn named_real_const(&self, s: &str) -> Ast<'_>

pub fn numbered_real_const(&self, i: u32) -> Ast<'_>

pub fn fresh_real_const<'ctx>(&'ctx self, prefix: &str) -> Ast<'ctx>

pub fn named_bitvector_const(&self, s: &str, sz: u32) -> Ast<'_>

pub fn numbered_bitvector_const(&self, i: u32, sz: u32) -> Ast<'_>

pub fn fresh_bitvector_const<'ctx>(&'ctx self, prefix: &str, sz: u32) -> Ast<'ctx>

pub fn from_bool(&self, b: bool) -> Ast<'_>

pub fn from_u64(&self, u: u64) -> Ast<'_>

pub fn from_i64(&self, i: i64) -> Ast<'_>

pub fn from_real(&self, num: i32, den: i32) -> Ast<'_>

Trait Implementations

impl Drop for Context

fn drop(&mut self)

Executes the destructor for this type.