#!/usr/bin/env python3
# -*- coding: utf-8 -*-
"""
Created on Fri Dec 18 10:34:46 2020

@author: nissa
"""

import sys
import csv
import os
import math
import numpy as np 
import matplotlib.pyplot as plt 

def read_csv_variable_information(filename):
    vars_steps = dict()
    vars_part  = dict()
    
    with open(filename,"r") as csvfile:
        reader = csv.DictReader(csvfile)
        for row in reader:
            var_id = int(row["Num Variable"])
            if var_id not in vars_steps.keys() :
                vars_steps[var_id] = set()
                vars_part[var_id]  = -1,False
            set_of_steps = { int(v) for v in row["Related Steps"].split() }
            vars_steps[var_id] = vars_steps[var_id].union(set_of_steps)
            pure_var = False
            if row["Pure Variable"] == "TRUE" :
                pure_var = True
            set_of_part = set()
            for v in row["Partition"]:
                if v == '-' :
                    set_of_part.add(-1)
                    break
                else :
                    set_of_part.add(int(v))
            vars_part[var_id] = set_of_part,pure_var
    
    return vars_steps,vars_part

def read_learnt_clauses(filename):
    clauses = dict()
    repartition_clauses = list()
    with open(filename, "r") as f :
        lines = f.readlines()
        i = -1
        for c in lines :
            if "c Distribution" in c :
                value_list = c.split()[3:]
                repartition_clauses = [ int(v) for v in value_list if "[" not in v ]
                avant_dernier = value_list[-1].split("[")
                repartition_clauses.append(int(avant_dernier[0]))
                repartition_clauses.append(int(avant_dernier[1][:-1]))
                continue
                
            if "c Number" in c :
                continue

            if "c (" in c :
                i = i + 1
                continue
            
            if i not in clauses.keys() : 
                clauses[i] = list()
            cls = [ int(v) for v in c.split()[:-1] ]
            clauses[i].append(cls)
            
    return clauses,repartition_clauses

def caracterize_learnt_clauses_interpolant(csvinfo, learntclauses):
    dic_vars_steps,dic_vars_part = read_csv_variable_information(csvinfo)
    clauses,repartition_clauses  = read_learnt_clauses(learntclauses)
    concerned_pure_junction_vars =  [ list(),list() ]
    repartition_comb_steps       = dict()
    repartition_comb_partition   = dict()
    totalVars = len(dic_vars_steps)


    for k,itp_clauses in clauses.items():
        for cls in itp_clauses:
            comb_partition = set()
            comb_step      = set()
            new_vars       = set()
            for v in cls:
                value = abs(v)
                if value not in dic_vars_steps.keys()  :
                    new_vars.add(value)
                    totalVars = totalVars + 1
                    continue
                comb_step = comb_step.union( dic_vars_steps[value] )
                set_part_id,pure_var = dic_vars_part[value]
                comb_partition = comb_partition.union(set_part_id)
                if pure_var :
                    concerned_pure_junction_vars[0].append(value)
                else :
                    concerned_pure_junction_vars[1].append(value)
            sorted_comb_step = sorted(comb_step)
            sorted_comb_part = sorted(comb_partition)
            for n in new_vars:
                dic_vars_steps[n] = sorted_comb_step
                dic_vars_part [n] = sorted_comb_part,False

            comb_partition_str = str(sorted_comb_part)
            comb_step_str = str(sorted_comb_step)
            if comb_step_str not in repartition_comb_steps.keys():
                repartition_comb_steps[comb_step_str] = 0
            repartition_comb_steps[comb_step_str] = repartition_comb_steps[comb_step_str] + 1
            if comb_partition_str not in repartition_comb_partition.keys():
                repartition_comb_partition[comb_partition_str] = 0
            repartition_comb_partition[comb_partition_str] = repartition_comb_partition[comb_partition_str] + 1
    return repartition_clauses,concerned_pure_junction_vars,repartition_comb_steps,repartition_comb_partition

MINVALUE = -1
def filter_result(keys, values):
    new_values = [math.log(v) for v in values]
    new_keys = list()
    new_new_values = list()
    for thelist,i in zip(keys,list(range(len(keys)))) :
        if new_values[i] < MINVALUE :
            continue
        new_new_values.append(new_values[i])
        thelist = thelist[1:]
        thelist = thelist[:-1]
        thelist = thelist.split(",")
        thelist= [ int(v) for v in thelist]
        minus = min(thelist)
        maxus = max(thelist)
        tick  = str(minus)+"-"+str(maxus) 
        new_keys.append( tick )
    return new_keys,new_new_values

