add ar
authorMart Lubbers <mart@martlubbers.net>
Tue, 20 Oct 2015 12:44:52 +0000 (14:44 +0200)
committerMart Lubbers <mart@martlubbers.net>
Tue, 20 Oct 2015 12:44:52 +0000 (14:44 +0200)
ar/assignments/src/2.py

index f276fcb..0d935af 100644 (file)
@@ -1,13 +1,16 @@
 #!/usr/bin/env python3
 
-pc = [(4, 22), (4, 22), (4, 22)]
+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 preamble
 print("(benchmark a4.smt")
 print(":logic QF_UFLIA")
 
-##Print variables
+# Print variables
 print(":extrafuns (")
 for i, (w, h) in enumerate(pc+rc, 1):
     print("(c{:02d}x Int)".format(i), end=' ')
@@ -16,26 +19,26 @@ for i, (w, h) in enumerate(pc+rc, 1):
     print("(c{:02d}h Int)".format(i), end=' ')
 print(")")
 
-##Preamble2
+# Preamble2
 print(":formula")
 print("(and")
 
-##Print the PC and RC subformulas
+# Print the PC and RC subformulas
 for i, (w, h) in enumerate(pc+rc, 1):
-    ##Print the width and height
+    # Print the width and height
     print((
         '\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))
 
-    ##Print the bounds of the coordinates
+    # Print the bounds of the coordinates
     print((
         '\t(> c{0:02d}x 0) (> c{0:02d}y 0)\n'
-        '\t(<= (+ c{0:02d}x c{0:02d}w) 29) (<= (+ c{0:02d}y c{0:02d}h) 22)\n'
-        ).format(i, w, h))
+        '\t(<= (+ c{0:02d}x c{0:02d}w) {1}) (<= (+ c{0:02d}y c{0:02d}h) {2})\n'
+        ).format(i, mx, my))
 
-    ##Print the non overlap with others
+    # Print the non overlap with others
     for j in range(1, 1+len(pc+rc)):
         print((
             '\t(or (= {0} {1})\n'
@@ -45,18 +48,18 @@ for i, (w, h) in enumerate(pc+rc, 1):
             '(< (+ c{0:02d}y c{0:02d}h) c{1:02d}y)'
             ')').format(i, j))
 
-##Print the PC distance to eachother
+# 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)) 17)\n'
-            '\t\t(> (- (/ (+ c{1:02d}x c{1:02d}w) 2) (/ (+ c{0:02d}x c{0:02d}w) 2)) 17)\n'
-            '\t\t(> (- (/ (+ c{0:02d}y c{0:02d}h) 2) (/ (+ c{1:02d}y c{1:02d}h) 2)) 17)\n'
-            '\t\t(> (- (/ (+ c{1:02d}y c{1:02d}h) 2) (/ (+ c{0:02d}y c{0:02d}h) 2)) 17)'
-            ')').format(i, j))
+            '\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
+# 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):
@@ -68,5 +71,5 @@ for i, _ in enumerate(rc, 1+len(pc)):
             ).format(i, j))
     print('\t)')
 
-## Close the and,benchmark parenthesis
+# Close the and,benchmark parenthesis
 print("))")