summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorPeter Wu <peter@lekensteyn.nl>2016-12-12 00:19:19 +0100
committerPeter Wu <peter@lekensteyn.nl>2016-12-12 00:19:19 +0100
commit6ad28d2780dfca381ed8f78ef4bb63f50636c8a5 (patch)
tree38b5dc7ffd6cc28a045493240c9380242ad5fc82
parentb96e78d0bc84b07c6c727f9f1e4a8a14dcaf706e (diff)
download2IMF25-AR-6ad28d2780dfca381ed8f78ef4bb63f50636c8a5.tar.gz
ChipDesign fixes
-rwxr-xr-xchip_design/generate-chipdesign.py15
-rwxr-xr-xchip_design/solution-to-latex.py95
-rw-r--r--part1.tex19
3 files changed, 121 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()
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}