From: Mart Lubbers <mart@martlubbers.net>
Date: Fri, 23 Oct 2015 07:43:54 +0000 (+0200)
Subject: cleaned up old directory
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=8e32acecac66ad7de8666ff492b62cc9b9c7dd38;p=master.git

cleaned up old directory
---

diff --git a/ar/assignments/.gitignore b/ar/assignments/.gitignore
deleted file mode 100644
index 9aa6a64..0000000
--- a/ar/assignments/.gitignore
+++ /dev/null
@@ -1 +0,0 @@
-output.log
diff --git a/ar/assignments/1.tex b/ar/assignments/1.tex
deleted file mode 100644
index 8506da9..0000000
--- a/ar/assignments/1.tex
+++ /dev/null
@@ -1,114 +0,0 @@
-\section{Problem 1}
-{\em
-Six trucks have to deliver pallets of obscure building blocks to a magic
-factory. Every truck has a capacity of 7800 kg and can carry at most
-eight pallets. In total, the following has to be delivered:
-\begin{itemize}
-	\item Four pallets of nuzzles, each of weight 700 kg.
-	\item A number of pallets of prittles, each of weight 800 kg.
-	\item Eight pallets of skipples, each of weight 1000 kg.
-	\item Ten pallets of crottles, each of weight 1500 kg.
-	\item Five pallets of dupples, each of weight 100 kg.
-\end{itemize}
-Prittles and crottles are an explosive combination: they are not allowed to be
-put in the same truck.
-
-Skipples need to be cooled; only two of the six trucks have facility for
-cooling skipples. Dupples are very valuable; to distribute the risk of loss no
-two pallets of dupples may be in the same truck.
-
-Investigate what is the maximum number of pallets of prittles that can be
-delivered, and show how for that number all pallets may be divided over the six
-trucks.
-}
-
-\newpage
-\subsection{Formal definition}
-For every truck $t_i$ for $i\in T$ where $T=\{1,\ldots,6\}$ in combination with
-every nuzzle $n$, prittle $p$, skipple $s$, crottle $c$ and dupple $d$ we
-declare a variable that holds the amount of that type of building block in that
-truck. We group all pallets $r\in P$ where $P=\{n,p,s,c,d\}$. We also
-define function $w(r)$ that defines the weight of the pallet and $n(r)$ that
-defines the number of pallets needed.
-
-This leads to the following formalization where we maximize $n(p)$.
-
-\begin{align}
-	\bigwedge^{T}_{i=1}\Biggl(
-	& \bigwedge_{r\in P}t_{i}r\geq0\\
-	& \wedge \sum_{r\in P}t_{i}r\leq8\\
-	& \wedge \left(\sum_{r\in P}t_{i}r\cdot w(r)\right)\leq7800)\\
-	& \wedge (t_{i}p=0\vee t_{i}c=0)\\
-	& \wedge t_{i}d\leq1\\
-	& \wedge (t_{i}=t_{1} \vee t_{i}=t_{2} \vee t_{i}s=0)\Biggr)\wedge\\
-	\bigwedge_{r\in P}\Biggl(
-	& \left(\sum^{T}_{i=1}t_{i}r\right)=n(r)\Biggr)
-\end{align}
-
-Every numbered subformula describes a constraint from the problem description.
-We can separated the subformulas in formulas going over all trucks and formulas
-going over all pallets.
-
-\begin{itemize}
-	\item \textbf{Trucks}
-	\begin{enumerate}
-		\item Makes sure you can not have a negative number of pallets
-			in a truck by stating that the number of pallets in a
-			truck is not smaller then $0$.
-		\item Makes sure you can not have more then $8$ pallets in a
-			truck by stating that the sum of all pallets in a truck
-			is not bigger then $8$.
-		\item Makes sure the weight will never go over the maximum
-			weight per truck by stating that all the pallets times
-			their weight in a truck will not go over $7800$kg.
-		\item Makes sure prittles and crottles are never together in a
-			truck by stating that either the number of prittles is
-			zero or the number of crottles is zero in a truck.
-		\item Makes sure that skipples are only in the first two cooled
-			trucks by stating that if the truck number not one or
-			two the number of skipples is zero.
-	\end{enumerate}
-	\item \textbf{Pallets}
-	\begin{enumerate}
-		\setcounter{enumi}{6}
-		\item Makes sure that all mandatory pallets are transported by
-			summing over all trucks and assuring the number of the
-			pallets of that type is exactly $n(r)$.
-	\end{enumerate}
-\end{itemize}
-
-\subsection{SMT format solution}
-The formula is easily convertable to SMT format and is listed in
-Listing~\ref{listing:a1.smt}. 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}.
-
-\lstinputlisting[language=bash,
-	caption={Iteratively find the largest solution for problem 1},
-	label={listing:1.bash}]{src/a1.bash}
-
-\subsection{Solution}
-The bash script finds and shows the maximal solution of $18$ prittles. Finding
-this solution takes less then $0.12$ seconds and is shown in Table~\ref{tab:s1}.
-
-\begin{table}[H]
-	\begin{tabular}{|l|lllll|l|l|}
-		\hline
-		Truck & Nuzzles & Prittles & Skipples & Crottles & Dupples &
-			Weight & Pallets\\
-		\hline
-		1 & 0 & 0 & 4 & 2 & 1 & 7100 & 7\\
-		2 & 0 & 3 & 4 & 0 & 1 & 6500 & 8\\
-		3 & 0 & 8 & 0 & 0 & 0 & 6400 & 7\\
-		4 & 0 & 7 & 0 & 0 & 1 & 5700 & 8\\
-		5 & 0 & 0 & 0 & 5 & 1 & 7600 & 6\\
-		6 & 4 & 0 & 0 & 3 & 1 & 7400 & 8\\
-		\hline
-		total & 4 & 18 & 8 & 10 & 5 & &\\
-		\hline
-	\end{tabular}
-	\caption{Solution visualization for problem 1}
-\label{tab:s1}
-\end{table}
diff --git a/ar/assignments/2.tex b/ar/assignments/2.tex
deleted file mode 100644
index 7fd4047..0000000
--- a/ar/assignments/2.tex
+++ /dev/null
@@ -1,121 +0,0 @@
-\section{Problem 2}
-{\em
- Give a chip design containing three power components and eight regular
-components satisfying the following constraints:
-
-\begin{itemize}
-	\item The width of the chip is 29 and the height is 22.
-	\item All power components have width 4 and height 2.
-	\item The sizes of the eight regular components are $9\times7$,
-		$12\times6,$ $10\times7,$ $18\times5,$ $20\times4,$
-		$10\times6,$ $8\times6$ and $10\times8$ respectively.
-	\item All components may be turned 90, but may not overlap.
-	\item In order to get power, all regular components should directly be
-		connected to a power component, that is, an edge of the
-		component should have at least one point in common with an edge
-		of the power component.
-	\item Due to limits on heat production the power components should be
-		not too close: their centres should differ at least $17$ in
-		either the $x$ direction or the $y$ direction (or both).
-\end{itemize}
-}
-
-\newpage
-\subsection{Formal definition}
-For every component $c_{i}$ for $i\in PC\cup RC$ where $PC=\{1,\ldots,3\}$ and
-$RC=\{4,\ldots,11\}$ we define a width, a height, an $x$ and a $y$ variables
-$c_{i}w$, $c_{i}h$, $c_{i}x$ and $c_{i}y$. $c_ih$ does not necessarily have the
-specified height of the components since the components may be rotated. For the
-specified width and height we introduce the functions $h(c)$ and $w(c)$ that
-return the specified width and height.
-
-This leads to the following formalization.
-
-\begin{align}
-	\bigwedge_{i\in PC\cup RC}\Biggl(
-	  & (c_{i}h=h(i)\vee c_{i}h=w(i))\wedge(c_{i}w=w(i)\vee c_{i}w=h(i))\\
-		& \wedge 29-c_{i}w\geq c_{i}x>0\wedge 22-c_{i}h\geq c_{i}y>0\\
-		& \wedge \bigwedge_{j\in PC\cup RC}\Bigl(j\geq i\\
-		\nonumber & \qquad\qquad\qquad \vee c_{i}x>c_{j}x+c_{j}w\\
-		\nonumber & \qquad\qquad\qquad \vee c_{i}x+c_{j}w<c_{j}x\\
-		\nonumber & \qquad\qquad\qquad \vee c_{i}y>c_{j}y+c_{j}h\\
-		\nonumber & \qquad\qquad\qquad 
-			\vee c_{i}y+c_{j}h<c_{j}h\Bigr)\Biggr)\wedge\\
-	\bigwedge_{i\in PC}\bigwedge_{j\in PC}\Biggl( & i=j\\
-		\nonumber & \vee c_{i}x+\nicefrac{c_{i}w}{2}-
-			c_{j}x+\nicefrac{c_{j}w}{2}>17\\
-		\nonumber & \vee c_{j}x+\nicefrac{c_{j}w}{2}-
-			c_{i}x+\nicefrac{c_{i}w}{2}>17\\
-		\nonumber & \vee c_{i}y+\nicefrac{c_{i}h}{2}-
-			c_{j}y+\nicefrac{c_{j}h}{2}>17\\
-		\nonumber & \vee c_{j}y+\nicefrac{c_{j}h}{2}-
-			c_{i}y+\nicefrac{c_{i}h}{2}>17\Biggr)\wedge\\
-	\bigwedge_{i\in RC}\bigvee_{j\in PC}\neg\Biggl(
-		& (c_{i}x-1>c_{j}x+c_{j}w\\
-		\nonumber & \vee c_{i}x+1+c_{j}w<c_{j}x\\
-		\nonumber & \vee c_{i}y-1>c_{j}y+c_{j}h\\
-		\nonumber & \vee c_{i}y+1+c_{j}h<c_{j}h\Biggr)
-\end{align}
-
-Every numbered subformula describes a constraint from the problem description.
-We can separated the subformulas in formulas going over all components, only
-power components and only regular components.
-\begin{itemize}
-	\item\textbf{All}
-		\begin{enumerate}
-			\setcounter{enumi}{7}
-			\item Makes sure the width and the height of the
-				component can be swapped thus allowing a
-				rotation.
-			\item Makes sure the components are placed on the
-				chip by stating that the $x$ and $y$
-				coordinates are bigger then $0$ and the $x$ and
-				$y$ plus their width or height does not exceed
-				the specified width and height of the chip.
-			\item Makes sure the components do not overlap by
-				defining for all pairs of components that they
-				either are strictly right, strictly left,
-				strictly above or strictly below the other.
-		\end{enumerate}
-	\item\textbf{Power only}
-		\begin{enumerate}
-			\setcounter{enumi}{10}
-			\item Makes sure power components are at least $17$
-				block away from other power components by
-				stating that the difference between the center
-				of each pair of components is bigger then $17$.
-		\end{enumerate}
-	\item\textbf{Regular only}
-		\begin{enumerate}
-			\setcounter{enumi}{11}
-			\item Makes sure regular components are connected to a
-				power component by stating, using the same
-				method as in the overlay, that it has overlap
-				with a power component that has had its size
-				increased by $1$.
-		\end{enumerate}
-\end{itemize}
-
-\subsection{SMT format solution}
-The formula is easily convertable via a Python script to SMT format 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}
-
-\lstinputlisting[language=bash,
-	caption={Find the shortest solution for problem 3},
-	label={listing:2.bash}]{src/a2.bash}
-
-\subsection{Solution}
-Finding this solution takes less then $35$ seconds and is shown in
-Figure~\ref{fig:s2}.
-
-Light gray blocks represent regular components and the darker gray
-blocks represent power components.
-
-\begin{figure}[H]
-	\includegraphics[scale=0.70]{s2.png}
-\label{fig:s2}
-	\caption{Solution visualization for problem 2}
-\end{figure}
diff --git a/ar/assignments/3.tex b/ar/assignments/3.tex
deleted file mode 100644
index 471f3e1..0000000
--- a/ar/assignments/3.tex
+++ /dev/null
@@ -1,76 +0,0 @@
-\section{Problem 2}
-{\em
-Twelve jobs numbered from 1 to 12 have to be executed satisfying the following
-requirements:
-\begin{itemize}
-	\item The running time of job $i$ is $i$, for $i=1,\ldots,12$
-	\item All jobs run without interrupt.
-	\item Job 3 may only start if jobs 1 and 2 have been finished.
-	\item Job 5 may only start if jobs 3 and 4 have been finished.
-	\item Job 7 may only start if jobs 3, 4 and 6 have been finished.
-	\item Job 9 may only start if jobs 5 and 8 have been finished
-	\item Job 11 may only start if job 10 has been finished.
-	\item Job 12 may only start if jobs 9 and 11 have been finished.
-	\item Jobs 5,7 en 10 require a special equipment of which only one copy
-		is available, so no two of these jobs may run at the same time.
-\end{itemize}
-
-Find a solution of this scheduling problem for which the total running time is
-minimal.
-}
-
-\newpage
-\subsection{Formal definition}
-For every job $j_{i}$ for $i\in J$ where $J=\{1,\ldots,12\}$ we define variable
-$j_{i}s$ for starting time. All jobs that have a shared resource we group as
-$J'=\{5,7,10\}$ and we define a function $p(i)$ that returns a set of all
-dependencies of job $i$. The total time it takes for all jobs to finish is $T$.
-
-This leads to the following formalization where we minimize $T$.
-\begin{align}
-	\bigwedge_{i\in J}\Biggl( 
-		& j_{i}>0\wedge j_{i}+i<T\\
-		& \wedge \bigwedge_{k\in p(i)} j_{i}>j_{k}+k\Biggr)\\
-		& \wedge \bigwedge_{i\in J'}\bigwedge_{k\in J'}
-		i=j\vee j_{i}>j_{k}+k \vee j_{i}+i<j_{k}
-\end{align}
-
-Every numbered subformula describes a group of constraints from the problem
-definition.
-\begin{itemize}
-	\setcounter{enumi}{12}
-	\item Makes sure that starting times are positive and that all jobs
-		finish before $T$.
-	\item Makes sure that job may not start before all their dependencies
-		are finished by stating that they start strictly after their
-		dependency.
-	\item Makes sure that never two more jobs use the shared resource by
-		stating that they either ends strictly before the other or
-		start strictly after the other.
-\end{itemize}
-
-\subsection{SMT format solution}
-The formula is easily convertable via a Python script to SMT format and said
-script is listed in Listing~\ref{listing:a3.py}. The Python 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}.
-
-\lstinputlisting[language=bash,
-	caption={Iteratively find the shortest solution for problem 3},
-	label={listing:3.bash}]{src/a3.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}. 
-
-Light gray blocks represent normal tasks and the darker gray blocks represent
-tasks from $J'$.
-
-\begin{figure}[H]
-	\includegraphics[width=\linewidth]{s3.png}
-\label{fig:s3}
-	\caption{Solution visualization for problem 3}
-\end{figure}
diff --git a/ar/assignments/4.tex b/ar/assignments/4.tex
deleted file mode 100644
index 6a827cb..0000000
--- a/ar/assignments/4.tex
+++ /dev/null
@@ -1,112 +0,0 @@
-\section{Problem 4}
-{\em
-Seven integer variables $a_1; a_2; a_3; a_4; a_5; a_6; a_7$ are given, for
-which the initial value of $a_i$ is $i$ for $i=1,\ldots,7$. The following steps are defined: choose $i$ with $1<i<7$ and execute
-$$a_i:=a_{i-1}+a_{i+1}$$
-that is, $a_i$ gets the sum of the values of its neighbors and all other
-values remain unchanged. Show how it is possible that after a number of steps
-a number of steps a number $\ge 50$ occurs at least twice in $a_1; a_2; a_3;
-a_4; a_5; a_6; a_7$.
-}
-
-\newpage
-\subsection{Formal definition}
-\paragraph{Precondition}
-Say we have $I$ $a$'s denoted as $a_i$ and we have $N$ iterations. $i_na_i$
-means variable $a_i$ in iteration $n$. Iteration $0$ is seen as the starting
-point and can be expressed as in Equation~\ref{eq:4pre}
-
-\begin{equation}\label{eq:4pre}
-	(a_1=1)\wedge
-	(a_I=I)\wedge
-	\bigwedge_{k=2}^{I-1} (i_0a_i=i)\\
-\end{equation}
-
-\paragraph{Program}
-Every iteration we can choose to do $a_i=a_{i-1}+a_{i+1}$ or nothing. To keep
-track of what we do we keep a counter $c_n$ for every $n$ that holds either the
-$i$ if an $a_i$ is chosen or $0$ if no action has been taken. Therefore for all
-iterations we can express this as in Equation~\ref{eq:4pro}
-
-{\medmuskip=0mu \thinmuskip=0mu \thickmuskip=0mu
-\begin{equation}
-\label{eq:4pro}
-	\bigwedge_{n=1}^{N}\left(
-		\bigvee_{k=2}^{I-1}\left(
-			(c_i = k)
-			\wedge
-			(i_na_j = i_{n-1}a_{j-1} + i_{n-1}a_{j+1})
-			\wedge
-			\bigwedge_{j=2}^{I-1}\left(
-				(j\neq k)\wedge (i_na_j = i_{n-1}a_j)
-			\right)
-		\right)
-		\vee
-		\bigwedge_{k=2}^{I-1}(i_na_k = i_{n-1}a_k) \wedge (c_i=0)
-	\right)
-\end{equation}
-}
-
-\paragraph{Postcondition}
-Finally the post condition can be described as $a_i>50$ and some other
-$a_i= a_j\wedge i\neq j$ for all $i$. This is expressed in
-Equation~\ref{eq:4pst}
-
-\begin{equation}\label{eq:4pst}
-	\bigvee_{k=2}^{I-1}\left(
-		(i_Na_k >= 50)\wedge
-		\left(\bigvee_{j=2}^{I-1}(i_Na_k=i_Na_j)\wedge(k\neq j)\right)
-	\right)
-\end{equation}
-
-\paragraph{Total}
-To tie this all together we just put $\wedge$ in between and that results in:
-$$\text{precondition }\wedge\text{ program }\wedge\text{ postcondition}$$
-
-\subsection{SMT format solution}
-Naming the precondition, program and postcondition respectively $p_1, p_2, p_3$
-we can easily convert it to a SMT format. The converting is tedious and takes a
-lot of time and therefore an automatization script has been created that is
-visible in the appendices in Listing~\ref{listing:4.py}. The script
-automatically assumes $11$ iterations and $7$ $a_i$ variables but via command
-line arguments this is easily extendable. To determine the minimal number of
-iterations a simple bash script can be made that iteratively increases the
-iterations as shown in Listing~\ref{listing:4bash}. The shortest solution with
-length $11$ is found in around $30$ seconds. Finding the smallest solution
-length incrementally takes around $75$ seconds.
-
-\begin{lstlisting}[language=bash,
-	caption={Iteratively find the shortest solution},label={listing:4bash}]
-i=1
-while [ "$(python a4.py $i | yices-smt)" = "unsat" ]
-do
-	echo $((++i));
-done
-\end{lstlisting}
-
-\subsection{Solution}
-The iterative solution terminates with $i=11$ so the minimum number of steps
-required is $11$. When we rerun the solution with $11$ steps and the
-\texttt{-m} flag we can see the solution as in Table~\ref{tab:s4}.
-The bold cells represent the $a_i$ after applying the function. After ten
-iterations cell $a_2$ and $a_6$ both hold $54$ thus satisfying the problem
-specification.
-\begin{table}[H]
-	\begin{tabular}{c|c|ccccc}
-		\# & $i$ & $a_2$ & $a_3$ & $a_4$ & $a_5$ & $a_6$\\
-		\hline
-		$0$ & - & $2$ & $3$ & $4$ & $5$ & $6$\\
-		$1$ & $4$ & $2$ & $3$ & $\bm{8}$ & $5$ & $6$\\
-		$2$ & $5$ & $2$ & $3$ & $8$ & $\bm{14}$ & $6$\\
-		$3$ & $2$ & $\bm{4}$ & $3$ & $8$ & $14$ & $6$\\
-		$4$ & $4$ & $4$ & $3$ & $\bm{17}$ & $14$ & $6$\\
-		$5$ & $5$ & $4$ & $3$ & $17$ & $\bm{23}$ & $6$\\
-		$6$ & $6$ & $4$ & $3$ & $17$ & $23$ & $\bm{30}$\\
-		$7$ & $5$ & $4$ & $3$ & $17$ & $\bm{47}$ & $30$\\
-		$8$ & $4$ & $4$ & $3$ & $\bm{50}$ & $47$ & $30$\\
-		$9$ & $3$ & $4$ & $\bm{54}$ & $50$ & $47$ & $30$\\
-		$10$ & $6$ & $4$ & $54$ & $50$ & $47$ & $\bm{54}$
-	\end{tabular}
-\caption{Solution table for problem 4}
-\label{tab:s4}
-\end{table}
diff --git a/ar/assignments/Makefile b/ar/assignments/Makefile
deleted file mode 100644
index 4cfb119..0000000
--- a/ar/assignments/Makefile
+++ /dev/null
@@ -1,18 +0,0 @@
-LATEX:=pdflatex
-
-DOCUMENT:=ar
-SOURCES:=$(filter-out preamble.tex,$(shell ls *.tex))
-
-.SECONDARY: $(addsuffix .fmt,$(DOCUMENT))
-
-all: $(DOCUMENT).pdf
-
-%.pdf: %.tex %.fmt $(SOURCES)
-	$(LATEX) $(basename $@)
-	$(LATEX) $(basename $@)
-
-%.fmt: preamble.tex
-	$(LATEX) -ini -jobname="$(basename $@)" "&$(LATEX) $<\dump"
-
-clean:
-	$(RM) -v $(addprefix $(DOCUMENT).,fmt aux bbl blg dvi log out toc pdf)
diff --git a/ar/assignments/a.tex b/ar/assignments/a.tex
deleted file mode 100644
index e0ac8a3..0000000
--- a/ar/assignments/a.tex
+++ /dev/null
@@ -1,22 +0,0 @@
-\section{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
-RAM: 8GB
-\end{lstlisting}
-
-\newpage
-\lstinputlisting[language=lisp,caption={a1.smt},
-	label={listing:a1.smt}]{src/a1.smt}
-
-\newpage
-\lstinputlisting[language=python,caption={a2.py},
-	label={listing:a2.py}]{src/a2.py}
-
-\newpage
-\lstinputlisting[language=python,caption={a3.py},
-	label={listing:a3.py}]{src/a3.py}
-
-\newpage
-\lstinputlisting[language=python,caption={a4.py},
-	label={listing:a4.py}]{src/a4.py}
diff --git a/ar/assignments/ar.tex b/ar/assignments/ar.tex
deleted file mode 100644
index 94e25f9..0000000
--- a/ar/assignments/ar.tex
+++ /dev/null
@@ -1,21 +0,0 @@
-%&ar
-\begin{document}
-\maketitle
-\tableofcontents
-
-\newpage
-\input{1.tex}
-
-\newpage
-\input{2.tex}
-
-\newpage
-\input{3.tex}
-
-\newpage
-\input{4.tex}
-
-\newpage
-\input{a.tex}
-
-\end{document}
diff --git a/ar/assignments/preamble.tex b/ar/assignments/preamble.tex
deleted file mode 100644
index a401ca6..0000000
--- a/ar/assignments/preamble.tex
+++ /dev/null
@@ -1,30 +0,0 @@
-\documentclass{article}
-
-\usepackage{hyperref}
-\usepackage{a4wide}
-\usepackage{bm}
-\usepackage{float}
-\usepackage{graphicx}
-\usepackage{amsmath}
-\usepackage{listings}
-\usepackage{nicefrac}
-
-\everymath{\displaystyle\allowdisplaybreaks}
-
-\lstset{%
-  basicstyle=\scriptsize,
-  breakatwhitespace=true,
-  breaklines=true,
-  keepspaces=true,
-  numbers=left,
-  numberstyle=\tiny,
-  frame=L,
-  showspaces=false,
-  showstringspaces=false,
-  showtabs=false,
-  tabsize=2
-}
-
-\author{Mart Lubbers (s4109503)}
-\title{Automated reasoning Assignment 1} 
-\date{\today}
diff --git a/ar/assignments/prnijm.pdf b/ar/assignments/prnijm.pdf
deleted file mode 100644
index a65fb82..0000000
Binary files a/ar/assignments/prnijm.pdf and /dev/null differ
diff --git a/ar/assignments/s2.png b/ar/assignments/s2.png
deleted file mode 100644
index 2876b39..0000000
Binary files a/ar/assignments/s2.png and /dev/null differ
diff --git a/ar/assignments/s3.png b/ar/assignments/s3.png
deleted file mode 100644
index 46e9e75..0000000
Binary files a/ar/assignments/s3.png and /dev/null differ
diff --git a/ar/assignments/src/a1.bash b/ar/assignments/src/a1.bash
deleted file mode 100644
index 847616c..0000000
--- a/ar/assignments/src/a1.bash
+++ /dev/null
@@ -1,5 +0,0 @@
-i=1
-while [ $(sed "s/<REP>/$i/g" a1.smt | yices-smt) = "sat" ]; do
-	i=$((i+1))
-done
-sed "s/<REP>/$((i-1))/g" a1.smt | yices-smt -m
diff --git a/ar/assignments/src/a1.smt b/ar/assignments/src/a1.smt
deleted file mode 100644
index cf5342e..0000000
--- a/ar/assignments/src/a1.smt
+++ /dev/null
@@ -1,60 +0,0 @@
-(benchmark a1.smt
-:logic QF_UFLIA
-:extrafuns (
-	(t1p Int) (t1n Int) (t1s Int) (t1c Int) (t1d Int)
-	(t2p Int) (t2n Int) (t2s Int) (t2c Int) (t2d Int)
-	(t3p Int) (t3n Int) (t3s Int) (t3c Int) (t3d Int)
-	(t4p Int) (t4n Int) (t4s Int) (t4c Int) (t4d Int)
-	(t5p Int) (t5n Int) (t5s Int) (t5c Int) (t5d Int)
-	(t6p Int) (t6n Int) (t6s Int) (t6c Int) (t6d Int)
-)
-:formula
-(and
-	(>= t1p 0) (>= t1n 0) (>= t1s 0) (>= t1c 0) (>= t1d 0)
-	(>= t2p 0) (>= t2n 0) (>= t2s 0) (>= t2c 0) (>= t2d 0)
-	(>= t3p 0) (>= t3n 0) (>= t3s 0) (>= t3c 0) (>= t3d 0)
-	(>= t4p 0) (>= t4n 0) (>= t4s 0) (>= t4c 0) (>= t4d 0)
-	(>= t5p 0) (>= t5n 0) (>= t5s 0) (>= t5c 0) (>= t5d 0)
-	(>= t6p 0) (>= t6n 0) (>= t6s 0) (>= t6c 0) (>= t6d 0)
-
-	(<= (+ t1p t1n t1s t1c t1d) 8)
-	(<= (+ t2p t2n t2s t2c t2d) 8)
-	(<= (+ t3p t3n t3s t3c t3d) 8)
-	(<= (+ t4p t4n t4s t4c t4d) 8)
-	(<= (+ t5p t5n t5s t5c t5d) 8)
-	(<= (+ t6p t6n t6s t6c t6d) 8)
-
-	(<= (+ (* t1n 700) (* t1p 800) (* t1s 1000) (* t1c 1500) (* t1d 100)) 7800)
-	(<= (+ (* t2n 700) (* t2p 800) (* t2s 1000) (* t2c 1500) (* t2d 100)) 7800)
-	(<= (+ (* t3n 700) (* t3p 800) (* t3s 1000) (* t3c 1500) (* t3d 100)) 7800)
-	(<= (+ (* t4n 700) (* t4p 800) (* t4s 1000) (* t4c 1500) (* t4d 100)) 7800)
-	(<= (+ (* t5n 700) (* t5p 800) (* t5s 1000) (* t5c 1500) (* t5d 100)) 7800)
-	(<= (+ (* t6n 700) (* t6p 800) (* t6s 1000) (* t6c 1600) (* t6d 100)) 7800)
-
-	(or (= 0 t1p) (= 0 t1c))
-	(or (= 0 t2p) (= 0 t2c))
-	(or (= 0 t3p) (= 0 t3c))
-	(or (= 0 t4p) (= 0 t4c))
-	(or (= 0 t5p) (= 0 t5c))
-	(or (= 0 t6p) (= 0 t6c))
-
-	(<= t1d 1)
-	(<= t2d 1)
-	(<= t3d 1)
-	(<= t4d 1)
-	(<= t5d 1)
-	(<= t6d 1)
-
-	(= t3s 0)
-	(= t4s 0)
-	(= t5s 0)
-	(= t6s 0)
-
-	(= (+ t1n t2n t3n t4n t5n t6n) 4)
-	(= (+ t1s t2s t3s t4s t5s t6s) 8)
-	(= (+ t1c t2c t3c t4c t5c t6c) 10)
-	(= (+ t1d t2d t3d t4d t5d t6d) 5)
-
-	(>= (+ t1p t2p t3p t4p t5p t6p) <REP>)
-)
-)
diff --git a/ar/assignments/src/a2.bash b/ar/assignments/src/a2.bash
deleted file mode 100644
index 5462573..0000000
--- a/ar/assignments/src/a2.bash
+++ /dev/null
@@ -1 +0,0 @@
-python3 a2.py | yices-smt -m
diff --git a/ar/assignments/src/a2.py b/ar/assignments/src/a2.py
deleted file mode 100644
index e5852e6..0000000
--- a/ar/assignments/src/a2.py
+++ /dev/null
@@ -1,71 +0,0 @@
-#!/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
-
-# Print preamble
-print("(benchmark a4.smt")
-print(":logic QF_UFLIA")
-
-# Print variables
-print(":extrafuns (")
-for i, (w, h) in enumerate(pc+rc, 1):
-    print("(c{:02d}x Int)".format(i), end=' ')
-    print("(c{:02d}y Int)".format(i), end=' ')
-    print("(c{:02d}w Int)".format(i), end=' ')
-    print("(c{:02d}h Int)".format(i))
-print(")")
-
-print(":formula")
-print("(and")
-
-# 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:02d}w {1}) (= c{0:02d}h {2})) '
-        '(and (= c{0:02d}w {2}) (= c{0:02d}h {1})))').format(i, w-1, h-1))
-
- # Print the bounds of the coordinates
-    print((
-         '(> c{0:02d}x 0) (> c{0:02d}y 0)'
-         '(<= (+ c{0:02d}x c{0:02d}w) {1}) (<= (+ c{0:02d}y c{0:02d}h) {2})'
-         ).format(i, mx, my))
-
- # Print the non overlap with others
-    for j in range(1, 1+len(pc+rc)):
-        if i != j:
-            print((
-                 '(or '
-                 '(> c{0:02d}x (+ c{1:02d}x c{1:02d}w)) (< (+ c{0:02d}x c{0:02d}w) c{1:02d}x) '
-                 '(> c{0:02d}y (+ c{1:02d}y c{1:02d}h)) (< (+ c{0:02d}y c{0:02d}h) c{1:02d}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:02d}x (/ c{0:02d}w 2) ) (+ c{1:02d}x (/ c{1:02d}w 2) ) ) {2} ) '
-                '(> (- (+ c{1:02d}x (/ c{1:02d}w 2)) (+ c{0:02d}x (/ c{0:02d}w 2))) {2}) '
-                '(> (- (+ c{0:02d}y (/ c{0:02d}h 2)) (+ c{1:02d}y (/ c{1:02d}h 2))) {2}) '
-                '(> (- (+ c{1:02d}y (/ c{1:02d}h 2)) (+ c{0:02d}y (/ c{0:02d}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:02d}x (+ c{1:02d}x 1 c{1:02d}w)) (< (+ c{0:02d}x c{0:02d}w) (- c{1:02d}x 1)) '
-            '(> c{0:02d}y (+ c{1:02d}y 1 c{1:02d}h)) (< (+ c{0:02d}y c{0:02d}h) (- c{1:02d}y 1))'
-            '))').format(i, j))
-    print(')')
-
-# Close the and,benchmark parenthesis
-print("))")
diff --git a/ar/assignments/src/a3.bash b/ar/assignments/src/a3.bash
deleted file mode 100644
index 115f1fd..0000000
--- a/ar/assignments/src/a3.bash
+++ /dev/null
@@ -1,5 +0,0 @@
-i=1
-while [ $(python3 a3.py $i | yices-smt) = "unsat" ]; do
-	i=$((i+1))
-done
-python3 a3.py $i | yices-smt -m
diff --git a/ar/assignments/src/a3.py b/ar/assignments/src/a3.py
deleted file mode 100644
index a295c8d..0000000
--- a/ar/assignments/src/a3.py
+++ /dev/null
@@ -1,47 +0,0 @@
-#!/usr/bin/env python3
-import sys
-
-if len(sys.argv) != 2:
-    print("usage: {} maxjobstart".format(sys.argv[0]))
-    exit()
-
-maxjobstart = sys.argv[1]
-jobs = 12
-J = range(1, jobs+1)
-Jprime = {5, 7, 10}
-pi = {
-    3: {1,2},
-    5: {3,4},
-    7: {3,4,6},
-    9: {5,8},
-    11: {10},
-    12: {9,11}
-}
-
-# Print preamble
-print("(benchmark a4.smt")
-print(":logic QF_UFLIA")
-
-# Print variables
-print(":extrafuns (")
-for i in J:
-    print("(j{} Int)".format(i), end=' ')
-print("\n)")
-
-print(":formula")
-print("(and")
-for i in J:
-    # Make sure the times are positive and within the bound
-    print("(> j{0} 0) (<= (+ j{0} {0}) {1})".format(i, maxjobstart))
-    # Make sure the dependencies are done when a task is scheduled
-    for k in pi.get(i, {}):
-        print("(>= j{0} (+ j{1} {1}))".format(i, k))
-# Make sure the shared resources are not used by two tasks at once
-for i in Jprime:
-    for k in Jprime:
-        if i != k:
-            print("(or (>= j{0} (+ j{1} {1}))".format(i,k), end=' ')
-            print("(<= (+ j{0} {0}) j{1}))".format(i,k))
-
-# Close the and,benchmark parenthesis
-print("))")
diff --git a/ar/assignments/src/a4.bash b/ar/assignments/src/a4.bash
deleted file mode 100644
index 569e152..0000000
--- a/ar/assignments/src/a4.bash
+++ /dev/null
@@ -1,5 +0,0 @@
-i=1
-while [ $(python3 a4.py $i | yices-smt) = "unsat" ]; do
-	i=$((i+1))
-done
-python3 a3.py $i | yices-smt -m
diff --git a/ar/assignments/src/a4.py b/ar/assignments/src/a4.py
deleted file mode 100644
index 51d5347..0000000
--- a/ar/assignments/src/a4.py
+++ /dev/null
@@ -1,60 +0,0 @@
-#!/usr/bin/env python3
-import sys
-iterations = int(sys.argv[1]) if len(sys.argv) > 1 else 11
-numa = int(sys.argv[2]) if len(sys.argv) > 2 else 7
-
-##Print preamble
-print("(benchmark a4.smt")
-print(":logic QF_UFLIA")
-
-##Print variables
-print(":extrafuns (")
-print("(a{} Int)".format(1))
-print("(a{} Int)".format(numa))
-for i in range(iterations):
-    for v in range(2,numa):
-        print("(i{}a{} Int) ".format(i,v))
-    print("(c{} Int)".format(i))
-print(")")
-
-##Print preconditions
-print(":formula")
-print("(and")
-print("(= c0 0)")
-print("(= a1 1)")
-print("(= a{0} {0})".format(numa, numa))
-for i in range(2,numa):
-    print("(= i0a{0} {0})".format(i))
-
-##Print iterations
-for i in range(1, iterations):
-    print("(or")
-    for v in range(2, numa):
-        print("(and")
-        print("(= c{} {})".format(i, v))
-        for ov in [k for k in range(2, numa) if k != v]:
-            print("(= i{0}a{1} i{2}a{1})".format(i, ov, i-1))
-        im1 = 'a1' if v == 2 else 'i{}a{}'.format(i, v-1)
-        ip1 = 'a{}'.format(numa) if v == numa-1 else 'i{}a{}'.format(i-1, v+1)
-        print("(= i{}a{} (+ {} {}))".format(i, v, im1, ip1))
-        print(")")
-    print("(and")
-    print("(= c{} 0)".format(i))
-    for ov in range(2, numa):
-        print("(= i{0}a{1} i{2}a{1})".format(i, ov, i-1))
-    print(")")
-    print(")")
-
-
-## Post conditions
-print("(or")
-for v in range(2, numa):
-    print("(and (>= i{}a{} 50)".format(iterations-1, v))
-    print("(or")
-    for ov in [k for k in range(2, numa) if k != v]:
-        print("(= i{0}a{1} i{0}a{2})".format(iterations-1, v, ov))
-    print("))")
-print(")")
-
-## Close the and,benchmark parenthesis
-print("))")