success with 4:)

[ar1516.git] / a2 / src / 4 / a4.py

diff --git a/a2/src/4/a4.py b/a2/src/4/a4.py
new file mode 100644 (file)
index 0000000..b216b3b
--- /dev/null
+++ b/a2/src/4/a4.py
@@ -0,0 +1,82 @@
+#!/bin/env python
+#pylint: disable-msg=too-many-locals,invalid-name
+"""hi"""
+
+def generate():
+    """Generates the yices code for peg solitaire"""
+    pos = [(x, y) for x in range(7) for y in range(7) if
+           not ((x < 2 and y < 2) or # exclude topleft
+                (x > 4 and y > 4) or # exclude bottomright
+                (x > 4 and y < 2) or # exclude topright
+                (x < 2 and y > 4))   # exclude bottomleft
+          ]
+    ill_middles = [
+        (2, 0), (4, 0), (0, 2), (0, 4), (6, 2), (6, 4), (2, 6), (4, 6)]
+    holes = [(3, 3)]
+    winning = (3, 3)
+
+
+    iterations = len(pos)-len(holes)
+    posp = [p for p in pos if p not in ill_middles]
+    print """
+    (benchmark a1.smt
+    :logic QF_UF
+    :extrapreds (
+        {}
+    )
+    :formula
+    (and\
+    """.format('\n\t'.join(' '.join('(i{}x{}y{})'.format(i, x, y)
+                                    for x, y in pos)
+                           for i in range(iterations)))
+    print ';Iteration 0'
+    print ' '.join('(not i0x{}y{})'.format(x, y) for x, y in holes),
+    print ' '.join('i0x{}y{}'.format(x, y)
+                   for x, y in pos if (x, y) not in holes)
+
+
+    for i in range(1, iterations):
+        print ';Iteration {}'.format(i)
+        print '(or'
+        for sx, sy in pos:
+            for mx, my in posp:
+                if mx == sx and my == sy:
+                    continue
+                for ex, ey in pos:
+                    if (ex == sx and ey == sy)or (ex == mx and ey == my):
+                        continue
+                    if not ((sy == my and my == ey and sx == mx+1 and
+                             mx == ex+1) or
+                            (sy == my and my == ey and sx == mx-1 and
+                             mx == ex-1) or
+                            (sx == mx and mx == ex and sy == my+1 and
+                             my == ey+1) or
+                            (sx == mx and mx == ex and sy == my-1 and
+                             my == ey-1)):
+                        continue
+                    print '(and'
+                    print ('i{0}x{1}y{2} '
+                           'i{0}x{3}y{4} '
+                           '(not i{0}x{5}y{6})').format(i-1,
+                                                        sx, sy, mx, my, ex, ey)
+                    print ('(not i{0}x{1}y{2}) '
+                           '(not i{0}x{3}y{4}) '
+                           'i{0}x{5}y{6}').format(i, sx, sy, mx, my, ex, ey)
+                    for ox, oy in pos:
+                        if not((ox == sx and oy == sy) or
+                               (ox == mx and oy == my) or
+                               (ox == ex and oy == ey)):
+                            print '(= i{0}x{1}y{2} i{3}x{1}y{2})'.format(
+                                i, ox, oy, i-1),
+                    print ')'
+        print ')'
+
+    print ';Negated winning condition'
+    print 'i{}x{}y{}'.format(iterations-1, winning[0], winning[1]),
+    print ' '.join('(not i{}x{}y{})'.format(iterations-1, x, y)
+                   for x, y in pos if (x, y) != winning)
+
+    print '))'
+
+if __name__ == '__main__':
+    generate()