2 solved

[ar1516.git] / a2 / ar.tex

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