Crate z3_ref

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

Structs

Ast

Ast (= abstract syntax tree) is a pointer to a Z3 formula. It can be created by methods of Push or Context object and should not live longer than the object from which it was created.

Context

Base Z3 objects that holds references to Z3 config, context, sort, solver and basic reusable formulae: true and false. Each interaction with Z3 should start with Context::new() and then calling the methods of the object.

Push

An abstract object that gets created after calling Z3 solver push, and on drop it calls Z3 solver pop. It cannot live longer than its parent (which is Context or another Push object), and makes sure that no Ast created between the push and pop can be used after the pop.

SolverResult

Enums

Evaluation

Traits

Stage

Context and Push have very similar semantics, both are references to the Z3 context + config + solver, Push has only an extra functionality to pop on drop. This module implements public common functions of Context and Push: operators of the logic, solver’s assert, check, and push functions.