pyndakaas 0.1.0

Python bindings for the pindakaas crate
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

import pindakaas


def test_cadical():
    slv = pindakaas.solver.CaDiCaL()
    x, y = slv.new_vars(2)
    slv.add_clause([x, y])
    slv.add_clause([~x, ~y])
    with slv.solve() as result:
        assert result.status == pindakaas.solver.Status.SATISFIED
        vx, vy = result.value(x), result.value(y)
        assert vx is not None
        assert vy is not None
        assert vx != vy


def test_assumptions():
    slv = pindakaas.solver.CaDiCaL()
    x, y = slv.new_vars(2)
    slv += x ^ y
    with slv.solve(assumptions=[x]) as result:
        assert result.status == pindakaas.solver.Status.SATISFIED
        assert result.value(x) is True
        assert result.value(y) is False
    with slv.solve(assumptions=[y]) as result:
        assert result.status == pindakaas.solver.Status.SATISFIED
        assert result.value(x) is False
        assert result.value(y) is True
    with slv.solve(assumptions=[x, y]) as result:
        assert result.status == pindakaas.solver.Status.UNSATISFIABLE