#!/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=' ')
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'
'(< (+ 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):
).format(i, j))
print('\t)')
-## Close the and,benchmark parenthesis
+# Close the and,benchmark parenthesis
print("))")