-
Notifications
You must be signed in to change notification settings - Fork 0
/
transvipr.py
72 lines (65 loc) · 2 KB
/
transvipr.py
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
#!/usr/bin/python
# usage: python create_cmatrix.py probname sdname ncluster
import sys
import matplotlib.pyplot as plt
import numpy as np
import re
import glob, os
from itertools import chain, combinations
def createSetNumber(Set):
ret = 0
for s in Set:
ret = ret + 2 ** (s - 1)
return ret - 1
def powerset(iterable):
"powerset([1,2,3]) --> () (1,) (2,) (3,) (1,2) (1,3) (2,3) (1,2,3)"
s = list(iterable)
return chain.from_iterable(combinations(s, r) for r in range(len(s)+1))
def createConversion( size ):
powS = list(powerset(range(1,size+1)))[1:]
c = 0
#print powS
convtbl = []
for s in powS:
#print (s)
#print createSetNumber(s)
convtbl.append( createSetNumber(s) )
c = c + 1
#print convtbl
return convtbl
vipfile = sys.argv[1]
size = int( sys.argv[2] )
outputname = vipfile + '.input'
table = createConversion(size)
with open(vipfile, 'r') as file:
outfile = open(outputname, 'w')
vartablestarted = False
for line in file.readlines():
if line.strip() == '':
continue
# we don't need the derivation section for coq-input checker
if line.startswith("DER"):
break
if not vartablestarted:
if line.split()[0] == 'VAR':
vartablestarted = True
outfile.write(line)
else:
if line.split()[0] == 'INT':
vartablestarted = False
outfile.write(line)
else:
elems = re.split('\$|#', line)
if len(elems) < 3:
outfile.write(line)
else:
#print elems
varIsX = (elems[1] == 'x')
index = int(elems[2])
#print varIsX
#print index
chgIndex = str(table[index])
elems[2] = chgIndex
outfile.write( "t_" + elems[1] + '#' + elems[2] + '\n')
file.close()
outfile.close()