High level interface to the Z3 SMT solver. Currently, only support for boolean logic is implemented. It is therefore usable only as a SAT solver. We have not yet considered thread safety or reasonable behaviour if multiple contexts are used at once.

``` use z3::Stage;

// Start to use Z3. let mut ctx = z3::Context::new();

// Create a variable. let foo = ctx.varfromstring("foo");

// Add it to the solver. ctx.assert(foo);

{ // Push Z3 solver's stack. let mut p = ctx.push();

// A basic example of combining formulae.
let foo_and_not_foo = p.and(vec![foo.inherit(), p.not(foo)]);
p.assert(foo_and_not_foo);

// No way to satisfy foo && !foo.
assert!(!p.is_sat())

} // Pop Z3 solver's stack.

assert!(ctx.is_sat()) ```