def hist_comparator(dic_comparator, x_label, y_label, labels, title, x_lim, a):
    
    a.set_xlabel(x_label, fontsize=11)
    a.set_ylabel(y_label, fontsize=11)
    a.set_title(title)
    if x_lim != -1 :
        a.set_xlim(left=0,right=x_lim)
    a.grid(which='both', linestyle='--')

    nb_hist = len(labels)
    
    for l,i in zip(dic_comparator,list(range(nb_hist))):

        k,h = filter_result(list(l.keys()),list(l.values()))
        a.bar(k, h, label=labels[i], edgecolor='red', color='yellow', align='edge', width=0.3)

        for tick in a.get_xticklabels():
            tick.set_rotation(90)
    a.legend()
    

def hist_comparator_simple(list_comparator, x_label,y_label, labels, title, a):
  
    a.set_xlabel(x_label, fontsize=11)
    a.set_ylabel(y_label, fontsize=11)
    a.set_title(title)
    a.grid(which='both', linestyle='--')

    len_list = list(range(len(list_comparator)))
    for l,i in zip(list_comparator,len_list):
        a.hist(l,label=labels[i])
    
    a.legend()
    

def plot_scatterplot_comparator(list_comparator, x_label, y_label, labels, title, axe):
    
    axe.set_xlabel(x_label, fontsize=11)
    axe.set_ylabel(y_label, fontsize=11)
    axe.set_title(title)
    axe.grid(which='both', linestyle='--')

    nb_scatter = len(list_comparator)

    for s,i in zip(list_comparator, list(range(nb_scatter))) :
        s_log = [ math.log(v) for v in s]
        axe.scatter(list(range(len(s))),s_log,label=labels[i] )

    axe.legend()


def Main(filenames):
    
    fig, axs = plt.subplots(2,1,sharex=False, figsize=(15,10))
    #fig.suptitle("Repartition of clauses and variable decision between root and leafs",fontsize=15)
    #fig.text(0.5,0.01,'Node (leaf,...,root)',ha='center',fontsize=15)
    fig.tight_layout(pad=5.0)

    labels = list()
    scatter_comparator_list_clauses = list()
    hist_comparator_list_pjvars     = list()
    hist_comparator_list_step       = list()
    hist_comparator_list_part       = list()
    
    
    for f in filenames :
        
        flearnt = f + ".learnt"
        fcsv    = f + ".csv"
        name    = os.path.basename(f)
        labels.append(name)
        r_clauses, p_j_vars, r_steps, r_partition = caracterize_learnt_clauses_interpolant(fcsv, flearnt)
        scatter_comparator_list_clauses.append(r_clauses)
        hist_comparator_list_pjvars.append(p_j_vars)
        hist_comparator_list_step.append(r_steps)
        hist_comparator_list_part.append(r_partition)
    
        hist_comparator(hist_comparator_list_step, "Combinaison de pas", "LOG", labels, "Liens entre les pas issue des ITP", -1, axs[0])    
        plot_scatterplot_comparator(scatter_comparator_list_clauses, "Partition", "Nombre de clauses", labels, "Répartition des clauses",axs[1])
    #    hist_comparator(hist_comparator_list_part, "Combinaison de partition", "", labels, "Liens entre les partitions issue des ITP", -1, axs[1])    
    #    hist_comparator_simple(hist_comparator_list_pjvars, "Variables (pures, jonctions)", "", labels, "Taux de variables pure et de jonctions issue des ITP", axs[2])    
        
        
        fig.show()
        fig.savefig(name+"variable_info",dpi=300)





def comparator_csv_runtime(filecsv):
    
    mean_runtime_solvers = list()
    solversname     = list()
    nbsolvers       = 0 
    nb_instance     = 0
    solversname     = list()
    
    kth = ["k10.","k20.","k40.","k60.","k80.","k100.","k120.","k140.","k160.","k180.","k200.","k400.","k600.","k800.","k1000","k1200","k1400","k1800","k2000"]
    counter_k = [ 0 for k in kth ]
    ktable_mean = list()
    with open(filecsv,"r") as csvfile:
        reader = csv.DictReader(csvfile)
        solversname = reader.fieldnames[1:]
        nbsolvers   = len(solversname)
        nb_solvers_decomp = nbsolvers - 1
        runtime_solvers = [ 0 for s in solversname ]
        mean_runtime_solvers = [ 0 for s in solversname]
        ktable_mean = [ [ 0 for s in solversname ] for k in kth ]
        nb_instance = 0
        for row in reader :
            if nb_instance == -1 :
                break
            inst_name = row["Instance"]
            for k,i in zip(kth,range(len(kth))):
                if k in inst_name :
                    ind = i
                    counter_k[ind] = counter_k[ind] + 1
                    break

            plt.figure(figsize=(7,6))
            plt.xlabel("Ratio of covereged step by the partitions (%)")
            plt.ylabel("Runtime (sec)")
            nb_instance = nb_instance + 1
            plt.title("Instance "+inst_name+" using decomposition starting from first steps")

            for i,s_k in  zip(range(nbsolvers),solversname) :
                value = float(row[s_k])
                runtime_solvers[i] = value
                mean_runtime_solvers[i] = mean_runtime_solvers[i] + value
                ktable_mean[ind][i]     = ktable_mean[ind][i]  + value
            plt.plot(solversname[1:], runtime_solvers[1:], label="DeSAT")
            plt.plot(solversname[1:], [ runtime_solvers[0] for i in range(nb_solvers_decomp) ], color="red", label="Minisat")
            plt.legend()
