97 lines
2.0 KiB
Python
97 lines
2.0 KiB
Python
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",
|
|
"X1 AND X2 OR X1 AND X3",
|
|
"!(X1 AND X2) OR (X1 OR X2)",
|
|
"X1 * X1 * X2 * X2",
|
|
"X1 + !X1 + X2",
|
|
"(X1 OR X2) AND (X2 OR X3) AND (X3 OR X1)",
|
|
"!!(X1 AND !X2) OR X3",
|
|
]
|
|
|
|
for f in formulas:
|
|
equivalent(f)
|