285 lines
11 KiB
Python
Executable File
285 lines
11 KiB
Python
Executable File
#!/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 = 3600
|
|
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
|
|
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"):
|
|
|
|
timestr = re.findall(r"real\s+(\d+\.\d+)", fstr)[-1]
|
|
|
|
# timestr = re.findall(r"real.*m.*s", fstr)[-1]
|
|
# minute = int(timestr.split('m')[0].split()[-1])
|
|
# second = float(timestr.split('m')[-1].split('s')[0])
|
|
self.datas[ins_name].time = float(timestr)
|
|
if (self.datas[ins_name].time > CUTOFF*PUNISH):
|
|
self.datas[ins_name].res="unknown"
|
|
# confstr = re.findall(r"c conflicts:.*per second", fstr)[-1]
|
|
# self.datas[ins_name].time = int(confstr.split()[-4])
|
|
|
|
return super().cal_soln(ins_name)
|
|
def to_string(self, state):
|
|
return super().to_string(state)
|
|
|
|
SOLVER_LEN = 20
|
|
SAMPLE_LEN = 20
|
|
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 += " | s".ljust(NUMBER_LEN+3)
|
|
title += " | TIME".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 += " | " + '-'*(NUMBER_LEN)
|
|
split += " | " + '-'*(NUMBER_LEN)
|
|
split += " |"
|
|
self.split_line = split
|
|
print(split)
|
|
|
|
#sota = self.solvers[0].solved_num * self.solvers[0].PAR_solved_time + CUTOFF * PUNISH * (self.sample_ins_ct - self.solvers[0].solved_num)
|
|
sota = self.solvers[0].PAR_all_time * self.sample_ins_ct
|
|
|
|
for slv in self.solvers:
|
|
|
|
s = (sota - CUTOFF * PUNISH * (self.sample_ins_ct - slv.solved_num)) / (slv.solved_num * slv.PAR_solved_time)
|
|
|
|
time = slv.solved_num * slv.PAR_solved_time + CUTOFF * PUNISH * (self.sample_ins_ct - slv.solved_num) / 1.5
|
|
time = time / self.sample_ins_ct
|
|
|
|
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 += " | " + str(round(s,2)).ljust(NUMBER_LEN)
|
|
line += " | " + str(round(time,2)).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
|
|
for slv in self.solvers:
|
|
slv.cal_soln(ins_name)
|
|
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]
|
|
line += slv.to_string(stt)
|
|
if(not stt.res == "unknown"):
|
|
no_answer = False
|
|
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
|
|
|
|
if __name__ == "__main__":
|
|
solvers = []
|
|
solvers.append(solver_SAT_standard_gnomon("./result","light-cloud-circle"))
|
|
# solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/huawei_sat/kissat-mab","origin-mab"))
|
|
# solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/huawei_simp/kissat-mab","preprocess-mab"))
|
|
samples = []
|
|
samples.append(["/pub/data/chenzh/data/sat2022/all.txt", "dump_sat"])
|
|
clt = calculater(solvers, samples)
|
|
clt.cal_and_show()
|
|
|
|
|