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.var_from_string("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())