#            plt.savefig(inst_name+"_AUG.png",dpi=300)
            

    plt.figure(figsize=(7,6))
    plt.xlabel("Ratio of covereged step by the partitions (%)")
    plt.ylabel("Average Runtime (sec)")
    plt.title("Average of "+str(nb_instance)+" using decomposition starting from first steps")

    mean_runtime_solvers = [ float(v/nb_instance) for v in mean_runtime_solvers ]
    plt.plot(solversname[1:], mean_runtime_solvers[1:], label="mean value" )
    plt.plot(solversname[1:], [ mean_runtime_solvers[0] for i in range(nbsolvers-1) ], color="red", label="Minisat")
    plt.legend()
    plt.savefig("avg_of_"+str(nb_instance)+"_AUG_LR.png",dpi=300)
            
            
    plt.figure(figsize=(7,6))
    plt.xlabel("Ratio of covereged step by the partitions (%)")
    plt.ylabel("Average Runtime (sec)")
    plt.title("Average of "+str(nb_instance)+" using decomposition starting from first steps")

    for k,i in zip(ktable_mean,range(len(kth))):
        if counter_k[i] == 0:
            continue
        mean_k = [ float(v/counter_k[i]) for v in k ]
        plt.plot(solversname, mean_k, label=kth[i])
    
    plt.legend()

    plt.savefig("avg_of_diff_k_AUG_LR.png",dpi=300)


    

def comparator_csv_cores(filename) :
    mean_core_ratio = list()
    nb_instance     = 0
    kth = ["k10.","k20.","k40.","k60.","k80.","k100.","k120.","k140.","k160.","k180.","k200.","k400.","k600.","k800.","k1000","k1200","k1400","k1800","k2000","k4000"]
    counter_k = [ 0 for k in kth ]
    ktable_mean = list()
    with open(filename,"r") as csvfile:
        reader = csv.DictReader(csvfile)
        ratios = reader.fieldnames[1:]
        nbsolvers   = len(ratios)
        core_ratio = [ 0 for s in ratios ]
        mean_core_ratio = [ 0 for s in ratios ]
        ktable_mean = [ [ 0 for s in ratios ] for k in kth ]
        nb_instance = 0
        for row in reader :
            if nb_instance == -1 :
                break
            inst_name = row["Instance"]
            for k,i in zip(kth,range(len(kth))):
                if k in inst_name :
                    ind = i
                    counter_k[ind] = counter_k[ind] + 1
                    break
            plt.figure(figsize=(7,6))
            plt.xlabel("Ratio of covereged step by the partitions (%)")
            plt.ylabel("Significative clauses rate (%)")
            nb_instance = nb_instance + 1
            plt.title("Instance "+inst_name+" using decomposition starting from first steps")

            for i,s_k in  zip(range(nbsolvers),ratios) :
                if "None" in row[s_k] :
                    value = 0
                else :
                    value = float(row[s_k].split("%")[0])
                core_ratio[i] = value
                mean_core_ratio[i] = mean_core_ratio[i] + value
                ktable_mean[ind][i]     = ktable_mean[ind][i]  + value

            plt.plot(ratios, core_ratio)
            plt.savefig(inst_name+"_core_ratio.png",dpi=300)
            
    plt.figure(figsize=(7,6))
    plt.xlabel("Ratio of covereged step by the partitions (%)")
    plt.ylabel("Average of Significative clauses rate (%)")
    plt.title("Average of "+str(nb_instance)+" instances using decomposition starting from first steps")

    mean_core_ratio = [ float(v/nb_instance) for v in mean_core_ratio ]
    plt.plot(ratios, mean_core_ratio, label="mean value" )
    plt.savefig("avg_of_"+str(nb_instance)+"inst_LR_core_ratio.png",dpi=300)
            
    plt.figure(figsize=(7,6))
    plt.xlabel("Ratio of covereged step by the partitions (%)")
    plt.ylabel("Average of Significative clauses rate (%)")
    plt.title("Average of "+str(nb_instance)+" instances using decomposition starting from first steps")

    for k,i in zip(ktable_mean,range(len(kth))):
        if counter_k[i] == 0:
            continue
        mean_k = [ float(v/counter_k[i]) for v in k ]
        plt.plot(ratios, mean_k, label=kth[i])
    
    plt.legend()
    plt.savefig("avg_of_diff_k_LR_core_ratio.png",dpi=300)



