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())

lib.rs:

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.

Examples

use z3_ref::Stage;
use z3_ref as z3;

// Create Z3 config, context and solver.
let mut ctx = z3::Context::new();

// Create variable, which is of type Ast, which itself represents an
// immutable reference to a Z3 AST object.
let foo = ctx.var_from_int(0);

ctx.assert(foo);

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

    // A basic example of combining Asts.
    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.check().is_some())
}
// Pop of the Z3 solver's stack happens here, with the drop of the push
// object p. Asts created between push and pop are no more valid, but this
// library ensures that the borrow checker would refuse any leak.

match ctx.check() {
    Some(result) => assert!(
        result.model() == vec![(0, z3::Evaluation::True)]),
    _ => panic!("the theory should have been satisfiable!"),
}

The following gets refused by the borrow checker because the value not_foo, which is created in the lifetime of p is used after p is dropped.

use z3_ref::Stage;
use z3_ref as z3;

let mut ctx = z3::Context::new();
let foo = ctx.var_from_int(0);
let not_foo;

{
    let mut p = ctx.push();

    not_foo = p.not(foo);
}

ctx.assert(not_foo);

Tricks like this one will also not work (because ctx is mutably borrowed by p).

use z3_ref::Stage;
use z3_ref as z3;

let mut ctx = z3::Context::new();
let foo = ctx.var_from_int(0);
let not_foo;

{
    let mut p = ctx.push();

    not_foo = ctx.not(foo);
}

ctx.assert(not_foo);