From: Mart Lubbers <mart@martlubbers.net>
Date: Mon, 26 Oct 2015 18:41:41 +0000 (+0100)
Subject: update
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=839f09c18f4381e46413d6a517c34c5b286691f7;p=ar1516.git

update
---

diff --git a/2.tex b/2.tex
index 12ed33d..ace6512 100644
--- a/2.tex
+++ b/2.tex
@@ -109,14 +109,11 @@ the command shown in Listing~\ref{listing:2.bash}
 
 \subsection{Solution}
 Finding this solution takes less then $35$ seconds and is shown in
-Figure~\ref{fig:s2}.
+Table~\ref{tab:s2}.
 
-Light gray blocks represent regular components and the darker gray
-blocks represent power components.
-
-\begin{figure}[H]
+\begin{table}[H]
 	\centering
-	\includegraphics[scale=0.70]{s2.png}
-\label{fig:s2}
+	\input{a2.tex}
+\label{tab:s2}
 	\caption{Solution visualization for problem 2}
-\end{figure}
+\end{table}
diff --git a/3.tex b/3.tex
index 457c1e9..8a4703a 100644
--- a/3.tex
+++ b/3.tex
@@ -64,14 +64,11 @@ script shown in Listing~\ref{listing:3.bash}.
 \subsection{Solution}
 The bash script finds and shows the minimal solution in which all jobs are
 finished in $37$ time units. Finding this solution takes less then $0.85$
-seconds and is shown in Figure~\ref{fig:s3}. 
+seconds and is shown in Figure~\ref{tab:s3}. 
 
-Light gray blocks represent normal tasks and the darker gray blocks represent
-tasks from $J'$.
-
-\begin{figure}[H]
+\begin{table}[H]
 	\centering
-	\includegraphics[width=\linewidth]{s3.png}
-\label{fig:s3}
+	\input{a3.tex}
+\label{tab:s3}
 	\caption{Solution visualization for problem 3}
-\end{figure}
+\end{table}
diff --git a/4.tex b/4.tex
index 68b3242..0414723 100644
--- a/4.tex
+++ b/4.tex
@@ -67,23 +67,7 @@ Every line in the table represents the iteration and the bold items represent
 the step chosen in transition between iterations.
 \begin{table}[H]
 	\centering
-	$\begin{array}{cc|ccccc}
-		\toprule
-		n & i & a_2 & a_3 & a_4 & a_5 & a_6\\
-		\midrule
-		0 & - & 2 & 3 & 4 & 5 & 6\\
-		1 & 4 & 2 & 3 & \mathbf{8} & 5 & 6\\
-		2 & 5 & 2 & 3 & 8 & \mathbf{14} & 6\\
-		3 & 2 & \mathbf{4} & 3 & 8 & 14 & 6\\
-		4 & 4 & 4 & 3 & \mathbf{17} & 14 & 6\\
-		5 & 5 & 4 & 3 & 17 & \mathbf{23} & 6\\
-		6 & 6 & 4 & 3 & 17 & 23 & \mathbf{30}\\
-		7 & 5 & 4 & 3 & 17 & \mathbf{47} & 30\\
-		8 & 4 & 4 & 3 & \mathbf{50} & 47 & 30\\
-		9 & 3 & 4 & \mathbf{54} & 50 & 47 & 30\\
-		10 & 6 & 4 & 54 & 50 & 47 & \mathbf{54}\\
-		\bottomrule
-	\end{array}$
+\input{a4.tex}
 \caption{Solution table for problem 4}
 \label{tab:s4}
 \end{table}
diff --git a/Makefile b/Makefile
index 99b075d..4efd4f1 100644
--- a/Makefile
+++ b/Makefile
@@ -19,7 +19,7 @@ all: $(DOCUMENT).pdf
 %.fmt: pre.tex
 	$(LATEX) -ini -jobname="$(basename $@)" "&$(LATEX) $<\dump"
 
-a%.tex: src/a%.bash
+a%.tex: src/a%.bash src src/a%.py
 	bash $< $@ >/dev/null
 
 clean:
diff --git a/ar.tex b/ar.tex
index b79c70c..9df4450 100644
--- a/ar.tex
+++ b/ar.tex
@@ -3,6 +3,7 @@
 \maketitle
 \tableofcontents
 
+\setcounter{section}{-1}
 \section{Introduction}
 Implementing all the problems by hand in SMT-Lib format would be too much work
 and therefore all problems have an accompanying bash script that does the
diff --git a/src/a1.py b/src/a1.py
index bcfa087..66e0fe9 100644
--- a/src/a1.py
+++ b/src/a1.py
@@ -1,28 +1,28 @@
 #!/usr/bin/env python3
 import sys
