# ---
# jupyter:
#   jupytext:
#     text_representation:
#       extension: .py
#       format_name: light
#       format_version: '1.5'
#       jupytext_version: 1.14.4
#   kernelspec:
#     display_name: Python 3 (Ubuntu Linux)
#     language: python
#     name: python3-ubuntu
#     resource_dir: /usr/local/share/jupyter/kernels/python3-ubuntu
# ---

from provers import *


# +
def uc2le(uc): 
    """return <= relation as a dict of sets"""
    us = {x:set([x]+uc[x]) for x in uc}
    done = False
    while not done:
        done = True
        for v0, v1s in us.items():
            old_len = len(v1s)
            for v2s in [us[v1] for v1 in v1s]:
                v1s |= v2s
            done = done and len(v1s) == old_len
    return us

def uc2p9(uc):
    le = uc2le(uc)
    print(le)
    return [(f"{i}<={j}" if j in le[i] else f"-({i}<={j})") for i in uc for j in uc]

def rn2p9(rn):
    return [f"-{i}={rn[i]}" for i in rn]

p92ltx={"u":"u","v":"v","w":"w","x":"x","y":"y","z":"z","c":"c","d":"d","e":"1","1":"1","0":"0","b":"\\bot","t":"\\top","f":"f","g":"g",
       "~":"\\sim","-":"-","dd":"\\diamond","bx":"\\box"," r ":"\\triangleright"," t ":"\\triangleleft","tr":"\\vartriangleright","tl":"\\vartriangleleft",
       "i":"^{-1}","c":"\\smallsmile","'":"'","^":"\\wedge"," v ":"\\vee","*":"\\cdot","/":"/","\\":"\\backslash",
       "+":"+","<-":"\\ominus"," o ":"\\circ","->":"\\to",
       "<=":"\\le",">=":"\\ge","=":"=","!=":"\\ne","&":"\\text{ and }","|":"\\text{ or }",
       " -> ":"\\implies","<->":"\\iff","all":"\\forall","exists":"\\exists"}

def uc2tikz(A):
    n = len(A['uc'])
    xy = A['xy']
    st = '\n\\begin{tikzpicture}\n'
    st += '\\node at(0,-1)[n]{$\\mathbf'+A['nm']+'$};\n'
    for i in range(n-1,-1,-1):
        st += '\\node({})at({},{})[label={}:${}$]'.format(i,xy[i][0],xy[i][1],'right' if xy[i][0]>0 else 'left',A['lb'][i])
        st += '{}'+''.join(['edge({})'.format(j) for j in A['uc'][i]])+';\n'
    return st + '\\end{tikzpicture}\n'

def latex_op(s,m,lb,rmbnds=True):
    if type(m)==list:
        if len(m)==0: return s+'=[]'
        base = list(reversed(range(1 if rmbnds else 0,len(m)-1 if rmbnds else len(m))))
        #print m,type(m[0])
        if type(m[0])==list:
            if len(m[0])==0: return s+'=[[]]'
            st = r'$\begin{array}{|c|'+"".join(['c' for i in base])+'|}\\hline\n'
            st += '\\W{'+p92ltx[s]+'}&'+'&'.join('\\W{'+lb[d]+'}' for d in base)+r'\\\hline'+'\n'
            for i in base: 
                st += lb[i]+'&'+'&'.join(('-' if m[i][j]==-1 \
                else '\\rd{'+lb[m[i][j]]+'}' if i==j and m[i][i]==i \
                else '\\g{'+lb[m[i][j]]+'}' if m[i][j]==m[j][i] and i<j \
                else lb[m[i][j]]) for j in base)+r'\\'+'\n'
            return st + '\\hline\n\\end{array}$'
        else: return ""
    else: return ''#latex_sym(s)+'='+(str(m) if m!=-1 else '')

def alg2latex(alg,nm,lb,rmbnds=True):
    ops = alg.operations.items()
    st = '\\ \n\\begin{tabular}[b]{c}\n'
    st += ''.join([latex_op(kv[0],kv[1],lb,rmbnds) for kv in ops])+'\\\\\n'
    st += r'$\mathbf{'+nm+r'}_{'+str(len(lb))+","+str(alg.index+1)+'}$\n'
    return st+'\\end{tabular}\n
'

# -

pos31={'uc':{0:[1],1:[],2:[]},
      #'rn':{0:1,1:0,2:2},
      'xy':{0:(0,0),1:(0,1),2:(1,.5)},
      'lb':{0:'a',1:'b',2:'c'},
      'nm':'{Pos}_{3,1}'}
pos41={'uc':{0:[2,3],1:[2,3],2:[],3:[]},
      #'rn':{0:1,1:0,2:2},
      'xy':{0:(0,0),1:(1,0),2:(0,1),3:(1,1)},
      'lb':{0:'a',1:'c',2:'b',3:'d'},
      'nm':'{Pos}_{4,1}'}
pos42={'uc':{0:[2],1:[2,3],2:[],3:[]},
      #'rn':{0:1,1:0,2:2},
      'xy':{0:(0,0),1:(1,0),2:(0,1),3:(1,1)},
      'lb':{0:'a',1:'c',2:'b',3:'d'},
      'nm':'{Pos}_{4,1}'}
pos43={'uc':{0:[2],1:[3],2:[],3:[]},
      #'rn':{0:1,1:0,2:2},
      'xy':{0:(0,0),1:(1,0),2:(0,1),3:(1,1)},
      'lb':{0:'a',1:'c',2:'b',3:'d'},
      'nm':'{Pos}_{4,1}'}
PoMag=['x<=x', 'x<=y & y<=x -> x=y', 'x<=y & y<=z -> x<=z', 
'(x<=y) -> ((x*z)<=(y*z))', '(x<=y) -> ((z*x)<=(z*y))']
Lr=['x*y<=z<->y<=x\ z']
R=Lr+['x*y<=z<->x<=z/y']
Sgrp=['((x*y)*z)=(x*(y*z))']
Mon=Sgrp+['(x*1)=x', '(1*x)=x']
rdct=pos31
ax=PoMag+Mon+uc2p9(rdct['uc'])#+rn2p9(rdct['rn'])
print(ax)
a=p9(ax,[],1000,1000,len(rdct['uc']))
print(a)
st=uc2tikz(rdct)
st+="".join(alg2latex(x,'PoMon',rdct['lb'],False) for x in a)
rdct=pos31
ax=PoMag+Sgrp+uc2p9(rdct['uc'])#+rn2p9(rdct['rn'])
print(ax)
a=p9(ax,[],1000,1000,len(rdct['uc']))
print(a)
st=uc2tikz(rdct)
st+="".join(alg2latex(x,'PoMon',rdct['lb'],False) for x in a)
rdct=pos41
ax=PoMag+Sgrp+Lr+uc2p9(rdct['uc'])#+rn2p9(rdct['rn'])
print(ax)
a=p9(ax,[],1000,1000,len(rdct['uc']))
print(a)
st+=uc2tikz(rdct)
st+="".join(alg2latex(x,'LrPoSgrp',rdct['lb'],False) for x in a)
rdct=pos42
ax=PoMag+Sgrp+Lr+uc2p9(rdct['uc'])#+rn2p9(rdct['rn'])
print(ax)
a=p9(ax,[],1000,1000,len(rdct['uc']))
print(a)
st+=uc2tikz(rdct)
st+="".join(alg2latex(x,'LrPoSgrp',rdct['lb'],False) for x in a)
rdct=pos43
ax=PoMag+Sgrp+Lr+uc2p9(rdct['uc'])#+rn2p9(rdct['rn'])
print(ax)
a=p9(ax,[],1000,1000,len(rdct['uc']))
print(a)
st+=uc2tikz(rdct)
st+="".join(alg2latex(x,'LrPoSgrp',rdct['lb'],False) for x in a)
print(st)



pos81={'uc':{0:[1,2],1:[3,4],2:[3,4],3:[5,6],4:[5,6],5:[7],6:[7],7:[]},
      'rn':{0:7,1:6,2:5,3:3,4:4,5:2,6:1,7:0},
      'xy':{0:(0,0),1:(-.5,1),2:(.5,1),3:(-.5,2),4:(.5,2),5:(.5,3),6:(-.5,3),7:(0,4)},
      'lb':{0:'0',1:'\\rn a',2:'\\rn b',3:'c',4:'d',5:'b',6:'a',7:'1'},
      'nm':'{InPos}_{8,1}'}
pos82={'uc':{0:[1],1:[2,3],2:[4,5],3:[4,5],4:[6],5:[6],6:[7],7:[]},
      'rn':{0:7,1:6,2:5,3:4,4:3,5:2,6:1,7:0},
      'xy':{0:(0,0),1:(0,1),2:(-.5,2),3:(.5,2),4:(.5,3),5:(-.5,3),6:(0,4),7:(0,5)},
      'lb':{0:'0',1:'\\rn a',2:'\\rn b',3:'\\rn c',4:'c',5:'b',6:'a',7:'1'},
      'nm':'{InPos}_{8,2}'}
D81={'uc':{0:[1],1:[2],2:[3,4],3:[5],4:[5],5:[6],6:[7],7:[]},
      'rn':{0:7,1:6,2:5,3:3,4:4,5:2,6:1,7:0},
      'xy':{0:(0,0),1:(0,1),2:(0,2),3:(-.5,3),4:(.5,3),5:(0,4),6:(0,5),7:(0,6)},
      'lb':{0:'0',1:'\\rn a',2:'\\rn b',3:'c',4:'d',5:'b',6:'a',7:'1'},
      'nm':'{InD}_{8,1}'}
InTo8={'uc':{0:[1],1:[2],2:[3],3:[4],4:[5],5:[6],6:[7],7:[]},
      'rn':{0:7,1:6,2:5,3:4,4:3,5:2,6:1,7:0},
      'xy':{0:(0,0),1:(0,1),2:(0,2),3:(0,3),4:(0,4),5:(0,5),6:(0,6),7:(0,7)},
      'lb':{0:'0',1:'\\rn a',2:'\\rn b',3:'\\rn c',4:'c',5:'b',6:'a',7:'1'},
      'nm':'{InTo}_{8}'}
Po=['x<=x', 'x<=y & y<=x -> x=y', 'x<=y & y<=z -> x<=z',]
InPocrim=['x<=x', 'x<=y & y<=x -> x=y', 'x<=y & y<=z -> x<=z', '-(-(x))=x', '((x*y)<=z) <-> (y<=-((-(z)*x)))', '((x*y)*z)=(x*(y*z))', '(x*y)=(y*x)', '(x*7)=x', 'x<=7']
CyInPorim=['x<=x', 'x<=y & y<=x -> x=y', 'x<=y & y<=z -> x<=z', '-(-(x))=x', '((x*y)<=z) <-> (y<=-((-(z)*x)))', '((x*y)<=z) <-> (x<=-((y*-(z))))', '((x*y)*z)=(x*(y*z))', '(x*e)=x', '(e*x)=x', 'x<=e', 'e=7']
ax=CyInPorim+uc2p9(pos81['uc'])+rn2p9(pos81['rn'])
print(ax)
a=p9(ax,[],1000,1000,8)
st=uc2tikz(pos81)
st+="".join(alg2latex(x,'CyInPorim',pos81['lb']) for x in a)
print(a)
rdct=D81
ax=CyInPorim+uc2p9(rdct['uc'])+rn2p9(rdct['rn'])
print(ax)
a=p9(ax,['x*y=y*x'],1000,1000,8)
st+=uc2tikz(rdct)
st+="".join(alg2latex(x,'CyIInDMon',rdct['lb']) for x in a)
print(a)
rdct=InTo8
ax=CyInPorim+uc2p9(rdct['uc'])+rn2p9(rdct['rn'])
print(ax)
a=p9(ax,['x*y=y*x'],1000,1000,8)
st+=uc2tikz(rdct)
st+="".join(alg2latex(x,'CyIInDMon',rdct['lb']) for x in a)
print(a)
ax=InPocrim+uc2p9(pos82['uc'])+rn2p9(pos82['rn'])
print(ax)
a=p9(ax,[],1000,1000,8)
st+=uc2tikz(pos82)
st+="".join(alg2latex(x,'InPocrim',pos82['lb']) for x in a)
print(st)

a



# +
#Python 2.7 program to draw in LaTeX/Tikz/PDF residuated lattices of size <=6
#<NAME> 2017-04-12

