#!/bin/python

# This script tests a file containing a list of GR(1) assumptions, one per line.
# It computes d1 and d2 of their conjunction
# Syntax: $ python testFileExample <src_file>
import sys
import timeit

import Weakness.src.weakness as w
import ref_utils.io_utils as io

infile = open(sys.argv[1],"r")
varfile = open(sys.argv[1]+"_vars","r")
phi = " & ".join([x.strip() for x in infile.readlines() if x[0:2] != "//"  and x != ""])
#gr1_units = [x.strip() for x in infile.readlines() if x[0:2] != "//"  and x != ""]


# subformulae = gr1_units
# while subformulae.__len__() > 5:
#     nextsubformulae = []
#     remainderformulae = subformulae[-1:-(subformulae.__len__() % 5) - 1]
#     for i in range(0,subformulae.__len__()/5):
#         nextsubformulae.append('('+' & '.join(subformulae[5*i:5+5*i])+')')
#     if remainderformulae.__len__() > 0:
#         nextsubformulae.append('('+' & '.join(remainderformulae)+')')
#     subformulae = nextsubformulae
#
# phi = subformulae[0]

vars = varfile.readlines()
vars = map(lambda x: x.strip(),vars)
print "vars: " + str(vars)
print "phi: "+ io.normalizeSpinFormulaSyntax(phi)

starttime = timeit.default_timer()
d2 = w.computeD2(phi,vars)
print "d2 = " + str(d2)
d1 = w.computeD1(phi,vars)
elapsed = timeit.default_timer() - starttime

print "d1 = " + str(d1)
print "time = " + str(elapsed)