import json
import os

def read_json(file_path):
    with open(file_path, 'r') as f:
        return json.load(f)

def extract_data(json_data):
    results = {}
    for test_name, values in json_data.items():
        # Ottieni il nome breve del test
        short_name = os.path.basename(test_name)
        
        # Ignora i test che non contengono "linux" nel nome
        if "linux" not in short_name:
            continue
        
        # Estrai i dati
        havoc = values.get("havoc", {})
        total = havoc.get("total", 0)
        lt = havoc.get("1_lt_than_2", 0)
        gt = havoc.get("1_gt_than_2", 0)
        un = havoc.get("incomparable", 0)
        eq = total - (lt + gt + un)
        
        results[short_name] = (eq, lt, gt, un)
    
    return results

def generate_latex_table(pos_data, def_data):
    common_keys = sorted(set(pos_data.keys()) & set(def_data.keys()))
    
    # Print mapping of test names
    print("Mapping of test names:")
    for idx, key in enumerate(common_keys, start=1):
        print(f"d{idx:02} -> {key}")
    
    # Compute totals for summary rows
    total_pos = [sum(x) for x in zip(*pos_data.values())]
    total_def = [sum(x) for x in zip(*def_data.values())]
    total_invs = sum(total_pos)
    total_percent_pos = [round((x / total_invs) * 100, 2) if total_invs > 0 else 0 for x in total_pos]
    total_percent_def = [round((x / total_invs) * 100, 2) if total_invs > 0 else 0 for x in total_def]
    
    latex_table = """
    \\begin{table}[t]
    \\begin{centering}
    \\begin{tabular}{|lr|rrrr|rrrr|}
    \hhline{~~--------}
    \multicolumn{2}{c|}{}
    & \multicolumn{4}{c|}{\luvpos ~\\textit{vs} original}
    & \multicolumn{4}{c|}{\luvdef ~\\textit{vs} original} \\\\
    \hhline{~~--------}
    \multicolumn{2}{c|}{}
    & EQ & LT & GT & UN & EQ & LT & GT & UN \\\\
    \hline
    
    \\# INVS & """ + f"""{total_invs} & {' & '.join(map(str, total_pos))} & {' & '.join(map(str, total_def))} \\\\ 
    \\% INVS & 100.00 & {' & '.join(map(lambda x: f'{x:.2f}', total_percent_pos))} & {' & '.join(map(lambda x: f'{x:.2f}', total_percent_def))} \\\\ """ + " \n\hline \n"
    
    for idx, key in enumerate(common_keys, start=1):
        test_name = f"d{idx:02}"
        pos_values = pos_data[key]
        def_values = def_data[key]
        latex_table += f"{test_name} & {sum(pos_values)} "
        latex_table += " & " + " & ".join(map(str, pos_values))
        latex_table += " & " + " & ".join(map(str, def_values))
        latex_table += " \\\\ \n"
    
    latex_table += "\\hline\n\\end{tabular}\n\\caption{SV-COMP benchmarks: invariant comparison for the interval domain. Boldface text highlights the differences between $\\luvpos$ and $\\luvdef$.}\n\\label{tab:driver-intra-int}\n\\end{centering}\n\\end{table}\n"
    
    return latex_table

if __name__ == "__main__":
    pos_path = "../output/int/pos-nonrel/clam-diff/clam-diff-results.json"
    def_path = "../output/int/def-nonrel/clam-diff/clam-diff-results.json"
    
    pos_data = extract_data(read_json(pos_path))
    def_data = extract_data(read_json(def_path))
    
    latex_code = generate_latex_table(pos_data, def_data)
    
    with open("table.tex", "w") as f:
        f.write(latex_code)
    
    print("LaTeX table successfully generated in table.tex")
