a2/src/4/a4.py

   1 #!/bin/env python
   2 #pylint: disable-msg=too-many-locals,invalid-name
   3 """hi"""
   4
   5 def generate():
   6     """Generates the yices code for peg solitaire"""
   7     pos = [(x, y) for x in range(7) for y in range(7) if
   8            not ((x < 2 and y < 2) or # exclude topleft
   9                 (x > 4 and y > 4) or # exclude bottomright
  10                 (x > 4 and y < 2) or # exclude topright
  11                 (x < 2 and y > 4))   # exclude bottomleft
  12           ]
  13     ill_middles = [
  14         (2, 0), (4, 0), (0, 2), (0, 4), (6, 2), (6, 4), (2, 6), (4, 6)]
  15     holes = [(3, 3)]
  16     winning = (3, 3)
  17
  18
  19     iterations = len(pos)-len(holes)
  20     posp = [p for p in pos if p not in ill_middles]
  21     print """
  22     (benchmark a1.smt
  23     :logic QF_UF
  24     :extrapreds (
  25         {}
  26     )
  27     :formula
  28     (and\
  29     """.format('\n\t'.join(' '.join('(i{}x{}y{})'.format(i, x, y)
  30                                     for x, y in pos)
  31                            for i in range(iterations)))
  32     print ';Iteration 0'
  33     print ' '.join('(not i0x{}y{})'.format(x, y) for x, y in holes),
  34     print ' '.join('i0x{}y{}'.format(x, y)
  35                    for x, y in pos if (x, y) not in holes)
  36
  37
  38     for i in range(1, iterations):
  39         print ';Iteration {}'.format(i)
  40         print '(or'
  41         for sx, sy in pos:
  42             for mx, my in posp:
  43                 if mx == sx and my == sy:
  44                     continue
  45                 for ex, ey in pos:
  46                     if (ex == sx and ey == sy)or (ex == mx and ey == my):
  47                         continue
  48                     if not ((sy == my and my == ey and sx == mx+1 and
  49                              mx == ex+1) or
  50                             (sy == my and my == ey and sx == mx-1 and
  51                              mx == ex-1) or
  52                             (sx == mx and mx == ex and sy == my+1 and
  53                              my == ey+1) or
  54                             (sx == mx and mx == ex and sy == my-1 and
  55                              my == ey-1)):
  56                         continue
  57                     print '(and'
  58                     print ('i{0}x{1}y{2} '
  59                            'i{0}x{3}y{4} '
  60                            '(not i{0}x{5}y{6})').format(i-1,
  61                                                         sx, sy, mx, my, ex, ey)
  62                     print ('(not i{0}x{1}y{2}) '
  63                            '(not i{0}x{3}y{4}) '
  64                            'i{0}x{5}y{6}').format(i, sx, sy, mx, my, ex, ey)
  65                     for ox, oy in pos:
  66                         if not((ox == sx and oy == sy) or
  67                                (ox == mx and oy == my) or
  68                                (ox == ex and oy == ey)):
  69                             print '(= i{0}x{1}y{2} i{3}x{1}y{2})'.format(
  70                                 i, ox, oy, i-1),
  71                     print ')'
  72         print ')'
  73
  74     print ';Negated winning condition'
  75     print 'i{}x{}y{}'.format(iterations-1, winning[0], winning[1]),
  76     print ' '.join('(not i{}x{}y{})'.format(iterations-1, x, y)
  77                    for x, y in pos if (x, y) != winning)
  78
  79     print '))'
  80
  81 if __name__ == '__main__':
  82     generate()