pub struct Context { /* private fields */ }
Implementations
sourceimpl Context
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
Auto Trait Implementations
impl RefUnwindSafe for Context
impl !Send for Context
impl !Sync for Context
impl Unpin for Context
impl UnwindSafe for Context
Blanket Implementations
sourceimpl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
const: unstable · sourcefn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more