1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
|
#!/usr/bin/env python
# Run with: $0 | z3 -smt -in
# Power components
powers = [
(4, 3),
(4, 3),
]
# Regular components
regulars = [
(4, 5),
(4, 6),
(5, 20),
(6, 9),
(6, 10),
(6, 11),
(7, 8),
(7, 12),
(10, 10),
(10, 20),
]
# Chip dimensions
chip_w, chip_h = (30, 30)
# Minimum distance between centers
power_distance = 17
all_components = powers + regulars
def fillin(cases, template_vars):
if type(cases) == str:
return cases.format(**template_vars)
return [template.format(**template_vars) for template in cases]
literals = []
preds = []
# Add X and Y coordinate for each component,
# and also the width/height
for i, (w, h) in enumerate(all_components):
var_x = 'x%d' % i
var_y = 'y%d' % i
var_w = 'w%d' % i
var_h = 'h%d' % i
literals += [
var_x,
var_y,
var_w,
var_h,
]
# Ensure each component stays in chip area
newpreds = [
'(>= {var_x} 0)',
'(>= {var_y} 0)',
'(<= {var_x} {chip_w})',
'(<= {var_y} {chip_h})',
]
# Dimensions are restricted:
# either width and height are w, h; or they are rotated.
newpreds += [
'(or'
' (and (= {var_w} {w}) (= {var_h} {h}))'
' (and (= {var_w} {h}) (= {var_h} {w}))'
')',
]
# Fill in template with vars
preds += fillin(newpreds, vars())
# Avoid overlap between any pair, so any other component must be outside the
# current pivot.
for i in range(len(all_components)):
for j in range(len(all_components)):
if i == j:
continue
# other (j) must be below, on the left of pivot (i).
# or above or on the right (mind the width/height!).
altpreds = [
'(<= y{j} y{i})',
'(<= x{j} x{i})',
'(>= y{j} (+ y{i} h{i}))',
'(>= x{j} (+ x{i} x{i}))',
]
preds += ['(or %s)' % ' '.join(fillin(altpreds, vars()))]
# require minimum distance between power components
for i in range(len(powers)):
for j in range(len(powers)):
if i == j:
continue
# need center_i >= center_j + distance (for center from {X,Y}, repeat
# for i and j swapped in case j occurs after i)
# center = x + w / 2
center_x_i = fillin('(+ x{i} (/ w{i} 2))', vars())
center_y_i = fillin('(+ y{i} (/ h{i} 2))', vars())
center_x_j = fillin('(+ x{j} (/ w{j} 2))', vars())
center_y_j = fillin('(+ y{j} (/ h{j} 2))', vars())
altpreds = [
'(>= {center_x_i} (+ {center_x_j} {power_distance}))',
'(>= {center_x_j} (+ {center_x_i} {power_distance}))',
'(>= {center_y_i} (+ {center_y_j} {power_distance}))',
'(>= {center_y_j} (+ {center_y_i} {power_distance}))',
]
preds += ['(or %s)' % ' '.join(fillin(altpreds, vars()))]
# Begin generator
s = """(benchmark test.smt
:logic QF_UFLRA
:extrafuns
(
"""
s += "\n".join("(%s Real)" % x for x in literals)
s += """
)
:formula
(and
"""
s += "\n".join(preds)
s += """
))
"""
try:
import sys
print(s)
# Hack to avoid printing a ugly error in case stdin of next pipe is closed.
sys.stdout.flush()
sys.stdout.close()
except BrokenPipeError:
pass
|
