#!/usr/bin/env python3

from util import kSAT
from util import minisat as mSatU
import argparse


def main():
    parser = argparse.ArgumentParser()
    parser.add_argument("-i", "--instance", help="instance file, has to be in DIMACS format", type=str)
    parser.add_argument("-r", "--result", help="minisat result file", type=str)
    args = parser.parse_args()
        
    instancePath = args.instance
    if instancePath == None:
        instancePath = str(input("Instance file: "))
        
    minisatResultFile = args.result
    if minisatResultFile == None:
        minisatResultFile = str(input("Minisat result file: "))
    
    print("Checking...")
    print("Instance:\t%s" % instancePath)
    print("Minisat result:\t%s" % minisatResultFile)
    
    checkStr = __checkResult(instancePath, minisatResultFile)
    
    print("check:\t\t%s" % checkStr)
    
    
def __checkResult(instancePath, minisatResultFile):
    sat = kSAT.kSAT()
    
    sat.readDIMACS(instancePath)
    
    minisatResult = mSatU.readMinisatResult(minisatResultFile)
    
    if minisatResult["satisfiable"]:
        if sat.checkAssignment(minisatResult["assignments"]):
            return "results do match"
        else:
            return "results do NOT match"
    else:
        return "unsatisfiable"
    
if __name__ == "__main__":
    main()