latex = r"""
\documentclass{amsart}
% process this file with LuaLaTeX to avoid memory errors

\usepackage{tikz}
\usepackage{pythontex}
\advance\textheight by 1.8in
\advance\textwidth by 2in
\advance\topmargin by -1in
\advance\oddsidemargin by -1in
\advance\evensidemargin by -1in
\title{Lattices of size up to 6}
\date{\today}
\begin{document}
\maketitle

\noindent
There are $1+1+1+2+5+15=25$ lattices with $\le 6$ elements.
In the list below, each lattice is named $B_k,C_n,D_{n,i}$ or $L_{n,i}$
depending on whether it is a Boolean algebra, a chain with $n\ge 3$ elements, 
a distributive lattice or
a nondistributive lattice with $n\ge 5$ elements. The number $i$ is an index that
enumerates nonisomorphic lattices of size $n$, in order
of increasing height, increasing width and decreasing number of lines.

\tikzstyle{every picture} = [scale=0.5]
\tikzstyle{every node} = [draw, fill=white, circle, inner sep=0pt, minimum size=5pt]
\tikzstyle{n} = [draw=none, rectangle, inner sep=0pt] %name style
\tikzstyle{i} = [draw, fill=black, circle, inner sep=0pt, minimum size=5pt] %idempotent
\tikzstyle{e} = [draw=none, rectangle, inner sep=0pt]
\tikzstyle{nci} = [draw, fill=black, rectangle, inner sep=0pt, minimum size=5pt]
\tikzstyle{nc} = [draw, fill=white, rectangle, inner sep=0pt, minimum size=5pt]

\setlength{\arraycolsep}{2pt}

%\begin{center}
\sloppy
"""

class Alg(object):
    def __init__(self, op={}, index=None, size=None, aut=[]):
        """
        Construct a finite algebra. The size of the algebra is the length of any nonconstant operation.

        INPUT:
            op -- a dictionary of operations on range(size).
                Entries are symbol:table pairs where symbol is a string 
                that denotes the operation symbol, e.g. 'cdot', and table is
                an n-dimensional array with entries from range(size).
                n >= 0 is the arity of the operation (not explicitly coded 
                but can be computed from the table).
            index -- a natural number giving the position of the algebra in a list
                of algebras
            aut -- an optional list of automorphisms (permutations of range(size))
        """
        self.op = op
        self.index = index
        self.size = size if size!=None else len(next(x for x in op.values() if type(x)==list))
        self.aut = aut

undefined = -1

def alg2latex(alg):
    ops = alg.op.items()
    st = r'$\begin{array}{|l|}\hline'+'\n'
    st += r'A_{'+str(alg.index)+'}'+\
        (r'\\|\text{Aut}(A)|='+str(len(self.aut)) if alg.aut!=[] else '')+'\\\\\n'
    st += '\\ '.join([latex_op(kv[0],kv[1]) for kv in ops])
    return st+r'\\\hline\end{array}$'

def latex_sym(s): return '\\'+s if s[0].isalpha() and len(s)>1 else s

def latex_op(s,m):
    if type(m)==list:
        if len(m)==0: return s+'=[]'
        base = range(len(m))
        #print m,type(m[0])
        if type(m[0])!=list:
            st = r'\begin{array}{c|c}'
            st += '&'+latex_sym(s)+r'\\\hline'+'\n'
            for i in base: st += str(i)+'&'+(str(m[i]) if m[i]!=undefined else '-')+r'\\'+'\n'
            return st + r'\end{array}'+'\n'
        else:
            if len(m[0])==0: return s+'=[[]]'
            st = r'\begin{array}{c|'+"".join(['c' for i in base])+r'}'
            st += latex_sym(s)+'&'+'&'.join(str(d) for d in base)+r'\\\hline'+'\n'
            #central = [i for i in base if all(m[i][j]==m[j][i] for j in base)]
            for i in base: 
                st += str(i)+'&'+'&'.join(('-' if m[i][j]==undefined \
                else '\\mathbf{'+str(m[i][j])+'}' if i==j and m[i][i]==i \
                else '\\textcolor{lightgray}{'+str(m[i][j])+'}' if m[i][j]==m[j][i] \
                else str(m[i][j])) for j in base)+r'\\'+'\n'
            return st + r'\end{array}'+'\n'
    else: return latex_sym(s)+'='+(str(m) if m!=undefined else '')

def permutations(m,n):
    """
    return Python generator for all permutations of {m,...,n-1}
    """
    p = [m+i for i in range(n-m)]
    yield p
    n = len(p)
    j = 1
    while j>=0:
        q = list(range(n))
        j = n-2
        while j>=0 and p[j]>p[j+1]: j = j-1
        if j>=0:
            for k in range(j): q[k] = p[k]
            k = n-1
            while p[j]>p[k]: k = k-1
            q[j] = p[k]
            i = n-1
            while i>j:
                q[i] = p[j+n-i]
                i = i-1
            q[j+n-k]=p[j]
            p = q
            yield q

def inverse_permutation(p):
    q = list(range(len(p)))
    for i in range(len(p)):
        q[p[i]]=i
    return q

def check_permutations(m):
    """
    If partial is false, return False if every completion of some isomorphic 
      copy q(m) of m will be lexicographically larger than m.
      Return True otherwise.
      Remove a permutation if 
    If partial is true,
    perms and invperms are lists of permuatations and their inverses
    pflags is an array of booleans deciding which perms still need to be checked
    pflags_list records which flags have been set (needed to restore on backtracking)
    For partial algebras, q is an isomorphism if m[i][j] defined ==> q[m[i][j]]=m[q[i]][q[j]]
    and the same must hold for the inverse qi
    """
    global perms, invperms, pflags, pflags_list
    base = range(len(m))
    for k in range(len(perms)):
        if pflags[k]:
            q = perms[k]
            qi = invperms[k]
            equal = True
            for i in base:
                for j in base:
                    mqi = m[qi[i]][qi[j]]
                    mij = m[i][j]
                    if mqi == undefined or mij != q[mqi]: equal = False
                    if mqi != undefined and q[mqi]<mij: return False
                    if mqi != undefined and mij != undefined and q[mqi]>mij: #get rid of q
                        pflags[k] = False
                        pflags_list += [k]
                    if not equal: break #equal means q[m[qi[i]][qi[j]]] == m[i][j] != undefined
                if not equal: break
    return True

def check_associativity(m,i,j):
    """
    This function may update the partial operation m.
    For an equation r(xyz)=m[s(xyz)][t(xyz)] 
      if lhs is defined and rhs is undefined, but s(xyz), t(xyz) are defined
      then assign m[s(xyz)][t(xyz)]=r(xyz) and add the pair (s(xyz),t(xyz)) to entries_list.
    Similarly for m[s(xyz)][t(xyz)]=r(xyz).
    Return False if both sides are defined but not equal.
    After trying all assignments, return True.
    This function can perhaps be made more efficient by using the values of i,j
    """
    global entries_list
    base = range(len(m))
    for x in base:
        for y in base:
            xy = m[x][y]
            if xy != undefined:
                for z in base:
                    xyz = m[xy][z];
                    if xyz != undefined:
                        yz = m[y][z]
                        if yz != undefined:
                            if m[x][yz] != undefined:
                                if xyz!=m[x][yz]: return False
                            else:
                                m[x][yz] = xyz
                                entries_list.append((x,yz))
                    else:
                        if m[y][z] != undefined and m[x][m[y][z]] != undefined:
                            m[xy][z] = m[x][m[y][z]]
                            entries_list.append((xy,z))
    return True

def check_commutativity(m,i,j):
    global entries_list
    if m[j][i]!=undefined:
        if m[j][i]!=m[i][j]: return False
    else:
        m[j][i] = m[i][j]    # since (i,j) is the first undefined position found, m[j][i] will always be undefined
        entries_list.append((j,i))
    return True

def is_partially_ordered(m,uc,le):
    n = len(m)
    for x in range(n):
        for y in uc[x]:
            for z in range(n):
                if m[x][z]>-1 and m[y][z]>-1 and le[m[x][z]][m[y][z]]==0:
                    return False
                if m[z][x]>-1 and m[z][y]>-1 and le[m[z][x]][m[z][y]]==0:
                    return False
    return True

def is_op_automorphism(m,q):
    n = len(m)
    for i in range(n):
        for j in range(n):
            if m[q[i]][q[j]]!=q[m[i][j]]: return False
    return True

def check_lattice_ordered(m,join):
    """
    Return False if partial optable  m  does not distribute over join
    Return True otherwise
    """
    global entries_list
    n = len(m)
    for x in range(n):
        for y in range(n):
            xy = m[x][y]
            if xy>-1:
                for z in range(n):
                    xz = m[x][z]
                    if xz>-1:
                        yz = join[y][z]
                        xyz = m[x][yz]
                        if xyz>-1:
                            if xyz!=join[xy][xz]: return False
                        else:
                            m[x][yz] = join[xy][xz]
                            entries_list.append((x,yz))
                    zy = m[z][y]
                    if zy>-1:
                        xz = join[x][z]
                        xyz = m[xz][y]
                        if xyz>-1:
                            if xyz!=join[xy][zy]: return False
                        else:
                            m[xz][y] = join[xy][zy]
                            entries_list.append((xz,y))
    return True

def check_divisible(m,down):
    """
    Return False if partial optable  m  is not divisible
    i.e. x<=y implies x=m[y][u]=m[v][y] for some u,v
    Return True otherwise
    Compute list S of elements in y-row (col).
    Compute k = |down[y] - S|.
    if k>#undefined in y-row, return False
    if #undefined=1 and k=1 let undefined = this elt.
    """
    global entries_list
    n = len(m)
    for y in range(n):
        S = set([m[y][u] for u in range(n) if m[y][u]>-1])
        E = set(down[y]).difference(S)
        U = [u for u in range(n) if m[y][u]==-1]
        if len(E)>len(U): return False
        if len(U)==1 and len(E)==1:
            m[y][U[0]] = E.pop()
            entries_list += [(y,U[0])]
    for y in range(n):
        S = set([m[u][y] for u in range(n) if m[u][y]>-1])
        E = set(down[y]).difference(S)
        U = [u for u in range(n) if m[u][y]==-1]
        if len(E)>len(U): return False
        if len(U)==1 and len(E)==1:
            m[U[0]][y] = E.pop()
            entries_list += [(U[0],y)]
    return True

def complete_l_operation(m,join,down,i,j,associative=False,commutative=False,divisible=False):
    """
    find next i,j where alg[i][j] = -1 = undefined; for each val=0..n-1
    set alg[i][j] = val, check axioms and permutations
    if ok, complete_ordered_operation(m,i,j+1) then restore and return
    """
    global algebra_list,entries_list,pflags,pflags_list,gl_index
    ok = True
    n = len(m)
    while ok and i<n:
        while j<n and m[i][j]>-1: j = j+1
        if j>=n:
            j = 0 
            i = i+1
        else: ok = False
    if ok:
        if check_lattice_ordered(m,join) and \
               (not divisible or check_divisible(m,down)):
            gl_index+=1
            algebra_list.append(Alg(op={'cdot':[x[:] for x in m],'vee':join},index=gl_index,size=n))
    else:
        for val in range(n):
            if all([join[x][i]!=i or m[x][j]==-1 or join[m[x][j]][val]==val \
                    for x in range(i)]) and \
               all([join[x][j]!=j or m[i][x]==-1 or join[m[i][x]][val]==val \
                    for x in range(j)]):
                ok = True
                el = len(entries_list)
                m[i][j] = val
                entries_list += [(i,j)]
                if commutative:
                    m[j][i] = val
                    entries_list += [(j,i)]
                if ok: ok = check_lattice_ordered(m,join)
                if ok and divisible: ok = check_divisible(m,down)
                if ok and associative: ok = check_associativity(m,i,j)
                pl = len(pflags_list)
                if ok: ok = check_permutations(m)
                if ok: complete_l_operation(m,join,down,i,j+1,associative,commutative,divisible)
                while len(entries_list)>el:
                    e = entries_list.pop()
                    m[e[0]][e[1]] = -1
                while len(pflags_list)>pl:
                    p = pflags_list.pop()
                    pflags[p] = True

def downsets(lat):
        n = lat.size
        jn = lat.op['vee']
        down = [[x for x in range(n) if jn[x][y]==y] for y in range(n)]
        return down

