blob: 3fb3daa88f345cae841b0e158eb04cad24186b9d (
plain)
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
|
#!/usr/bin/env python3
import re
import sys
# Maximum number of elements
n = 8
matrix = []
for line in sys.stdin:
line = line.strip()
if line == "unsat":
sys.exit('unsat!')
if line == "sat":
continue
m = re.match(r'a(\d+)_(\d+) -> (\d+)', line)
var_number, step, value = map(int, m.groups())
# auto-detect size, extending matrix size if necessary.
while len(matrix) <= step:
matrix.append([None] * n)
matrix[step][var_number - 1] = value
# List of cells that have changed since the previous iteration. Note that the
# first row has no changed cell and therefore stores "None"
changedCells = [None]
for i, cells in enumerate(matrix):
if i == 0:
continue # skip first row
previousRow = matrix[i - 1]
for col, prevValue in enumerate(previousRow):
if cells[col] != prevValue:
# Found changed cell!
changedCells.append(col)
break
else:
# Should not happen! Something got stuck?
changedCells.append(None)
line = " "
for col in range(len(matrix[0])):
line += " & $a_%d$" % (col + 1)
line += r" \\"
print(line)
print(r"\hline")
for step, cells in enumerate(matrix):
line = "%2d" % step
for col, value in enumerate(cells):
if changedCells[step] == col:
line += r" & \bf%2d" % value
else:
line += " & %5d" % value
line += r" \\"
if step > 0 and changedCells[step] is None:
line += " % unchanged!"
print(line)
|
