Skip to content

Instantly share code, notes, and snippets.

@MarisaKirisame
Created July 31, 2018 14:09
Show Gist options
  • Save MarisaKirisame/72f8c2b42b01a87d8506673a80709966 to your computer and use it in GitHub Desktop.
Save MarisaKirisame/72f8c2b42b01a87d8506673a80709966 to your computer and use it in GitHub Desktop.
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment