From e69377a6dc7a9d13c6b87f00131a575f31ea53a1 Mon Sep 17 00:00:00 2001
From: Mart Lubbers <mart@martlubbers.net>
Date: Mon, 26 Oct 2015 20:09:00 +0100
Subject: [PATCH] final bijna

---
 1.tex       |  3 ++-
 2.tex       | 11 +++++++----
 3.tex       |  9 ++++++---
 4.tex       |  5 +++--
 Makefile    |  2 +-
 a.tex       | 18 +++++++++++++-----
 ar.tex      | 15 +++++++++------
 src/a1.bash |  4 ++--
 src/a2.bash |  2 +-
 src/a2.py   |  8 +++++---
 src/a3.bash |  3 ++-
 src/a3.py   |  4 +++-
 src/a4.bash |  3 ++-
 13 files changed, 56 insertions(+), 31 deletions(-)

diff --git a/1.tex b/1.tex
index 585e0cd..ff39c58 100644
--- a/1.tex
+++ b/1.tex
@@ -83,7 +83,8 @@ listed in Listing~\ref{listing:a1.bash}. The maximization is done by
 incrementing a special variable called \texttt{<REP>} which is an instantiation
 of $n(p)$.  When the iteration yields unsat we know that the current number
 minus one is the maximum amount of prittles the trucks can carry. The
