ipasir-sys 0.3.0

A Rust crate that contains FFI bindings for IPASIR-compatible SAT solvers.
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
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60

use ipasir_sys::*;

#[test]
fn it_can_incrementally_solve_a_coloring_problem() {
    let a_is_white = 1;
    let a_is_black = 2;

    let b_is_white = 3;
    let b_is_black = 4;

    unsafe {
        let solver = ipasir_init();

        // a is white or black
        ipasir_add(solver, a_is_white);
        ipasir_add(solver, a_is_black);
        ipasir_add(solver, 0);

        // b is white or black
        ipasir_add(solver, b_is_white);
        ipasir_add(solver, b_is_black);
        ipasir_add(solver, 0);

        // both a and b cannot be white
        ipasir_add(solver, -a_is_white);
        ipasir_add(solver, -b_is_white);
        ipasir_add(solver, 0);

        // both a and b cannot be black
        ipasir_add(solver, -a_is_black);
        ipasir_add(solver, -b_is_black);
        ipasir_add(solver, 0);

        // assume a and b are both white
        ipasir_assume(solver, a_is_white);
        ipasir_assume(solver, b_is_white);

        // the formula is unsatisfiable
        let unsat_status = ipasir_solve(solver);
        assert_eq!(unsat_status, 20);

        // this assumption caused its unsatisfiability
        let caused_unsat = ipasir_failed(solver, a_is_white);
        assert_eq!(caused_unsat, 1);

        // assume only a is white
        ipasir_assume(solver, a_is_white);

        // the formula is satisfiable
        let sat_status = ipasir_solve(solver);
        assert_eq!(sat_status, 10);

        // the solver has assigned a as white and b as black
        assert_eq!(ipasir_val(solver, a_is_white), a_is_white);
        assert_eq!(ipasir_val(solver, a_is_black), -a_is_black);

        assert_eq!(ipasir_val(solver, b_is_white), -b_is_white);
        assert_eq!(ipasir_val(solver, b_is_black), b_is_black);
    }
}