+import re
 
 trucks = {}
 pallets = {'p': 'Prittles', 'n': 'Nuzzles', 'c': 'Crottles',
            's': 'Skipples', 'd': 'Dupples'}
 
 for line in sys.stdin:
-    if line.startswith('(='):
-        truck = line[4]
-        pallet = line[5]
-
-        number = int(line[7:-2])
-        trucks[truck] = trucks.get(truck, {})
-        trucks[truck][pallets[pallet]] = number
+    match = re.match('\(= t(?P<t>\d+)(?P<p>.) (?P<v>\d+)\)', line)
+    if match:
+        trucks[match.group('t')] = trucks.get(match.group('t'), {})
+        trucks[match.group('t')][pallets[match.group('p')]] = \
+            int(match.group('v'))
 
 print('$\\begin{array}{|l|lllll|}')
 print('\t\\toprule')
-print('\tTruck & {}\\\\'.format(' & '.join(sorted(pallets.values()))))
+print('\t\\text{{Truck}} & {}\\\\'.format(
+    ' & '.join('\\text{{{}}}'.format(p) for p in sorted(pallets.values()))))
 print('\t\\midrule')
 for truck in sorted(trucks):
     print('\t{} & {}\\\\'.format(truck, ' & '.join(
         str(p[1]) for p in sorted(trucks[truck].items()))))
 print('\t\\midrule')
-print('\tTotal & {}\\\\'.format(' & '.join(
+print('\t\\text{{Total}} & {}\\\\'.format(' & '.join(
     str(sum(t[p] for t in trucks.values())) for p in
     sorted(pallets.values()))))
 print('\t\\bottomrule')
diff --git a/src/a2.bash b/src/a2.bash
index 5462573..082e2f2 100644
--- a/src/a2.bash
+++ b/src/a2.bash
@@ -1 +1,99 @@
-python3 a2.py | yices-smt -m
+#!/bin/bash
+MAXX=29
+MAXY=22
+PD=17
+PC="1 2 3"
+RC="4 5 6 7 8 9 10 11"
+
+function wp {
+	case $1 in
+		1) echo 3;;
+		2) echo 3;;
+		3) echo 3;;
+		4) echo 8;;
+		5) echo 11;;
+		6) echo 9;;
+		7) echo 17;;
+		8) echo 19;;
+		9) echo 9;;
+		10) echo 7;;
+		11) echo 9;;
+		*);;
+	esac
+}
+
+function hp {
+	case $1 in
+		1) echo 1;;
+		2) echo 1;;
+		3) echo 1;;
+		4) echo 6;;
+		5) echo 5;;
+		6) echo 6;;
+		7) echo 4;;
+		8) echo 3;;
+		9) echo 5;;
+		10) echo 5;;
+		11) echo 7;;
+		*);;
+	esac
+}
+
+function generate {
+	local i j
+	echo "(benchmark a4.smt"
+	echo ":logic QF_UFLIA"
+	echo ":extrafuns ("
+	for i in $PC $RC; do
+		echo "(c${i}x Int) (c${i}y Int) (c${i}w Int) (c${i}h Int)"
+	done
+	echo ")"
+	echo ":formula"
+	echo "(and"
+	for i in $PC $RC; do
+		echo "(or"
+		echo "(and (= c${i}w $(wp $i)) (= c${i}h $(hp $i)))"
+		echo "(and (= c${i}w $(hp $i)) (= c${i}h $(wp $i)))"
+		echo ")"
+
+		echo "(> c${i}x 0) (> c${i}y 0)"
+		echo "(<= (+ c${i}x c${i}w) $MAXX) (<= (+ c${i}y c${i}h) $MAXY)"
+
+		for j in $PC $RC; do
+			if [ $i != $j ]; then
+				echo "(or"
+				echo "(> c${i}x (+ c${j}x c${j}w)) (< (+ c${i}x c${i}w) c${j}x)"
+				echo "(> c${i}y (+ c${j}y c${j}h)) (< (+ c${i}y c${i}h) c${j}y)"
+				echo ")"
+			fi
+		done
+	done
+
+	for i in $PC; do
+		for j in $PC; do
+			if [ $i != $j ]; then
+				echo "(or"
+				echo "(> (- (+ c${i}x (/ c${i}w 2)) (+ c${j}x (/ c${j}w 2))) $PD)"
+				echo "(> (- (+ c${j}x (/ c${j}w 2)) (+ c${i}x (/ c${i}w 2))) $PD)"
+				echo "(> (- (+ c${i}y (/ c${i}h 2)) (+ c${j}y (/ c${j}h 2))) $PD)"
+				echo "(> (- (+ c${j}y (/ c${j}h 2)) (+ c${i}y (/ c${i}h 2))) $PD)"
+				echo ")"
+			fi
+		done
+	done
+
+	for i in $RC; do
+		echo "(or"
+		for j in $PC; do
+			if [ $i != $j ]; then
+				echo "(not (or "
+				echo "(> c${i}x (+ c${j}x 1 c${j}w)) (< (+ c${i}x c${i}w) (- c${j}x 1))"
+				echo "(> c${i}y (+ c${j}y 1 c${j}h)) (< (+ c${i}y c${i}h) (- c${j}y 1))"
+				echo "))"	
+			fi
+		done
+		echo ")"
+	done
+	echo "))"
+}
+generate | yices-smt -m | python3 src/a2.py > $1
diff --git a/src/a2.py b/src/a2.py
index a782fe7..eb1f164 100644
--- a/src/a2.py
+++ b/src/a2.py
@@ -1,64 +1,33 @@
 #!/usr/bin/env python3
