import itertools

from anf import convert
from anf.parser import Parser, tokenize


def parse(expr):
    return Parser(tokenize(expr)).parse()


def eval_poly(poly, env):
    res = False
    for mono in poly:
        term = True
        for v in mono:
            term &= env.get(v, False)
        res ^= term
    return res


def eval_expr(expr, env):
    py = expr
    py = py.replace("!", " not ")
    py = py.replace("AND", " and ")
    py = py.replace("OR", " or ")
    py = py.replace("+", " or ")
    py = py.replace("*", " and ")
    return eval(py, {"__builtins__": {}}, env)


def equivalent(expr):
    poly = parse(expr)
    vars_ = sorted({t for t in tokenize(expr) if t.startswith("X")})

    for values in itertools.product([False, True], repeat=len(vars_)):
        env = dict(zip(vars_, values))
        assert eval_expr(expr, env) == eval_poly(poly, env)


# ------------------------
# Tests
# ------------------------

def test_basic_or():
    assert equivalent("X1 OR X2") is None


def test_basic_and():
    assert equivalent("X1 AND X2") is None


def test_not():
    assert equivalent("!X1") is None


def test_plus_star_syntax():
    assert equivalent("X1 * (X2 + !X3)") is None


def test_idempotent():
    assert convert("X1 OR X1") == "X1"


def test_contradiction():
    assert convert("X1 AND !X1") == "0"


def test_big_formula():
    expr = (
        "!X11 AND (!X3 AND !X4 OR X3 AND X4 OR X3 AND !X4 AND X12) OR X11 AND !X12 AND (X3 OR X4)"
    )

    expected = (
        "1⊕X11⊕X3⊕X4⊕(X3⸱X12)⊕(X4⸱X11⸱X12)⊕(X3⸱X4⸱X11)⊕(X3⸱X4⸱X12)"
    )

    assert convert(expr) == expected


def test_equivalence_suite():
    formulas = [
        "X1 OR X2",
        "X1 AND !X2",
        "!(X1 OR X2)",
        "(X1 + X2) * (!X1 + X3)",
        "!X1 AND (!X2 OR X3) OR X1 AND X2",
    ]

    for f in formulas:
        equivalent(f)