logic.py

class LVal: # logical value. store fact we know about a logical variable
    pass

class Unknown(LVal): # we dont know it's value
    pass

class Known(LVal): # we know it's value
    def __init__(self, x):
        self.x = x

class EqualTo(LVal): # we know it's equal to another lvar, which might become known at some stage
    def __init__(self, eq_to):
        assert isinstance(eq_to, LVar)
        assert isinstance(eq_to.lval, Unknown)
        self.eq_to = eq_to

class LVar: # logical variable
    def __init__(self, lval=Unknown()):
        assert isinstance(lval, LVal)
        self.lval = lval

    def deduce(self):
        while isinstance(self.lval, EqualTo) and self.lval.eq_to != self and not isinstance(self.lval.eq_to.lval, Unknown):
            self.lval = self.lval.eq_to.lval
        if isinstance(self.lval, EqualTo) and self.lval.eq_to == self:
            self.lval = Unknown

    def unify(self, rhs):
        assert isinstance(rhs, LVar)
        self.deduce()
        rhs.deduce()
        if isinstance(self.lval, Unknown):
            if isinstance(rhs.lval, Unknown):
                self.lval = EqualTo(rhs)
            elif isinstance(rhs.lval, Known):
                self.lval = Known(rhs)
            else:
                assert isinstance(rhs.lval, EqualTo)
                assert isinstance(rhs.lval.eq_to.lval, Unknown)
                self.lval = EqualTo(rhs.lval.eq_to)
        elif isinstance(self.lval, Known):
            if isinstance(rhs.lval, Unknown):
                rhs.unify(self)
            elif isinstance(rhs.lval, Known):
                if self.lval.x != rhs.lval.x:
                    raise Exception("unification error")
            else:
                assert isinstance(rhs.lval, EqualTo)
                assert isinstance(rhs.lval.eq_to.lval, Unknown)
                rhs.lval.eq_to.lval = self.lval
        else:
            assert isinstance(self.lval, EqualTo)
            assert isinstance(self.lval.eq_to.lval, Unknown)
            if isinstance(rhs.lval, Unknown):
                rhs.unify(self)
            elif isinstance(rhs.lval, Known):
                rhs.unify(self)
            else:
                assert isinstance(rhs.lval, EqualTo)
                assert isinstance(rhs.lval.eq_to.lval, Unknown)
                rhs.lval.eq_to.lval = self.lval