From: Mart Lubbers 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\d+)(?P

.) (?P\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\d+)(?P.) (?P\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\d+) (?P\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\d+)a(?P\d+) (?P\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}$')