"""
This script is written for running Uwe Schöning's WalkSAT algorithm
    [Uwe Schöning:
    A probabilistic algorithm for k-SAT and constraint satisfaction problems.
    In: Proceedings of FOCS 1999, IEEE, pages 410–414.]
via the command line
by specifying the instance to solve, and the seed to use.
Uwe Schöning's WalkSAT algorithm can be seen as a special case of the probSAT algorithm
    [Adrian Balint, Uwe Schöning:
    Choosing Probability Distributions for Stochastic Local Search and the Role of Make versus Break.    
    In: Lecture Notes in Computer Science, 2012, Volume 7317, Theory and Applications of Satisfiability Testing - SAT 2012, pages 16-29.
    https://www.uni-ulm.de/fileadmin/website_uni_ulm/iui.inst.190/Mitarbeiter/balint/SAT2012.pdf]
with exponential function (break-only-exp-algorithm) and c_b = 1.

The script will record the number of flips, the time used, and the seed used.
"""

import argparse
from subprocess import Popen, PIPE
from time import sleep
from os.path import exists
import sys
from timeit import default_timer as timer
import pathlib as pl

def run_alg(instance):
    solve_instance_path = pl.Path(__file__).absolute().parent / "util" / "solve_instance.sh"
    
    p = Popen(["bash", str(solve_instance_path), instance], stdin = PIPE, stdout = PIPE, stderr=PIPE)

    output, err = p.communicate()
    rc = p.returncode
    err = err.decode("utf-8") if err else ""
    if err != "":
        print(err, file=sys.stderr)

    return output.decode("utf-8")

def parse_result(res_str):
    res = {}
    
    for line in res_str.splitlines():
        if line.startswith("c restarts"):
            res["restarts"] = int(line.split(":")[1].strip().split(" ")[0])
        elif line.startswith("c conflicts"):
            res["conflicts"] = int(line.split(":")[1].strip().split(" ")[0])
        elif line.startswith("c decisions"):
            res["decisions"] = int(line.split(":")[1].strip().split(" ")[0])
        elif line.startswith("c propagations"):
            res["propagations"] = int(line.split(":")[1].strip().split(" ")[0])
        elif line.startswith("c nb reduced Clauses"):
            res["reduced_clauses"] = int(line.split(":")[1])
        elif line.startswith("c CPU time"):
            res["cpu_time"] = float(line.split(":")[1].strip().split(" ")[0])
        elif line.startswith("s"):
            res["result"] = line.split(" ")[1].strip()

    return res

def parse_instance_path(ipath):
    name = pl.Path(ipath).name.strip()

    instance = name[:-len(".cnf.bz2")]

    return instance



if __name__ == '__main__':
    parser = argparse.ArgumentParser()
    parser.add_argument("-s", "--seed", type=int, default=1909, help="The seed.")
    parser.add_argument("-i", "--instance", help="The instance.")

    args = parser.parse_args()

    res_str = run_alg(str(pl.Path(args.instance).absolute()))

    iname = parse_instance_path(args.instance)

    res = parse_result(res_str)
    
    res_vals = [ iname
                ,res["restarts"]
                ,res["conflicts"]
                ,res["decisions"]
                ,res["propagations"]
                ,res["reduced_clauses"]
                ,res["cpu_time"]
                ,res["result"]] 

    print(','.join(list(map(str, res_vals))))