-pc = [(4, 2), (4, 2), (4, 2)]
-rc = [(9, 7), (12, 6), (10, 7), (18, 5), (20, 4), (10, 6), (8, 6), (10, 8)]
-mx = 29
-my = 22
-pd = 17
+import sys
+import re
 
-# Print variables and preamble
-print('(benchmark a4.smt')
-print(':logic QF_UFLIA')
-print(':extrafuns (')
-for i, (w, h) in enumerate(pc+rc, 1):
-    print('(c{}x Int)'.format(i), end=' ')
-    print('(c{}y Int)'.format(i), end=' ')
-    print('(c{}w Int)'.format(i), end=' ')
-    print('(c{}h Int)'.format(i))
-print(')')
+comps = {}
 
-print(':formula')
-print('(and')
+for line in sys.stdin:
+    match = re.match('\(= c(?P<c>\d+)(?P<t>.) (?P<v>\d+)\)', line)
+    if match:
+        comps[match.group('c')] = comps.get(match.group('c'), {})
+        comps[match.group('c')][match.group('t')] = int(match.group('v'))
 
-# Print the PC and RC subformulas
-for i, (w, h) in enumerate(pc+rc, 1):
-    # Print the width and height
-    print(('(or '
-           '(and (= c{0}w {1}) (= c{0}h {2})) '
-           '(and (= c{0}w {2}) (= c{0}h {1})))').format(i, w-1, h-1))
-    # Print the bounds of the coordinates
-    print(('(> c{0}x 0) (> c{0}y 0)'
-           '(<= (+ c{0}x c{0}w) {1}) (<= (+ c{0}y c{0}h) {2})'
-           ).format(i, mx, my))
+maxx = max(c['x']+c['w'] for c in comps.values())
+maxy = max(c['y']+c['h'] for c in comps.values())
+print('$\\begin{{array}}{{|l|{}|}}'.format('@{}c@{}'*maxx))
+print('\t\\toprule')
+print('\t & {}\\\\'.format(
+    ' & '.join(map(str, range(1, maxx+1)))))
+print('\t\\midrule')
+for y in range(1, maxy+1):
+    print('\t{} & '.format(y), end='')
+    for x in range(1, maxx+1):
+        cs = [c for c in comps if
+              comps[c]['y'] + comps[c]['h'] >= y and comps[c]['y'] <= y and
+              comps[c]['x'] + comps[c]['w'] >= x and comps[c]['x'] <= x]
+        if cs:
+            print('\\hspace{{.5mm}}{}\\hspace{{.5mm}}'.format(cs[0]), end='')
+        if x != maxx:
+            print(' & ', end='')
+    print('\\\\')
 