##########################################################################################

def extract_filename(filename):
    realname = filename.split("/")[-1]
    list_possible_name = realname.split(".")
    for possible_namefile in list_possible_name:
        if "_k" in possible_namefile and possible_namefile[-1].isdigit() :
            realname = possible_namefile
            break
    return realname


def comptage_size_cls_type_variables(learntclauses, csvinfo) :
    dic_vars_steps,dic_vars_part = read_csv_variable_information(csvinfo)
    clauses,repartition_clauses  = read_learnt_clauses(learntclauses)

    
    # Begin Identify number of pure and junction variables
    max_variable_problem = 0
    total_variables      = 0
    pure_variable        = 0
    junct_variable       = 0
    for k,v in dic_vars_part.items() :
        total_variables = total_variables + 1
        partition_set, pure = v
        if pure :
            pure_variable = pure_variable + 1
        else :
            junct_variable = junct_variable + 1
        if k >= max_variable_problem :
            max_variable_problem = k
    ratio_pure = pure_variable * 100. /total_variables
    ratio_junct= 100 - ratio_pure
    # End Identify number of pure and junction variables
    new_fresh_variable_set = set()
    clause_size = dict()
    total_variables_pure_learnt  = set()
    total_variables_junct_learnt = set()
    total_number_learnt_clauses  = 0
    for part,clause_partition in clauses.items() :
        for cls in clause_partition :
            total_number_learnt_clauses = total_number_learnt_clauses + 1
            thesize = len(cls)
            if thesize not in clause_size.keys() :
                clause_size[ thesize ] = 0
            clause_size[thesize] = clause_size[thesize] + 1
            for v in cls :
                value = abs(v)
                if value > max_variable_problem :
                    new_fresh_variable_set.add(value)
                else :
                    p, pure = dic_vars_part[value]
                    if pure :
                        total_variables_pure_learnt.add(value)
                    else :
                        total_variables_junct_learnt.add(value)
                        
                
    total_fresh_variables = len(new_fresh_variable_set)
    clause_ratio_size = dict()
    for k,v in clause_size.items() :
        clause_ratio_size[k] = round(v * 100. / total_number_learnt_clauses,2)

    strout = str(int(ratio_pure))+","+str(int(ratio_junct))+","+str(int(total_fresh_variables))+","+str(len(total_variables_pure_learnt))+","+str(len(total_variables_junct_learnt))+","+str(clause_ratio_size)
    
    return strout        



def Main2(directory) :
    
    files = os.listdir(directory+"/learnt")
    outputfile = directory+"/LearntClauseInfo.txt"
    str_out = ""
    with open(outputfile,"w") as fout :
        fout.write("Instances,% Model Variables,% Abstract Variables,Number Variable Conversion,Number Variable Model in Learnt Clauses,Number Abstract Variable in Learnt Clauses,Clause Size\n")
        for f in files:
            if ".learnt" in f :
                name       = extract_filename(f)
                learntfile = directory+"/learnt/"+name+".learnt"
                csvfile    = directory+"/csv/"+name+".csv"
                if os.path.isfile(csvfile) == False :
                    continue
                
                str_out = comptage_size_cls_type_variables(learntfile, csvfile)
                fout.write(name+","+str_out+"\n")
    
    
    
    
    
    
    
Main2(sys.argv[1])
    
#Main([sys.argv[1]])
    
#Main(["/home/nissa/Documents/Thesis/bmctool_main/octo_bmctool/bmctool/inst_learnt/abp8_k60_r100"])

#comparator_csv_cores("/home/nissa/Documents/Thesis/bmctool_main/REUNION/23-12-2020/core_ratio.csv")



#comparator_csv_runtime("/home/nissa/Documents/Thesis/bmctool_main/REUNION/23-12-2020/runtime_aug_inst.csv")

#comparator_csv_runtime("/home/nissa/Documents/Thesis/bmctool_main/REUNION/23-12-2020/SeqDeSAT_various_decomposition.csv")