def find_l_groupoids(l,associative=False,commutative=False,divisible=False,idempotent=False,identity=False,id=None,zero=False):
    """
    Return list of lattice ordered groupoids of lattice  l  as nxn matrices.
    The lattice is given by the join table.
    The operation is compatible with the order.
    """
    global algebra_list,perms,invperms,entries_list,pflags,pflags_list
    algebra_list=[]
    entries_list=[]
    n = l.size
    join = l.op['vee']
    down = downsets(l)
    m = [[-1 for x in range(n)] for x in range(n)]
    perms = [[0]+p+[n-1] for p in permutations(1,n-1) \
             if is_op_automorphism(join,[0]+p+[n-1])] if zero else \
             [p+[n-1] for p in permutations(0,n-1) \
             if is_op_automorphism(join,p+[n-1])]
    if idempotent:
        for x in range(n):
            m[x][x] = x
    if zero:
        #perms = [[0]+p for p in permutations(1,n)]
        for x in range(n):
            m[x][0] = 0
            m[0][x] = 0
    if identity:
        if id==None: #should only try all canconical identity positions
            t = n
            if zero and n>1: s = 1
            else: s = 0
        else: s = id; t = id+1
        for e in range(s,t):
            for x in range(n):
                m[e][x] = x
                m[x][e] = x
            perms = [[0]+p+[n-1] for p in permutations(1,n-1) \
                     if is_op_automorphism(join,[0]+p+[n-1])] if zero else \
                     [p+[n-1] for p in permutations(0,n-1) \
                     if is_op_automorphism(join,p+[n-1])]
            if all([p[e]>=e for p in perms]): # eliminate isomorphic (P,e)
                perms = [p for p in perms if p[e]==e] #keep e fixed
                invperms = [inverse_permutation(p) for p in perms]
                pflags = [True for i in range(len(perms))]
                pflags_list = []
                complete_l_operation(m,join,down,0,0,associative,commutative,divisible)
            for x in range(n):
                m[e][x] = -1
                m[x][e] = -1
    else:
        invperms = [inverse_permutation(p) for p in perms]
        pflags = [True for i in range(len(perms))]
        pflags_list = []
        complete_l_operation(m,join,down,0,0,associative,commutative,divisible)
    return algebra_list

def find_l_semigroups(l):
    return find_l_groupoids(l,associative=True)

def find_idempotent_semirings(n): #not correct
    alg_list = []
    for l in find_joinsemilattices(n):
        alg_list.extend(find_l_semigroups(l))
    return alg_list

def find_l_semigroups_with_zero(l,e=None):
    return find_l_groupoids(l,associative=True,id=e,zero=True)

def find_semirings0(n):
    alg_list = []
    for l in find_lattices(n):
        alg_list.extend(find_l_semigroups_with_zero(l))
    return alg_list

def find_commutative_l_semigroups(l):
    return find_l_groupoids(l,associative=True,commutative=True)

def find_l_bands(l):
    return find_l_groupoids(l,associative=True,idempotent=True)

def find_l_semilattices(l):
    return find_l_groupoids(l,associative=True,commutative=True,idempotent=True)

def find_l_monoids(l,e=None):
    return find_l_groupoids(l,associative=True,identity=True,id=e)

def find_idempotent_semirings_with_unit(n): #not correct
    alg_list = []
    for l in find_joinsemilattices(n):
        alg_list.extend(find_l_monoids(l))
    return alg_list

def find_commutative_l_monoids(l,e=None):
    return find_l_groupoids(l,associative=True,commutative=True,identity=True,id=e)

def find_commutative_idempotent_semirings_with_unit(n): #not correct
    alg_list = []
    for l in find_joinsemilattices(n):
        alg_list.extend(find_commutative_l_monoids(l))
    return alg_list

def find_l_monoids_with_zero(l,e=None):
    return find_l_groupoids(l,associative=True,identity=True,id=e,zero=True)

#a=Alg({"\\cdot":[[0,1],[1,-1]], "\\sim":[0,-1]},1)
#a.uc={0:[1],1:[]}
#a.pos=[(0,0),(0,1)]

lattices=[  # list of lattices of size up to 5
{'pos': {0: (0, 0)},
 'uc': {0: []}}, 
{'pos': {0: (0, 0), 1: (0, 1)},
 'uc': {0: [1], 1: []}}, 
{'pos': {0: (0, 0), 1: (0, 1), 2: (0, 2)},
 'uc':{0: [1], 1: [2], 2: []}}, 
{'pos': {0: (0, 0), 1: (0, 1), 2: (0, 2), 3:(0, 3)},
 'uc': {0: [1], 1: [2], 2: [3], 3: []}}, 
{'pos': {0: (0, 0), 1:(-1, 1), 2: (1, 1), 3: (0, 2)},
 'uc': {0: [1, 2], 1: [3], 2: [3], 3: []}}, 
{'pos': {0: (0, 0), 1: (0, 1), 2: (0, 2), 3: (0, 3), 4: (0, 4)},
 'uc': {0: [1], 1: [2], 2: [3], 3: [4], 4: []}}, 
{'pos': {0: (0, 0), 1: (-1, 1), 2: (1, 1), 3: (0, 2), 4: (0, 3)},
 'uc': {0: [1, 2], 1: [3], 2: [3], 3: [4], 4: []}}, 
{'pos': {0: (0, 0), 1: (0, 1), 2: (-1, 2), 3: (1, 2), 4: (0, 3)},
 'uc': {0: [1], 1: [2, 3], 2: [4], 3: [4], 4: []}},
{'pos': {0: (0, 0), 1: (1, 1), 2: (-1, 1.5), 3: (1, 2), 4: (0, 3)},
 'uc': {0: [2, 1], 1: [3], 2: [4], 3: [4], 4: []}}, 
{'pos': {0: (0, 0), 1: (-1, 1), 2: (0, 1), 3: (1, 1), 4: (0, 2)},
 'uc': {0: [1, 2, 3], 1: [4], 2: [4], 3: [4], 4: []}}, 
{'pos': {0: (0, 0), 1: (0, 1), 2: (0, 2), 3: (0, 3), 4: (0, 4), 5: (0, 5)},
 'uc': {0: [1], 1: [2], 2: [3], 3: [4], 4: [5], 5: []}}, 
{'pos': {0: (0, 0), 1: (-1, 1), 2: (1, 1), 3: (0, 2), 4: (0, 3), 5: (0, 4)},
 'uc': {0: [1, 2], 1: [3], 2: [3], 3: [4], 4: [5], 5: []}}, 
{'pos': {0: (0, 0), 1: (0, 1), 2: (-1, 2), 3: (1, 2), 4: (0, 3), 5: (0, 4)},
 'uc': {0: [1], 1: [2, 3], 2: [4], 3: [4], 4: [5], 5: []}},
{'pos': {0: (0, 0), 1: (0, 1), 2: (0, 2), 3: (-1, 3), 4: (1, 3), 5: (0, 4)},
 'uc': {0: [1], 1: [2], 2: [3, 4], 3: [5], 4: [5], 5: []}}, 
{'pos': {0: (0, 0), 1: (1, 1), 2: (-1, 2), 3: (1, 2), 4: (1, 3), 5: (0, 4)},
 'uc': {0: [2, 1], 1: [3], 2: [5], 3: [4], 4: [5], 5: []}},
{'pos': {0: (0, 0), 1: (1, 1), 2: (-1, 1.5), 3: (1, 2), 4: (0, 3), 5: (0, 4)},
 'uc': {0: [2, 1], 1: [3], 2: [4], 3: [4], 4: [5], 5: []}},
{'pos': {0: (0, 0), 1: (0, 1), 2: (1, 2), 3: (-1,2.5), 4: (1, 3), 5: (0, 4)},
 'uc': {0: [1], 1: [2, 3], 2: [4], 3: [5], 4: [5], 5: []}},
{'pos': {0:(-.5, 0), 1:(-1.5, 1), 2:(.5, 1), 3:(-.5, 2), 4:(1.5, 2), 5:(.5, 3)},
 'uc': {0: [1, 2], 1: [3], 2: [3, 4], 3: [5], 4: [5], 5: []}}, 
{'pos': {0: (0, 0), 1: (-1, 1), 2: (0, 1), 3: (1, 1), 4: (0, 2), 5: (0, 3)},
 'uc': {0: [1, 2, 3], 1: [4], 2: [4], 3: [4], 4: [5], 5: []}}, 
{'pos': {0: (0, 0), 1: (0, 1), 2: (-1, 2), 3: (0, 2), 4: (1, 2), 5: (0, 3)},
 'uc': {0: [1], 1: [2, 3, 4], 2: [5], 3: [5], 4: [5], 5: []}}, 
{'pos': {0: (0, 0), 1: (-1, 1), 2: (1, 1), 3: (-1, 2), 4: (1, 2), 5: (0, 3)},
 'uc': {0: [2, 1], 1: [3], 2: [4], 3: [5], 4: [5], 5: []}}, 
{'pos': {0: (0, 0), 1: (1, 1), 2: (-1, 1.5), 3: (0, 1.5), 4: (1, 2), 5: (0, 3)},
 'uc': {0: [2, 3, 1], 1: [4], 2: [5], 3: [5], 4: [5], 5: []}},
{'pos': {0: (0, 0), 1:(-.01, 1), 2: (1, 1), 3: (-1, 1.5), 4: (1, 2), 5: (0, 3)},
 'uc': {0: [3, 1, 2], 1: [4], 2: [4], 3: [5], 4: [5], 5: []}}, 
{'pos': {0: (0, 0), 1: (1, 1), 2: (-1, 1.5), 3:(-.01, 2), 4: (1, 2), 5: (0, 3)},
 'uc': {0: [2, 1], 1: [3, 4], 2: [5], 3: [5], 4: [5], 5: []}}, 
{'pos': {0:(0, 0), 1:(-1.5, 1), 2:(-0.5, 1), 3:(0.5, 1), 4:(1.5, 1), 5:(0, 2)},
 'uc': {0: [1, 2, 3, 4], 1: [5], 2: [5], 3: [5], 4: [5], 5: []}},
#jsl
{'uc':{0:[2],1:[2],2:[]}, 'pos': {0:(0,0),1:(1,0),2:(.5,1)}}, 
{'uc':{0:[3],1:[3],2:[3],3:[]}, 'pos': {0:(0,0),1:(.7,0),2:(1.4,0),3:(.7,1)}}, 
{'uc':{0:[2],1:[2],2:[3],3:[]}, 'pos': {0:(0,0),1:(1,0),2:(.5,1),3:(.5,2)}}, 
{'uc':{0:[1],1:[3],2:[3],3:[]}, 'pos': {0:(0,0),1:(0,1),2:(1,1),3:(.5,2)}},
#msl
{'uc':{0:[1,2],1:[],2:[]}, 'pos': {0:(0,0),1:(-.5,1),2:(.5,1)}},
{'uc':{0:[1,2,3],1:[],2:[],3:[]}, 'pos': {0:(0,0),1:(-.7,1),2:(0,1),3:(.7,1)}},
{'uc':{0:[1,2],1:[],2:[3],3:[]}, 'pos': {0:(0,0),1:(-.5,1),2:(.5,1),3:(.5,2)}},
{'uc':{0:[1],1:[2,3],2:[],3:[]}, 'pos': {0:(0,0),1:(0,1),2:(-.5,2),3:(.5,2)}},
#posets
{'uc':{0:[1],1:[],2:[]}, 'pos':{0:(0,0),1:(0,1),2:(.7,0)}},
{'uc':{0:[2,3],1:[2,3],2:[],3:[]}, 'pos':{0:(0,0),1:(1,0),2:(0,1),3:(1,1)}},
{'uc':{0:[2],1:[2,3],2:[],3:[]}, 'pos':{0:(0,0),1:(1,0),2:(0,1),3:(1,1)}},
{'uc':{0:[2],1:[3],2:[],3:[]}, 'pos':{0:(0,0),1:(1,0),2:(0,1),3:(1,1)}},
{'uc':{0:[2,3],1:[],2:[],3:[]}, 'pos':{0:(0,0),1:(.7,0),2:(-.5,1),3:(.5,1)}},
{'uc':{0:[2],1:[2],2:[],3:[]}, 'pos':{0:(0,0),1:(1,0),2:(.5,1),3:(1.7,0)}},
{'uc':{0:[1],1:[],2:[],3:[]}, 'pos':{0:(0,0),1:(0,1),2:(.7,0),3:(1.4,0)}},
{'uc':{0:[1],1:[2],2:[],3:[]}, 'pos':{0:(0,0),1:(0,1),2:(0,2),3:(.7,0)}},
]


def permuted_binary_op(m,q):
    qi = inverse_permutation(q)
    return [[q[m[qi[x]][qi[y]]] for y in range(len(m))] for x in range(len(m))]


def leq2uc(le): # assumes le[x][y] => x <= y (topologically sorted)
    n = len(le)
    uc = []
    for a in range(n):
        S = []   # accumulate upper covers of a
        for x in range(a+1,n):
            if le[a][x]==1:
                y = len(S)-1
                while y>=0 and le[S[y]][x]==0:
                    y = y-1
                if y<0: S.append(x)
        uc.append(S)
    return uc

