Merge branch 'main' of gitlab.inria.fr:prognf/progAedificabo into main

.gitignore

 *.tar
+j-geduld-parsat/Zpattern.txt

j-geduld-parsat/.gitignore

 *sat
 *cnf
+__pycache__/
+data/
+*dat

j-geduld-parsat/a-geduld1.py

+import sys
 N=5
 TR=8
 

j-geduld-parsat/c-genReps.py

+
+import zElem as elem
+from collections import deque
+
+NOPROD=False#True
+
+tabcond0to1=["*11100***", "11100****", "*00100***","00100****","**010100*"]
+tabcond1to0=["11101****", "*0101*0**", "**0110***", "***110110", "***0110**", "****1101*"]
+tabpass=['**001110*', '*1001010*', '01*01001*', '0*0001000', '**0101011', '10*001110', '*0101011*', '*10*00*0*',
+         '10*00*000', '*10100*1*', '**0111*00', '*111101*1', '*000001**', '0*101111*', '**001*111', '10*000001',
+         '10100*1*1', '*0110**1*', '*0*111110', '**0000010', '01101*10*', '*1111111*', '*1*111*01', '01100*0**',
+         '**0*01100', '00000000*', '**0101101', '*00101*10', '110001000', '011*0111*', '0110001**', '*0001001*',
+         '*0111*111', '**0010110', '**0001*01', '*0101110*', '11111000*', '*10*01010', '101*01001', '000001110',
+         '*00011110', '**110110*', '*1000*11*', '11110111*', '**111*100', '*0*01010*', '*00001010', '*11111000', 
+         '10101111*', '*00*01111', '*111010**', '**0111111', '*10*11110', '**111001*', '*00111*01', '*01101000', 
+         '011*1000*', '10100*01*', '*1010111*', '**000*011', '10100*100', '01100110*', '*0111*000', '*0111**01', 
+         '**001000*', '01101011*', '11001001*', '*01100*0*', '101000110', '001101001']
+
+def negSign(bit,varName):
+    if bit=='0':
+          return "+"+varName
+    if bit=='1':
+          return "-"+varName
+    return "" #case '*': do nothing
+
+def posSign(bit,varName):
+    assert bit=='0' or bit=='1'
+    if bit=='0':
+          return "-"+varName
+    if bit=='1':
+          return "+"+varName
+
+
+
+
+def genTransitionHBO(bitpatternI, transitionResult, varName, komm):
+    """ one transition of the HBO rule :
+    bitpattern=rule, varnames = table, names of the vars,  transition "0" or "1", comment
+    """
+    assert len(bitpatternI)==9
+    assert len(varName)==9+1
+    #print("HBO rule:",bitpatternI,transitionResult,varName)
+    strout=""
+    for k in range(9):
+        strout+=negSign( bitpatternI[k], varName[k] )
+        if not strout.endswith(" "):
+            strout+=" "
+    strout+= posSign(transitionResult, varName[9])
+    strout+= " KOMM-HBO"+komm
+    return strout
+
+def hbo(varName):
+    """ varName, table of size 9+1 """
+    assert len(varName) == 9+1
+    for cond0 in tabcond0to1:
+        c0= genTransitionHBO(cond0,"1",varName,"one")
+        print(c0,cond0)
+    for cond1 in tabcond1to0:
+        c1= genTransitionHBO(cond1,"0",varName,"zero")
+        print(c1,cond1)
+    for condp in tabpass:
+        nextstate=condp[4] #central cell
+        cp=genTransitionHBO(condp, nextstate, varName,"pssv")
+        print(cp,condp)
+
+def generateReps(sz):
+    """ all binary s-representants, excluding all-0 and all-1 """
+    nconfig=2**sz
+    Reps=[]
+    nonReps=set()
+    for i in range(1,nconfig-1):
+        word=format(i,'b').zfill(sz)
+        if not word in nonReps:
+            Reps.append(word)
+            #print("%3d -- %s "%(i,word))
+            for delta in range(sz-1):
+                word=elem.shift(word)
+                nonReps.add(word)
+    return Reps
+
+def genRect(t,I,J):
+    prefix=elem.intToLetterL(t);
+    t=[[""]*I for j in range(J)]
+    for j in range(J):
+        for i in range(I):
+            t[j][i]=prefix + elem.intToLetterU(j) + str(i)
+            #print(t[j][i]) #=10*j+i
+    return t
+
+############# RULE INTERPRETATION ###########################
+def prod(lenx,cmdseq,vartab):
+    """ take one command and process it
+    lenx : size of the initial cond. x"""
+    cmd = cmdseq.popleft()
+    #print("analysing:%s"%cmd)
+    match cmd.split():
+        case ["ini",word]: #each is  a seprate line
+            assert lenx == len(word)
+            outline=""
+            for i in range(lenx):
+                outline=posSign(word[i],vartab[0][i])+ " KOMM-ini"
+                print(outline)
+        case ["line",numline]:
+            for i in range(lenx):
+                outline="cell %s %d"%(numline,i)
+                cmdseq.append(outline)
+        case ["cell",tstr,istr]:
+            #print(cmd)
+            t,i=int(tstr),int(istr)
+            oline="hbo"
+            for k in range(-4,4+1): #radius 4 !
+                pos=(i+k+2*lenx)%lenx
+                oline+=" %s"% vartab[t][pos]
+            oline+= " %s"%(vartab[t+1][i])
+            cmdseq.append(oline)
+        case ["hbo",arg1,arg2,arg3,arg4,arg5,arg6,arg7,arg8,arg9,arg10]: # Final 
+            varName=[arg1,arg2,arg3,arg4,arg5,arg6,arg7,arg8,arg9,arg10]
+            if NOPROD:
+                print ("PROD:"+cmd)        
+            else:
+                hbo(varName)
+        case _:
+            print("no match:%s"%cmd)
+    
+
+
+NADHOC=10
+
+def processOneInitCond(seqnum, word, Tevol):
+    """ coherent evolution between time t=0 and time t=Tevol """
+    #print(" digesting :",word)
+    lenx=len(word)
+    vartab=genRect(seqnum,lenx,Tevol+1)
+    
+    inicmd= "ini " + word
+    linecmd= [ "line %d"%i for i in range(Tevol) ] #init commands : coherence conditions
+
+    cmdseq=deque(linecmd)
+    cmdseq.appendleft(inicmd)
+    while (cmdseq):
+        prod(lenx,cmdseq, vartab)
+    # should always be empty 
+    # print(cmdseq)
+
+
+def tstMatch(initcondSeq):
+    seqnum=0
+    for word in initcondSeq:
+        Tevol=len(word)-1 # choice : Time = len
+        processOneInitCond(seqnum, word, Tevol)
+        seqnum+=1
+
+#print("-------- starting ---------") 
+
+def tstHBO():
+    varName=['a','b','c','d','E','f','g','h', 'i','EE']
+    #tst= genTransitionHBO("0*0100011","1",varName,"tst")
+    #print(tst)
+    hbo(varName)
+
+#tab=genRect(2,3,7)
+#print(tab)
+#print(tab[5][2])
+
+#tstMatch();
+initcond3=generateReps(3)
+initcond5=generateReps(5)
+initcond7=generateReps(7)
+tstMatch(initcond3)
+
+#tstHBO()
\ No newline at end of file

