Struct z3::Context [−][src]
pub struct Context { /* fields omitted */ }
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);
Implementations
impl Context
[src]
pub fn new(cfg: &Config) -> Context
[src]
pub fn interrupt(&self)
[src]
Interrupt a solver performing a satisfiability test, a tactic processing a goal, or simplify functions.
pub fn handle(&self) -> ContextHandle<'_>
[src]
Obtain a handle that can be used to interrupt computation from another thread.
Trait Implementations
impl Debug for Context
[src]
impl Drop for Context
[src]
impl Eq for Context
[src]
impl PartialEq<Context> for Context
[src]
impl StructuralEq for Context
[src]
impl StructuralPartialEq for Context
[src]
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
impl<T> Any for T where
T: 'static + ?Sized,
[src]
T: 'static + ?Sized,
impl<T> Borrow<T> for T where
T: ?Sized,
[src]
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
[src]
T: ?Sized,
pub fn borrow_mut(&mut self) -> &mut T
[src]
impl<T> From<T> for T
[src]
impl<T, U> Into<U> for T where
U: From<T>,
[src]
U: From<T>,
impl<T, U> TryFrom<U> for T where
U: Into<T>,
[src]
U: Into<T>,
type Error = Infallible
The type returned in the event of a conversion error.
pub fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>
[src]
impl<T, U> TryInto<U> for T where
U: TryFrom<T>,
[src]
U: TryFrom<T>,