183 lines
5.5 KiB
Python
183 lines
5.5 KiB
Python
|
from sys import argv
|
||
|
from pathlib import Path
|
||
|
|
||
|
from common import printc, printerr
|
||
|
from Graph import Graph
|
||
|
|
||
|
# Increase if hasse diagram becomes too clobbered
|
||
|
HEIGHT_SEPARATOR = 1
|
||
|
|
||
|
def pairToString(pair):
|
||
|
if str(pair[0]).isdigit() or str(pair[1]).isdigit():
|
||
|
return f'({pair[0]},{pair[1]})'
|
||
|
else:
|
||
|
return pair[0] + pair[1]
|
||
|
|
||
|
def stringToPair(string):
|
||
|
if string[0] == '(':
|
||
|
return tuple(string.split(',')[0][1:], string.split(',')[0][:-1])
|
||
|
else:
|
||
|
return tuple(list(string))
|
||
|
|
||
|
|
||
|
class Relation:
|
||
|
def __init__(self, pairs): # pair = (str,str)
|
||
|
self.pairs = set(pairs)
|
||
|
|
||
|
def __str__(self):
|
||
|
return f'\\{{ {", ".join(x + y for x,y in self.pairs)} \}}'
|
||
|
|
||
|
@classmethod
|
||
|
def fromString(cls, string):
|
||
|
relations = (stringToPair(x) for x in relations.split(' '))
|
||
|
return cls(relations)
|
||
|
|
||
|
@classmethod
|
||
|
def fromDivisibilityPosetTo(cls, n):
|
||
|
pairs = set()
|
||
|
for dst in range(n):
|
||
|
pairs.add((dst, dst))
|
||
|
for src in range(1, dst):
|
||
|
if dst % src == 0:
|
||
|
pairs.add((src, dst))
|
||
|
return cls(pairs)
|
||
|
|
||
|
|
||
|
def isReflexive(self):
|
||
|
elements = set(list(sum(self.pairs, ())))
|
||
|
result = all((x,x) in self.pairs for x in elements)
|
||
|
|
||
|
if not result:
|
||
|
printc('Not reflexive, missing following pairs:', color='green')
|
||
|
missingPairs = [(x,x) for x in elements if (x,x) not in self.pairs]
|
||
|
print(f'\\[ {", ".join(pairToString(p) for p in missingPairs)} \\]')
|
||
|
|
||
|
return result
|
||
|
|
||
|
def isSymmetric(self):
|
||
|
result = all((y,x) in self.pairs for x,y in self.pairs)
|
||
|
|
||
|
if not result:
|
||
|
printc('Not symmetric, missing following pairs:', color='green')
|
||
|
missingPairs = [(x,y) for x,y in self.pairs if (y,x) not in self.pairs]
|
||
|
print(f'\\[ {", ".join(pairToString(p) for p in missingPairs)} \\]')
|
||
|
|
||
|
return result
|
||
|
|
||
|
def isAntiSymmetric(self):
|
||
|
result = not any((y,x) in self.pairs and y != x for x,y in self.pairs)
|
||
|
|
||
|
if not result:
|
||
|
printc('Not antisymmetric, following pairs are symmetric:', color='green')
|
||
|
symmetricPairs = [((x,y), (y,x)) for x,y in self.pairs if (y,x) in self.pairs and y > x]
|
||
|
print(f'\\[ {", ".join(f"{pairToString(p)} and {pairToString(q)}" for p,q in symmetricPairs)} \\]')
|
||
|
|
||
|
return result
|
||
|
|
||
|
def isTransitive(self):
|
||
|
result = True
|
||
|
nonTransitivePairs = []
|
||
|
|
||
|
for x,y in self.pairs:
|
||
|
for z,w in self.pairs:
|
||
|
if not (y != z or ((x,w) in self.pairs)):
|
||
|
nonTransitivePairs.append(((x,y), (z,w)))
|
||
|
result = False
|
||
|
|
||
|
if not result:
|
||
|
printc('Not transitive, following pairs are missing its transitive counterpart:', color='green')
|
||
|
print(f'\\[ {", ".join(f"{pairToString(p)} and {pairToString(q)} without {pairToString((p[0], q[1]))}" for p,q in nonTransitivePairs)} \\]')
|
||
|
|
||
|
return result
|
||
|
|
||
|
def isEquivalenceRelation(self):
|
||
|
return self.isReflexive() and self.isSymmetric() and self.isTransitive()
|
||
|
|
||
|
def isPartialOrder(self):
|
||
|
return self.isReflexive() and self.isAntiSymmetric() and self.isTransitive()
|
||
|
|
||
|
def getHassePairs(self):
|
||
|
if not self.isPartialOrder():
|
||
|
printerr('This is not a partial order')
|
||
|
return
|
||
|
hassePairs = set()
|
||
|
for x1, y1 in self.pairs:
|
||
|
for x2, y2 in self.pairs:
|
||
|
if y1 == x2:
|
||
|
hassePairs.add((x1, y2))
|
||
|
return self.pairs - hassePairs
|
||
|
|
||
|
def latexifyHasseDiagram(self):
|
||
|
hasse = self.getHassePairs()
|
||
|
min_el = set(a for a,b in hasse if a not in list(zip(*hasse))[1])
|
||
|
keys = set(item for tup in hasse for item in tup)
|
||
|
y_pos = dict.fromkeys(keys, 0)
|
||
|
|
||
|
i = 0
|
||
|
while len(next_row := [val for key,val in hasse if key in [x for x,y in y_pos.items() if y == i] ]) != 0:
|
||
|
for item in next_row:
|
||
|
y_pos[item] = i + 1
|
||
|
i += 1
|
||
|
|
||
|
inv_ypos = dict()
|
||
|
for key in set(y_pos.values()):
|
||
|
inv_ypos[key] = [x for x,y in y_pos.items() if y == key]
|
||
|
|
||
|
output = []
|
||
|
|
||
|
for y in inv_ypos.keys():
|
||
|
for i, n in enumerate(inv_ypos[y]):
|
||
|
output.append(f'\\node ({n}) at ({i - len(inv_ypos[y])/2}, {y * HEIGHT_SEPARATOR}) {{${n}$}};')
|
||
|
|
||
|
output.append('')
|
||
|
|
||
|
for x,y in hasse:
|
||
|
output.append(f'\\draw ({x}) -- ({y});')
|
||
|
|
||
|
|
||
|
printc(f"Minimal elements: $\{{ {', '.join(str(e) for e in min_el)} \}}$ \\\\")
|
||
|
|
||
|
max_el = set(v for k,v in hasse if v not in (x for x,_ in hasse))
|
||
|
printc(f"Maximal elements: $\{{ {', '.join(str(e) for e in max_el)} \}}$" )
|
||
|
|
||
|
return '\n'.join(output)
|
||
|
|
||
|
def latexifyGraph(self):
|
||
|
if self.isEquivalenceRelation():
|
||
|
graphType = 'undirected'
|
||
|
pairs = [(x,y) for x,y in self.pairs if x != y]
|
||
|
else:
|
||
|
graphType = 'directed'
|
||
|
pairs = self.pairs
|
||
|
|
||
|
pass
|
||
|
|
||
|
|
||
|
def processFileContent(raw, template):
|
||
|
outputType, inp = raw.split('\n\n')
|
||
|
|
||
|
if inp.startsWith('divisibilityPosetTo'):
|
||
|
n = int(inp.split(' ')[1])
|
||
|
relation = Relation.fromDivisibilityPosetTo(n)
|
||
|
else:
|
||
|
relation = Relation.fromString(inp)
|
||
|
|
||
|
if outputType == 'proveEquivalence':
|
||
|
content = relation.isEquivalenceRelation()
|
||
|
elif outputType == 'provePoset':
|
||
|
content = relation.isPartialOrder()
|
||
|
elif outputType == 'hasseDiagram':
|
||
|
content = relation.latexifyHasseDiagram()
|
||
|
elif outputType == 'graph':
|
||
|
content = relation.latexifyGraph()
|
||
|
|
||
|
content = Relation.fromString(raw).latexifyHasseDiagram()
|
||
|
return template.replace("%CONTENT", content)
|
||
|
|
||
|
if __name__ == '__main__':
|
||
|
inp = 'AA BB CC DD AB AC AD BC BD CD'
|
||
|
relations = [stringToPair(p) for p in inp.split(' ')]
|
||
|
# print(Relation(relations).isEquivalenceRelation())
|
||
|
print(Relation(relations).isPartialOrder())
|
||
|
print(Relation.fromDivisibilityPosetTo(30).isPartialOrder())
|