Struct seer_z3::Context

pub struct Context { /* fields omitted */ }

Methods

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.