a2/ar.tex

   1 %&ar
   2 \begin{document}
   3 \maketitle
   4 \tableofcontents
   5
   6 %\setcounter{section}{-1}
   7 %\section{General approach}
   8 %Implementing all the problems by hand in SMT-Lib format would be too much work
   9 %and therefore all problems have an accompanying bash script contains a function
  10 %\lstinline{generate} that generates the SMT-Lib format. The script feeds the
  11 %SMT-Lib format to yices after which the output is feeded to a Python script
  12 %that visualizes the solution. This means that for all problems $p$ for $p\in
  13 %\{1,\ldots, 4\}$ there exist $2$ files. \texttt{ap.bash} that generates the
  14 %solution and \texttt{ap.py} that visualizes the solution. All solving is done
  15 %on the benchmark system listed in Listing~\ref{listing:benchmark}.
  16 %
  17 %\begin{lstlisting}[caption={Benchmark system},label={listing:benchmark}]
  18 %CPU: 3600MHz AMD FX(tm)-4100 Quad-Core Processor
  19 %RAM: 8GB
  20 %
  21 %Yices: 2.4.1
  22 %SMT-Lib: 1.2
  23 %Bash: 4.3.30(1)
  24 %\end{lstlisting}
  25
  26 \newpage
  27 \input{1.tex}
  28
  29 \newpage
  30 \input{2.tex}
  31
  32 \newpage
  33 \input{3.tex}
  34
  35 \newpage
  36 \input{4.tex}
  37
  38 \end{document}