blob: 4cb77c34bdf6b90da07d26a6c00f3c88b9f699c7 (
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
|
#!/usr/bin/env python3
import re
import sys
# Maximum number of elements
n = 5
matrix = []
nextNodes = {}
# The pair that shows a loop (for b)
pair_for_b = [None] * 2
for line in sys.stdin:
line = line.strip()
if line == "unsat":
sys.exit('unsat!')
if line == "sat":
continue
m = re.match(r's(\d+)_(\d+) -> (\d+)', line)
if m:
villagenr, step, value = map(int, m.groups())
# auto-detect size, extending matrix size if necessary.
while len(matrix) <= step:
matrix.append([None] * n)
matrix[step][villagenr] = value
elif line.startswith('k'):
m = re.match(r'k(\d+) -> (\d+)', line)
step, value = map(int, m.groups())
pair_for_b[step] = value
else:
m = re.match(r'l(\d+) -> (\d+)', line)
step, value = map(int, m.groups())
nextNodes[step] = value
if False:
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 = "%3d" % step
for col, value in enumerate(cells):
if nextNodes.get(step) == col and col > 0:
line += r" &\bf%3d" % value
#line += r" & %4d." % value
else:
line += " & %5d" % value
line += r" & %s \\" % "SABCD"[nextNodes[step]]
if any(x == step for x in pair_for_b):
line += " % PAIR"
#line += r" \\"
print(line)
|
