#!/usr/bin/env python3

from util import SATquboResult
import argparse
from util.kSAT import kSAT
from util import minisat as mSatU
from util import SATquboResult
import os
import json

def main():
    args = __parseArguments()
    
    
    comparison = __compare(args["instancePath"],
                           args["minisatResult"],
                           args["quboResult"])
    
    outputFilePath = os.path.join(args["outputDir"],
                                  args["instanceFileName"] + ".cmp")
                                  
    __writeComparison(comparison, outputFilePath)


def __parseArguments():
    parser = argparse.ArgumentParser()
    parser.add_argument("-i", "--instance", help="instance file, has to be in DIMACS format", type=str)
    parser.add_argument("-m", "--minisat_result", help="Minisat result file", type=str)
    parser.add_argument("-q", "--qubo_result", help="Qubo result file", type=str)
    parser.add_argument("-o", "--output", help="Directory to store the comparison (optional)", type=str)
    args = parser.parse_args()
    
    arguments = {}
    
    arguments["instancePath"] = args.instance
    if arguments["instancePath"] == None:
         arguments["instancePath"] = str(input("Instance file: "))
    
    #arguments["instancePath"]
    arguments["instanceFileName"] = os.path.basename(arguments["instancePath"])
    
    arguments["minisatResult"] = args.minisat_result
    if arguments["minisatResult"] == None:
         arguments["minisatResult"] = str(input("Minisat result file: "))
         
    arguments["quboResult"] = args.qubo_result
    if arguments["quboResult"] == None:
         arguments["quboResult"] = str(input("Qubo result file: "))
    
    arguments["outputDir"] = args.output
    if arguments["outputDir"] == None:
        arguments["outputDir"] = str(input("Output directory: "))
        
    arguments["outputDir"] = os.path.abspath(arguments["outputDir"])
    
    
    
    return arguments

def __compare(instancePath, msatResultFile, quboResultFile):
    comparison = {}
    sat = kSAT()
    sat.readDIMACS(instancePath)
    
    comparison["instance"] = os.path.basename(instancePath)
    comparison["minisat_satisfiable"] = __getMinisatSatisfiability(msatResultFile)
    comparison["qubo_satisfiable"] = __getQuboSatisfiability(quboResultFile)
    comparison["degrees_of_variables"] = sat.getDegreesOfVariables()
    comparison["conflicts_per_variable"] = __countConflicts(sat.getConflicts())
    
    return comparison
            

def __getMinisatSatisfiability(resultFile):
    minisatResult = mSatU.readMinisatResult(resultFile)
    
    return minisatResult["satisfiable"]

def __getQuboSatisfiability(resultFile):
    results = SATquboResult.readResultsFromFile(resultFile)
    
    for result in results:
        if result.satisfiesInstance():
            return True
    
    return False

def __writeComparison(comparison, outputFilePath):
    if outputFilePath == None:
        return
    
    outputFile = open(outputFilePath, "w+")
    
    outputFile.write(json.dumps(comparison) + "\n")
    
    outputFile.close()

def __countConflicts(conflicts):
    conflictsPerVariable = {}
    
    for conflict in conflicts:
        varLabel = abs(conflict[0][1])
        
        if varLabel not in conflictsPerVariable:
            conflictsPerVariable[varLabel] = 1
        else:
            conflictsPerVariable[varLabel] += 1
            
    return conflictsPerVariable
    
if __name__ == "__main__":
    main()