class Posetuc(object):
    def __init__(self,uppercovers):
        self.uc = dict([(x,uppercovers[x]) for x in range(len(uppercovers))])

    def size(self):
        return len(self.uc)

    def get_leq(self):
        if hasattr(self,'leq'): return self.leq
        n = self.size()
        leq = [[0 for y in range(n)] for x in range(n)]
        for i in range(n):
            leq[i][i] = 1
            for j in self.uc[i]:
                leq[i][j] = 1
        for i in range(n):
            for j in range(i+1,n):
                if leq[i][j]:
                    for k in range(j+1,n):
                        if leq[j][k]: leq[i][k] = 1
        self.leq = leq
        return leq

    def get_join(self): # Freese-Jezek-Nation p217
        if hasattr(self,'join'): return self.join
        n = self.size()
        join = [[0 for x in range(n)] for x in range(n)]
        le = self.get_leq()
        if not all([le[x][n-1]==1 for x in range(n)]):
            return "poset has no top element"
        p = range(n-1,-1,-1)
        uc = [sorted([p[y] for y in self.uc[x]]) for x in p]
        S = []
        for x in range(n): # x=x_k
            join[x][x] = x
            for y in S:
                T = []
                for z in uc[x]:
                    T.append(join[y][z]) # T = {x_i \vee z : z>-x_k}
                q = T[0]
                for z in T[1:]:
                    if z>q: q = z #error in Listing 11.9
                for z in T:
                    if not le[p[q]][p[z]]:
                        return "poset is not a semilattice: x="+x+" y="+y
                join[x][y] = q
                join[y][x] = q
            S.append(x)
        self.join = permuted_binary_op(join,p)
        return self.join

    def get_meet(self): # Freese-Jezek-Nation p217
        if hasattr(self,'meet'): return self.meet
        n = self.size()
        meet = [[0 for x in range(n)] for x in range(n)]
        le = self.get_leq()
        if not all([le[0][x]==1 for x in range(n)]):
            return "poset has no bottom element"
        lc = self.get_lowercovers()
        S = []
        for x in range(n): # x=x_k
            meet[x][x] = x
            for y in S:
                T = []
                for z in lc[x]:
                    T.append(meet[y][z]) # T = {x_i \wedge z : z>-x_k}
                q = T[0]
                for z in T[1:]:
                    if z>q: q = z
                for z in T:
                    if not le[z][q]:
                        return "poset is not a semilattice: x="+x+" y="+y
                meet[x][y] = q
                meet[y][x] = q
            S.append(x)
        self.meet = meet
        return meet

    def get_lowercovers(self):
        if hasattr(self,'lc'): return self.lc
        lc = [[] for x in range(self.size())]
        for i in range(self.size()):
            for j in self.uc[i]:
                lc[j].append(i)
        self.lc = lc
        return lc

    def depths(self): # assumes P is topologically sorted
        l = [0 for x in range(len(self.uc))]
        lc = self.get_lowercovers()
        for i in range(len(self.uc)-1,-1,-1):
            for j in lc[i]:
                if l[j]<l[i]+1: l[j]=l[i]+1
        return l

def findid(m):
    for e in range(len(m)):
        if all(m[e][x]==x for x in range(len(m))): return e

def identitydepth(A):
    m = A.op["cdot"]
    jn = A.op["vee"]
    B = range(A.size)
    P = Posetuc(leq2uc([[1 if jn[x][y]==y else 0 for y in B] for x in B]))
    return P.depths()[findid(m)]+1

def idemdepths(A):
    m = A.op["cdot"]
    jn = A.op["vee"]
    B = range(A.size)
    P = Posetuc(leq2uc([[1 if jn[x][y]==y else 0 for y in B] for x in B]))
    d = P.depths()
    return sum(d[x] for x in B if m[x][x]==x)

def idempotents(A):
    m = A.op["cdot"]
    return [i for i in range(A.size) if m[i][i]==i]

def centrals(A):
    m = A.op["cdot"]
    B = range(A.size)
    return [i for i in B if all(m[i][j]==m[j][i] for j in B)]

def sortkey(A):
    return (identitydepth(A),A.size-len(centrals(A)),A.size-len(idempotents(A)),idemdepths(A))

def findLats(lat):
    global gl_index
    gl_index = 0
    p = Posetuc(lat["uc"])
    alg = Alg(index=0,size=len(p.uc))#op={"uc":p.uc})#"vee":p.get_join(),"wedge":p.get_meet()})
    alg.uc = p.uc
    return [alg]

RL = [findLats(x) for x in lattices]
print([len(x) for x in RL])

def join2uc(jn): # assumes jn[x][y]=y => x <= y (topologically sorted)
    n = len(jn)
    uc = []
    for a in range(n):
        S = []   # accumulate upper covers of a
        for x in range(a+1,n):
            if jn[a][x]==x:
                y = len(S)-1
                while y>=0 and jn[S[y]][x]!=x:
                    y = y-1
                if y<0: S.append(x)
        uc.append(S)
    return uc

def table2list(A,sym="cdot"):
    jn = A.op["vee"]
    m = A.op[sym]
    e = findid(m)
    n = A.size
    B = list(range(1,e))+list(range(e+1,n)) #assumes 0=bottom
    d = dict((x,[]) for x in range(n))
    p = A.pos
    for x in B:
        for y in B:
            if ((x>y and p[x][1]!=p[y][1]) or (x<y and p[x][1]==p[y][1]) \
                or (x==y and m[x][x]!=x) or m[x][y]!=m[y][x]) and \
                (x!=n-1 or y!=n-1):
                d[m[x][y]].append((x,y))
    for x in range(n):#filter z's that are max or min in d[x]
        d[x] = [z for z in d[x] if ((all(jn[y[0]][z[0]]!=z[0] or \
                jn[y[1]][z[1]]!=z[1] or y==z for y in d[x]) and x!=0) or \
                (all(jn[y[0]][z[0]]!=y[0] or jn[y[1]][z[1]]!=y[1] or y==z \
                     for y in d[x]) and x!=n-1)) and \
        (x!=m[x][x] or x!=z[1] or jn[z[0]][z[1]]!=z[0] or jn[z[0]][e]!=e) and \
        (x!=m[x][x] or x!=z[0] or jn[z[0]][z[1]]!=z[0] or jn[z[1]][e]!=z[1]) ]
        # not x^2=x=z[1]<=z[0]<=e and not e<=z[1]<=z[0]=x^2=x
    return d

def labels(A):
    m = A.op["cdot"]
    e = findid(m)
    n = A.size-1
    labstr=["a","b","c","d","e","f","g"]
    B = list(range(1,e))+list(range(e+1,n))
    elts = sorted(B,key=lambda i:(A.pos[i][1],-A.pos[i][0]))[::-1]
    labs = dict((elts[i],labstr[i]) for i in range(len(elts)))
    labs[0] = "\\bot "
    labs[A.size-1] = "\\top "
    equs = {}
    tl = table2list(A)
    for i in range(A.size):
        equs[i] = "{=}".join([labs[x[0]]+(labs[x[1]] if x[0]!=x[1] else "^2")\
                              for x in tl[i]])
    labs[0] = " "
    labs[A.size-1] = " "
    labs[e] = "1"
    for i in range(A.size):
        labs[i] += ("" if labs[i]==" " or equs[i]=="" else "{=}")+equs[i]
    return labs

def uc2tikz(A):
    n = A.size
    st = '\n\\quad\n\\begin{tikzpicture}[baseline=0pt]\n'
    st += '\\node at (0,-1)[n]{$R_{'+str(A.size)+','+str(A.latindex)+'}$};\n'
    st += '\\node at (0,-2)[n]{$ $};\n'
    longlabel = []
    for i in range(n-1,-1,-1):
        st += '\\node({}) at ({},{})'.format(i,A.pos[i][0],A.pos[i][1])
#        st += 'label='+('left' if A.pos[i][0]<0 else 'right')+':$'
#        if i==n-1 or i==0 or A.pos[i+1][1]>A.pos[i][1] or \
#           A.pos[i-1][1]<A.pos[i][1] or len(A.label[i])<=1:
#            st += A.label[i]
#        else:
#            st += A.label[i][:1]
#            longlabel.append(A.label[i])
        st += '{}'+''.join([' edge ({})'.format(j) for j in A.uc[i]])+';\n'
    return st + '\\end{tikzpicture}'

def drawLats(li,pos,latindex):
    st = ""
    c=0
    for i in range(len(li)):
        c+=1
        x=li[i]
        A=Alg(index=c,size=x.size)
        A.uc=x.uc #A.op["uc"]#join2uc(x.op["vee"])
        A.pos=pos
        A.latindex=latindex
        st += uc2tikz(A)
    return st

def savefile(fn,st):
    fh = open(fn,'w')
    fh.write(st)
    fh.close()

def main():
    global latex
    ind = 0
    si = 1
    for i in range(len(RL)):
        ind += 1
        if si<RL[i][0].size:
            si = RL[i][0].size
            ind = 1
        latex += drawLats(RL[i],lattices[i]["pos"],ind)
    latex += "%\\end{center}\n\\end{document}\n"
    savefile("Lat5.tex", latex)

main()


# +
#Python 2.7 program to draw in LaTeX/Tikz/PDF residuated lattices of size <=6
#<NAME> 2017-04-12

latex = r"""
\documentclass{amsart}
% process this file with LuaLaTeX to avoid memory errors

\usepackage{tikz}
\usepackage{pythontex}
\advance\textheight by 1.8in
\advance\textwidth by 2in
\advance\topmargin by -1in
\advance\oddsidemargin by -1in
\advance\evensidemargin by -1in
\title{Residuated lattices of size up to 6}
\author{<NAME>}
\author{<NAME>}
\date{\today}
\begin{document}
\maketitle

\noindent
There are $1+1+3+20+149+1488=1662$ residuated lattices with $\le 6$ elements.
In the list below, each algebra is named $R^{mn}_{ij}$ where $m$ is the 
cardinality and $n$ enumerates nonisomorphic lattices of size $m$, in order
of decreasing height. The depth of the identity element $1$ is given by $i$, 
and $j$ enumerates nonisomorphic algebras. For lattices of the same height
distributive lattices appear before modular lattices, followed by nonmodular
lattices, and selfdual lattices appear
before nonselfdual lattices. Algebras with more central elements (round 
circles) are listed earlier, hence commutative residuated lattices precede 
noncommutative ones. Finally, algebras are listed in decreasing order of 
number of idempotents (black nodes).

The monoid operation is indicated by labels. If a nonobvious product $xy$ 
is not listed, then it can be deduced from the given information: either
it follows from idempotence ($x^2=x$) indicated by a black node
or from commutativity or there are products $uv=wz$ such that
$u\le x\le w$ and $v\le y\le z$ (possibly $uv=\bot\bot$ or $wz=\top\top$).

If you have comments or notice any issues in this list, please 
email \texttt{jipsen.AT.chapman.edu}.

\tikzstyle{every picture} = [scale=0.5]
\tikzstyle{every node} = [draw, fill=white, circle, inner sep=0pt, minimum size=5pt]
\tikzstyle{n} = [draw=none, rectangle, inner sep=0pt] %name style
\tikzstyle{i} = [draw, fill=black, circle, inner sep=0pt, minimum size=5pt] %idempotent
\tikzstyle{e} = [draw=none, rectangle, inner sep=0pt]
\tikzstyle{nci} = [draw, fill=black, rectangle, inner sep=0pt, minimum size=5pt]
\tikzstyle{nc} = [draw, fill=white, rectangle, inner sep=0pt, minimum size=5pt]

\begin{tikzpicture}
\draw(0,1.4)node[label=right:{\ $=$ central nonidempotent}]{};
\draw(0,2.1)node[i,label=right:{\ $=$ central idempotent}]{};
\draw(0,0)node[nc,label=right:{\ $=$ noncentral nonidempotent}]{};
\draw(0,0.7)node[nci,label=right:{\ $=$ noncentral idempotent}]{};
\end{tikzpicture}

\setlength{\arraycolsep}{2pt}

%\begin{center}
\sloppy
"""

class Alg(object):
    def __init__(self, op={}, index=None, size=None, aut=[]):
        """
        Construct a finite algebra. The size of the algebra is the length of any nonconstant operation.

        INPUT:
            op -- a dictionary of operations on range(size).
                Entries are symbol:table pairs where symbol is a string 
                that denotes the operation symbol, e.g. 'cdot', and table is
                an n-dimensional array with entries from range(size).
                n >= 0 is the arity of the operation (not explicitly coded 
                but can be computed from the table).
            index -- a natural number giving the position of the algebra in a list
                of algebras
            aut -- an optional list of automorphisms (permutations of range(size))
        """
        self.op = op
        self.index = index
        self.size = size if size!=None else len(next(x for x in op.values() if type(x)==list))
        self.aut = aut

