\usetikzlibrary{external,shapes.symbols,automata,positioning,arrows.meta,decorations.pathmorphing}

\usepackage{pgfplots}
\usepgfplotslibrary{fillbetween}
\pgfplotsset{compat=1.18}
\usetikzlibrary{external,shapes.symbols,automata,positioning,arrows.meta,decorations.pathmorphing,datavisualization.formats.functions,patterns}

    Satisfiability and entailment checks are computed using the SMT-Solver Z3.
    projections are calculated using the library Apron and the Parma polyhedra
    library included therein. Both, Z3 and Apron are already in use in
    \gls{koat} and are fit for the task.
    Boxes and other special polyhedra can be used trivially through the apron
    api and provide quicker but less tight alternative to polyhedra. However,
    we will consider them out of scope for this thesis.

\section{Theory}\label{sec:theory}

\section{Partial evaluation on probabilistic programs}\label{sec:theory}

\section{Abstraction}

\subsection{Choosing properties heuristically}
\todo{describe the original heuristic}

\begin{comment}
    motivate abstraction
\end{comment}
\subsection{Abstract everything}
\begin{comment}
    pro: easy to implement
    contra: 
    - abstractions are expensive
    - abstractions loose precision
    open question:
    - how to select properties
\end{comment}
\subsection{Abstract Loop heads}
\begin{comment}
    technique: 
    - offline
    - daikstra
    - FVS
    pro: 
    - probably close to optimal
    - heuristic from domenech19
    - unclear how to propagate for overlapping loops.
    contra:
    - fvs is NP-complete [citation needed]
    - possibly cheaper for scc instead of whole program
    - unclear what a loop-head is.
\end{comment}

\todo{find a better heuristic?}

\subsection{$k$-encounters}
\begin{comment}
    technique: 
    - online
    - daikstra during traversal
    pro: 
    - takes unreachable loops into account
    - allows for some constantly bounded loops to be perfectly unrolled. 
    contra: 
    - hard to implement 
    - hard to reason on
\end{comment}
\subsection{Considering probability}
\begin{comment}
    - probability is not important for finding loops.
    - all transitions that exist have a non-zero probability and hence are
    walkable in theory
\end{comment}
\section{Choosing properties}

\begin{comment}
    termination:
    - assume the abstraction method cuts every cycle
    - only finitely many abstractions exist
    -> the partial evaluation graph is finite
    -> the algorithm terminates
    correctness:
    - the abstraction is entailed by the state
    - every walkable path in the program/scc exists in the partial evaluation
    graph
\end{comment}
\section{Refining invariants}
\begin{comment}
    because we use polyhedra instead of boxes, our invariants are probably
    tighter than the original ones. When this is the case replace them in the
    program. 
\end{comment}

Koat2 can work on integer programs with polynomial integer
arithmetic.\cite{Brockschmidt16} To represent states and invariants in such a
program, one needs polynomial constraints. As an extended concept Koat2 uses
boxes and we will use polyhedra for the partial evaluation. Since those concepts
are closely related we will introduce them together. 

%
% Koat2 can work on integer programs with polynomial integer
% arithmetic.\cite{Brockschmidt16} To represent states and invariants in such a
% program, one needs polynomial constraints. As an extended concept Koat2 uses
% boxes and we will use polyhedra for the partial evaluation. Since those concepts
% are closely related we will introduce them together. 

integer arithmetic. Let $V$ be a finite set of variables. 

integer arithmetic. Let $\V = \{v_1, \dots v_n\}$ be a finite set of variables.

    For a given finite set of variables $\V = {v_1, \dots v_n}$, the set of 
    \textit{linear} constraints $\L$ over the variables $\V$ is defined as the 
    set $\set{a_0 + \sum_{i=1}^{|\V|} a_i v_i < 0}{a_i \in \Z, v_i \in \V}$.
    The set of \textit{polynomial} constraints $\C$ is defined as the set $\{e <
    0 | e \in \Z[\V]\}$. 

    For a given finite set of variables $\V$, the set of \textit{linear}
    constraints $\L$ over the variables $\V$ is defined as the set $\set{a_0 +
    \sum_{i=1}^{|\V|} a_i v_i < 0}{a_i \in \Z}$. The set of
    \textit{polynomial} constraints $\C$ is defined as the set $\set{e < 0}{e
    \in \Z[\V]}$. 

