a2/src/4/print4z3.py

   1 #!/bin/env python
   2 """hi"""
   3
   4 import sys
   5 import re
   6
   7 PAT = r'\(= i(?P<i>\d+)x(?P<x>\d+)y(?P<y>\d+) (?P<v>true|false)\)'
   8
   9 def print_board(previous, data, tofile):
  10     """Prints a peg solitaire board"""
  11     tofile.write('$\\xymatrix@=1.2pt@M=1.2pt{')
  12     begin = None
  13     if data is not None:
  14         end = None
  15         begin = []
  16         for yco in range(7):
  17             for xco in range(7):
  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]
  20                 if pos and poso:
  21                     if pos[0][2] and not poso[0][2]:
  22                         end = pos[0]
  23                     elif pos[0][2] != poso[0][2]:
  24                         begin.append(pos[0])
  25         if begin and end:
  26             if begin[0][0] < end[0]:
  27                 direction = 'rr'
  28                 begin = min(begin, key=lambda x: x[0])
  29             elif begin[0][0] > end[0]:
  30                 direction = 'll'
  31                 begin = max(begin, key=lambda x: x[0])
  32             elif begin[0][1] < end[1]:
  33                 direction = 'dd'
  34                 begin = min(begin, key=lambda x: x[1])
  35             elif begin[0][1] > end[1]:
  36                 direction = 'uu'
  37                 begin = max(begin, key=lambda x: x[1])
  38             else:
  39                 direction = None
  40
  41     for yco in range(7):
  42         for xco in range(7):
  43             pos = [d for d in previous if d[0] == xco and d[1] == yco]
  44             if not pos:
  45                 tofile.write('&')
  46             else:
  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))
  50                 tofile.write('&')
  51         tofile.write('\\\\\n')
  52     tofile.write('}$\n')
  53
  54 def parse(lines, output):
  55     """Parse the model from yices"""
  56     data = {}
  57     for line in lines:
  58         line = line.strip()
  59         match = re.match(PAT, line)
  60         if match:
  61             ite = int(match.group('i'))
  62             if ite not in data:
  63                 data[ite] = []
  64             data[ite].append((int(match.group('x')), int(match.group('y')),
  65                               match.group('v') == 'true'))
  66     output.write('\\begin{tabular}{cccccc}\n')
  67     prev = None
  68     for i, (_, dat) in enumerate(sorted(data.items())):
  69         if prev is None:
  70             prev = dat
  71         else:
  72             print_board(prev, dat, output)
  73             prev = dat
  74             output.write(' & ')
  75             if i % 5 == 0:
  76                 output.write('\\\\\\\\')
  77     print_board(prev, None, output)
  78     output.write('\\end{tabular}\n')
  79
  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)
  86     else:
  87         with open(sys.argv[1], 'r') as fin, open(sys.argv[2], 'w') as fout:
  88             parse(fin, fout)