#!/usr/bin/env python3

from util.kSAT import kSAT
from util import SATquboResult
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="WMIS qubo result file", type=str)
    args = parser.parse_args()
        
    instancePath = args.instance
    if instancePath == None:
        instancePath = str(input("Instance file: "))
        
    resultFile = args.result
    if resultFile == None:
        resultFile = str(input("WMIS qubo result file: "))
        
    __verify(instancePath, resultFile)
    
    
def __verify(instancePath, resultFile):
    sat = kSAT()
    sat.readDIMACS(instancePath)
    
    assignments = SATquboResult.readAssignmentsFromFile(resultFile)
    
    
    evaluations = sat.evaluate(assignments)
    
    for i in range(len(assignments)):
        print(assignments[i], evaluations[i])
        

if __name__ == "__main__":
    main()