pub struct Context { /* fields omitted */ }
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.
Creating a context with the default configuration:
use z3::{Config, Context};
let cfg = Config::new();
let ctx = Context::new(&cfg);
Interrupt a solver performing a satisfiability test, a tactic processing a goal, or simplify functions.
Obtain a handle that can be used to interrupt computation from another thread.
Formats the value using the given formatter. Read more
Executes the destructor for this type. Read more
This method tests for self
and other
values to be equal, and is used
by ==
. Read more
This method tests for !=
.
impl<T> Any for T where
T: 'static + ?Sized,
Immutably borrows from an owned value. Read more
Mutably borrows from an owned value. Read more
impl<T, U> Into<U> for T where
U: From<T>,
The type returned in the event of a conversion error.
The type returned in the event of a conversion error.