Source

pyarith / tests / test_prop.py

#!/usr/local/bin/python
# -*- coding: utf-8 -*-

import pytest
import logics.prop as lp

p = lp.Var('p')
q = lp.Var('q')
r = lp.Var('r')
s = lp.Var('s')


equivs = [(p & ~p, lp.F),
          (p | ~p, lp.T),
          (lp.IfThen(lp.IfThen(p, q) & lp.IfThen(q, r), lp.IfThen(p, r)), lp.T),
          (lp.IfThen(p, q) & lp.IfThen(q, p), lp.Iff(p, q)),
          (lp.IfThen(p & lp.IfThen(p, q), q), lp.T)
          ]


@pytest.mark.parametrize(
    ('lhs', 'rhs'),
    equivs
)
def test_equivalent_DNF(lhs, rhs):
    assert lp.equivalent_DNF(lhs, rhs)


@pytest.mark.parametrize(
    ('lhs', 'rhs'),
    equivs
)
def test_equivalent_CNF(lhs, rhs):
    assert lp.equivalent_CNF(lhs, rhs)


@pytest.mark.parametrize(
    ('prop', 'dnf'),
    [(lp.T, lp.T),
     (lp.F, lp.F),
     (~lp.T, lp.F),
     (~lp.F, lp.T),
     (p, p),
     (~p, ~p),
     (~~p, p),
     (p & ~lp.F, p & lp.T),
     (p & ~lp.T, p & lp.F),
     (~(p & q), (~p) | (~q)),
     (~(p | q), (~p) & (~q)),
     ((p & q) & r, p & (q & r)),
     ((p & q) & (r & s), p & (q & (r & s))),
     ((p | q) | r, p | (q | r)),
     (p & (q | r), (p & q) | (p & r)),
     (p | (q & r), p | (q & r)),
     ((p | q) & (r | s), (p & r) | ((p & s) | ((q & r) | (q & s)))),
     ((p & q) | (r & s), (p & q) | (r & s)),
     (p & (q & (r | s)), (p & (q & r) | (p & (q & s)))),
     (p | (q | (r & s)), p | (q | (r & s))),
     (lp.IfThen(p, q), ~p | q),
     (lp.Iff(p, q), (p & q) | (~p & ~q)),
     (lp.IfThen(p, q) | lp.IfThen(p, r), ~p | (q | (~p | r))),
     (~p & (q & r), ~p & (q & r)),
     (p ^ p, (p & ~p) | (~p & p))
     ]
)
def test_normalize_DNF(prop, dnf):
    assert lp.normalize_DNF(prop) == dnf


@pytest.mark.parametrize(
    ('prop', 'cnf'),
    [(lp.T, lp.T),
     (lp.F, lp.F),
     (~lp.T, lp.F),
     (~lp.F, lp.T),
     (p, p),
     (~p, ~p),
     (~~p, p),
     (p & ~lp.F, p & lp.T),
     (p & ~lp.T, p & lp.F),
     (~(p & q), (~p) | (~q)),
     (~(p | q), (~p) & (~q)),
     ((p & q) & r, p & (q & r)),
     ((p & q) & (r & s), p & (q & (r & s))),
     ((p | q) | r, p | (q | r)),
     (p & (q | r), p & (q | r)),
     (p | (q & r), (p | q) & (p | r)),
     ((p | q) & (r | s), (p | q) & (r | s)),
     ((p & q) | (r & s), (p | r) & ((p | s) & ((q | r) & (q | s)))),
     (p & (q & (r | s)), p & (q & (r | s))),
     (p | (q | (r & s)), (p | (q | r)) & (p | (q | s))),
     (lp.IfThen(p, q), ~p | q),
     (lp.Iff(p, q), (p | ~p) & ((p | ~q) & ((q | ~p) & (q | ~q)))),
     (lp.IfThen(p, q) | lp.IfThen(p, r), ~p | (q | (~p | r))),
     (~p & (q & r), ~p & (q & r)),
     (p ^ p, (p | ~p) & ((p | p) & ((~p | ~p) & (~p | p))))
     ]
)
def test_normalize_CNF(prop, cnf):
    assert lp.normalize_CNF(prop) == cnf


