import pytest
import fol


@pytest.mark.parametrize(['imp', 'res'], [
    ('\\exists x (Pre(y) -> Post(y))',
     '\\exists x (~Pre(y) | Post(y))'),
    ('Pre(x) -> Post(x)', '~Pre(x) | Post(x)'),
    ('Pre(x) -> (Aux(y) -> Post(x))',
     '~Pre(x) | (~Aux(y) | Post(x))'),
    ('(Pre(x) & Aux(y)) -> Post(x)', '~(Pre(x) & Aux(y)) | Post(x)')
])
def test_cnf_imp(imp, res):
    assert fol.cnf.elim_imp(fol.p(imp)).equals(fol.p(res))


@pytest.mark.parametrize(['f', 'res'], [
    ('~(Pre(x) | Post(y))', '~Pre(x) & ~Post(y)'),
    ('~(Pre(x) & Post(y))', '~Pre(x) | ~Post(y)'),
    ('~(Pre(x) & (Post(y) | Post(z)))',
     '~Pre(x) | (~Post(y) & ~Post(z))'),
])
def test_cnf_neg(f, res):
    assert fol.cnf.neg(fol.p(f)).equals(fol.p(res))


@pytest.mark.parametrize(['f', 'res'], [
    ('Pre(x) -> Post(x)', 'Pre(x0) -> Post(x0)'),
    ('Pre(x) -> Post(y)', 'Pre(x0) -> Post(x1)'),
    ('Pre(x, y) -> Post(y, x)', 'Pre(x0, x1) -> Post(x1, x0)'),
    ('Pre(f(x)) -> Post(g(g(y), x))',
     'Pre(f(x0)) -> Post(g(g(x1), x0))'),
])
def test_cnf_normalize(f, res):
    counter = fol.cnf.Counter()
    assert fol.cnf.normalize(fol.p(f), counter).equals(fol.p(res))


@pytest.mark.parametrize(['f', 'res'], [
    # FOR ALL
    ('~(\\forall x Pre(x))', '\\exists x ~Pre(x)'),

    ('(\\forall x Pre(x)) & Post(x)',
     '\\forall x (Pre(x) & Post(x))'),

    ('(\\forall x Pre(x)) | Post(x)',
     '\\forall x (Pre(x) | Post(x))'),

    ('(\\forall x Pre(x)) -> Post(x)',
     '\\exists x (Pre(x) -> Post(x))'),

    ('Pre(x) & (\\forall x Post(x))',
     '\\forall x (Pre(x) & Post(x))'),

    ('Pre(x) | (\\forall x Post(x))',
     '\\forall x (Pre(x) | Post(x))'),

    ('Pre(x) -> (\\forall x Post(x))',
     '\\forall x (Pre(x) -> Post(x))'),
    # EXISTS
    ('~(\\exists x Pre(x))', '\\forall x ~Pre(x)'),

    ('(\\exists x Pre(x)) & Post(x)',
     '\\exists x (Pre(x) & Post(x))'),

    ('(\\exists x Pre(x)) | Post(x)',
     '\\exists x (Pre(x) | Post(x))'),

    ('(\\exists x Pre(x)) -> Post(x)',
     '\\forall x (Pre(x) -> Post(x))'),

    ('Pre(x) & (\\exists x Post(x))',
     '\\exists x (Pre(x) & Post(x))'),

    ('Pre(x) | (\\exists x Post(x))',
     '\\exists x (Pre(x) | Post(x))'),

    ('Pre(x) -> (\\exists x Post(x))',
     '\\exists x (Pre(x) -> Post(x))'),

])
def test_cnf_prenex(f, res):
    assert fol.cnf.prenex(fol.p(f)).equals(fol.p(res))


@pytest.mark.parametrize(['imp', 'res'], [
    ('\\exists x (Pre(x) -> Post(x))', 'Pre(S0) -> Post(S0)'),

    ('\\exists x (\\exists y (Pre(x) -> Post(y)))',
     'Pre(S0) -> Post(S1)'),

    ('\\forall a (\\exists x (Pre(a, x) -> Post(x)))',
     '\\forall a (Pre(a, s0(a)) -> Post(s0(a)))'),

    ('\\forall a (\\forall b (\\exists x (Pre(a, x) -> Post(x))))',
     '\\forall a (\\forall b (Pre(a, s0(a, b)) -> Post(s0(a, b))))'),

    ('\\forall a (\\exists x (\\forall b (Pre(x) -> Post(x))))',
     '\\forall a (\\forall b (Pre(s0(a)) -> Post(s0(a))))'),

    ('\\forall a (\\exists x (\\forall b (Pre(x) -> Post(x))))',
     '\\forall a (\\forall b (Pre(s0(a)) -> Post(s0(a))))'),
])
def test_cnf_skolem(imp, res):
    assert fol.cnf.skolem(fol.p(imp)).equals(fol.p(res))


@pytest.mark.parametrize(['f', 'oracle'], [
    ('Pre(x) | (Aux(x) & Post(x))',
     '(Pre(x) | Aux(x)) & (Pre(x) | Post(x))'),
    ('(Aux(x) & Post(x)) | Pre(x)',
     '(Aux(x) | Pre(x)) & (Post(x) | Pre(x))')
])
def test_distrib(oracle, f):
    assert fol.cnf.distrib(fol.p(f)).equals(fol.p(oracle))


@pytest.mark.parametrize(['f', 'oracle'], [
    ('Friend(x, y) -> Friend(y, x)',
     '~Friend(x0, x1) | Friend(x1, x0)'),

    ('(Friend(x, y) & Friend(y, z)) -> Friend(x, z)',
     '(~Friend(x0, x1) | ~Friend(x1, x2)) | Friend(x0, x2)')
])
def test_cnf(oracle, f):
    print(fol.pretty.get(fol.p(f)))
    print(fol.pretty.get(fol.cnf.cnf(fol.p(f))))
    assert fol.cnf.cnf(fol.p(f)).equals(fol.p(oracle))