undefined = -1

def alg2latex(alg):
    ops = alg.op.items()
    st = r'$\begin{array}{|l|}\hline'+'\n'
    st += r'A_{'+str(alg.index)+'}'+\
        (r'\\|\text{Aut}(A)|='+str(len(self.aut)) if alg.aut!=[] else '')+'\\\\\n'
    st += '\\ '.join([latex_op(kv[0],kv[1]) for kv in ops])
    return st+r'\\\hline\end{array}$'

def latex_sym(s): return '\\'+s if s[0].isalpha() and len(s)>1 else s

def latex_op(s,m):
    if type(m)==list:
        if len(m)==0: return s+'=[]'
        base = range(len(m))
        #print m,type(m[0])
        if type(m[0])!=list:
            st = r'\begin{array}{c|c}'
            st += '&'+latex_sym(s)+r'\\\hline'+'\n'
            for i in base: st += str(i)+'&'+(str(m[i]) if m[i]!=undefined else '-')+r'\\'+'\n'
            return st + r'\end{array}'+'\n'
        else:
            if len(m[0])==0: return s+'=[[]]'
            st = r'\begin{array}{c|'+"".join(['c' for i in base])+r'}'
            st += latex_sym(s)+'&'+'&'.join(str(d) for d in base)+r'\\\hline'+'\n'
            #central = [i for i in base if all(m[i][j]==m[j][i] for j in base)]
            for i in base: 
                st += str(i)+'&'+'&'.join(('-' if m[i][j]==undefined \
                else '\\mathbf{'+str(m[i][j])+'}' if i==j and m[i][i]==i \
                else '\\textcolor{lightgray}{'+str(m[i][j])+'}' if m[i][j]==m[j][i] \
                else str(m[i][j])) for j in base)+r'\\'+'\n'
            return st + r'\end{array}'+'\n'
    else: return latex_sym(s)+'='+(str(m) if m!=undefined else '')

def permutations(m,n):
    """
    return Python generator for all permutations of {m,...,n-1}
    """
    p = [m+i for i in range(n-m)]
    yield p
    n = len(p)
    j = 1
    while j>=0:
        q = list(range(n))
        j = n-2
        while j>=0 and p[j]>p[j+1]: j = j-1
        if j>=0:
            for k in range(j): q[k] = p[k]
            k = n-1
            while p[j]>p[k]: k = k-1
            q[j] = p[k]
            i = n-1
            while i>j:
                q[i] = p[j+n-i]
                i = i-1
            q[j+n-k]=p[j]
            p = q
            yield q

def inverse_permutation(p):
    q = list(range(len(p)))
    for i in range(len(p)):
        q[p[i]]=i
    return q

def check_permutations(m):
    """
    If partial is false, return False if every completion of some isomorphic 
      copy q(m) of m will be lexicographically larger than m.
      Return True otherwise.
      Remove a permutation if 
    If partial is true,
    perms and invperms are lists of permuatations and their inverses
    pflags is an array of booleans deciding which perms still need to be checked
    pflags_list records which flags have been set (needed to restore on backtracking)
    For partial algebras, q is an isomorphism if m[i][j] defined ==> q[m[i][j]]=m[q[i]][q[j]]
    and the same must hold for the inverse qi
    """
    global perms, invperms, pflags, pflags_list
    base = range(len(m))
    for k in range(len(perms)):
        if pflags[k]:
            q = perms[k]
            qi = invperms[k]
            equal = True
            for i in base:
                for j in base:
                    mqi = m[qi[i]][qi[j]]
                    mij = m[i][j]
                    if mqi == undefined or mij != q[mqi]: equal = False
                    if mqi != undefined and q[mqi]<mij: return False
                    if mqi != undefined and mij != undefined and q[mqi]>mij: #get rid of q
                        pflags[k] = False
                        pflags_list += [k]
                    if not equal: break #equal means q[m[qi[i]][qi[j]]] == m[i][j] != undefined
                if not equal: break
    return True

def check_associativity(m,i,j):
    """
    This function may update the partial operation m.
    For an equation r(xyz)=m[s(xyz)][t(xyz)] 
      if lhs is defined and rhs is undefined, but s(xyz), t(xyz) are defined
      then assign m[s(xyz)][t(xyz)]=r(xyz) and add the pair (s(xyz),t(xyz)) to entries_list.
    Similarly for m[s(xyz)][t(xyz)]=r(xyz).
    Return False if both sides are defined but not equal.
    After trying all assignments, return True.
    This function can perhaps be made more efficient by using the values of i,j
    """
    global entries_list
    base = range(len(m))
    for x in base:
        for y in base:
            xy = m[x][y]
            if xy != undefined:
                for z in base:
                    xyz = m[xy][z];
                    if xyz != undefined:
                        yz = m[y][z]
                        if yz != undefined:
                            if m[x][yz] != undefined:
                                if xyz!=m[x][yz]: return False
                            else:
                                m[x][yz] = xyz
                                entries_list.append((x,yz))
                    else:
                        if m[y][z] != undefined and m[x][m[y][z]] != undefined:
                            m[xy][z] = m[x][m[y][z]]
                            entries_list.append((xy,z))
    return True

def check_commutativity(m,i,j):
    global entries_list
    if m[j][i]!=undefined:
        if m[j][i]!=m[i][j]: return False
    else:
        m[j][i] = m[i][j]    # since (i,j) is the first undefined position found, m[j][i] will always be undefined
        entries_list.append((j,i))
    return True

def is_partially_ordered(m,uc,le):
    n = len(m)
    for x in range(n):
        for y in uc[x]:
            for z in range(n):
                if m[x][z]>-1 and m[y][z]>-1 and le[m[x][z]][m[y][z]]==0:
                    return False
                if m[z][x]>-1 and m[z][y]>-1 and le[m[z][x]][m[z][y]]==0:
                    return False
    return True

def is_op_automorphism(m,q):
    n = len(m)
    for i in range(n):
        for j in range(n):
            if m[q[i]][q[j]]!=q[m[i][j]]: return False
    return True

def check_lattice_ordered(m,join):
    """
    Return False if partial optable  m  does not distribute over join
    Return True otherwise
    """
    global entries_list
    n = len(m)
    for x in range(n):
        for y in range(n):
            xy = m[x][y]
            if xy>-1:
                for z in range(n):
                    xz = m[x][z]
                    if xz>-1:
                        yz = join[y][z]
                        xyz = m[x][yz]
                        if xyz>-1:
                            if xyz!=join[xy][xz]: return False
                        else:
                            m[x][yz] = join[xy][xz]
                            entries_list.append((x,yz))
                    zy = m[z][y]
                    if zy>-1:
                        xz = join[x][z]
                        xyz = m[xz][y]
                        if xyz>-1:
                            if xyz!=join[xy][zy]: return False
                        else:
                            m[xz][y] = join[xy][zy]
                            entries_list.append((xz,y))
    return True

def check_divisible(m,down):
    """
    Return False if partial optable  m  is not divisible
    i.e. x<=y implies x=m[y][u]=m[v][y] for some u,v
    Return True otherwise
    Compute list S of elements in y-row (col).
    Compute k = |down[y] - S|.
    if k>#undefined in y-row, return False
    if #undefined=1 and k=1 let undefined = this elt.
    """
    global entries_list
    n = len(m)
    for y in range(n):
        S = set([m[y][u] for u in range(n) if m[y][u]>-1])
        E = set(down[y]).difference(S)
        U = [u for u in range(n) if m[y][u]==-1]
        if len(E)>len(U): return False
        if len(U)==1 and len(E)==1:
            m[y][U[0]] = E.pop()
            entries_list += [(y,U[0])]
    for y in range(n):
        S = set([m[u][y] for u in range(n) if m[u][y]>-1])
        E = set(down[y]).difference(S)
        U = [u for u in range(n) if m[u][y]==-1]
        if len(E)>len(U): return False
        if len(U)==1 and len(E)==1:
            m[U[0]][y] = E.pop()
            entries_list += [(U[0],y)]
    return True

def complete_l_operation(m,join,down,i,j,associative=False,commutative=False,divisible=False):
    """
    find next i,j where alg[i][j] = -1 = undefined; for each val=0..n-1
    set alg[i][j] = val, check axioms and permutations
    if ok, complete_ordered_operation(m,i,j+1) then restore and return
    """
    global algebra_list,entries_list,pflags,pflags_list,gl_index
    ok = True
    n = len(m)
    while ok and i<n:
        while j<n and m[i][j]>-1: j = j+1
        if j>=n:
            j = 0 
            i = i+1
        else: ok = False
    if ok:
        if check_lattice_ordered(m,join) and \
               (not divisible or check_divisible(m,down)):
            gl_index+=1
            algebra_list.append(Alg(op={'cdot':[x[:] for x in m],'vee':join},index=gl_index,size=n))
    else:
        for val in range(n):
            if all([join[x][i]!=i or m[x][j]==-1 or join[m[x][j]][val]==val \
                    for x in range(i)]) and \
               all([join[x][j]!=j or m[i][x]==-1 or join[m[i][x]][val]==val \
                    for x in range(j)]):
                ok = True
                el = len(entries_list)
                m[i][j] = val
                entries_list += [(i,j)]
                if commutative:
                    m[j][i] = val
                    entries_list += [(j,i)]
                if ok: ok = check_lattice_ordered(m,join)
                if ok and divisible: ok = check_divisible(m,down)
                if ok and associative: ok = check_associativity(m,i,j)
                pl = len(pflags_list)
                if ok: ok = check_permutations(m)
                if ok: complete_l_operation(m,join,down,i,j+1,associative,commutative,divisible)
                while len(entries_list)>el:
                    e = entries_list.pop()
                    m[e[0]][e[1]] = -1
                while len(pflags_list)>pl:
                    p = pflags_list.pop()
                    pflags[p] = True

def downsets(lat):
        n = lat.size
        jn = lat.op['vee']
        down = [[x for x in range(n) if jn[x][y]==y] for y in range(n)]
        return down

def find_l_groupoids(l,associative=False,commutative=False,divisible=False,idempotent=False,identity=False,id=None,zero=False):
    """
    Return list of lattice ordered groupoids of lattice  l  as nxn matrices.
    The lattice is given by the join table.
    The operation is compatible with the order.
    """
    global algebra_list,perms,invperms,entries_list,pflags,pflags_list
    algebra_list=[]
    entries_list=[]
    n = l.size
    join = l.op['vee']
    down = downsets(l)
    m = [[-1 for x in range(n)] for x in range(n)]
    perms = [[0]+p+[n-1] for p in permutations(1,n-1) \
             if is_op_automorphism(join,[0]+p+[n-1])] if zero else \
             [p+[n-1] for p in permutations(0,n-1) \
             if is_op_automorphism(join,p+[n-1])]
    if idempotent:
        for x in range(n):
            m[x][x] = x
    if zero:
        #perms = [[0]+p for p in permutations(1,n)]
        for x in range(n):
            m[x][0] = 0
            m[0][x] = 0
    if identity:
        if id==None: #should only try all canconical identity positions
            t = n
            if zero and n>1: s = 1
            else: s = 0
        else: s = id; t = id+1
        for e in range(s,t):
            for x in range(n):
                m[e][x] = x
                m[x][e] = x
            perms = [[0]+p+[n-1] for p in permutations(1,n-1) \
                     if is_op_automorphism(join,[0]+p+[n-1])] if zero else \
                     [p+[n-1] for p in permutations(0,n-1) \
                     if is_op_automorphism(join,p+[n-1])]
            if all([p[e]>=e for p in perms]): # eliminate isomorphic (P,e)
                perms = [p for p in perms if p[e]==e] #keep e fixed
                invperms = [inverse_permutation(p) for p in perms]
                pflags = [True for i in range(len(perms))]
                pflags_list = []
                complete_l_operation(m,join,down,0,0,associative,commutative,divisible)
            for x in range(n):
                m[e][x] = -1
                m[x][e] = -1
    else:
        invperms = [inverse_permutation(p) for p in perms]
        pflags = [True for i in range(len(perms))]
        pflags_list = []
        complete_l_operation(m,join,down,0,0,associative,commutative,divisible)
    return algebra_list

def find_l_semigroups(l):
    return find_l_groupoids(l,associative=True)

