pub struct Context { /* private fields */ }
Expand description
Manager of all other Z3 objects, global configuration options, etc.
An application may use multiple Z3 contexts. Objects created in one context cannot be used in another one. However, several objects may be “translated” from one context to another. It is not safe to access Z3 objects from multiple threads.
Examples:
Creating a context with the default configuration:
use z3::{Config, Context};
let cfg = Config::new();
let ctx = Context::new(&cfg);
See also:
Implementations§
source§impl Context
impl Context
pub fn new(cfg: &Config) -> Context
sourcepub fn interrupt(&self)
pub fn interrupt(&self)
Interrupt a solver performing a satisfiability test, a tactic processing a goal, or simplify functions.
sourcepub fn handle(&self) -> ContextHandle<'_>
pub fn handle(&self) -> ContextHandle<'_>
Obtain a handle that can be used to interrupt computation from another thread.
See also:
sourcepub fn update_param_value(&mut self, k: &str, v: &str)
pub fn update_param_value(&mut self, k: &str, v: &str)
sourcepub fn update_bool_param_value(&mut self, k: &str, v: bool)
pub fn update_bool_param_value(&mut self, k: &str, v: bool)
Trait Implementations§
source§impl PartialEq<Context> for Context
impl PartialEq<Context> for Context
impl Eq for Context
impl StructuralEq for Context
impl StructuralPartialEq for Context
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§
source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere T: ?Sized,
source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more