% Satisfiability 

accordingly. 

accordingly.

    \beta) \models \LAnd_{c_i \in \C} c_i$. 

    \beta) \models \LAnd_{c_i \in C} c_i$. 

    \subset \C$, respectively.

    \subseteq \C$, respectively.

\begin{align*}
    \llbracket c_1 \Land c_2 \rrbracket &= \llbracket c_1 \rrbracket \intersect

\begin{align}
    \llbracket c_1 \Land c_2 \rrbracket = \llbracket c_1 \rrbracket \intersect

    \llbracket C \rrbracket &= \llbracket \LAnd_{c_i \in C} c_i \rrbracket \\
        &=  \Intersect_{c_i \in C} \llbracket c_i \rrbracket
\end{align*}

    \llbracket C \rrbracket = \llbracket \LAnd_{c_i \in C} c_i \rrbracket 
        =  \Intersect_{c_i \in C} \llbracket c_i \rrbracket
\end{align}

Koat2 uses this representation internally and it makes proofs more concise.

\gls{koat} uses this representation internally and it makes proofs more concise.

Hence, we will use the all operators above, whenever it improves readability, 
but assume the constraints to be into the simplified form from the definition, 
in formal proofs. 

Hence, we will use the all operators above, whenever it improves readability,
but assume the constraints to be of the simplified form, in formal proofs. 
Another way of reasoning about constraints is to see them in an $n$-dimensional
space. Constraints partition the space excluding one half. In case of integer
arithmetic the solutions are discrete points in this space. Linear constraints
describe half-spaces and a set of linear constraints describes a (possibly
open) convex polyhedron. More about polyhedron in \Sref{sec:polyhedron}.

The problem of determining, if a set of constraints is satisfiable or finding a
valid or all valid variable assignment is called \Gls{smt} and well
studied.\todo{Quellenangaben} We will use the SMT-solver Z3\todo{Quellenangaben}
for this thesis.

\begin{example}\label{ex:1}
    \begin{figure}[h]\label{fig:ex1}
        \centering
        \subbottom[Formula $\varphi_1$]{
            \centering
            \input{figures/ch1_example1_phi1}
        }
        \subbottom[Formula $\varphi_2$]{
            \centering
            \input{figures/ch1_example1_phi2}
        }
        \subbottom[Formula $\varphi_3 = \varphi_1 \land \varphi_2$]{
            \centering
            \input{figures/ch1_example1_phi3}
        }
        \caption{Graphical representation of the set of constraints $\varphi_1$,
        $\varphi_2$ and $\varphi_3$ from Example \ref{ex:1}. Every constraint is
        represented by a line and the excluded side is marked by hatchings. }
    \end{figure}
    Consider the following constraints over the variables $\V = \{x, y\}$:
    \begin{align}
        \varphi_1 &= 2y \leq x \\
        \varphi_2 &= 2y > x^2 - 4
    \end{align}
    They are graphically represented in \fref{fig:ex1} using a 2D-coordinate
    system. Since the space is two-dimensional the linear constraint $\varphi_1$
    can be represented as a straight line and $\varphi_2$ as a parabola. 

% Entailment

    The solutions are marked as circles. For example, the assignment $\sigma: x
    \mapsto 0, y \mapsto -2$ (colored red) satisfies $\varphi_1$ but not
    $\varphi_2$. The conjunction $\varphi_3 = \varphi_1 \land \varphi_2$ is
    clearly equal to the intersection of both sets of solutions. While
    $\varphi_1$ and $\varphi_2$ have infinitely many solutions, the conjunction
    $\varphi_3$ has not. 
\end{example}
The problem of determining, if a set of constraints is satisfiable or finding
valid variable assignments for a given formula is called \gls{smt}-solving and
is well researched. The theories relevant for this thesis the are
quantifier-free linear integer arithmetic (usually called \texttt{QF\_LIA}) and
quantifier-free polynomial integer arithmetic (\texttt{QF\_PIA}). 

    Let $A, B \subseteq \C$. If $A \models B$ then, $\llbracket A \rrbracket \subset
    \llbracket B \rrbracket$ and we say that $A$ \textit{entails} $B$.

    Let $\varphi_1, \varphi_2$ be FO-formulas with variables $\V$. If $\varphi_1
    \models \varphi_2$, then $\llbracket \varphi_1 \rrbracket \subseteq
    \llbracket \varphi_2 \rrbracket$ and we say that $\varphi_1$
    \textit{entails} $\varphi_2$.