def find_idempotent_semirings(n): #not correct
    alg_list = []
    for l in find_joinsemilattices(n):
        alg_list.extend(find_l_semigroups(l))
    return alg_list

def find_l_semigroups_with_zero(l,e=None):
    return find_l_groupoids(l,associative=True,id=e,zero=True)

def find_semirings0(n):
    alg_list = []
    for l in find_lattices(n):
        alg_list.extend(find_l_semigroups_with_zero(l))
    return alg_list

def find_commutative_l_semigroups(l):
    return find_l_groupoids(l,associative=True,commutative=True)

def find_l_bands(l):
    return find_l_groupoids(l,associative=True,idempotent=True)

def find_l_semilattices(l):
    return find_l_groupoids(l,associative=True,commutative=True,idempotent=True)

def find_l_monoids(l,e=None):
    return find_l_groupoids(l,associative=True,identity=True,id=e)

def find_idempotent_semirings_with_unit(n): #not correct
    alg_list = []
    for l in find_joinsemilattices(n):
        alg_list.extend(find_l_monoids(l))
    return alg_list

def find_commutative_l_monoids(l,e=None):
    return find_l_groupoids(l,associative=True,commutative=True,identity=True,id=e)

def find_commutative_idempotent_semirings_with_unit(n): #not correct
    alg_list = []
    for l in find_joinsemilattices(n):
        alg_list.extend(find_commutative_l_monoids(l))
    return alg_list

def find_l_monoids_with_zero(l,e=None):
    return find_l_groupoids(l,associative=True,identity=True,id=e,zero=True)

#a=Alg({"\\cdot":[[0,1],[1,-1]], "\\sim":[0,-1]},1)
#a.uc={0:[1],1:[]}
#a.pos=[(0,0),(0,1)]

lattices=[  # list of lattices of size up to 5
{'pos': {0: (0, 0)},
 'uc': {0: []}}, 
{'pos': {0: (0, 0), 1: (0, 1)},
 'uc': {0: [1], 1: []}}, 
{'pos': {0: (0, 0), 1: (0, 1), 2: (0, 2)},
 'uc':{0: [1], 1: [2], 2: []}}, 
{'pos': {0: (0, 0), 1: (0, 1), 2: (0, 2), 3:(0, 3)},
 'uc': {0: [1], 1: [2], 2: [3], 3: []}}, 
{'pos': {0: (0, 0), 1:(-1, 1), 2: (1, 1), 3: (0, 2)},
 'uc': {0: [1, 2], 1: [3], 2: [3], 3: []}}, 
{'pos': {0: (0, 0), 1: (0, 1), 2: (0, 2), 3: (0, 3), 4: (0, 4)},
 'uc': {0: [1], 1: [2], 2: [3], 3: [4], 4: []}}, 
{'pos': {0: (0, 0), 1: (-1, 1), 2: (1, 1), 3: (0, 2), 4: (0, 3)},
 'uc': {0: [1, 2], 1: [3], 2: [3], 3: [4], 4: []}}, 
{'pos': {0: (0, 0), 1: (0, 1), 2: (-1, 2), 3: (1, 2), 4: (0, 3)},
 'uc': {0: [1], 1: [2, 3], 2: [4], 3: [4], 4: []}},
{'pos': {0: (0, 0), 1: (1, 1), 2: (-1, 1.5), 3: (1, 2), 4: (0, 3)},
 'uc': {0: [2, 1], 1: [3], 2: [4], 3: [4], 4: []}}, 
{'pos': {0: (0, 0), 1: (-1, 1), 2: (0, 1), 3: (1, 1), 4: (0, 2)},
 'uc': {0: [1, 2, 3], 1: [4], 2: [4], 3: [4], 4: []}}, 
    ]
lat6=[
{'pos': {0: (0, 0), 1: (0, 1), 2: (0, 2), 3: (0, 3), 4: (0, 4), 5: (0, 5)},
 'uc': {0: [1], 1: [2], 2: [3], 3: [4], 4: [5], 5: []}}, 
{'pos': {0: (0, 0), 1: (-1, 1), 2: (1, 1), 3: (0, 2), 4: (0, 3), 5: (0, 4)},
 'uc': {0: [1, 2], 1: [3], 2: [3], 3: [4], 4: [5], 5: []}}, 
{'pos': {0: (0, 0), 1: (0, 1), 2: (-1, 2), 3: (1, 2), 4: (0, 3), 5: (0, 4)},
 'uc': {0: [1], 1: [2, 3], 2: [4], 3: [4], 4: [5], 5: []}},
{'pos': {0: (0, 0), 1: (0, 1), 2: (0, 2), 3: (-1, 3), 4: (1, 3), 5: (0, 4)},
 'uc': {0: [1], 1: [2], 2: [3, 4], 3: [5], 4: [5], 5: []}}, 
{'pos': {0: (0, 0), 1: (1, 1), 2: (-1, 2), 3: (1, 2), 4: (1, 3), 5: (0, 4)},
 'uc': {0: [2, 1], 1: [3], 2: [5], 3: [4], 4: [5], 5: []}},
{'pos': {0: (0, 0), 1: (1, 1), 2: (-1, 1.5), 3: (1, 2), 4: (0, 3), 5: (0, 4)},
 'uc': {0: [2, 1], 1: [3], 2: [4], 3: [4], 4: [5], 5: []}},
{'pos': {0: (0, 0), 1: (0, 1), 2: (1, 2), 3: (-1,2.5), 4: (1, 3), 5: (0, 4)},
 'uc': {0: [1], 1: [2, 3], 2: [4], 3: [5], 4: [5], 5: []}},
{'pos': {0:(-.5, 0), 1:(-1.5, 1), 2:(.5, 1), 3:(-.5, 2), 4:(1.5, 2), 5:(.5, 3)},
 'uc': {0: [1, 2], 1: [3], 2: [3, 4], 3: [5], 4: [5], 5: []}}, 
{'pos': {0: (0, 0), 1: (-1, 1), 2: (0, 1), 3: (1, 1), 4: (0, 2), 5: (0, 3)},
 'uc': {0: [1, 2, 3], 1: [4], 2: [4], 3: [4], 4: [5], 5: []}}, 
{'pos': {0: (0, 0), 1: (0, 1), 2: (-1, 2), 3: (0, 2), 4: (1, 2), 5: (0, 3)},
 'uc': {0: [1], 1: [2, 3, 4], 2: [5], 3: [5], 4: [5], 5: []}}, 
{'pos': {0: (0, 0), 1: (-1, 1), 2: (1, 1), 3: (-1, 2), 4: (1, 2), 5: (0, 3)},
 'uc': {0: [2, 1], 1: [3], 2: [4], 3: [5], 4: [5], 5: []}}, 
{'pos': {0: (0, 0), 1: (1, 1), 2: (-1, 1.5), 3: (0, 1.5), 4: (1, 2), 5: (0, 3)},
 'uc': {0: [2, 3, 1], 1: [4], 2: [5], 3: [5], 4: [5], 5: []}},
{'pos': {0: (0, 0), 1:(-.01, 1), 2: (1, 1), 3: (-1, 1.5), 4: (1, 2), 5: (0, 3)},
 'uc': {0: [3, 1, 2], 1: [4], 2: [4], 3: [5], 4: [5], 5: []}}, 
{'pos': {0: (0, 0), 1: (1, 1), 2: (-1, 1.5), 3:(-.01, 2), 4: (1, 2), 5: (0, 3)},
 'uc': {0: [2, 1], 1: [3, 4], 2: [5], 3: [5], 4: [5], 5: []}}, 
{'pos': {0:(0, 0), 1:(-1.5, 1), 2:(-0.5, 1), 3:(0.5, 1), 4:(1.5, 1), 5:(0, 2)},
 'uc': {0: [1, 2, 3, 4], 1: [5], 2: [5], 3: [5], 4: [5], 5: []}}]


def permuted_binary_op(m,q):
    qi = inverse_permutation(q)
    return [[q[m[qi[x]][qi[y]]] for y in range(len(m))] for x in range(len(m))]


def leq2uc(le): # assumes le[x][y] => x <= y (topologically sorted)
    n = len(le)
    uc = []
    for a in range(n):
        S = []   # accumulate upper covers of a
        for x in range(a+1,n):
            if le[a][x]==1:
                y = len(S)-1
                while y>=0 and le[S[y]][x]==0:
                    y = y-1
                if y<0: S.append(x)
        uc.append(S)
    return uc

class Posetuc(object):
    def __init__(self,uppercovers):
        self.uc = dict([(x,uppercovers[x]) for x in range(len(uppercovers))])

    def size(self):
        return len(self.uc)

    def get_leq(self):
        if hasattr(self,'leq'): return self.leq
        n = self.size()
        leq = [[0 for y in range(n)] for x in range(n)]
        for i in range(n):
            leq[i][i] = 1
            for j in self.uc[i]:
                leq[i][j] = 1
        for i in range(n):
            for j in range(i+1,n):
                if leq[i][j]:
                    for k in range(j+1,n):
                        if leq[j][k]: leq[i][k] = 1
        self.leq = leq
        return leq

    def get_join(self): # Freese-Jezek-Nation p217
        if hasattr(self,'join'): return self.join
        n = self.size()
        join = [[0 for x in range(n)] for x in range(n)]
        le = self.get_leq()
        if not all([le[x][n-1]==1 for x in range(n)]):
            return "poset has no top element"
        p = range(n-1,-1,-1)
        uc = [sorted([p[y] for y in self.uc[x]]) for x in p]
        S = []
        for x in range(n): # x=x_k
            join[x][x] = x
            for y in S:
                T = []
                for z in uc[x]:
                    T.append(join[y][z]) # T = {x_i \vee z : z>-x_k}
                q = T[0]
                for z in T[1:]:
                    if z>q: q = z #error in Listing 11.9
                for z in T:
                    if not le[p[q]][p[z]]:
                        return "poset is not a semilattice: x="+x+" y="+y
                join[x][y] = q
                join[y][x] = q
            S.append(x)
        self.join = permuted_binary_op(join,p)
        return self.join

    def get_meet(self): # Freese-Jezek-Nation p217
        if hasattr(self,'meet'): return self.meet
        n = self.size()
        meet = [[0 for x in range(n)] for x in range(n)]
        le = self.get_leq()
        if not all([le[0][x]==1 for x in range(n)]):
            return "poset has no bottom element"
        lc = self.get_lowercovers()
        S = []
        for x in range(n): # x=x_k
            meet[x][x] = x
            for y in S:
                T = []
                for z in lc[x]:
                    T.append(meet[y][z]) # T = {x_i \wedge z : z>-x_k}
                q = T[0]
                for z in T[1:]:
                    if z>q: q = z
                for z in T:
                    if not le[z][q]:
                        return "poset is not a semilattice: x="+x+" y="+y
                meet[x][y] = q
                meet[y][x] = q
            S.append(x)
        self.meet = meet
        return meet

    def get_lowercovers(self):
        if hasattr(self,'lc'): return self.lc
        lc = [[] for x in range(self.size())]
        for i in range(self.size()):
            for j in self.uc[i]:
                lc[j].append(i)
        self.lc = lc
        return lc

    def depths(self): # assumes P is topologically sorted
        l = [0 for x in range(len(self.uc))]
        lc = self.get_lowercovers()
        for i in range(len(self.uc)-1,-1,-1):
            for j in lc[i]:
                if l[j]<l[i]+1: l[j]=l[i]+1
        return l

def findid(m):
    for e in range(len(m)):
        if all(m[e][x]==x for x in range(len(m))): return e

def identitydepth(A):
    m = A.op["cdot"]
    jn = A.op["vee"]
    B = range(A.size)
    P = Posetuc(leq2uc([[1 if jn[x][y]==y else 0 for y in B] for x in B]))
    return P.depths()[findid(m)]+1

def idemdepths(A):
    m = A.op["cdot"]
    jn = A.op["vee"]
    B = range(A.size)
    P = Posetuc(leq2uc([[1 if jn[x][y]==y else 0 for y in B] for x in B]))
    d = P.depths()
    return sum(d[x] for x in B if m[x][x]==x)

def idempotents(A):
    m = A.op["cdot"]
    return [i for i in range(A.size) if m[i][i]==i]

def centrals(A):
    m = A.op["cdot"]
    B = range(A.size)
    return [i for i in B if all(m[i][j]==m[j][i] for j in B)]

def sortkey(A):
    return (identitydepth(A),A.size-len(centrals(A)),A.size-len(idempotents(A)),idemdepths(A))