@pytest.mark.parametrize(
    ('prop', 'dnf'),
    [(q & p, p & q),
     (~q | ~p, (p & ~q) | ~p),

     (p & p, p),
     (~p | ~p, ~p),

     (~p & ~p, ~p),
     (p | p, p),

     (p & ~p, lp.F),
     (~p | p, lp.T),

     (p & lp.T, p),
     (~p | lp.F, ~p),

     (lp.T & p, p),
     (lp.F | ~p, ~p),

     (p & lp.F, lp.F),
     (~p | lp.T, lp.T),

     (lp.F & p, lp.F),
     (lp.T | ~p, lp.T),

     (p & (q & ~p), lp.F),
     (~p | (~q | p), lp.T),

     (p & (q & p), p & q),
     (~p | (~q | ~p), (p & ~q) | ~p),

     (p | q, p | (~p & q)),
     (~p & ~q, ~p & ~q),

     (q | p, p | (~p & q)),
     (~q & ~p, ~p & ~q),

     (p | (q & p), p),
     (~p & (~q | ~p), ~p),

     ((q & p) | p, p),
     ((~q | ~p) & ~p, ~p),

     (p | (q | r), p | (~p & (q | (~q & r)))),
     (~p & (~q & ~r), ~p & (~q & ~r)),

     ((p & q) | (q & r), (p & q) | (~p & (q & r))),
     ((~p | ~q) & (~q | ~r), (p & ~q) | (~p & ((q & ~r) | ~q))),

     ((p & q) | (r & s),
      (p & (q | (~q & (r & s)))) | (~p & (r & s))),
     ((~p | ~q) & (~r | ~s),
      (p & (~q & ((r & ~s) | ~r))) | (~p & ((r & ~s) | ~r))),

     (lp.T & (p & p), p),
     (lp.F | (~p | ~p), ~p),

     (p ^ p, lp.F),
     (p ^ (~p), lp.T),

     (lp.IfThen(p, p), lp.T),

     (lp.IfThen(p, q), (p & q) | ~p),

     (lp.Iff(p, p), lp.T),
     (lp.Iff(p, ~p), lp.F),

     (lp.IfThen(lp.IfThen(p, q) & lp.IfThen(q, r), lp.IfThen(p, r)), lp.T)
     ]
)
def test_canonicalize_DNF(prop, dnf):
    assert lp.canonicalize_DNF(prop) == dnf

@pytest.mark.parametrize(
    ('prop', 'cnf'),
    [(q & p, p & (~p | q)),
     (~q | ~p, ~p | ~q),

     (p & p, p),
     (~p | ~p, ~p),

     (~p & ~p, ~p),
     (p | p, p),

     (p & ~p, lp.F),
     (~p | p, lp.T),

     (p & lp.T, p),
     (~p | lp.F, ~p),

     (lp.T & p, p),
     (lp.F | ~p, ~p),

     (p & lp.F, lp.F),
     (~p | lp.T, lp.T),

     (lp.F & p, lp.F),
     (lp.T | ~p, lp.T),

     (p & (q & ~p), lp.F),
     (~p | (~q | p), lp.T),

     (p & (q & p), p & (~p | q)),
     (~p | (~q | ~p), ~p | ~q),

     (p | q, p | q),
     (~p & ~q, (p | ~q) & ~p),

     (q | p, p | q),
     (~q & ~p, (p | ~q) & ~p),

     (p | (q & p), p),
     (~p & (~q | ~p), ~p),

     ((q & p) | p, p),
     ((~q | ~p) & ~p, ~p),

     (p | (q | r), p | (q | r)),
     (~p & (~q & ~r), (p | ((q | ~r) & ~q)) & ~p),

     ((p & q) | (q & r), (p | (q & (~q | r))) & (~p | q)),
     ((~p | ~q) & (~q | ~r), (p | (~q | ~r)) & (~p | ~q)),

     ((p & q) | (r & s),
      (p | ((r & (~r | s)))) & (~p | (q | (r & (~r | s))))),
     ((~p | ~q) & (~r | ~s),
      (p | (~r | ~s)) & (~p | ((q | (~r | ~s)) & ~q))),

     (lp.T & (p & p), p),
     (lp.F | (~p | ~p), ~p),

     (p ^ p, lp.F),
     (p ^ (~p), lp.T),

     (lp.IfThen(p, p), lp.T),

     (lp.IfThen(p, q), ~p | q),

     (lp.Iff(p, p), lp.T),
     (lp.Iff(p, ~p), lp.F),

     (lp.IfThen(lp.IfThen(p, q) & lp.IfThen(q, r), lp.IfThen(p, r)), lp.T)
     ]
)
def test_canonicalize_CNF(prop, cnf):
    assert lp.canonicalize_CNF(prop) == cnf


@pytest.mark.parametrize(
    ('prop', 'environment'),
    [(0, 0)]
)
def test_eval(prop, environment):
    pass