3 pc
= [(4, 2), (4, 2), (4, 2)]
4 rc
= [(9, 7), (12, 6), (10, 7), (18, 5), (20, 4), (10, 6), (8, 6), (10, 8)]
10 print("(benchmark a4.smt")
11 print(":logic QF_UFLIA")
15 for i
, (w
, h
) in enumerate(pc
+rc
, 1):
16 print("(c{:02d}x Int)".format(i
), end
=' ')
17 print("(c{:02d}y Int)".format(i
), end
=' ')
18 print("(c{:02d}w Int)".format(i
), end
=' ')
19 print("(c{:02d}h Int)".format(i
))
26 # Print the PC and RC subformulas
27 for i
, (w
, h
) in enumerate(pc
+rc
, 1):
28 # Print the width and height
31 '(and (= c{0:02d}w {1}) (= c{0:02d}h {2})) '
32 '(and (= c{0:02d}w {2}) (= c{0:02d}h {1}))'
33 ')').format(i
, w
-1, h
-1))
35 # Print the bounds of the coordinates
37 '\t(> c{0:02d}x 0) (> c{0:02d}y 0)\n'
38 '\t(<= (+ c{0:02d}x c{0:02d}w) {1}) (<= (+ c{0:02d}y c{0:02d}h) {2})\n'
41 # Print the non overlap with others
42 for j
in range(1, 1+len(pc
+rc
)):
46 '\t\t(> c{0:02d}x (+ c{1:02d}x c{1:02d}w)) '
47 '(< (+ c{0:02d}x c{0:02d}w) c{1:02d}x)\n'
48 '\t\t(> c{0:02d}y (+ c{1:02d}y c{1:02d}h)) '
49 '(< (+ c{0:02d}y c{0:02d}h) c{1:02d}y)'
52 # Print the PC distance to eachother
53 #for i, _ in enumerate(pc, 1):
54 # for j, _ in enumerate(pc, 1):
58 # '\t\t(> (- (/ (+ c{0:02d}x c{0:02d}w) 2) '
59 # '(/ (+ c{1:02d}x c{1:02d}w) 2)) {2})\n'
60 # '\t\t(> (- (/ (+ c{1:02d}x c{1:02d}w) 2) '
61 # '(/ (+ c{0:02d}x c{0:02d}w) 2)) {2})\n'
62 # '\t\t(> (- (/ (+ c{0:02d}y c{0:02d}h) 2) '
63 # '(/ (+ c{1:02d}y c{1:02d}h) 2)) {2})\n'
64 # '\t\t(> (- (/ (+ c{1:02d}y c{1:02d}h) 2) '
65 # '(/ (+ c{0:02d}y c{0:02d}h) 2)) {2})'
66 # ')').format(i, j, pd))
68 # Print the constraint that they have to be connected to a ps
69 for i
, _
in enumerate(rc
, 1+len(pc
)):
71 for j
, _
in enumerate(pc
, 1):
74 '\t\t(> c{0:02d}x (+ c{1:02d}x 1 c{1:02d}w)) '
75 '(< (+ c{0:02d}x c{0:02d}w) (- c{1:02d}x 1))\n'
76 '\t\t(> c{0:02d}y (+ c{1:02d}y 1 c{1:02d}h)) '
77 '(< (+ c{0:02d}y c{0:02d}h) (- c{1:02d}y 1))'
81 # Close the and,benchmark parenthesis