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
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
|
#!/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} {var_w}) {chip_w})',
'(<= (+ {var_y} {var_h}) {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} h{j}) y{i})',
'(<= (+ x{j} w{j}) x{i})',
'(>= y{j} (+ y{i} h{i}))',
'(>= x{j} (+ x{i} w{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()))]
# Require that each component is attached to power resource
for i in range(len(powers), len(all_components)):
altpreds = []
for j in range(len(powers)):
# Power (j) top/right side hits component (i) bottom/left side or
# Power (j) bottom/left side hits component (i) top/right side.
# (note: copied from above overlap check with '>='/'<=' -> '='.)
# Additionally: to "hit" the power resource over the X axis, an
# component Y coordinate must be within the power resource.
# FIXME need to check whether there is an overlap
pr_range = ' (>= x{j} )'
altpreds += fillin([
'(and (= (+ y{j} h{j}) y{i})'' )',
'(and (= (+ x{j} w{j}) x{i})'' )',
'(and (= y{j} (+ y{i} h{i}))'' )',
'(and (= x{j} (+ x{i} w{i}))'' )',
], vars())
preds += ['(or %s)' % ' \n'.join(altpreds)]
# Begin generator
s = """(benchmark test.smt
:logic QF_UFLIA
:extrafuns
(
"""
s += "\n".join("(%s Int)" % 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
|
