+#!/usr/bin/env python3
+
+pc = [(4, 22), (4, 22), (4, 22)]
+rc = [(9, 7), (12, 6), (10, 7), (18, 5), (20, 4), (10, 6), (8, 6), (10, 8)]
+
+##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{: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(")")
+
+##Preamble2
+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((
+ '\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((
+ '\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))
+
+ ##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))
+
+##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))
+
+#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))
+ print('\t)')
+
+## Close the and,benchmark parenthesis
+print("))")