Example: $X < 1 \Land Y \leq X$ entails $Y \leq 0$.

\begin{lemma}
    $\varphi_1$ entails $\varphi_2$ if and only if $\varphi_1 \lor \neg
    \varphi_2$ is unsatisfiable.
    \begin{proof}
        Assume $\varphi_1$ entails $\varphi_2$. Let $\sigma \models \varphi_1$ be
        any satisfying assignment of $\varphi_1$. From the assumption follows
        $\sigma \models \varphi_2$ and in turn $\sigma \not\models
        \neg\varphi_2$ by FO-semantics.
        Since every satisfying assignment of $\varphi_1$ cannot satisfy $\neg
        \varphi_2$ at the same time, $\varphi_1 \land \neg \varphi_2$ has no
        satisfying assignments.
    \end{proof}
\end{lemma}
\begin{example}
    Lets take a look at some examples for entailment:
    \begin{itemize}
        \item $x > 1 \land y \geq x$ entails $y \geq 0$. 
        \item $1 < 0$ entails any constraints, because $\llbracket 1 < 0
            \rrbracket = \emptyset$ and the empty set is subset of any other
            set. 
        \item $x > 0$ does not entail $x > 1$, since the assignment $\sigma(x) =
            1$ satisfies $x > 0$ but not $x > 1$.
    \end{itemize}
\end{example}
Sometimes one want's to remove a variable from a formula or a set of
constraints. It is especially useful, when having a formula with temporary
variables that are only relevant to a certain transition but should not
influence the program after wards. 
Formally, removing a variable is equivalent to existentially quantifying it.
However, existential quantification is not available in quantifier free integer
arithmetic. Instead one searches for a formula that describes all original
solutions but restricted to the smaller domain. 

    Let $X \subset V$ and $C \subset \C$ be a set of constraints over the
    variables $V$. Then the $\text{proj}_X(C)$ -- say the projection of $C$
    onto the variables $X$ -- is the set of constraints $C'$ such that
    $\llbracket C' \rrbracket = \{\beta|_X \hspace{0.5em} | \hspace{0.5em} \beta
    \in \llbracket C \rrbracket \}$.

    Let $X \subseteq V$ and $\varphi$ be an FO-formula over the variables $V$
    and let $\sigma|_X$ denote the restriction of $\sigma$ to the smaller to
    domain $X$.
    The projection of $\varphi$ onto $X$ denoted as $\text{proj}_X(\varphi)$ is
    a formula $\varphi'$, with $\llbracket \varphi' \rrbracket =
    \set{\sigma|_X}{\sigma \in \llbracket \varphi \rrbracket}$. 
    \todo{use $\sigma$ and $\beta$ consistently.}

For a finite set of variables $|V| = n $, one can think of all possible
assignments as a set of points in an n-dimensional space. In case of linear 
constraints, the set of solutions the convex-hull around the possible solutions 
is called a polyhedron. The polyhedron doesn't need to be finite or closed in 
all dimensions, if for example, the value of the variable is unimportant to the
satisfiability of the constraints. A set of constraints $A$ entails $B$ if the
polyhedron is encloses by the other. Calculating polyhedra, projections
and testing for entailment can be done with libraries like the
\gls{ppl}.\todo{citation} In Koat2, Apron is used that uses \gls{ppl} under the
hood. 

Geometrically, the projection can be seen as set of solutions projected
(casting a shadow) onto the remaining dimensions. 
\begin{example}
    Take the formula $\varphi = y < x + 4 \land y < -x + 4 \land y > x + 1
    \land y > -x + 1 $ over the variables $\V = \{x, y\}$, for example. The
    solutions to the formula are points in a two-dimensional space. Projecting
    the formula $\varphi$ onto the variables $X = \{x\}$ gives the following
    formula $\text{proj}_X(\varphi) = x \geq -1 \land x \leq 1$.
    The projection is equal to casting the shadow of the 2D-polyhedron onto the
    $x$-axis like shown in \fref{fig:ex2}. 
    \begin{figure}\label{fig:ex2}
        \centering
        \input{figures/ch1_example2}
        \caption{Projecting a
        2D-constraint.}
    \end{figure}
\end{example}
\subsection{Convex Polyhedron}\label{sec:polyhedron}