success with 4:)

[ar1516.git] / a2 / ar.tex

diff --git a/a2/ar.tex b/a2/ar.tex
index 91fe795..5dabd82 100644 (file)
--- a/a2/ar.tex
+++ b/a2/ar.tex
@@ -3,36 +3,12 @@
 \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}