def findRLs(lat):
    global gl_index
    gl_index = 0
    p = Posetuc(lat["uc"])
    alg = Alg(op={"vee":p.get_join(),"wedge":p.get_meet()})
    RLs = find_l_monoids_with_zero(alg)
    return sorted(RLs, key=sortkey)

RL = [findRLs(x) for x in lattices]
print([len(x) for x in RL])

def join2uc(jn): # assumes jn[x][y]=y => x <= y (topologically sorted)
    n = len(jn)
    uc = []
    for a in range(n):
        S = []   # accumulate upper covers of a
        for x in range(a+1,n):
            if jn[a][x]==x:
                y = len(S)-1
                while y>=0 and jn[S[y]][x]!=x:
                    y = y-1
                if y<0: S.append(x)
        uc.append(S)
    return uc

def table2list(A,sym="cdot"):
    jn = A.op["vee"]
    m = A.op[sym]
    e = findid(m)
    n = A.size
    B = list(range(1,e))+list(range(e+1,n)) #assumes 0=bottom
    d = dict((x,[]) for x in range(n))
    p = A.pos
    for x in B:
        for y in B:
            if ((x>y and p[x][1]!=p[y][1]) or (x<y and p[x][1]==p[y][1]) \
                or (x==y and m[x][x]!=x) or m[x][y]!=m[y][x]) and \
                (x!=n-1 or y!=n-1):
                d[m[x][y]].append((x,y))
    for x in range(n):#filter z's that are max or min in d[x]
        d[x] = [z for z in d[x] if ((all(jn[y[0]][z[0]]!=z[0] or \
                jn[y[1]][z[1]]!=z[1] or y==z for y in d[x]) and x!=0) or \
                (all(jn[y[0]][z[0]]!=y[0] or jn[y[1]][z[1]]!=y[1] or y==z \
                     for y in d[x]) and x!=n-1)) and \
        (x!=m[x][x] or x!=z[1] or jn[z[0]][z[1]]!=z[0] or jn[z[0]][e]!=e) and \
        (x!=m[x][x] or x!=z[0] or jn[z[0]][z[1]]!=z[0] or jn[z[1]][e]!=z[1]) ]
        # not x^2=x=z[1]<=z[0]<=e and not e<=z[1]<=z[0]=x^2=x
    return d

def labels(A):
    m = A.op["cdot"]
    e = findid(m)
    n = A.size-1
    labstr=["a","b","c","d","e","f","g"]
    B = list(range(1,e))+list(range(e+1,n))
    elts = sorted(B,key=lambda i:(A.pos[i][1],-A.pos[i][0]))[::-1]
    labs = dict((elts[i],labstr[i]) for i in range(len(elts)))
    labs[0] = "\\bot "
    labs[A.size-1] = "\\top "
    equs = {}
    tl = table2list(A)
    for i in range(A.size):
        equs[i] = "{=}".join([labs[x[0]]+(labs[x[1]] if x[0]!=x[1] else "^2")\
                              for x in tl[i]])
    labs[0] = " "
    labs[A.size-1] = " "
    labs[e] = "1"
    for i in range(A.size):
        labs[i] += ("" if labs[i]==" " or equs[i]=="" else "{=}")+equs[i]
    return labs

def uc2tikz(A):
    n = A.size
    st = '\n\\quad\n\\begin{tikzpicture}[baseline=0pt]\n'
    st += '\\node at (0,-1)[n]{$R^{'+str(A.size)+','+str(A.latindex)+\
        '}_{'+str(A.iddepth)+','+str(A.index)+'}$};\n'
    st += '\\node at (0,-2)[n]{$ $};\n'
    longlabel = []
    for i in range(n-1,-1,-1):
        st += '\\node({}) at ({},{})['.format(i,A.pos[i][0],A.pos[i][1])
        if i not in A.centrals:
            if i in A.idems: st += 'nci'
            else: st += 'nc'
        elif i in A.idems: st += 'i'
        st += ',label='+('left' if A.pos[i][0]<0 else 'right')+':$'
        if i==n-1 or i==0 or A.pos[i+1][1]>A.pos[i][1] or \
           A.pos[i-1][1]<A.pos[i][1] or len(A.label[i])<=1:
            st += A.label[i]
        else:
            st += A.label[i][:1]
            longlabel.append(A.label[i])
        st += '$]{}'+''.join([' edge ({})'.format(j) for j in A.uc[i]])+';\n'
    for i in range(len(longlabel)):
        st += '\\node at (0,'+str(A.pos[n-1][1]+len(longlabel)-i)+')[n]{$'+\
              longlabel[i]+'$};\n'
    return st + '\\end{tikzpicture}'

def drawRLs(li,pos,latindex):
    st = ""
    c=0
    iddepth=1
    for i in range(len(li)):
        c+=1
        x=li[i]
        x.op["1"]=findid(x.op["cdot"])
        A=Alg(index=c,op=x.op,size=x.size)
        A.uc=join2uc(x.op["vee"])
        A.pos=pos
        A.latindex=latindex
        A.label=labels(A)
        A.iddepth=identitydepth(A)
        A.idems=idempotents(A)
        A.centrals=centrals(A)
        if A.iddepth>iddepth:
            c=1
            A.index=1
            iddepth=A.iddepth
        st += uc2tikz(A)
    return st

def savefile(fn,st):
    fh = open(fn,'w')
    fh.write(st)
    fh.close()

def main():
    global latex
    ind = 0
    si = 1
    for i in range(len(RL)):
        ind += 1
        if si<RL[i][0].size:
            si = RL[i][0].size
            ind = 1
        latex += drawRLs(RL[i],lattices[i]["pos"],ind)
    latex += "%\\end{center}\n\\end{document}\n"
    savefile("RLlist5.tex", latex)

main()


# +
#PJ: This is a lengthy program that parses LaTeX formulas and extracts substrings from latex_st
from IPython.display import display, Math
from provers import *
import time

def readfile(fn):
    fh=open(fn)
    st=fh.read()
    fh.close()
    return st
latex_fn="SPoAchapters.tex"
latex_st=readfile(latex_fn)
print(latex_fn,len(latex_st),'characters')
#latex_fn="SPoAch2-5.tex"
#latex_st+=readfile(latex_fn)
#print("+"+latex_fn,len(latex_st),'characters')
#latex_fn="SPoAch6-9.tex"
#latex_st+=readfile(latex_fn)
#print("+"+latex_fn,len(latex_st),'characters')

def writefile(fn,st):
    fh=open(fn,'w')
    fh.write(st)
    fh.close()
    return "Wrote "+str(len(st))+" characters"

# Signature for input and output (the LaTeX symbols can be changed to agree with other conventions)

# Constant operation symbols
Cons="c"; Cond="d"; Iden="1"; Zero="0"; Bot="\\bot"; Top="\\top"

# Prefix unary operation symbols
Fop="f"; Gop="g"; Lneg="\\sim"; Rneg="-"; Dia="\\diamond"; Box="\\box"; Rtri="\\vartriangleright"; Ltri="\\vartriangleleft"

# Postfix unary operation symbols
Star="^*"; Inv="^{-1}"; Conv="\\smallsmile"; Pri="'"

# Infix binary operation symbols
Meet="\\wedge"; Join="\\vee"; Mult="\\cdot"; Lres="/"; Rres="\\backslash"; Omult="\\odot"; Smul="*";
Add="+"; Oadd="\\oplus"; Comp="\\circ"; Rimp="\\to"; Limp="\\leftarrow"; Ominus="\\ominus"; triR="\\triangleright"; triL="\\triangleleft"

# Infix binary relation symbols
Le="\\le"; Ge="\\ge"; Eq="="; Neq="\\ne"

# First-order logic connectives and quantifiers
And="\\text{ and }"; Or="\\text{ or }"; Imp="\\implies"; Not="\\neg"; Iff="\\iff"; All="\\forall"; Exists="\\exists"

VAR = set(["u","v","w","x","y","z"])|set("x_"+str(i) for i in range(10))|set("y_"+str(i) for i in range(10))
CONST = set([Cons,Cond,Iden,Zero,Bot,Top])
PREFIX = [(Fop,11),(Gop,11),(Lneg,11),(Rneg,11),(Dia,11),(Box,11),(Rtri,11),(Ltri,11),(Not,5)] # (symbol, precedence)
POSTFIX = [(Star,12),(Inv,12),(Conv,12),(Pri,12)]
INFIX = [(Mult,10),(Omult,10),(Comp,10),(Rres,9),(Lres,9),(triR,9),(triL,9),(Add,8),(Oadd,8),(Ominus,8),(Meet,7),(Join,7),
         (Rimp,6),(Limp,6),(Le,5),(Eq,5),(Neq,5),(And,4),(Or,4),(Imp,3),(Iff,2)]
QUANT = [(All,5),(Exists,5)]

# can add further \newcommand macros in the string below
Macros=""  #r"\newcommand{\coimp}{-\!\raisebox{.5pt}{\scriptsize<}\,}"

p9sym={"u":"u","v":"v","w":"w","x":"x","y":"y","z":"z","c":"c","d":"d","1":"1","0":"0","\\bot":"b","\\top":"t","f":"f","g":"g",
       "\\sim":"~","-":"-","\\diamond":"dd","\\box":"bx","\\triangleright":" r ","\\triangleleft":" t ","\\vartriangleright":"tr","\\vartriangleleft":"tl",
       "^*":"'","^{-1}":"'","\\smallsmile":"'","'":"'","\\wedge":"^","\\vee":" v ","\\cdot":"*","/":"/","\\backslash":"\ ",
       "\\odot":"*","*":"*","+":"+","\\oplus":"+","\\ominus":"<-","\\circ":"*","\\to":"->","\\leftarrow":"<-",
       "\\le":"<=","\\ge":">=","=":"=","\\ne":"!=","\\text{ and }":" & ","\\text{ or }":" | ",
       "\\implies":" -> ","\\iff":" <-> ","\\forall":"all","\\exists":"exists"}

opts=["op(700,infix,\"r\")","op(700,infix,\"t\")"]

################## Parser code (can ignore this) #################
# Terms are read using <NAME>'s top-down parsing algorithm #

symbol_table = {}

def wrap(subt, t): # decide when to add parentheses during printing of terms
    return subt.tex() if subt.lbp > t.lbp or len(subt.a)<=1 else "("+subt.tex()+")"

class symbol_base(object):
    a = []
    def __repr__(self): 
        return self.tex()
    def tex(self):
        if len(self.a) == 0: return self.id
        if len(self.a) == 1: 
          if self.id[0]=="^": return wrap(self.a[0],self)+self.id
          return self.id+" "+wrap(self.a[0],self)
        if len(self.a) == 2: 
          return wrap(self.a[0],self)+self.id+(" " if self.id[0]=='\\' else "")+wrap(self.a[1],self)
        return self.id+" "+self.a[0].id+self.a[1].id+self.a[2].id

def symbol(id, bp=0): # identifier, binding power
    if id in symbol_table:
        s = symbol_table[id]    # look symbol up in table
        s.lbp = max(bp, s.lbp)  # update left binding power
    else:
        class s(symbol_base):   # create class for this symbol
            pass
        s.id = id
        s.lbp = bp
        s.nulld = lambda self: self
        symbol_table[id] = s
    return s

def advance(id=None):
    global token
    if id and token.id != id:
        raise SyntaxError("Expected "+id+" got "+token.id)
    token = next()

def nulld(self): # null denotation
    expr = expression()
    advance(")")
    return expr

def infix(id, bp):
    def leftd(self, left): # left denotation
        self.a = [left]
        self.a.append(expression(bp))
        return self
    symbol(id, bp).leftd = leftd

def prefix(id, bp):
    global token
    def nulld(self): # null denotation
        global token
        if token.id != "(":
            self.a = [expression(bp)]
            return self
        else:
            token = next()
            self.a = []
            if token.id != ")":
                while 1:
                    self.a.append(expression())
                    if token.id != ",":
                        break
                    advance(",")
            advance(")")
            return self
    symbol(id, bp).nulld = nulld

def postfix(id, bp):
    def leftd(self,left): # left denotation
        self.a = [left]
        return self
    symbol(id, bp).leftd = leftd

symbol("(").nulld = nulld
symbol(")")
symbol("[").nulld = nulld
symbol("]")
symbol("(end)")

for st in VAR|CONST: symbol(st)
for t in PREFIX: prefix(t[0],t[1])
for t in POSTFIX: postfix(t[0],t[1])
for t in INFIX: infix(t[0],t[1])
for st in VAR:
    for t in QUANT: prefix(t[0]+" "+st,t[1])

