diff --git a/.gitignore b/.gitignore
index d874ad67cc881f97e9cbc302a3bf49e5c2686e46..9c98fbd4a0ddfc23c405a1efea7196fb9b361737 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1 +1,2 @@
*.tar
+j-geduld-parsat/Zpattern.txt
diff --git a/j-geduld-parsat/.gitignore b/j-geduld-parsat/.gitignore
index ad5f2073b3a7d7e9f07a90640450ed40ffacee95..78349153512f75d12cc57eb70b91516532a634f5 100644
--- a/j-geduld-parsat/.gitignore
+++ b/j-geduld-parsat/.gitignore
@@ -1,2 +1,5 @@
*sat
*cnf
+__pycache__/
+data/
+*dat
diff --git a/j-geduld-parsat/a-geduld1.py b/j-geduld-parsat/a-geduld1.py
index fca221392b173701991cee590025e5eb78aeb9fd..2af3d1f5f497ed660eec629c90aada07d5c755d8 100644
--- a/j-geduld-parsat/a-geduld1.py
+++ b/j-geduld-parsat/a-geduld1.py
@@ -1,3 +1,4 @@
+import sys
N=5
TR=8
diff --git a/j-geduld-parsat/c-genReps.py b/j-geduld-parsat/c-genReps.py
new file mode 100644
index 0000000000000000000000000000000000000000..84b8a206b51b2900201bc6b20ceb6b76e9cf2d20
--- /dev/null
+++ b/j-geduld-parsat/c-genReps.py
@@ -0,0 +1,171 @@
+
+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
diff --git a/j-geduld-parsat/makefile b/j-geduld-parsat/makefile
index 8e15f9372bcc4dff22882ef6c8a2b09e1d462fb6..abbf833021424df828cb357dc4d17094b91c9e6e 100644
--- a/j-geduld-parsat/makefile
+++ b/j-geduld-parsat/makefile
@@ -1,3 +1,10 @@
+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:
diff --git a/j-geduld-parsat/old-yNaming.py b/j-geduld-parsat/varia/old-yNaming.py
similarity index 100%
rename from j-geduld-parsat/old-yNaming.py
rename to j-geduld-parsat/varia/old-yNaming.py
diff --git a/j-geduld-parsat/convertToSat.py b/j-geduld-parsat/x1-convertToSat.py
similarity index 100%
rename from j-geduld-parsat/convertToSat.py
rename to j-geduld-parsat/x1-convertToSat.py
diff --git a/j-geduld-parsat/x-convertToSat.py b/j-geduld-parsat/x2-convertToSat.py
similarity index 100%
rename from j-geduld-parsat/x-convertToSat.py
rename to j-geduld-parsat/x2-convertToSat.py
diff --git a/j-geduld-parsat/x3-convertToSat.py b/j-geduld-parsat/x3-convertToSat.py
new file mode 100644
index 0000000000000000000000000000000000000000..28091a47dceba08d981c77f03fd14aa2ef8eccaa
--- /dev/null
+++ b/j-geduld-parsat/x3-convertToSat.py
@@ -0,0 +1,35 @@
+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)
diff --git a/j-geduld-parsat/yNaming.py b/j-geduld-parsat/yNaming.py
index 83c70dc87820ef4d7040187b1a825cb7b35d3ee8..ee085e58caeab906629657bd1e2857b45f24634e 100644
--- a/j-geduld-parsat/yNaming.py
+++ b/j-geduld-parsat/yNaming.py
@@ -1,24 +1,21 @@
########### 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'
diff --git a/j-geduld-parsat/zElem.py b/j-geduld-parsat/zElem.py
new file mode 100644
index 0000000000000000000000000000000000000000..d6b2d628cde4058e9f8f5934ca691a535890260f
--- /dev/null
+++ b/j-geduld-parsat/zElem.py
@@ -0,0 +1,32 @@
+# 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)
+