2021-05-17 00:33:41 +02:00
from sys import argv
from pathlib import Path
2021-05-17 18:39:28 +02:00
from common import printc , printerr , replaceContent
import Graph
2021-05-17 00:33:41 +02:00
# Increase if hasse diagram becomes too clobbered
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 ) )
2021-05-17 18:39:28 +02:00
def textLatex ( string ) :
return ' \\ text { ' + string + ' } '
def mathModeListLatex ( elements ) :
if len ( elements ) > 7 or len ( elements ) and max ( len ( str ( e ) ) for e in elements ) > 10 :
return ' \\ begin { gather*} \n ' \
+ ' \\ \\ \n ' . join ( elements ) + ' \n ' \
+ ' \\ end { gather*} '
else :
return f ' \\ [ { " , " . join ( elements ) } \\ ] '
2021-05-17 00:33:41 +02:00
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 ) :
2021-05-17 18:39:28 +02:00
relations = ( stringToPair ( x ) for x in string . split ( ' ' ) )
2021-05-17 00:33:41 +02:00
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 )
2021-05-17 18:39:28 +02:00
def isReflexive ( self , verbose = False ) :
2021-05-17 00:33:41 +02:00
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 ) } \\ ] ' )
2021-05-17 18:39:28 +02:00
if verbose :
return ( False , missingPairs )
if verbose :
return ( True , [ ( x , x ) for x in elements if ( x , x ) in self . pairs ] )
2021-05-17 00:33:41 +02:00
return result
2021-05-17 18:39:28 +02:00
def isSymmetric ( self , verbose = False ) :
2021-05-17 00:33:41 +02:00
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 ) } \\ ] ' )
2021-05-17 18:39:28 +02:00
if verbose :
return ( False , missingPairs )
if verbose :
return ( True , [ ( ( x , y ) , ( y , x ) ) for x , y in self . pairs if ( y , x ) in self . pairs and x < y ] )
2021-05-17 00:33:41 +02:00
return result
2021-05-17 18:39:28 +02:00
def isAntiSymmetric ( self , verbose = False ) :
2021-05-17 00:33:41 +02:00
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 ]
2021-05-17 18:39:28 +02:00
print ( f ' \\ [ { " , " . join ( f """ { pairToString ( p ) } { textLatex ( " and " ) } { pairToString ( q ) } """ for p , q in symmetricPairs ) } \\ ] ' )
if verbose :
return ( False , symmetricPairs )
if verbose :
return ( True , [ ] )
2021-05-17 00:33:41 +02:00
return result
2021-05-17 18:39:28 +02:00
def isTransitive ( self , verbose = False ) :
2021-05-17 00:33:41 +02:00
result = True
2021-05-17 18:39:28 +02:00
transitivePairs = [ ]
2021-05-17 00:33:41 +02:00
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
2021-05-17 18:39:28 +02:00
elif ( y == z and x != y != w and ( ( x , w ) in self . pairs ) ) :
transitivePairs . append ( ( ( x , y ) , ( z , w ) ) )
2021-05-17 00:33:41 +02:00
if not result :
printc ( ' Not transitive, following pairs are missing its transitive counterpart: ' , color = ' green ' )
2021-05-17 18:39:28 +02:00
print ( f ' \\ [ { " , " . join ( f """ { pairToString ( p ) } { textLatex ( " and " ) } { pairToString ( q ) } { textLatex ( " without " ) } { pairToString ( ( p [ 0 ] , q [ 1 ] ) ) } """ for p , q in nonTransitivePairs ) } \\ ] ' )
if verbose :
return ( False , nonTransitivePairs )
if verbose :
return ( True , transitivePairs )
2021-05-17 00:33:41 +02:00
return result
2021-05-17 18:39:28 +02:00
def isEquivalenceRelation ( self , verbose = False ) :
if verbose :
isReflexive , reflexivePairs = self . isReflexive ( verbose = True )
isSymmetric , symmetricPairs = self . isSymmetric ( verbose = True )
isTransitive , transitivePairs = self . isTransitive ( verbose = True )
if not isReflexive :
return ' The relation is not an equivalence relation, because it is not reflexive. '
+ ' The following elements should be related: \n \n '
+ f ' \\ [ { " , " . join ( pairToString ( p ) for p in reflexivePairs ) } \\ ] '
if not isSymmetric :
return ' The relation is not an equivalence relation, because it is not symmetric. '
+ ' It is missing the following symmetric pairs of relations \n \n '
+ f ' \\ [ { " , " . join ( f """ { pairToString ( p ) } { textLatex ( " and " ) } { pairToString ( q ) } """ for p , q in symmetricPairs ) } \\ ] '
if not isTransitive :
return ' The relation is not an equivalence relation, because it is not transitive. '
+ ' The following pairs of relations are missing its transitive counterpart \n \n '
+ f ' \\ [ { " , " . join ( f """ { pairToString ( p ) } { textLatex ( " and " ) } { pairToString ( q ) } { textLatex ( " without " ) } { pairToString ( ( p [ 0 ] , q [ 1 ] ) ) } """ for p , q in transitivePairs ) } \\ ] '
rxStr = mathModeListLatex ( [ pairToString ( p ) for p in reflexivePairs ] )
smStr = mathModeListLatex ( [ f """ { pairToString ( p ) } { textLatex ( " and " ) } { pairToString ( q ) } """ for p , q in symmetricPairs ] )
trStr = mathModeListLatex ( [ f """ { pairToString ( p ) } { textLatex ( " and " ) } { pairToString ( q ) } { textLatex ( " with " ) } { pairToString ( ( p [ 0 ] , q [ 1 ] ) ) } """ for p , q in transitivePairs ] )
return replaceContent (
( rxStr , smStr , trStr ) ,
' Relations/EquivalenceProof ' ,
lambda temp , cont : temp . replace ( ' % REFLEXIVE ' , cont [ 0 ] ) . replace ( ' % SYMMETRIC ' , cont [ 1 ] ) . replace ( ' % TRANSITIVE ' , cont [ 2 ] )
)
2021-05-17 00:33:41 +02:00
return self . isReflexive ( ) and self . isSymmetric ( ) and self . isTransitive ( )
2021-05-17 18:39:28 +02:00
def isPartialOrder ( self , verbose = False ) :
result = self . isReflexive ( ) and self . isAntiSymmetric ( ) and self . isTransitive ( )
if result :
hasse = self . getHassePairs ( checkIfPartialOrder = False )
min_el = set ( a for a , b in hasse if a not in list ( zip ( * hasse ) ) [ 1 ] )
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 ) } \ }} $ " )
if verbose :
isReflexive , reflexivePairs = self . isReflexive ( verbose = True )
isAntiSymmetric , antiSymmetricPairs = self . isAntiSymmetric ( verbose = True )
isTransitive , transitivePairs = self . isTransitive ( verbose = True )
if not isReflexive :
return ' The relation is not a partial order, because it is not reflexive. '
+ ' The following elements should be related: \n \n '
+ f ' \\ [ { " , " . join ( pairToString ( p ) for p in reflexivePairs ) } \\ ] '
if not isAntiSymmetric :
return ' The relation is not a partial order, because it is not antisymmetric. '
+ ' The following relations are symmetric \n \n '
+ f ' \\ [ { " , " . join ( f """ { pairToString ( p ) } { textLatex ( " and " ) } { pairToString ( q ) } """ for p , q in antiSymmetricPairs ) } \\ ] '
if not isTransitive :
return ' The relation is not a partial order, because it is not transitive. '
+ ' The following pairs of relations are missing its transitive counterpart \n \n '
+ f ' \\ [ { " , " . join ( f """ { pairToString ( p ) } { textLatex ( " and " ) } { pairToString ( q ) } { textLatex ( " without " ) } { pairToString ( ( p [ 0 ] , q [ 1 ] ) ) } """ for p , q in transitivePairs ) } \\ ] '
rxStr = mathModeListLatex ( [ pairToString ( p ) for p in reflexivePairs ] )
trStr = mathModeListLatex ( [ f """ { pairToString ( p ) } { textLatex ( " and " ) } { pairToString ( q ) } { textLatex ( " with " ) } { pairToString ( ( p [ 0 ] , q [ 1 ] ) ) } """ for p , q in transitivePairs ] )
return replaceContent (
( rxStr , trStr ) ,
' Relations/PosetProof ' ,
lambda temp , cont : temp . replace ( ' % REFLEXIVE ' , cont [ 0 ] ) . replace ( ' % TRANSITIVE ' , cont [ 1 ] )
)
return result
def getHassePairs ( self , checkIfPartialOrder = True ) :
if checkIfPartialOrder and not self . isPartialOrder ( ) :
2021-05-17 00:33:41 +02:00
printerr ( ' This is not a partial order ' )
return
2021-05-17 18:39:28 +02:00
nonReflexivePairs = set ( ( x , y ) for x , y in self . pairs if x != y )
2021-05-17 00:33:41 +02:00
hassePairs = set ( )
2021-05-17 18:39:28 +02:00
for x1 , y1 in nonReflexivePairs :
for x2 , y2 in nonReflexivePairs :
2021-05-17 00:33:41 +02:00
if y1 == x2 :
hassePairs . add ( ( x1 , y2 ) )
2021-05-17 18:39:28 +02:00
return nonReflexivePairs - hassePairs
2021-05-17 00:33:41 +02:00
def latexifyHasseDiagram ( self ) :
hasse = self . getHassePairs ( )
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 ] ) :
2021-05-17 18:39:28 +02:00
output . append ( f ' \\ node ( { n } ) at ( { i - len ( inv_ypos [ y ] ) / 2 } , { y * 0.5 * ( len ( hasse ) * * 0.4 ) } ) {{ $ { n } $ }} ; ' )
2021-05-17 00:33:41 +02:00
output . append ( ' ' )
for x , y in hasse :
output . append ( f ' \\ draw ( { x } ) -- ( { y } ); ' )
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
2021-05-17 18:39:28 +02:00
nodes = set ( )
for x , y in pairs :
nodes . add ( x )
nodes . add ( y )
2021-05-17 00:33:41 +02:00
2021-05-17 18:39:28 +02:00
edges = " \n " . join ( pairToString ( p ) for p in pairs )
processingString = f ' toGraph \n \n { graphType } \n \n { " " . join ( nodes ) } \n \n { edges } '
return Graph . processFileContent ( processingString )
2021-05-17 00:33:41 +02:00
2021-05-17 18:39:28 +02:00
def processFileContent ( raw ) :
2021-05-17 00:33:41 +02:00
outputType , inp = raw . split ( ' \n \n ' )
2021-05-17 18:39:28 +02:00
if inp . startswith ( ' divisibilityPosetTo ' ) :
2021-05-17 00:33:41 +02:00
n = int ( inp . split ( ' ' ) [ 1 ] )
relation = Relation . fromDivisibilityPosetTo ( n )
else :
relation = Relation . fromString ( inp )
if outputType == ' proveEquivalence ' :
2021-05-17 18:39:28 +02:00
content = relation . isEquivalenceRelation ( verbose = True )
return content
2021-05-17 00:33:41 +02:00
elif outputType == ' provePoset ' :
2021-05-17 18:39:28 +02:00
content = relation . isPartialOrder ( verbose = True )
return content
2021-05-17 00:33:41 +02:00
elif outputType == ' hasseDiagram ' :
content = relation . latexifyHasseDiagram ( )
2021-05-17 18:39:28 +02:00
return replaceContent ( content , ' Relations/Hasse ' )
2021-05-17 00:33:41 +02:00
elif outputType == ' graph ' :
content = relation . latexifyGraph ( )
2021-05-17 18:39:28 +02:00
return content
2021-05-17 00:33:41 +02:00
if __name__ == ' __main__ ' :
2021-05-17 18:39:28 +02:00
pass
# 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())