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. Both files are
15 present in the Section~
\ref{sec:appendix
}. All solving is done on the benchmark
16 system listed in Listing~
\ref{listing:benchmark
}.
18 \begin{lstlisting
}[caption=
{Benchmark system
},label=
{listing:benchmark
}]
19 CPU:
3600MHz AMD FX(tm)-
4100 Quad-Core Processor