j-geduld-parsat/makefile

+runa:
+	python3 c-genReps.py > testIC3.dat
+runb:
+	python3 x3-convertToSat.py testIC3.dat > A-CNF.sat
+runc:
+	minisat A-CNF.sat B-sol.cnf
+
 spa:
 	python3 e-spaceTimeHBO.py > qq.sat
 spb:

j-geduld-parsat/x3-convertToSat.py

+import sys
+DIC= {}
+NUMKEY=1
+
+def addToDic(key):
+        global NUMKEY
+        DIC[key]=NUMKEY
+        NUMKEY+=1
+
+
+def processDIC(line):
+    """transforms each line"""
+    output=""
+    for token in line.split():
+        if token.startswith("+") or token.startswith("-"):
+            varname=token[1:]
+            if not varname in DIC:
+                 addToDic(varname) #notoptimal
+            index=DIC[varname] 
+            output+=token[0]+ "%d "%index
+        if token.startswith("KOMM"): # comment should be the last element
+             break
+    output+="0" # end of line
+    output+= " c "+ token[4:] 
+    print(output)
+
+def readfile(filename):
+    f = open(filename, "r")
+    lines = f.readlines()
+    for line in lines:
+        processDIC(line)
+
+filename=sys.argv[1]
+print("converting:%s"%filename)
+readfile(filename)

j-geduld-parsat/yNaming.py

 ########### Naming scheme ##################
 
-def letterpos(k):
+def letterpos(pos):
     """ from int <26 to letter with the alphabet [a-z] s"""
-    ascii=ord('a')+k
+    ascii=ord('a')+pos
     return chr(ascii)
 
-def vname(k):
+def vname(pos):
     """ recursive, from int to letter sequence """
-    if (k<26):
-        return letterpos(k)
+    if (pos<26):
+        return letterpos(pos)
     else: 
-        return vname(k//26)+vname(k%26)
+        return vname(pos//26)+vname(pos%26)
 
 def vnamet(t,i):
     """ name(t,i) % note the order """
     return vname(t)+str(i)
 
-def name(namevar,i):
-    return namevar+str(i%N)
-
 def signedVar(bit,varName):
     """ bit determines the sign of the variable"""
     assert bit=='0' or bit=='1'

j-geduld-parsat/zElem.py

+# elementary functions
+
+def shift(strin):
+    return strin[1:]+strin[0]
+
+
+def letterPosL(pos):
+    """ LOWERCASE : from int <26 to letter in [a-z] """
+    ascii=ord('a')+pos
+    return chr(ascii)
+
+def intToLetterL(pos):
+    """ recursive, from int to letter sequence """
+    if (pos<26):
+        return letterPosL(pos)
+    else: 
+        return intToLetterL(pos//26) + intToLetterL(pos%26)
+
+
+
+def letterPosU(pos):
+    """ UPPERCASE : from int <26 to letter in [A-Z] """
+    ascii=ord('A')+pos
+    return chr(ascii)
+
+def intToLetterU(pos):
+    """ recursive, from int to letter sequence """
+    if (pos<26):
+        return letterPosU(pos)
+    else: 
+        return intToLetterU(pos//26) + intToLetterU(pos%26)
+