1 files changed, 95 insertions, 0 deletions
diff --git a/chip_design/solution-to-latex.py b/chip_design/solution-to-latex.py
new file mode 100755
index 0000000..aec9948
--- /dev/null
+++ b/chip_design/solution-to-latex.py
@@ -0,0 +1,95 @@
+#!/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)
+
+        # For easier detection, reduce box dimension (add margin)
+        margin = 0.1
+        x += margin
+        y += margin
+        x2 -= margin
+        y2 -= margin
+
+        tpl = r"\draw[{attrs}] ({x}, {y}) rectangle ({x2}, {y2});"
+        print(tpl.strip().format(**vars()))
+
+def print_grid():
+    # XXX currently hard-coding grid size
+    print(r'\draw[step=1,gray,very thin] (0, 0) grid (30, 30);')
+
+if not True:
+    # Complete picture
+    print(r'\begin{tikzpicture}')
+    print_grid()
+    print_boxes()
+    print(r'\end{tikzpicture}')
+else:
+    # Just the boxes.
+    print_boxes()