summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorPeter Wu <peter@lekensteyn.nl>2016-12-12 00:45:30 +0100
committerPeter Wu <peter@lekensteyn.nl>2016-12-12 00:45:30 +0100
commitbf32a02e180a030307f7bc27896976abeaeb2c1a (patch)
tree63a286df84d2db5beda2125af0333ed63f13fb59
parent6ad28d2780dfca381ed8f78ef4bb63f50636c8a5 (diff)
download2IMF25-AR-bf32a02e180a030307f7bc27896976abeaeb2c1a.tar.gz
ChipDesign: attempt at hitting the power resource
-rwxr-xr-xchip_design/generate-chipdesign.py15
-rwxr-xr-xchip_design/solution-to-latex.py2
-rw-r--r--part1.tex24
3 files changed, 28 insertions, 13 deletions
diff --git a/chip_design/generate-chipdesign.py b/chip_design/generate-chipdesign.py
index 862053e..d834078 100755
--- a/chip_design/generate-chipdesign.py
+++ b/chip_design/generate-chipdesign.py
@@ -104,6 +104,21 @@ for i in range(len(powers)):
]
preds += ['(or %s)' % ' '.join(fillin(altpreds, vars()))]
+# Require that each component is attached to power resource
+for i in range(len(powers), len(all_components)):
+ altpreds = []
+ for j in range(len(powers)):
+ # Power (j) top/right side hits component (i) bottom/left side or
+ # Power (j) bottom/left side hits component (i) top/right side.
+ # (note: copied from above overlap check with '>='/'<=' -> '='.)
+ altpreds += fillin([
+ '(= (+ y{j} h{j}) y{i})',
+ '(= (+ x{j} w{j}) x{i})',
+ '(= y{j} (+ y{i} h{i}))',
+ '(= x{j} (+ x{i} w{i}))',
+ ], vars())
+ preds += ['(or %s)' % ' \n'.join(altpreds)]
+
# Begin generator
s = """(benchmark test.smt
:logic QF_UFLIA
diff --git a/chip_design/solution-to-latex.py b/chip_design/solution-to-latex.py
index aec9948..2028b1b 100755
--- a/chip_design/solution-to-latex.py
+++ b/chip_design/solution-to-latex.py
@@ -71,7 +71,7 @@ def print_boxes():
attrs = ','.join(attrs)
# For easier detection, reduce box dimension (add margin)
- margin = 0.1
+ margin = 0.01
x += margin
y += margin
x2 -= margin
diff --git a/part1.tex b/part1.tex
index 7278e04..04ccb40 100644
--- a/part1.tex
+++ b/part1.tex
@@ -70,18 +70,18 @@ their centres should differ at least 17 in either the x direction or the y direc
%\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);
+\draw[draw=red,fill=red] (27.01, 20.01) rectangle (29.99, 23.99);
+\draw[draw=green,fill=red] (7.01, 11.01) rectangle (9.99, 14.99);
+\draw[draw=blue] (10.01, 11.01) rectangle (14.99, 14.99);
+\draw[draw=cyan] (21.01, 21.01) rectangle (26.99, 24.99);
+\draw[draw=magenta] (10.01, 25.01) rectangle (29.99, 29.99);
+\draw[draw=gray] (7.01, 15.01) rectangle (12.99, 23.99);
+\draw[draw=darkgray] (0.01, 24.01) rectangle (9.99, 29.99);
+\draw[draw=lightgray] (12.01, 0.01) rectangle (17.99, 10.99);
+\draw[draw=brown] (13.01, 15.01) rectangle (19.99, 22.99);
+\draw[draw=olive] (0.01, 11.01) rectangle (6.99, 22.99);
+\draw[draw=orange] (2.01, 1.01) rectangle (11.99, 10.99);
+\draw[draw=pink] (20.01, 0.01) rectangle (29.99, 19.99);
\end{tikzpicture}
\section*{Problem: Job scheduling}