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
|
#!/usr/bin/env python
# Takes the solution from z3's output and converts it into a picture for LaTeX.
import operator
import re
import sys
# Map component index to (x, y, width, height)
boxes = {}
for line in sys.stdin:
line = line.strip()
if line == 'sat':
continue
m = re.match(r'([whxy])(\d+) -> (?:([0-9.]+)|\(/ ([0-9.]+) ([0-9.]+)\))', line)
what = m.group(1)
component_index = int(m.group(2))
num = m.group(3)
if num is not None:
num = float(num)
else:
num = float(m.group(4)) / float(m.group(5))
# Convert to something more readable if possible.
if num.is_integer():
num = int(num)
if component_index not in boxes:
boxes[component_index] = [None] * 4
boxes_index = 'xywh'.index(what)
assert boxes_index >= 0
boxes[component_index][boxes_index] = num
# Predefined colors from https://en.wikibooks.org/wiki/LaTeX/PGF/TikZ#Color
colors = [
'red',
'green',
'blue',
'cyan',
'magenta',
#'yellow',
#'black',
'gray',
'darkgray',
'lightgray',
'brown',
#'lime',
'olive',
'orange',
'pink',
'purple',
'teal',
'violet',
#'white',
]
def is_power_component(i):
return i < 2
def print_boxes():
# Print results, sorted by the operator index (for consistency).
for i, component in sorted(boxes.items(), key=operator.itemgetter(0)):
x, y, w, h = component
x2, y2 = x + w, y + h
attrs = []
# Add color
attrs += ["draw=%s" % colors[i]]
if is_power_component(i):
attrs += ["fill=%s" % "red"]
attrs = ','.join(attrs)
# HACK: print coords for debugging
if sys.argv[-1] == 'debug':
print(x, y, w, h)
continue
# For easier detection, reduce box dimension (add margin)
margin = 0.01
x += margin
y += margin
x2 -= margin
y2 -= margin
tpl = r"\draw[{attrs}] ({x}, {y}) rectangle ({x2}, {y2});"
print(tpl.strip().format(**vars()))
# Reset for printing text
x, y, w, h = component
x2, y2 = x + w, y + h
# Draw number for debugging
tx = x + w/2
ty = y + h/2
text = r"%s\\(%s,%s)\\(%s x %s)" % (i, x, y, w, h)
print(r'\node[align=center] at (%f,%f) {%s};' % (tx, ty, text))
# Just the boxes.
print_boxes()
|
