f276fcbfa7957659a380116118bdfcc9f5de70d6
3 pc
= [(4, 22), (4, 22), (4, 22)]
4 rc
= [(9, 7), (12, 6), (10, 7), (18, 5), (20, 4), (10, 6), (8, 6), (10, 8)]
7 print("(benchmark a4.smt")
8 print(":logic QF_UFLIA")
12 for i
, (w
, h
) in enumerate(pc
+rc
, 1):
13 print("(c{:02d}x Int)".format(i
), end
=' ')
14 print("(c{:02d}y Int)".format(i
), end
=' ')
15 print("(c{:02d}w Int)".format(i
), end
=' ')
16 print("(c{:02d}h Int)".format(i
), end
=' ')
23 ##Print the PC and RC subformulas
24 for i
, (w
, h
) in enumerate(pc
+rc
, 1):
25 ##Print the width and height
28 '(and (= c{0:02d}w {1}) (= c{0:02d}h {2})) '
29 '(and (= c{0:02d}w {2}) (= c{0:02d}h {1}))'
32 ##Print the bounds of the coordinates
34 '\t(> c{0:02d}x 0) (> c{0:02d}y 0)\n'
35 '\t(<= (+ c{0:02d}x c{0:02d}w) 29) (<= (+ c{0:02d}y c{0:02d}h) 22)\n'
38 ##Print the non overlap with others
39 for j
in range(1, 1+len(pc
+rc
)):
42 '\t\t(> c{0:02d}x (+ c{1:02d}x c{1:02d}w)) '
43 '(< (+ c{0:02d}x c{0:02d}w) c{1:02d}x)\n'
44 '\t\t(> c{0:02d}y (+ c{1:02d}y c{1:02d}h)) '
45 '(< (+ c{0:02d}y c{0:02d}h) c{1:02d}y)'
48 ##Print the PC distance to eachother
49 for i
, _
in enumerate(pc
, 1):
50 for j
, _
in enumerate(pc
, 1):
53 '\t\t(> (- (/ (+ c{0:02d}x c{0:02d}w) 2) (/ (+ c{1:02d}x c{1:02d}w) 2)) 17)\n'
54 '\t\t(> (- (/ (+ c{1:02d}x c{1:02d}w) 2) (/ (+ c{0:02d}x c{0:02d}w) 2)) 17)\n'
55 '\t\t(> (- (/ (+ c{0:02d}y c{0:02d}h) 2) (/ (+ c{1:02d}y c{1:02d}h) 2)) 17)\n'
56 '\t\t(> (- (/ (+ c{1:02d}y c{1:02d}h) 2) (/ (+ c{0:02d}y c{0:02d}h) 2)) 17)'
59 #Print the constraint that they have to be connected to a ps
60 for i
, _
in enumerate(rc
, 1+len(pc
)):
62 for j
, _
in enumerate(pc
, 1):
64 '\t\t(= c{0:02d}x (+ c{1:02d}x c{1:02d}w 1))\n'
65 '\t\t(= (+ c{0:02d}x c{0:02d}w 1) c{1:02d}x)\n'
66 '\t\t(= c{0:02d}y (+ c{1:02d}y c{1:02d}h 1))\n'
67 '\t\t(= (+ c{0:02d}y c{0:02d}h 1) c{1:02d}y)'
71 ## Close the and,benchmark parenthesis