class Expr:
    def __init__(self, p, q):
        self.p = p
        self.q = q
        needsbrackets = False
        if self.p.precedence >= self.q.precedence:
            needsbrackets == True


class And(Expr):
    precedence = 2
    def __str__(self):
        if self.needsbrackets == True:
            return '('+str(self.p)+'&'+str(self.q)+')'
        else:
            return "{}&{}".format(self.p, self.q)

class Or(Expr):
    precedence = 1
    def __str__(self):
        if self.needsbrackets == True:
            return '('+str(self.p)+'|'+str(self.q)+')'
        else:
            return "{}|{}".format(self.p, self.q)

class Not(Expr):
    precedence = 3
    def __init__(self, something):
        self.val = something

    def __str__(self):
        if self.needsbrackets == True:
            return '('+'!'+str(self.q)+')'
        else:
            return "!{}".format(self.val)

class Var:
    precedence = 0
    def __init__(self, chary):
        self.chary = chary

    def __str__(self):
        return "{}".format(self.chary)

    def eval(self, log):
        return self.chary

class Dict(object):

    def fromkeys(klass, iterable, value=None):
        "Emulate dict_fromkeys() in Objects/dictobject.c"
        d = klass()
        for key in iterable:
            d[key] = value
        return d
    fromkeys = classmethod(fromkeys)


#Equiv gives: x&z|!x&!z
#e3 should give: !(x&y)&(!x|!y)|!!(x&y)&!(!x|!y)

e = Var("x"), Var("z")

e1 = Or(Var("x"),Not(Var("x")))
def Equiv(p,q) :
    return Or(And(p,q),And(Not(p),Not(q)))
e2 = Equiv(Var("x"),Not(Not(Var("x"))))
e3 = Equiv(Not(And(Var("x"),Var("y"))),Or(Not(Var("x")),Not(Var("y"))))
e4 = Equiv(Not(And(Var("x"),Var("y"))),And(Not(Var("x")),Not(Var("y"))))

log = {"x" : 1, "y" : 2}

'''
from sympy.logic.inference import satisfiable
from sympy import Symbol
x = Symbol('x')
y = Symbol('y')
satisfiable(...)'''

def isTauto(f) :

    for x in [True,False] :
        for y in [True,False] :
            if not f(x,y) :
                return False
    return True