-maximization is done with a bash script shown in Listing~\ref{listing:1.bash}.
+maximization is done with a bash script shown in Listing~\ref{listing:1.bash}
+and visualized with the python script shown in Listing~\ref{listing:a1.py}
 
 \lstinputlisting[language=bash,firstline=66,
 	caption={Iteratively find the largest solution for problem 1},
diff --git a/2.tex b/2.tex
index ace6512..a8fdc66 100644
--- a/2.tex
+++ b/2.tex
@@ -98,10 +98,11 @@ power components and only regular components.
 
 \subsection{SMT format solution}
 The formula is easily convertable via a Python script to SMT format by literal
-conversion and said script is listed in Listing~\ref{listing:a2.py}. The Python
-script optimizes a little bit from the original formula by leaving out the
-overlap checking between the same components. The solution is calculated using
-the command shown in Listing~\ref{listing:2.bash}
+conversion and said script is listed in Listing~\ref{listing:a2.bash}. The
+Python script optimizes a little bit from the original formula by leaving out
+the overlap checking between the same components. The solution is calculated
+using the command shown in Listing~\ref{listing:2.bash} and visualized with the
+python script shown in Listing~\ref{listing:a2.py}
 
 \lstinputlisting[language=bash,
 	caption={Find the shortest solution for problem 3},
@@ -111,6 +112,8 @@ the command shown in Listing~\ref{listing:2.bash}
 Finding this solution takes less then $35$ seconds and is shown in
 Table~\ref{tab:s2}.
 
+The bold items represent the power components.
+
 \begin{table}[H]
 	\centering
 	\input{a2.tex}
diff --git a/3.tex b/3.tex
index 8a4703a..9f24095 100644
--- a/3.tex
+++ b/3.tex
@@ -55,7 +55,8 @@ conversion and said script is listed in Listing~\ref{listing:a3.bash}. The
 script optimizes a little bit from the original formula by leaving out the
 shared resource checking for the same jobs. The minimization is done by
 incrementing variable $T$ every time the current $T$ yields unsat with a bash
-script shown in Listing~\ref{listing:3.bash}.
+script shown in Listing~\ref{listing:3.bash} and visualized with the python
+script shown in Listing~\ref{listing:a3.py}.
 
 \lstinputlisting[language=bash,firstline=46,
 	caption={Iteratively find the shortest solution for problem 3},
@@ -63,8 +64,10 @@ 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{tab:s3}. 
+finished in $37$ time units. Finding this solution takes less then $0.42$
+seconds and is shown in Table~\ref{tab:s3}. 
+
+The bold items represent the jobs using shared resources.
 
 \begin{table}[H]
 	\centering
diff --git a/4.tex b/4.tex
index 0414723..0ddc5de 100644
--- a/4.tex
+++ b/4.tex
@@ -52,7 +52,8 @@ the $i=j$ comparison in subformula 17 and 18 by removing them from the set
 looped over. The script also optimizes by not checking variables $a_0^n$ and
 $a_I^n$ since they always stay the same anyways. The minimization is done by
 incrementing variable $N$ every time the current $N$ yields unsat with a bash
-script shown in Listing~\ref{listing:4.bash}.
+script shown in Listing~\ref{listing:4.bash} and visualized with the python
+script shown in Listing~\ref{listing:a4.py}.
 
 \lstinputlisting[language=bash,firstline=58,
 	caption={Iteratively find the shortest solution for problem 4},
@@ -60,7 +61,7 @@ script shown in Listing~\ref{listing:4.bash}.
 
 \subsection{Solution}
 The bash script finds and shows the minimal solution in which the postcondition
-is satisfied for $N=10$. Finding this solution takes less then $75$ seconds and
+is satisfied for $N=10$. Finding this solution takes less then $20$ seconds and
 is shown in Table~\ref{tab:s4}.
 
 Every line in the table represents the iteration and the bold items represent
diff --git a/Makefile b/Makefile
index 4efd4f1..eeb35e7 100644
--- a/Makefile
+++ b/Makefile
@@ -20,7 +20,7 @@ all: $(DOCUMENT).pdf
 	$(LATEX) -ini -jobname="$(basename $@)" "&$(LATEX) $<\dump"
 
 a%.tex: src/a%.bash src src/a%.py
-	bash $< $@ >/dev/null
+	bash $< $@
 
 clean:
 	$(RM) -v $(addprefix $(DOCUMENT).,fmt aux log out toc pdf) $(SOLUTIONS)
diff --git a/a.tex b/a.tex
index ef0b82a..c5d9ce1 100644
--- a/a.tex
+++ b/a.tex
@@ -1,4 +1,4 @@
-\section{Appendix}
+\section{Appendix}\label{sec:appendix}
 \begin{lstlisting}[caption={Benchmark system}]
 OS: Linux 3.16.0-4-amd64 #1 SMP Debian 3.16 x86_64 GNU/Linux
 CPU: 3600MHz AMD FX(tm)-4100 Quad-Core Processor
@@ -6,17 +6,25 @@ RAM: 8GB
 \end{lstlisting}
 
 \newpage
-\lstinputlisting[language=lisp,caption={a1.bash},
+\lstinputlisting[language=bash,caption={a1.bash},
 	label={listing:a1.bash}]{src/a1.bash}
+\lstinputlisting[language=python,caption={a1.py},
+	label={listing:a1.py}]{src/a1.py}
 
 \newpage
+\lstinputlisting[language=bash,caption={a2.bash},
+	label={listing:a2.bash}]{src/a2.bash}
 \lstinputlisting[language=python,caption={a2.py},
 	label={listing:a2.py}]{src/a2.py}
 
 \newpage
-\lstinputlisting[language=python,caption={a3.bash},
-	label={listing:a3.py}]{src/a3.bash}
+\lstinputlisting[language=bash,caption={a3.bash},
+	label={listing:a3.bash}]{src/a3.bash}
+\lstinputlisting[language=python,caption={a3.py},
+	label={listing:a3.py}]{src/a3.py}
 
 \newpage
-\lstinputlisting[language=python,caption={a4.bash},
+\lstinputlisting[language=bash,caption={a4.bash},
 	label={listing:a4.bash}]{src/a4.bash}
+\lstinputlisting[language=python,caption={a4.py},
+	label={listing:a4.py}]{src/a4.py}
diff --git a/ar.tex b/ar.tex
index 9df4450..f650658 100644
--- a/ar.tex
+++ b/ar.tex
@@ -4,13 +4,16 @@
 \tableofcontents
 
 \setcounter{section}{-1}
-\section{Introduction}
+\section{General approach}
 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
-generation and/or the mini or maximization. The bash scripts all have a
-function defined called \lstinline{generate} with a parameter that will be used
-for mini or maximization. All solving is done on the benchmark system listed in
-Listing~\ref{listing:benchmark}.
+and therefore all problems have an accompanying bash script contains a function
+\lstinline{generate} that generates the SMT-Lib format. The script feeds the
+SMT-Lib format to yices after which the output is feeded to a Python script
+that visualizes the solution. This means that for all problems $p$ for $p\in
+\{1,\ldots, 4\}$ there exist $2$ files. \texttt{ap.bash} that generates the
+solution and \texttt{ap.py} that visualizes the solution. Both files are
+present in the Section~\ref{sec:appendix}. All solving is done on the benchmark
+system listed in Listing~\ref{listing:benchmark}.
 
 \begin{lstlisting}[caption={Benchmark system},label={listing:benchmark}]
 CPU: 3600MHz AMD FX(tm)-4100 Quad-Core Processor
diff --git a/src/a1.bash b/src/a1.bash
index 5e71a17..6304074 100644
--- a/src/a1.bash
+++ b/src/a1.bash
@@ -54,11 +54,11 @@ function generate {
 )
 GENERATE
 }
-
-i=1
+time { i=1
 while [ $(generate $i | yices-smt) = "sat" ]; do
 	echo "n(p)=$i is still sat"
 	i=$((i+1))
 done
 echo "n(p)=$i is unsat thus maximum n(p)=$((i-1))"
+}
 generate $((i-1)) | yices-smt -m | python3 src/a1.py > $1
diff --git a/src/a2.bash b/src/a2.bash
index 082e2f2..6796956 100644
--- a/src/a2.bash
+++ b/src/a2.bash
@@ -96,4 +96,4 @@ function generate {
 	done
 	echo "))"
 }
-generate | yices-smt -m | python3 src/a2.py > $1
+time generate | yices-smt -m | python3 src/a2.py > $1
diff --git a/src/a2.py b/src/a2.py
index eb1f164..6a609e7 100644
--- a/src/a2.py
+++ b/src/a2.py
@@ -7,8 +7,9 @@ comps = {}
 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'))
+        c = int(match.group('c'))
+        comps[c] = comps.get(c, {})
+        comps[c][match.group('t')] = int(match.group('v'))
 
 maxx = max(c['x']+c['w'] for c in comps.values())
 maxy = max(c['y']+c['h'] for c in comps.values())
@@ -24,7 +25,8 @@ for y in range(1, maxy+1):
               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='')
+            print('\\hspace{{.5mm}}{}\\hspace{{.5mm}}'.format(
+                '\mathbf{{{}}}'.format(cs[0]) if cs[0] <= 3 else cs[0]), end='')
         if x != maxx:
             print(' & ', end='')
     print('\\\\')
diff --git a/src/a3.bash b/src/a3.bash
index 8ce0b83..dba5f43 100644
--- a/src/a3.bash
+++ b/src/a3.bash
@@ -43,9 +43,10 @@ function generate {
 	echo "))"
 }
 
-i=1
+time { i=1
 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
index b5aac8c..6feaeb6 100644
--- a/src/a3.py
+++ b/src/a3.py
@@ -29,7 +29,9 @@ for d in range(depth):
     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='')
+            print('\\hspace{{.5mm}}{}\\hspace{{.5mm}}'.format(
+                '\\mathbf{{{}}}'.format(cj[0])
+                if cj[0] in [5, 7, 10] else cj[0]), end='')
         if t != tmax-1:
             print(' & ', end='')
     print('\\\\')
diff --git a/src/a4.bash b/src/a4.bash
index 61d4529..9b4f4d4 100644
--- a/src/a4.bash
+++ b/src/a4.bash
@@ -55,10 +55,11 @@ function generate {
 	echo ")))"
 }
 
-i=1
+time { i=1
 while [ $(generate $i | yices-smt) = "unsat" ]; do
 	echo "N=$i is still unsat"
 	i=$((i+1))
 done
 echo "N=$i is sat thus minimum N=$i"
+}
 generate $i | yices-smt -m | python src/a4.py > $1
-- 
2.20.1