--- /dev/null
+LATEX:=pdflatex
+
+DOCUMENT:=ar
+PROBLEMS:=1 2 3 4
+
+SOURCES:=$(DOCUMENT).tex $(addsuffix .tex,$(PROBLEMS))
+
+.SECONDARY: $(DOCUMENT).fmt $(SOLUTIONS)
+
+all: $(DOCUMENT).pdf
+
+%.pdf: %.tex %.fmt $(SOURCES)
+ $(LATEX) $<
+ $(LATEX) $<
+
+%.fmt: pre.tex
+ $(LATEX) -ini -jobname="$(basename $@)" "&$(LATEX) $<\dump"
+
+clean:
+ $(RM) -v $(addprefix $(DOCUMENT).,fmt aux log out toc pdf)
--- /dev/null
+%&ar
+\begin{document}
+\maketitle
+\tableofcontents
+
+\setcounter{section}{-1}
+\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 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. 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
+RAM: 8GB
+
+Yices: 2.4.1
+SMT-Lib: 1.2
+Bash: 4.3.30(1)
+\end{lstlisting}
+
+\newpage
+\input{1.tex}
+
+\newpage
+\input{2.tex}
+
+\newpage
+\input{3.tex}
+
+\newpage
+\input{4.tex}
+
+\end{document}
--- /dev/null
+\documentclass{article}
+
+\usepackage{hyperref} % For clickable links
+\usepackage{a4wide} % For better page usage
+\usepackage{float} % For better placement of tables/figures
+\usepackage{amsmath} % For align
+\usepackage{listings} % For code snippets
+\usepackage{booktabs} % For nice tables
+
+\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 2}
+\date{\today}