ChipDesign fixes

2 files changed, 102 insertions, 8 deletions

diff --git a/chip_design/generate-chipdesign.py b/chip_design/generate-chipdesign.py
index d231c8d..862053e 100755
--- a/chip_design/generate-chipdesign.py
+++ b/chip_design/generate-chipdesign.py
@@ -27,7 +27,6 @@ chip_w, chip_h = (30, 30)
 # Minimum distance between centers
 power_distance = 17
 
-
 all_components = powers + regulars
 
 def fillin(cases, template_vars):
@@ -55,8 +54,8 @@ for i, (w, h) in enumerate(all_components):
     newpreds = [
         '(>= {var_x} 0)',
         '(>= {var_y} 0)',
-        '(<= {var_x} {chip_w})',
-        '(<= {var_y} {chip_h})',
+        '(<= (+ {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.
@@ -78,10 +77,10 @@ for i in range(len(all_components)):
         # 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} h{j}) y{i})',
+            '(<= (+ x{j} w{j}) x{i})',
             '(>= y{j} (+ y{i} h{i}))',
-            '(>= x{j} (+ x{i} x{i}))',
+            '(>= x{j} (+ x{i} w{i}))',
         ]
         preds += ['(or %s)' % ' '.join(fillin(altpreds, vars()))]
 
@@ -107,11 +106,11 @@ for i in range(len(powers)):
 
 # Begin generator
 s = """(benchmark test.smt
-:logic QF_UFLRA
+:logic QF_UFLIA
 :extrafuns
 (
 """
-s += "\n".join("(%s Real)" % x for x in literals)
+s += "\n".join("(%s Int)" % x for x in literals)
 s += """
 )
 :formula
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()