7 PAT
= r
'\(= i(?P<i>\d+)x(?P<x>\d+)y(?P<y>\d+) (?P<v>true|false)\)'
9 def print_board(previous
, data
, tofile
):
10 """Prints a peg solitaire board"""
11 tofile
.write('$\\xymatrix@=1.2pt@M=1.2pt{')
18 pos
= [d
for d
in data
if d
[0] == xco
and d
[1] == yco
]
19 poso
= [d
for d
in previous
if d
[0] == xco
and d
[1] == yco
]
21 if pos
[0][2] and not poso
[0][2]:
23 elif pos
[0][2] != poso
[0][2]:
26 if begin
[0][0] < end
[0]:
28 begin
= min(begin
, key
=lambda x
: x
[0])
29 elif begin
[0][0] > end
[0]:
31 begin
= max(begin
, key
=lambda x
: x
[0])
32 elif begin
[0][1] < end
[1]:
34 begin
= min(begin
, key
=lambda x
: x
[1])
35 elif begin
[0][1] > end
[1]:
37 begin
= max(begin
, key
=lambda x
: x
[1])
43 pos
= [d
for d
in previous
if d
[0] == xco
and d
[1] == yco
]
47 tofile
.write('\\circ ' if pos
[0][2] else '\\times ')
48 if begin
and pos
[0][0] == begin
[0] and pos
[0][1] == begin
[1]:
49 tofile
.write('\\ar@{{-)}}[{}]'.format(direction
))
51 tofile
.write('\\\\\n')
54 def parse(lines
, output
):
55 """Parse the model from yices"""
59 match
= re
.match(PAT
, line
)
61 ite
= int(match
.group('i'))
64 data
[ite
].append((int(match
.group('x')), int(match
.group('y')),
65 match
.group('v') == 'true'))
66 output
.write('\\begin{tabular}{cccccc}\n')
68 for i
, (_
, dat
) in enumerate(sorted(data
.items())):
72 print_board(prev
, dat
, output
)
76 output
.write('\\\\\\\\')
77 print_board(prev
, None, output
)
78 output
.write('\\end{tabular}\n')
80 if __name__
== '__main__':
81 if len(sys
.argv
) == 1:
82 parse(sys
.stdin
, sys
.stdout
)
83 elif len(sys
.argv
) == 2:
84 with
open(sys
.argv
[1], 'r') as fin
:
85 parse(fin
, sys
.stdout
)
87 with
open(sys
.argv
[1], 'r') as fin
, open(sys
.argv
[2], 'w') as fout
: