ar finished

[master.git] / ar / assignment1 / src / a2.py

diff --git a/ar/assignment1/src/a2.py b/ar/assignment1/src/a2.py
new file mode 100644 (file)
index 0000000..85473a3
--- /dev/null
+++ b/ar/assignment1/src/a2.py
@@ -0,0 +1,66 @@
+#!/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
+
+# Print preamble
+print("(benchmark a4.smt")
+print(":logic QF_UFLIA")
+
+# Print variables
+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(")")
+
+print(":formula")
+print("(and")
+
+# 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))
+
+    # 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("))")