Z3 SMT求解器的高级接口。目前，仅实现了对布尔逻辑的支持。因此，它只能作为SAT求解器使用。我们尚未考虑在同时使用多个上下文时的线程安全性或合理行为。

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:

Z3 SMT求解器的高级接口。目前，仅实现了对布尔逻辑的支持。因此，它只能作为SAT求解器使用。我们尚未考虑在同时使用多个上下文时的线程安全性或合理行为。

示例

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!"),
}

以下示例因为值 not_foo 在 p 的生命周期中创建，在 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 = p.not(foo);
}

ctx.assert(not_foo);

此类技巧也无法工作（因为 ctx 被可变借用 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);