nzm

n-vivace-satreach-cyber/c-ECApaths.py

@@ -2,52 +2,73 @@ import os, sys
 import subprocess
 import re
 import yNaming as naming
+import random
 
-
-ECA=170
+ECA=150
 TSTEPS=70
-x, y = "010101001111010011011101", "101110110001110110111001"
+N=24
+#x, y = "010101001111010011011101", "101110110001110110111001"
+Xbug="110001010011101101011110"
+Ybug="101000100011001001110000"
 
 EXCEPTIONMINISAT=2560
 
+def randomconfig(ncell):
+    """ random uniform binary config of size ncell"""
+    tab= [random.choice(['0','1']) for i in range(ncell)]
+    cfg=''.join( tab )
+    return cfg
+
 def runcmd(cmd):
     cmdresult= os.system(cmd)
     print("cmd:%s"%(cmd))
     if cmdresult!=0 and cmdresult!=EXCEPTIONMINISAT:
         sys.exit("\nFATAL ERROR code:%d raised by script command:\n[%s"%(cmdresult,cmd))
+
+
+def analyseRes3(res3):
+    if ("CPU time" not in res3):
+        print("res3:[%s]"%res3)
+        print("CPUtime not found")
+        sys.exit(-999)
+    itimeCPU=res3.index("CPU time")
+    
+    part= res3[itimeCPU+20:itimeCPU+35].strip()
+    
+    indexsol=res3.index("SATIS")
+    part2=res3[indexsol-2:].strip()
+    print("part2:[%s]"%part2)
+    satres=re.search("^U?N?SAT",part2)
+    print("res:",satres.group(0))
+    tim=re.search("\d[.]?\d+", part)
+    if tim:
+        print("satsolver CPU time:%s"%tim.group(0))
+    else:
+        print("time could not be extracted")
     
 
+
 def run():
+    x,y=randomconfig(N),randomconfig(N)
     hashx,hashy=naming.shorthash(x),naming.shorthash(y) # configs : using short hash for
     basename="ECA%d-%s-%s"%(ECA,hashx,hashy)
     cmd1="python3 b-satkubernetes.py %d %d %s %s > data/%s.dat"%(ECA, TSTEPS, x, y, basename)
     cmd2="python3 x2-convertToSat.py data/%s.dat "%basename
     cmd3="minisat data/%s.cnf data/%s-sol.cnf"%(basename,basename)
     ncells=len(x)+2
-    cmd4="python3 w-prnCNFsolution.py data/%d data/%s-sol.cnf"%(ncells, basename)
+    cmd4="python3 w-prnCNFsolution.py %d data/%s-sol.cnf"%(ncells, basename)
     cmdseq=[cmd1,cmd2,cmd3,cmd4]
     for cmd in cmdseq:
         print(cmd)
     subprocess.getoutput(cmd1)
-    subprocess.getoutput(cmd2)
+    res2=subprocess.run(cmd2.split(), capture_output=True)
+    #print("res2::[%s]"%res2)
+    #subprocess.getoutput(cmd2)
     #------------------------------
     res3 = subprocess.getoutput(cmd3)
     #------------------------------
-    subprocess.getoutput(cmd4)
-    
-    itimeCPU=res3.index("CPU time")
-    part= res3[itimeCPU+20:itimeCPU+35].strip()
-    
-    indexsol=res3.index("SATIS")
-    part2=res3[indexsol-2:].strip()
-    print("part2:[%s]"%part2)
-    satres=re.search("^U?N?SAT",part2)
-    print("res:",satres.group(0))
-    tim=re.search("\d[.]?\d+", part)
-    if tim:
-        print("satsolver CPU time:%s"%tim.group(0))
-    else:
-        print("time could not be extracted")
-    
+    subprocess.getoutput(cmd4) 
+    analyseRes3(res3)
+
 run()
 

n-vivace-satreach-cyber/x2-convertToSat.py

@@ -59,7 +59,8 @@ def processFile(filename,fileoutput):
 
 def run():        
         filesrc=sys.argv[1]
-        fileoutput=filesrc.rstrip(".dat")+".cnf"
+        assert filesrc.endswith(".dat")
+        fileoutput=filesrc[:-4]+".cnf"
         print("converting:%s to %s"%(filesrc,fileoutput))
         processFile(filesrc,fileoutput)