#!/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()