ar.tex

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