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}