Update

diff --git a/ar/assignments/2.tex b/ar/assignments/2.tex
index d1b13f1..5731d97 100644 (file)
--- a/ar/assignments/2.tex
+++ b/ar/assignments/2.tex
@@ -42,10 +42,11 @@ specified width and height.
                \nonumber & \vee\frac{c_jx+c_jw}{2}-\frac{c_ix+c_iw}{2}>15\\
                \nonumber & \vee\frac{c_iy+c_ih}{2}-\frac{c_jy+c_jh}{2}>15\\
                \nonumber & \vee\frac{c_jy+c_jh}{2}-\frac{c_iy+c_ih}{2}>15\Biggr)\wedge\\
-       \bigwedge_{i\in RC}\bigvee_{j\in PC}\Biggl( & c_ix=c_jx+c_jw+1\\
-               \nonumber & \vee c_ix+c_iw+1=c_jx\\
-               \nonumber & \vee c_iy=c_jy+c_jh+1\\
-               \nonumber & \vee c_iy+c_ih+1=c_jy\Biggr)
+       \bigwedge_{i\in RC}\bigvee_{j\in PC}\Biggl(
+               \nonumber & !(     c_ix-1     >c_jx+c_jw\\
+               \nonumber & \vee c_ix+1+c_jw<c_jx\\
+               \nonumber & \vee c_iy-1     >c_jy+c_jh\\
+               \nonumber & \vee c_iy+1+c_jh<c_jh\Biggr)\\
 \end{align}
 
 \subsection{SMT format solution}

diff --git a/ar/assignments/src/2.py b/ar/assignments/src/2.py
index 0d935af..bbaabf0 100644 (file)
--- a/ar/assignments/src/2.py
+++ b/ar/assignments/src/2.py
@@ -16,7 +16,7 @@ for i, (w, h) in enumerate(pc+rc, 1):
     print("(c{:02d}x Int)".format(i), end=' ')
     print("(c{:02d}y Int)".format(i), end=' ')
     print("(c{:02d}w Int)".format(i), end=' ')
-    print("(c{:02d}h Int)".format(i), end=' ')
+    print("(c{:02d}h Int)".format(i))
 print(")")
 
 # Preamble2
@@ -30,7 +30,7 @@ for i, (w, h) in enumerate(pc+rc, 1):
         '\t(or '
         '(and (= c{0:02d}w {1}) (= c{0:02d}h {2})) '
         '(and (= c{0:02d}w {2}) (= c{0:02d}h {1}))'
-        ')').format(i, w, h))
+        ')').format(i, w-1, h-1))
 
     # Print the bounds of the coordinates
     print((
@@ -40,35 +40,42 @@ for i, (w, h) in enumerate(pc+rc, 1):
 
     # Print the non overlap with others
     for j in range(1, 1+len(pc+rc)):
-        print((
-            '\t(or (= {0} {1})\n'
-            '\t\t(> c{0:02d}x (+ c{1:02d}x c{1:02d}w)) '
-            '(< (+ c{0:02d}x c{0:02d}w) c{1:02d}x)\n'
-            '\t\t(> c{0:02d}y (+ c{1:02d}y c{1:02d}h)) '
-            '(< (+ c{0:02d}y c{0:02d}h) c{1:02d}y)'
-            ')').format(i, j))
+        if i != j:
+            print((
+                '\t(or \n'
+                '\t\t(> c{0:02d}x (+ c{1:02d}x c{1:02d}w)) '
+                '(< (+ c{0:02d}x c{0:02d}w) c{1:02d}x)\n'
+                '\t\t(> c{0:02d}y (+ c{1:02d}y c{1:02d}h)) '
+                '(< (+ c{0:02d}y c{0:02d}h) c{1:02d}y)'
+                ')').format(i, j))
 
 # Print the PC distance to eachother
-for i, _ in enumerate(pc, 1):
-    for j, _ in enumerate(pc, 1):
-        print((
-            '\t(or (= {0} {1})\n'
-            '\t\t(> (- (/ (+ c{0:02d}x c{0:02d}w) 2) (/ (+ c{1:02d}x c{1:02d}w) 2)) {2})\n'
-            '\t\t(> (- (/ (+ c{1:02d}x c{1:02d}w) 2) (/ (+ c{0:02d}x c{0:02d}w) 2)) {2})\n'
-            '\t\t(> (- (/ (+ c{0:02d}y c{0:02d}h) 2) (/ (+ c{1:02d}y c{1:02d}h) 2)) {2})\n'
-            '\t\t(> (- (/ (+ c{1:02d}y c{1:02d}h) 2) (/ (+ c{0:02d}y c{0:02d}h) 2)) {2})'
-            ')').format(i, j, pd))
+#for i, _ in enumerate(pc, 1):
+#    for j, _ in enumerate(pc, 1):
+#        if i != j:
+#            print((
+#                '\t(or \n'
+#                '\t\t(> (- (/ (+ c{0:02d}x c{0:02d}w) 2) '
+#                '(/ (+ c{1:02d}x c{1:02d}w) 2)) {2})\n'
+#                '\t\t(> (- (/ (+ c{1:02d}x c{1:02d}w) 2) '
+#                '(/ (+ c{0:02d}x c{0:02d}w) 2)) {2})\n'
+#                '\t\t(> (- (/ (+ c{0:02d}y c{0:02d}h) 2) '
+#                '(/ (+ c{1:02d}y c{1:02d}h) 2)) {2})\n'
+#                '\t\t(> (- (/ (+ c{1:02d}y c{1:02d}h) 2) '
+#                '(/ (+ c{0:02d}y c{0:02d}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('\t(or')
     for j, _ in enumerate(pc, 1):
         print((
-            '\t\t(= c{0:02d}x (+ c{1:02d}x c{1:02d}w 1))\n'
-            '\t\t(= (+ c{0:02d}x c{0:02d}w 1) c{1:02d}x)\n'
-            '\t\t(= c{0:02d}y (+ c{1:02d}y c{1:02d}h 1))\n'
-            '\t\t(= (+ c{0:02d}y c{0:02d}h 1) c{1:02d}y)'
-            ).format(i, j))
+            '\t(not (or \n'
+            '\t\t(> c{0:02d}x (+ c{1:02d}x 1 c{1:02d}w)) '
+            '(< (+ c{0:02d}x c{0:02d}w) (- c{1:02d}x 1))\n'
+            '\t\t(> c{0:02d}y (+ c{1:02d}y 1 c{1:02d}h)) '
+            '(< (+ c{0:02d}y c{0:02d}h) (- c{1:02d}y 1))'
+            '))').format(i, j))
     print('\t)')
 
 # Close the and,benchmark parenthesis