#!/usr/bin/python
# -*- coding: UTF-8 -*-
from multiprocessing import set_forkserver_preload
import os
import os.path
from posixpath import split
from random import sample
import re
import shutil
from time import monotonic, sleep
from tokenize import Number
# global limit
CUTOFF = 5000
PUNISH = 2 #PAR2
MEMS_MAX = 61440 # 60G
class states(object):
res = "unknown"
time = CUTOFF*PUNISH
mems = MEMS_MAX
mono = False # only this one can solve
best = False # show the best performance
ls_time = 0 # LS_time
class solver(object):
def __init__(self, res_dir, name):
self.res_dir = res_dir # save the results files
self.print_name = name # names want to show
self.datas = dict() # datas[ins] save the instances
def reset(self):
# SAT-ins UNSAT-ins solved-ins all-ins
self.sat_num = self.unsat_num = self.solved_num = self.all_num = 0
self.avg_sat_time = self.avg_unsat_time = self.avg_solved_time = self.avg_all_time = 0.0
self.PAR_sat_time = self.PAR_unsat_time = self.PAR_solved_time = self.PAR_all_time = 0.0
self.mono_num = 0
self.best_num = 0
def cal_soln(self, ins_name):
self.all_num += 1
state = self.datas[ins_name]
if(self.datas[ins_name].time > CUTOFF):
self.datas[ins_name] = states()
if(state.res=="sat"):
self.sat_num += 1
self.solved_num += 1
self.avg_sat_time += state.time
self.avg_solved_time += state.time
self.avg_all_time += state.time
self.PAR_sat_time += state.time
self.PAR_solved_time += state.time
self.PAR_all_time += state.time
elif(state.res=="unsat"):
self.unsat_num += 1
self.solved_num += 1
self.avg_unsat_time += state.time
self.avg_solved_time += state.time
self.avg_all_time += state.time
self.PAR_unsat_time += state.time
self.PAR_solved_time += state.time
self.PAR_all_time += state.time
else:
self.avg_all_time += CUTOFF
self.PAR_all_time += CUTOFF * PUNISH
def deal_avg(self):
if(self.sat_num>0):
self.avg_sat_time /= self.sat_num
self.PAR_sat_time /= self.sat_num
if(self.unsat_num>0):
self.avg_unsat_time /= self.unsat_num
self.PAR_unsat_time /= self.unsat_num
if(self.solved_num>0):
self.avg_solved_time /= self.solved_num
self.PAR_solved_time /= self.solved_num
if(self.all_num>0):
self.avg_all_time /= self.all_num
self.PAR_all_time /= self.all_num
def to_string(self, state):
line = ""
line += str(state.res) + " "
line += str(round(state.time,2))
if state.mono:
line += "[M]"
elif state.best:
line += "[B]"
# if (state.byCDCL):
# line += "{C}"
# elif(state.byLS):
# line += "{L}"
# line += str()
return line.ljust(18)
return super().to_string(state)
class solver_SAT_standard_gnomon(solver):
def cal_soln(self, ins_name):
if(not ins_name in self.datas):
self.datas[ins_name] = states()
real_file_path = self.res_dir + "/" + ins_name
if (not os.path.isfile(real_file_path)):
return super().cal_soln(ins_name)
fstr = open(real_file_path, "r").read()
if(not len(re.findall(r"s\s+UNSATISFIABLE", fstr))==0):
self.datas[ins_name].res = "unsat"
elif(not len(re.findall(r"s\s+SATISFIABLE", fstr))==0):
self.datas[ins_name].res = "sat"
if(not self.datas[ins_name].res == "unknown"):
if (not self.print_name.find("kissat") == -1):
self.datas[ins_name].time = float(re.findall(r"c process-time:.*seconds", fstr)[0].split()[-2])
else:
timestr = re.findall(r"real.*m.*s", fstr)[0]
minute = int(timestr.split('m')[0].split()[-1])
second = float(timestr.split('m')[-1].split('s')[0])
self.datas[ins_name].time = minute * 60 + second
return super().cal_soln(ins_name)
def to_string(self, state):
return super().to_string(state)
SOLVER_LEN = 20
SAMPLE_LEN = 15
NUMBER_LEN = 8
print_title = True
class calculater(object):
solvers = []
sample_dirs = [] # sample dirs, [sample_dir, sample_name]s
def __init__(self, solvers, sample_dirs):
self.solvers = solvers
self.sample_dirs = sample_dirs
def __show_in_mark_down(self, samp_name):
global print_title
if(print_title):
print_title = False
title = "| sample".ljust(SAMPLE_LEN+2)
title += " | solver".ljust(SOLVER_LEN+3)
title += " | #SAT".ljust(NUMBER_LEN+3)
title += " | avg_t".ljust(NUMBER_LEN+3)
title += " | #UNSAT".ljust(NUMBER_LEN+3)
title += " | avg_t".ljust(NUMBER_LEN+3)
title += " | #ALL".ljust(NUMBER_LEN+3)
title += " | PAR2_t".ljust(NUMBER_LEN+3)
title += " | best".ljust(NUMBER_LEN+3)
title += " | mono".ljust(NUMBER_LEN+3)
title += " |"
print(title)
split = "| " + '-'*(SAMPLE_LEN)
split += " | " + '-'*(SOLVER_LEN)
split += " | " + '-'*(NUMBER_LEN)
split += " | " + '-'*(NUMBER_LEN)
split += " | " + '-'*(NUMBER_LEN)
split += " | " + '-'*(NUMBER_LEN)
split += " | " + '-'*(NUMBER_LEN)
split += " | " + '-'*(NUMBER_LEN)
split += " | " + '-'*(NUMBER_LEN)
split += " | " + '-'*(NUMBER_LEN)
split += " |"
self.split_line = split
print(split)
for slv in self.solvers:
line = "| " + (samp_name + "("+str(self.sample_ins_ct) + ")").ljust(SAMPLE_LEN)
line += " | " + slv.print_name.ljust(SOLVER_LEN)
line += " | " + str(slv.sat_num).ljust(NUMBER_LEN)
line += " | " + str(round(slv.avg_sat_time,2)).ljust(NUMBER_LEN)
line += " | " + str(slv.unsat_num).ljust(NUMBER_LEN)
line += " | " + str(round(slv.avg_unsat_time,2)).ljust(NUMBER_LEN)
line += " | " + str(slv.solved_num).ljust(NUMBER_LEN)
line += " | " + str(round(slv.PAR_all_time,2)).ljust(NUMBER_LEN)
line += " | " + str(slv.best_num).ljust(NUMBER_LEN)
line += " | " + str(slv.mono_num).ljust(NUMBER_LEN)
line += " |"
print(line)
def cal_and_show(self):
for sample in self.sample_dirs:
title_line = ""
for slv in self.solvers:
title_line += slv.print_name.ljust(18)
print(title_line)
samp_dir = sample[0]
samp_name = sample[1]
print_line_ct = 0
sample_ins_ct = 0
for slv in self.solvers:
slv.reset()
for ins_name in open(samp_dir):
sample_ins_ct += 1
ins_name = ins_name.strip()
best_time = CUTOFF*PUNISH
solved_ct = 0
first_time = -1
for slv in self.solvers:
slv.cal_soln(ins_name)
if (first_time == -1):
first_time = slv.datas[ins_name].time
best_time = min(slv.datas[ins_name].time, best_time)
if not slv.datas[ins_name].res == "unknown":
solved_ct += 1
if(not best_time == CUTOFF*PUNISH):
for slv in self.solvers:
if(slv.datas[ins_name].time == best_time):
slv.datas[ins_name].best = True
slv.best_num += 1
if(solved_ct == 1):
slv.datas[ins_name].mono = True
slv.mono_num += 1
line = ""
no_answer = True
answer_this = "unknown"
all_can_solve = True
have_diff_res = False
for slv in self.solvers:
stt = slv.datas[ins_name]
ratio = first_time / slv.datas[ins_name].time
line += slv.to_string(stt) + "\t"
# line += str(round(ratio, 2)) + "\t"
if(not stt.res == "unknown"):
no_answer = False
if (not answer_this == "unknown"):
if (not answer_this == stt.res):
have_diff_res = True
answer_this = stt.res
elif(stt.res == "unknown"):
all_can_solve = False
line += ins_name
if(not all_can_solve and not no_answer):
have_diff_res = True
# if(True):
# if(False):
# if(no_answer):
# if(all_can_solve):
if(have_diff_res):
# if(have_diff_res and answer_this == "sat"):
# if(self.solvers[-2].datas[ins_name].res != self.solvers[-1].datas[ins_name].res):
print_line_ct += 1
print(line)
self.sample_ins_ct = sample_ins_ct
for slv in self.solvers:
slv.deal_avg()
self.__show_in_mark_down(samp_name)
if(print_line_ct>0):
print("print line ct = ", print_line_ct)
else:
print(self.split_line)
def gen_samples(dir):
samples = []
for root, dirs, files in os.walk(dir):
for file in files:
sample_name = file.strip(".txt")
sample_dir = os.path.join(root, file)
# print(sample_dir, sample_name)
samples.append([sample_dir, sample_name])
return samples
def append_all_solvers_in_dir(solvers, path):
dirs = os.listdir(path)
dirs.sort()
for dir in dirs:
# print(dir)
solvers.append(solver_SAT_standard_gnomon(path + dir, dir))
if __name__ == "__main__":
solvers = []
# solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-3-nps-tc2","thread32"))
# solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/sota/NPS","NPS"))
# solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/sota/p-mcomsps","p-mcomsps"))
# solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/sota/pakis22","pakis22"))
# solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/sota/treengeling","treengeling"))
# solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/sota/pakis-mab","pakis"))
# solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-3-nps","4-3-sharing-nps"))
# solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-3-nps-rp-tc2","4-3-sharing-nps-rp2"))
# solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-3-nps-p","4-3-sharing-nps-p"))
# solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-3-nps-tc2","4-3-sharing-nps2"))
# solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-3-nps-rp","4-3-sharing-nps-rp"))
# solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-3-nps-p-tc2","4-3-sharing-nps-p2"))
# solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-3-nosharing-r","4-3-nosharing"))
# solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-3-nopre-sharing-r","4-3-nopre"))
# solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v5-7-dps-20-2k","5-7-dps-20-2k"))
# solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v6-0-nps","6-0-nps"))
# solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/sota/kissat-inc","kissat-inc"))
# solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-4-nps-2","thread2"))
# solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-4-nps-4","thread4"))
# solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-4-nps-8","thread8"))
# solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-4-nps-16","thread16"))
# solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-3-nps-tc2","thread32"))
# solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-4-nps-64","thread64"))
# solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-4-nps-64-2","thread64-2"))
solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-3-nps-tc3","4-3-sharing-nps3"))
# solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-3-nps-tc4","4-3-sharing-nps4"))
# solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v5-5-dps-20","5-5-dps-20"))
# solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v5-6-dps-20","5-6-dps-20"))
# solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v5-6-dps-2","5-6-dps-2"))
solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v5-7-dps-20-1k","5-7-dps-20-1k"))
solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v5-7-dps-20-2k","5-7-dps-20-2k"))
solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v5-7-dps-10-1k","5-7-dps-10-1k"))
solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v5-7-dps-10-2k","5-7-dps-10-2k"))
# solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v5-7-dps-5-1k","5-7-dps-5-1k"))
solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v6-0-dps-15-1k","6-0-dps-15-1k"))
solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v6-0-dps-15-2k","6-0-dps-15-2k"))
solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v6-1-dps-15-2k","6-1-dps-15-2k"))
solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v6-2-dps-15-2k","6-2-dps-15-2k"))
# solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v5-7-dps-20-4k","5-7-dps-20-4k"))
# append_all_solvers_in_dir(solvers, "/pub/data/chenzh/res/light/")
samples = []
# samples.append(["/pub/data/chenzh/data/sat2020/vbs.txt", "vbs"])
# samples.append(["/pub/data/chenzh/data/sat2021/vbs.txt", "vbs"])
# samples.append(["/pub/data/chenzh/data/sat2022/vbs.txt", "vbs"])
# samples.append(["/pub/data/chenzh/data/sat2022/satvbs.txt", "satvbs"])
# samples.append(["/pub/data/chenzh/data/sat2022/unsatvbs.txt", "unsatvbs"])
samples.append(["/pub/data/chenzh/data/sat2022/all.txt", "all"])
# samples.append(["/pub/data/chenzh/data/sat2022/unknown.txt", "unknown"])
clt = calculater(solvers, samples)
clt.cal_and_show()