added time for z4 problem 4

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

diff --git a/a2/src/4/print4z3.py b/a2/src/4/print4z3.py
new file mode 100644 (file)
index 0000000..e3eed1f
--- /dev/null
+++ b/a2/src/4/print4z3.py
@@ -0,0 +1,88 @@
+#!/bin/env python
+"""hi"""
+
+import sys
+import re
+
+PAT = r'\(= i(?P<i>\d+)x(?P<x>\d+)y(?P<y>\d+) (?P<v>true|false)\)'
+
+def print_board(previous, data, tofile):
+    """Prints a peg solitaire board"""
+    tofile.write('$\\xymatrix@=1.2pt@M=1.2pt{')
+    begin = None
+    if data is not None:
+        end = None
+        begin = []
+        for yco in range(7):
+            for xco in range(7):
+                pos = [d for d in data if d[0] == xco and d[1] == yco]
+                poso = [d for d in previous if d[0] == xco and d[1] == yco]
+                if pos and poso:
+                    if pos[0][2] and not poso[0][2]:
+                        end = pos[0]
+                    elif pos[0][2] != poso[0][2]:
+                        begin.append(pos[0])
+        if begin and end:
+            if begin[0][0] < end[0]:
+                direction = 'rr'
+                begin = min(begin, key=lambda x: x[0])
+            elif begin[0][0] > end[0]:
+                direction = 'll'
+                begin = max(begin, key=lambda x: x[0])
+            elif begin[0][1] < end[1]:
+                direction = 'dd'
+                begin = min(begin, key=lambda x: x[1])
+            elif begin[0][1] > end[1]:
+                direction = 'uu'
+                begin = max(begin, key=lambda x: x[1])
+            else:
+                direction = None
+
+    for yco in range(7):
+        for xco in range(7):
+            pos = [d for d in previous if d[0] == xco and d[1] == yco]
+            if not pos:
+                tofile.write('&')
+            else:
+                tofile.write('\\circ ' if pos[0][2] else '\\times ')
+                if begin and pos[0][0] == begin[0] and pos[0][1] == begin[1]:
+                    tofile.write('\\ar@{{-)}}[{}]'.format(direction))
+                tofile.write('&')
+        tofile.write('\\\\\n')
+    tofile.write('}$\n')
+
+def parse(lines, output):
+    """Parse the model from yices"""
+    data = {}
+    for line in lines:
+        line = line.strip()
+        match = re.match(PAT, line)
+        if match:
+            ite = int(match.group('i'))
+            if ite not in data:
+                data[ite] = []
+            data[ite].append((int(match.group('x')), int(match.group('y')),
+                              match.group('v') == 'true'))
+    output.write('\\begin{tabular}{cccccc}\n')
+    prev = None
+    for i, (_, dat) in enumerate(sorted(data.items())):
+        if prev is None:
+            prev = dat
+        else:
+            print_board(prev, dat, output)
+            prev = dat
+            output.write(' & ')
+            if i % 5 == 0:
+                output.write('\\\\\\\\')
+    print_board(prev, None, output)
+    output.write('\\end{tabular}\n')
+
+if __name__ == '__main__':
+    if len(sys.argv) == 1:
+        parse(sys.stdin, sys.stdout)
+    elif len(sys.argv) == 2:
+        with open(sys.argv[1], 'r') as fin:
+            parse(fin, sys.stdout)
+    else:
+        with open(sys.argv[1], 'r') as fin, open(sys.argv[2], 'w') as fout:
+            parse(fin, fout)