def tokenize(st):
    i = 0
    while i<len(st):
        tok = st[i] #read single-letter token
        j = i+1
        if j<len(st) and st[j]=="_": #read subscript
            j+=1
            if st[j]=="{": j+=1
            while j<len(st) and st[j]>='0' and st[j]<='9': j+=1
            if j<len(st) and st[j]=="}": j+=1
            tok = st[i:j]
        elif j<len(st) and st[i]=="^": #read postfix superscript operation
            if st[j]=="{": j+=1
            if st[j]=="-" or st[j]=="*" or st[j]=="\\": j+=1
            if st[j]=="1": j+=1
            if st[j-1]=='\\':
                while j<len(st) and ((st[j]>='a' and st[j]<='z') or (st[j]>='A' and st[j]<='Z')): j+=1
            if j<len(st) and st[j]=="}": j+=1
            tok = st[i:j]
        elif tok=="{":
            tok = st[j]
            j+=1
        if tok=="\\": #read Latex symbol
            while j<len(st) and ((st[j]>='a' and st[j]<='z') or (st[j]>='A' and st[j]<='Z')): j+=1
            if st[i]=="{" and st[j]=="}": j+=1
            tok = st[i:j]
            if tok in ["\\mathbf","\\forall","\\exists"]:
              j+=2
              if j<len(st) and st[j]=="_": #read subscript
                j+=1
                if st[j]=="{": j+=1
                while j<len(st) and st[j]>='0' and st[j]<='9': j+=1
                if j<len(st) and st[j]=="}": j+=1
              tok = st[i:j]
            elif tok=="\\text":
              j+=2
              while j<len(st) and st[j]>='a' and st[j]<='z': j+=1
              j+=1
              if j<len(st) and st[j]=="}": j+=1
              tok = st[i:j]
        i = j
        if tok!=' ':
            symb = symbol_table[tok]
            if not symb: raise SyntaxError("Unknown operator")
            yield symb()
    symb = symbol_table["(end)"]
    yield symb()

def expression(rbp=0):
    global token
    t = token
    token = next()
    left = t.nulld()
    while rbp < token.lbp:
        t = token
        token = next()
        left = t.leftd(left)
    return left

def parse(str): # e.g., t = parse(r"(p\circ q)\lor \mathbf t")
    global token, next
    next = tokenize(str.replace("{\\sim}","\\sim ").replace("{-}","-")).__next__
    token = next()
    return expression()

def show(A, info=True): # display a (list of) formula(s)
  st = A if type(A)==str else repr(A)
  if info==True: display(Math(Macros+st))

########### end of parser #####################################

# code below assumes 'latex_st' contains the survey (SOASn.tex) 

import re
def section(cl,st=latex_st): #find section of the class cl
    cl = cl.replace('\\','\\\\').replace('$','\\$').replace('{','\\{')
    return re.search(r"(\\hypertarget{"+cl+r"}{.*?)\\hypertarget",st,flags=re.DOTALL).group(1)

def chapter(n,st=latex_st): #find chapter number n
    li = re.findall(r"(\\chapter{.*?%%endchapter)",st,flags=re.DOTALL)
    return li[n-1]

def classname(cl): #find long class name of the class cl
    return re.search(r"\\section{.*?:(.*?)}",section(cl),flags=re.DOTALL).group(1)

def sectiontitle(cl): #find full section title of the class cl
    return re.search(r"\\section{(.*?)}",section(cl),flags=re.DOTALL).group(1)

def fulldefinition(cl): #find axioms in full definition of the class cl
    ax=re.search(r"\\begin{fulldefinition}(.*?)\\end{fulldefinition}",section(cl),flags=re.DOTALL)
    if ax==None: return 'none'
    li=re.findall("\$(.*?)\$",ax.group(1),flags=re.DOTALL)
    return [s for s in li if (s.find("=")>0 or s.find("\\le")>0) and s.find('\\langle')==-1 and s.find('\\mathbf')==-1]

def finitemembers(cl,info=False): #find fine spectrum in the class cl
    fs = re.search(r"\\begin{finitemembers}(.*?)\\end{finitemembers}",section(cl),flags=re.DOTALL)
    if info: print(fs)
    li = re.findall("\$(.*?)\$",fs.group(1),flags=re.DOTALL)
    if info: print(li)
    ind = [s.split("_")[1].split("=")[0].strip() for s in li if s.find("_")>=0 and s.find("=")>=0]
    ind = [int(s[1:-1]) if s[0]=="{" else int(s) for s in ind if s.find('n')==-1 and s.find('k')==-1]
    for i in range(min(8,len(ind))): 
        if ind[i]!=i+1: raise Exception("index error at: ", i+1)
    val = [s.split("_")[1].split("=")[1].strip() for s in li if s.find("_")>=0 and s.find("=")>=0]
    return [int(s) for s in val if s!="" and s.find("n")==-1 and s.find("k")==-1]

def subclasses(cl,info=False): #find subclasses of the class cl
    fs = re.search(r"\\begin{subclasses}(.*?)\\end{subclasses}",section(cl),flags=re.DOTALL)
    if info: print(fs)
    return re.findall(r"\\hyperlink{(.*?)}{",fs.group(1),flags=re.DOTALL)

def set_subclasses(cl,sbcli,longname,st=latex_st): #replace subclasses with those in sbcli
    mo = section_mo(cl,st)
    newsbc = r"\\begin{subclasses}\n"+"\n\n".join(r"  \\hyperlink{"+x+"}{"+x+":"+(longname[x] if x in longname.keys() else "")+"}" for x in sbcli)+r"\n\\end{subclasses}"
    newst = re.sub(r"\\begin{subclasses}.*?\\end{subclasses}",newsbc,mo.group(1),flags=re.DOTALL)
    return st[:mo.start(1)]+newst+st[mo.end(1):]

def subclassposet():
    m = re.findall(r"\\hypertarget{(.*?)}{",latex_st,flags=re.DOTALL)
    return {s:subclasses(s) for s in m}

def superclasses(cl,info=False): #find subclasses of the class cl
    fs = re.search(r"\\begin{superclasses}(.*?)\\end{superclasses}",section(cl),flags=re.DOTALL)
    if info: print(fs)
    return re.findall(r"\\hyperlink{(.*?)}{",fs.group(1),flags=re.DOTALL)

def set_superclasses(cl,spcli,longname,st=latex_st): #replace superclasses with those in spcli
    mo = section_mo(cl,st)
    newspc = r"\\begin{superclasses}\n"+"\n\n".join(r"  \\hyperlink{"+x+"}{"+x+":"+(longname[x] if x in longname.keys() else "")+"}" for x in spcli)+r"\n\\end{superclasses}"
    newst = re.sub(r"\\begin{superclasses}.*?\\end{superclasses}",newspc,mo.group(1),flags=re.DOTALL)
    return st[:mo.start(1)]+newst+st[mo.end(1):]

def superclassposet():
    m = re.findall(r"\\hypertarget{(.*?)}{",latex_st,flags=re.DOTALL)
    return {s:superclasses(s) for s in m}

def finitememberslatex(li): #convert list of numbers to fine spectrum in LaTeX
    return ",\n".join("$f_"+(str(i) if i<10 else "{"+str(i)+"}")+" = "+str(li[i-1])+"$" for i in range(1,len(li)+1))+"\n"

def p9out(A): #output formula A in Prover9 format
  if A.a==[]: return p9sym[A.id]
  if A.id[:7] in ["\\forall","\\exists"]:
    return p9sym[A.id[:7]]+" "+A.id[8:]+"("+p9out(A.a[0])+")"
  if len(A.a)==1:
    #if symbol_table[p9sym[A.id]].lbp!=12:
      return p9sym[A.id]+"("+p9out(A.a[0])+")"
    #return "("+p9out(A.a[0])+")"+p9sym[A.id]
  return "("+p9out(A.a[0])+p9sym[A.id]+p9out(A.a[1])+")"

po=["x<=x","x<=y & y<=x -> x=y","x<=y & y<=z -> x<=z"]
msl=["(x^y)^z=x^(y^z)","x^y=y^x","x^x=x","x^y=x<->x<=y"]
jsl=["(x v y)v z=x v(y v z)","x v y=y v x","x v x=x","x v y=y<->x<=y"]
lat=msl+jsl+["x v(x^y)=x","x^(x v y)=x"]
dlat=lat+["x^(y v z)=(x^y)v(x^z)"]
to=lat+["x^y=x | x^y=y"] #["x<=y | y<=x"]
ba=dlat+["x'v x=t","x'^x=b"]
uo=[]
axioms=[po,jsl,msl,lat,dlat,to,ba,uo]

cli = [allclasses(chapter(i)) for i in range(2,10)]
fam = {x:cx for cx in range(8) for x in cli[cx]}

def finespectrum(cl,n,info=True,f=fam,new_ax=None): 
  # call Prover9 on the translated full definition of cl and find the fine spectrum up to n
    if info: print(cl)
    try:
        ax = [p9out(parse(e)) for e in fulldefinition(cl)]
    except:
        print("############### Error, skipping", cl)
        return []
    ax = [(x[1:-1] if x[0]=='(' and x[-1]==')' else x) for x in ax]
    ch_axioms = axioms[fam[cl]] if new_ax==None else new_ax
    if info: 
        print(ch_axioms+ax)
        t = time.time()
    a = [[1]]+[prover9(ch_axioms+ax,[],10000,10000,k,options=opts) for k in range(2,n+1)]
    if info: print("Time: {:.2f}".format(time.time()-t), "sec")
    return [len(x) for x in a]

def section_mo(cl,st=latex_st):
    cl = cl.replace('\\','\\\\').replace('$','\\$').replace('{','\\{')
    return re.search(r"(\\hypertarget{"+cl+r"}{.*?)\\hypertarget",st,flags=re.DOTALL)

def set_finitemembers(cl,li,st=latex_st): #read cl string from latex_st, replace finitemembers entry and return new latex_st
    mo = section_mo(cl,st)
    newst = re.sub(r"\\begin{finitemembers}.*?\\end{finitemembers}",r"\\begin{finitemembers}\n"+finitememberslatex(li)+r"\\end{finitemembers}",mo.group(1),flags=re.DOTALL)
    return st[:mo.start(1)]+newst+st[mo.end(1):]

def set_classname(cl,new_name,st=latex_st): #replace long class name of the class cl
    mo = section_mo(cl,st)
    newst = re.sub(r"\\section{.*?}",r"\\section{"+new_name+r"}",mo.group(1),flags=re.DOTALL)
    return st[:mo.start(1)]+newst+st[mo.end(1):]

ch=jsl
def compareandupdatefs(chax,cl):
    li = finitemembers(cl)
    sli = [x for x in li if x <= 1000]
    n = min(max(len(sli),3),6)
    fs = finespectrum(chax,cl,n,True)
    print(cl,li)
    return li[:n]==fs or fs==[], fs

def sectionnames(st):
    return re.findall(r"\\hypertarget{(.*?)}{",st,flags=re.DOTALL)

#axioms=[[],["x<=y->x=y"],po,jsl,msl,lat,dlat,to,ba,uo]
def checkfs(li,info=False):
    global latex_st
    m=[[] for x in range(10)]
    for ch in li:
        st1=chapter(ch,latex_st)
        m[ch]=sectionnames(st1)
    print([len(x) for x in m])
    for ch in li:
        print(ch,axioms[ch])
        for cl in m[ch]:
            if fulldefinition(cl)!="none":
                fl = compareandupdatefs(axioms[ch-2],cl)
                if not fl[0]:
                    print("***********",fl)
                    latex_st = set_finitemembers(cl,fl[1],latex_st)

def allclasses(st=latex_st): #return list of class names in st
    li=re.findall(r"\\hypertarget{(.*?)}{",st,flags=re.DOTALL)
    print("Number of classes:", len(li))
    return li

def allclassposets(st=latex_st): #return list of tikz diagrams
    return re.findall(r"(\\begin{tikzpicture}\[xscale=.6.*?\\end{tikzpicture}\n)",latex_st,flags=re.DOTALL)

def allnodes(st): #return list of node names in st
    li=re.findall(r"\\node\((.*?)\)",st,flags=re.DOTALL)
    print("Number of nodes:", len(li))
    return li

def lowercovers(nd,st): #return list of lowercovers of node name nd in st
    edges=re.search(r"\\draw\("+nd+"\)(.*?);",st,flags=re.DOTALL)
    return re.findall(r"edge.*?\((.*?)\)",edges.group(1),flags=re.DOTALL) if edges!=None else []

def lc2uc(lc):
    uc={x:[] for x in lc}
    for x in lc:
        for y in lc[x]:
            if y in uc: uc[y].append(x)
    return uc


StarcoderdataJupyterScriptsDedupFiltered