z3d 0.1.0

Z3 DSL interface for Rust
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27

#![feature(proc_macro_hygiene)]

use z3;
use z3d::dec;

fn default_ctx() -> z3::Context {
    z3::Context::new(&z3::Config::default())
}

#[test]
fn modus_tollens() {
    let ctx = &default_ctx();
    let solver = z3::Solver::new(ctx);
    let p = dec!(p: bool in ctx);
    let q = dec!(q: bool in ctx);

    solver.assert(&p.implies(&q));
    solver.assert(&q.not());
    assert_eq!(solver.check(), z3::SatResult::Sat);

    solver.push();
    solver.assert(&p);
    assert_eq!(solver.check(), z3::SatResult::Unsat);

    solver.pop(1);
    assert_eq!(solver.check(), z3::SatResult::Sat);
}