#! /usr/bin/env python3

import os
import time
import argparse
from pathlib import Path
import sys
import multiprocessing
import random

path = Path(__file__)
rootpath = str(path.parent.absolute().parent)
sys.path.append(rootpath)

current_dir = os.getcwd()

from src.fuzz import fuzz
from src.argument_parser.parser import MainArgumentParser
from src.collect import collect_buggy_formula
from src.simplify import standardize_instance
from src.building_blocks import export_buggy_seed
from src.association import export_association_rules
from src.skeleton import export_skeleton

skeletons = rootpath + "/skeletons/skeleton.smt2"
rules = rootpath + "/config/rules.txt"
buggy = rootpath + "/seeds"
temp = rootpath + "/temp"


def run(skeleton_file, argument, solver1, solver2, solver1_bin, solver2_bin, core_num, cores, add_option, tactic=None):
    for i in range(cores):
        process = multiprocessing.Process(target=fuzz, args=(
            skeleton_file, solver1, solver2, solver1_bin, solver2_bin, 10, argument["incremental"], core_num, add_option, rules, buggy, temp, argument, tactic))
        time.sleep(1)
        process.start()
        os.system("taskset -p -c " + str(core_num) + " " + str(process.pid))
        core_num += 1


def auto_collect_buggy_formulas(token, store_path):
    """
    collect bug-triggering formulas in several solvers' bug trackers
    :param token: GitHub personal token
    :param store_path:
    :return:
    """
    solvers = ["z3", "cvc5", "yices2", "opensmt", "cvc5-projects"]
    process_pool = []
    for solver in solvers:
        p = multiprocessing.Process(target=collect_buggy_formula, args=(token, solver, store_path))
        p.start()
        process_pool.append(p)
    while process_pool:
        for index, process in enumerate(process_pool):
            if not process.is_alive():
                process_pool.pop(index)
                break


def main():
    arguments = MainArgumentParser()
    arguments.parse_arguments(argparse.ArgumentParser())
    parsedArguments = arguments.get_arguments()
    # print(parsedArguments)
    if parsedArguments["update"]:
        token_path = rootpath + "/config/token.txt"
        if parsedArguments["token"] is None:
            if os.path.exists(token_path):
                with open(token_path) as f:
                    parsedArguments["token"] = f.read().replace("\n", "")
            else:
                print("Please provide your GitHub token.")
                return
        else:
            with open(token_path, "w") as token_file:
                token_file.write(parsedArguments["token"])
        if parsedArguments["bugfolder"] is None:
            parsedArguments["bugfolder"] = rootpath + "/bug_triggering_formulas"
        auto_collect_buggy_formulas(parsedArguments["token"], parsedArguments["bugfolder"])
        print("recheck SMT instances......")
        standardize_instance(parsedArguments["bugfolder"])
        print("finished")
        print("generating configuration files......")
        export_buggy_seed(parsedArguments["bugfolder"], buggy)
        export_skeleton(parsedArguments["bugfolder"], skeletons)
        export_association_rules(parsedArguments["bugfolder"], rules, parsedArguments["sup"], parsedArguments["conf"])
        print("update finished")
    else:
        solver1 = parsedArguments["solver1"]
        solver2 = parsedArguments["solver2"]
        solver1_bin = parsedArguments["solverbin1"]
        solver2_bin = parsedArguments["solverbin2"]
        if None in [solver1, solver2, solver1_bin, solver2_bin]:
            print("Please check if the correct solvers and their binaries are given.")
            return
        core_num = int(parsedArguments["core"])
        cores = int(parsedArguments["cores"])
        run(skeletons, parsedArguments, solver1, solver2, solver1_bin, solver2_bin, core_num, cores, parsedArguments["option"])


if __name__ == "__main__":
    main()
