ar.tex

   1 %&ar
   2 \begin{document}
   3 \maketitle
   4 \tableofcontents
   5
   6 \section{Introduction}
   7 Implementing all the problems by hand in SMT-Lib format would be too much work
   8 and therefore all problems have an accompanying bash script that does the
   9 generation and/or the mini or maximization. The bash scripts all have a
  10 function defined called \lstinline{generate} with a parameter that will be used
  11 for mini or maximization. All solving is done on the benchmark system listed in
  12 Listing~\ref{listing:benchmark}.
  13
  14 \begin{lstlisting}[caption={Benchmark system},label={listing:benchmark}]
  15 CPU: 3600MHz AMD FX(tm)-4100 Quad-Core Processor
  16 RAM: 8GB
  17
  18 Yices: 2.4.1
  19 SMT-Lib: 1.2
  20 Bash: 4.3.30(1)
  21 \end{lstlisting}
  22
  23 \newpage
  24 \input{1.tex}
  25
  26 \newpage
  27 \input{2.tex}
  28
  29 \newpage
  30 \input{3.tex}
  31
  32 \newpage
  33 \input{4.tex}
  34
  35 \newpage
  36 \input{a.tex}
  37
  38 \end{document}