#z3 #sat #smt

z3_ref

High level interface to the Z3 SMT solver

5 releases

0.1.4 Oct 3, 2018
0.1.3 Sep 24, 2018
0.1.2 Sep 24, 2018
0.1.1 Sep 21, 2018
0.1.0 Sep 20, 2018

#7 in #sat

24 downloads per month

MIT license

17KB
321 lines

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

No runtime deps

~1.5MB
~30K SLoC