#!python3

from pysat.formula import CNF
from pysat.solvers import Glucose4

import pathlib as pl
import random
import bz2
import sys
import argparse 


def main():
    args = parse_args()

    instances = get_instance_paths(pl.Path(args.instance_dir))
    
    global CORE_DIR
    CORE_DIR = pl.Path(args.cores_dir)

    global EXTENDED_DIR 
    EXTENDED_DIR = pl.Path(args.extensions_dir)
   
    print(CORE_DIR)

    for instance in instances:
        run(instance, args.nr_per_instance)

def parse_args():
    parser = argparse.ArgumentParser()
    parser.add_argument( "-i"
                        ,"--instance_dir"
                        ,type=str
                        ,default="./instances"
                        ,help="directory containing the instances")
    parser.add_argument( "-c"
                        ,"--cores_dir"
                        ,type=str
                        ,default="./cores"
                        ,help="directory containing the cores")
    parser.add_argument( "-e"
                        ,"--extensions_dir"
                        ,type=str
                        ,default="./extensions"
                        ,help="directory containing the core extensions")
    parser.add_argument( "-n"
                        ,"--nr_per_instance"
                        ,type=int
                        ,default=1
                        ,help="number of extensions per instance")

    return parser.parse_args()

def get_instance_paths(instances_dir):
    instances = []

    for p in instances_dir.iterdir():
        if str(p).endswith(".cnf.bz2"):
            instances.append(p)

    return instances 

def run(instance, calls_per_instance):
    ipath = pl.Path(instance)
    iname = ipath.stem[:-4]

    f = CNF(str(ipath))

    for i in range(calls_per_instance):
        cores = parse_cores(iname)

        print(iname)
        print(len(f.clauses), len(cores))
        print("{0:.3g}".format(len(cores) * 100 / len(f.clauses)))

        print()

def parse_cores(instance):
    cores = []
    
    with bz2.open(CORE_DIR / (instance + ".cores.bz2"), "tr") as cores_file:
        cores = list(map(lambda l: l.strip(), cores_file.readlines()))
    
    cores = list(map(lambda l: l.split(","), cores))
    
    for i in range(len(cores)):
        cores[i] = list(map(int, cores[i]))
        cores[i] = list(map(lambda lit: -1 * lit, cores[i]))

    return cores

def next_file_path(name):
    counter = 0

    ext_file_path = EXTENDED_DIR / ("{}_{:04}.cnf.bz2".format(name, counter))

    while ext_file_path.exists():
        counter += 1
        ext_file_path = EXTENDED_DIR / ("{}_{:04}.cnf.bz2".format(name, counter))
        
    return ext_file_path, counter 

if __name__ == "__main__":
    main()