From 6ad28d2780dfca381ed8f78ef4bb63f50636c8a5 Mon Sep 17 00:00:00 2001
From: Peter Wu <peter@lekensteyn.nl>
Date: Mon, 12 Dec 2016 00:19:19 +0100
Subject: ChipDesign fixes

---
 chip_design/generate-chipdesign.py | 15 +++---
 chip_design/solution-to-latex.py   | 95 ++++++++++++++++++++++++++++++++++++++
 part1.tex                          | 19 ++++++++
 3 files changed, 121 insertions(+), 8 deletions(-)
 create mode 100755 chip_design/solution-to-latex.py

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()
diff --git a/part1.tex b/part1.tex
index 5b2fc45..7278e04 100644
--- a/part1.tex
+++ b/part1.tex
@@ -5,6 +5,7 @@
 \usepackage{epic}
 \usepackage{graphicx}
 \usepackage{gensymb}
+\usepackage{tikz}
 %\pagestyle{empty}
 \newcommand{\tr}{\mbox{\sf true}}
 \newcommand{\fa}{\mbox{\sf false}}
@@ -65,6 +66,24 @@ their centres should differ at least 17 in either the x direction or the y direc
 
 \subsection*{Solution:}
 
+\begin{tikzpicture}[scale=0.5]
+%\draw[step=1,gray,very thin] (0, 0) grid (30, 30);
+\draw[red,thick] (-.5, -.5) rectangle (30.5, 30.5);
+
+\draw[draw=red,fill=red] (20.1, 19.1) rectangle (22.9, 22.9);
+\draw[draw=green,fill=red] (27.1, 0.1) rectangle (29.9, 3.9);
+\draw[draw=blue] (12.1, 15.1) rectangle (15.9, 19.9);
+\draw[draw=cyan] (16.1, 15.1) rectangle (21.9, 18.9);
+\draw[draw=magenta] (0.1, 0.1) rectangle (4.9, 19.9);
+\draw[draw=gray] (6.1, 10.1) rectangle (11.9, 18.9);
+\draw[draw=darkgray] (5.1, 0.1) rectangle (10.9, 9.9);
+\draw[draw=lightgray] (21.1, 0.1) rectangle (26.9, 10.9);
+\draw[draw=brown] (22.1, 11.1) rectangle (29.9, 17.9);
+\draw[draw=olive] (23.1, 18.1) rectangle (29.9, 29.9);
+\draw[draw=orange] (11.1, 0.1) rectangle (20.9, 9.9);
+\draw[draw=pink] (0.1, 20.1) rectangle (19.9, 29.9);
+\end{tikzpicture}
+
 \section*{Problem: Job scheduling}
 Twelve jobs numbered from 1 to 12 have to be executed satisfying the following requirements:
 \begin{itemize}
-- 
cgit v1.2.1