diff --git a/n-vivace-satreach-cyber/c-ECApaths.py b/n-vivace-satreach-cyber/c-ECApaths.py index 1234f43e9cde53db89016c193bc0ca4d427462bb..c3714ece0bef23323147d8a0338cb8249609da56 100644 --- a/n-vivace-satreach-cyber/c-ECApaths.py +++ b/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() diff --git a/n-vivace-satreach-cyber/x2-convertToSat.py b/n-vivace-satreach-cyber/x2-convertToSat.py index 772e823f734a558891b368a84edc9f3969b8bfbf..566870f7329ccf82d2a997098bf64439f3eca6ce 100644 --- a/n-vivace-satreach-cyber/x2-convertToSat.py +++ b/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)