update

[ar1516.git] / src / a2.py

diff --git a/src/a2.py b/src/a2.py
index a782fe7..eb1f164 100644 (file)
--- a/src/a2.py
+++ b/src/a2.py
@@ -1,64 +1,33 @@
 #!/usr/bin/env python3
-pc = [(4, 2), (4, 2), (4, 2)]
-rc = [(9, 7), (12, 6), (10, 7), (18, 5), (20, 4), (10, 6), (8, 6), (10, 8)]
-mx = 29
-my = 22
-pd = 17
+import sys
+import re
 
-# Print variables and preamble
-print('(benchmark a4.smt')
-print(':logic QF_UFLIA')
-print(':extrafuns (')
-for i, (w, h) in enumerate(pc+rc, 1):
-    print('(c{}x Int)'.format(i), end=' ')
-    print('(c{}y Int)'.format(i), end=' ')
-    print('(c{}w Int)'.format(i), end=' ')
-    print('(c{}h Int)'.format(i))
-print(')')
+comps = {}
 
-print(':formula')
-print('(and')
+for line in sys.stdin:
+    match = re.match('\(= c(?P<c>\d+)(?P<t>.) (?P<v>\d+)\)', line)
+    if match:
+        comps[match.group('c')] = comps.get(match.group('c'), {})
+        comps[match.group('c')][match.group('t')] = int(match.group('v'))
 
-# Print the PC and RC subformulas
-for i, (w, h) in enumerate(pc+rc, 1):
-    # Print the width and height
-    print(('(or '
-           '(and (= c{0}w {1}) (= c{0}h {2})) '
-           '(and (= c{0}w {2}) (= c{0}h {1})))').format(i, w-1, h-1))
-    # Print the bounds of the coordinates
-    print(('(> c{0}x 0) (> c{0}y 0)'
-           '(<= (+ c{0}x c{0}w) {1}) (<= (+ c{0}y c{0}h) {2})'
-           ).format(i, mx, my))
+maxx = max(c['x']+c['w'] for c in comps.values())
+maxy = max(c['y']+c['h'] for c in comps.values())
+print('$\\begin{{array}}{{|l|{}|}}'.format('@{}c@{}'*maxx))
+print('\t\\toprule')
+print('\t & {}\\\\'.format(
+    ' & '.join(map(str, range(1, maxx+1)))))
+print('\t\\midrule')
+for y in range(1, maxy+1):
+    print('\t{} & '.format(y), end='')
+    for x in range(1, maxx+1):
+        cs = [c for c in comps if
+              comps[c]['y'] + comps[c]['h'] >= y and comps[c]['y'] <= y and
+              comps[c]['x'] + comps[c]['w'] >= x and comps[c]['x'] <= x]
+        if cs:
+            print('\\hspace{{.5mm}}{}\\hspace{{.5mm}}'.format(cs[0]), end='')
+        if x != maxx:
+            print(' & ', end='')
+    print('\\\\')
 
-    # Print the non overlap with others
-    for j in range(1, 1+len(pc+rc)):
-        if i != j:
-            print((
-                 '(or '
-                 '(> c{0}x (+ c{1}x c{1}w)) (< (+ c{0}x c{0}w) c{1}x) '
-                 '(> c{0}y (+ c{1}y c{1}h)) (< (+ c{0}y c{0}h) c{1}y)'
-                 ')').format(i, j))
-
-# Print the PC distance to eachother
-for i, _ in enumerate(pc, 1):
-    for j, _ in enumerate(pc, 1):
-        if i != j:
-            print(('(or '
-                   '(> (- (+ c{0}x (/ c{0}w 2)) (+ c{1}x (/ c{1}w 2))) {2}) '
-                   '(> (- (+ c{1}x (/ c{1}w 2)) (+ c{0}x (/ c{0}w 2))) {2}) '
-                   '(> (- (+ c{0}y (/ c{0}h 2)) (+ c{1}y (/ c{1}h 2))) {2}) '
-                   '(> (- (+ c{1}y (/ c{1}h 2)) (+ c{0}y (/ c{0}h 2))) {2})'
-                   ')').format(i, j, pd))
-
-            # Print the constraint that they have to be connected to a ps
-for i, _ in enumerate(rc, 1+len(pc)):
-    print('(or')
-    for j, _ in enumerate(pc, 1):
-        print(('(not (or '
-               '(> c{0}x (+ c{1}x 1 c{1}w)) (< (+ c{0}x c{0}w) (- c{1}x 1)) '
-               '(> c{0}y (+ c{1}y 1 c{1}h)) (< (+ c{0}y c{0}h) (- c{1}y 1))'
-               '))').format(i, j))
-    print(')')
-
-# Close the and,benchmark parenthesis
-print('))')
+print('\t\\bottomrule')
+print('\\end{array}$')