-    # Print the non overlap with others
-    for j in range(1, 1+len(pc+rc)):
-        if i != j:
-            print((
-                 '(or '
-                 '(> c{0}x (+ c{1}x c{1}w)) (< (+ c{0}x c{0}w) c{1}x) '
-                 '(> c{0}y (+ c{1}y c{1}h)) (< (+ c{0}y c{0}h) c{1}y)'
-                 ')').format(i, j))
-
-# Print the PC distance to eachother
-for i, _ in enumerate(pc, 1):
-    for j, _ in enumerate(pc, 1):
-        if i != j:
-            print(('(or '
-                   '(> (- (+ c{0}x (/ c{0}w 2)) (+ c{1}x (/ c{1}w 2))) {2}) '
-                   '(> (- (+ c{1}x (/ c{1}w 2)) (+ c{0}x (/ c{0}w 2))) {2}) '
-                   '(> (- (+ c{0}y (/ c{0}h 2)) (+ c{1}y (/ c{1}h 2))) {2}) '
-                   '(> (- (+ c{1}y (/ c{1}h 2)) (+ c{0}y (/ c{0}h 2))) {2})'
-                   ')').format(i, j, pd))
-
-            # Print the constraint that they have to be connected to a ps
-for i, _ in enumerate(rc, 1+len(pc)):
-    print('(or')
-    for j, _ in enumerate(pc, 1):
-        print(('(not (or '
-               '(> c{0}x (+ c{1}x 1 c{1}w)) (< (+ c{0}x c{0}w) (- c{1}x 1)) '
-               '(> c{0}y (+ c{1}y 1 c{1}h)) (< (+ c{0}y c{0}h) (- c{1}y 1))'
-               '))').format(i, j))
-    print(')')
-
-# Close the and,benchmark parenthesis
-print('))')
+print('\t\\bottomrule')
+print('\\end{array}$')
diff --git a/src/a3.bash b/src/a3.bash
index 5b16adc..8ce0b83 100644
--- a/src/a3.bash
+++ b/src/a3.bash
@@ -48,3 +48,4 @@ while [ $(generate $i | yices-smt) = "unsat" ]; do
 	echo "T=$((i++)) is still unsat"
 done
 echo "T=$i is sat thus the minimum T=$i"
+generate $i | yices-smt -m | python3 src/a3.py > $1
diff --git a/src/a3.py b/src/a3.py
new file mode 100644
index 0000000..b5aac8c
--- /dev/null
+++ b/src/a3.py
@@ -0,0 +1,37 @@
+#!/usr/bin/env python3
+import sys
+import re
+
+schedule = {}
+jobs = set()
+levels = {}
+for line in sys.stdin:
+    match = re.match('\(= j(?P<j>\d+) (?P<x>\d+)\)', line)
+    if match:
+        j = int(match.group('j'))
+        x = int(match.group('x'))
+        jobs.add(j)
+        for t in range(x, x+j):
+            schedule[t] = schedule.get(t, [])
+            schedule[t].append(j)
+
+tmax = max(schedule)+1
+levels = {j:max(schedule[t].index(j) if j in schedule[t] else 0
+          for t in range(1, tmax)) for j in jobs}
+schedule = {k:sorted(v) for k,v in schedule.items()}
+depth = max(map(len, schedule.values()))
+print('$\\begin{{array}}{{|{}}}'.format('@{}c@{}|'*tmax))
+print('\t\\toprule')
+print('\t{}\\\\'.format(' & '.join(map(str, range(1, tmax)))))
+print('\t\\midrule')
+for d in range(depth):
+    print('\t', end='')
+    for t in range(1, tmax):
+        cj = [j for j in jobs if levels[j] == d and j in schedule[t]]
+        if cj:
+            print('\\hspace{{.5mm}}{}\\hspace{{.5mm}}'.format(cj[0]), end='')
+        if t != tmax-1:
+            print(' & ', end='')
+    print('\\\\')
+print('\t\\bottomrule')
+print('\\end{array}$')
diff --git a/src/a4.bash b/src/a4.bash
index 7f9e0f9..61d4529 100644
--- a/src/a4.bash
+++ b/src/a4.bash
@@ -61,3 +61,4 @@ while [ $(generate $i | yices-smt) = "unsat" ]; do
 	i=$((i+1))
 done
 echo "N=$i is sat thus minimum N=$i"
+generate $i | yices-smt -m | python src/a4.py > $1
diff --git a/src/a4.py b/src/a4.py
new file mode 100644
index 0000000..541ca18
--- /dev/null
+++ b/src/a4.py
@@ -0,0 +1,23 @@
+#!/usr/bin/env python3
+import sys
+import re
+
+iterations = {}
+
+for line in sys.stdin:
+    match = re.match('\(= i(?P<i>\d+)a(?P<a>\d+) (?P<v>\d+)\)', line)
+    if match:
+        iterations[match.group('i')] = iterations.get(match.group('i'), {})
+        iterations[match.group('i')][match.group('a')] = match.group('v')
+
+print('$\\begin{array}{|l|lllllll|}')
+print('\t\\toprule')
+print('\t\\text{{n}} & a_1 & {} & a_7\\\\'.format(
+    ' & '.join('a_{}'.format(a) for a in sorted(iterations['0']))))
+print('\t\\midrule')
+for i in sorted(iterations, key=int):
+    print('\t{} & 1 & {} & 7\\\\'.format(i, ' & '.join(
+          iterations[i][a] for a in sorted(iterations[i], key=int)
+            )))
+print('\t\\bottomrule')
+print('\\end{array}$')