\LoadClass[a4paper,12pt,twoside,openright]{memoir}

\LoadClass[a4paper,11pt,twoside,openright]{memoir}

\RequirePackage{stmaryrd}

\newtheorem{example}{Example}

\newcommand{\C}[0]{\mathcal{C}} % Set of Constraints

\newcommand{\C}[0]{\mathcal{C}} % Set of polynomial constraints
\renewcommand{\L}{\mathcal{L}} % Set of polynomial constraints

\newcommand{\Zs}[0]{\mathfrak{Z}} % the structure of integer arithmetic.

\newcommand{\Land}[0]{\wedge}
\newcommand{\LAnd}[0]{\bigwedge}
\newcommand{\set}[2]{\{#1\hspace{0.5em}|\hspace{0.5em}#2\}}

\subsection{Constraints, Polyhedra, Projections}

\subsection{Constraints}
%
\newacronym{smt}{SMT}{Satisfiability Modulo Theory}
\newacronym{ppl}{PPL}{Parma Polyhedra Library}
\newacronym{koat}{KoAT2}{KoAT2} \todo{wrong acronym}
%

program, one needs polynomial constraints. As an extended concept Koat uses
Boxes and we will use Polyhedra for the partial evaluation. Since those concepts

program, one needs polynomial constraints. As an extended concept Koat2 uses
boxes and we will use polyhedra for the partial evaluation. Since those concepts

Let $\PV$ be a set of program variables and $\TV$ be a set of temporary
variables. Together they form the set of variables $\V := \PV \union \TV$. 
Let $(\N, +, \cdot, 0, 1, <)$ be the structure of 
The set of constraints $\C$ is defined as the minimal as $\{c = e < 0 | e \in
\Z[\V]\}$. That is the set of all constraints over integer polynomials less than
zero.

Let $\Zs := (\Z, +, \cdot, 0, 1, <)$ be the structure of ordered standard
integer arithmetic. Let $\PV$ be a finite set of program variables and $\TV$ be
a finite set of temporary variables. Together they form the set of variables $\V
:= \PV \union \TV$. 
\begin{definition}[Constraint]
    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]\}$. 
\end{definition}
% Satisfiability 
Constraints are a subset of FO formulas and thus the semantics according to the
semantics of FO-formulas. 
\begin{definition}[Satisfiability]
    A constraint $c \in \C$ is \textit{satisfiable} when the formula $\varphi=
    c$ is satisfiable in $\Zs$ or $\Zs \models c$. We say a variable assignment
    $\beta: \V \mapsto \Z$ \textit{satisfies} the constraint $c$ when $(\Zs,
    \beta) \models c$. 

Note that all constraint $e_1 \diamond e_2$ with the operators $\diamond
\in >, <, \leq, \geq$ can be transformed into an equivalent constraint $e' < 0
\in \C$:

    Analogously, satisfiability of a set of constraints is defined by the
    satisfiability of its conjunction. A set of constraints $C \subseteq \C$ is
    \textit{satisfiable} when $\Zs \models \LAnd_{c_i \in C} c_i$. Moreover, an
    assignment $\beta$ \textit{satisfies} the set of constraints $C$ when $(\Zs,
    \beta) \models \LAnd{c_i \in \C} c_i$. 
\end{definition}

We also write $\Zs \models C$ and $(\Zs, \beta)\models C$ instead of $\Zs
\models \LAnd_{c_i \in C} c_i$ and $(\Zs, \beta)\models \LAnd {c_i \in C} c_i$,
respectively. Furthermore, we use conjunctions and sets of constraints
interchangeably. 
Note that by definition constraints are restricted to the form $e < 0$, because
Koat2 uses this representation internally and it makes proofs more concise.
However, all constraint $e_1 \diamond e_2$ with the operators $\diamond \in >,
<, \leq, \geq$ can be transformed into equivalent constraints $e' < 0 \in \C$. 

    e_1 \leq e_2 &\equiv e_1 - e_2 < 0

    e_1 \leq e_2 &\equiv e_1 - e_2 - 1< 0 \\
    e_1 > e_2 &\equiv e_2 - e_1 < 0 \\
    e_1 < e_2 &\equiv e_1 - e_2 < 0

and so on. Koat2 internaly represents all constraints in the simplified form, 
and one can assume that all constraints are given in the simplified form. 
However, for better readability we will use the general form in the examples. 

Given a variable assignment $\sigma: \PV \mapsto \Z$ for the program variables
we say $\sigma$ satisfies the constraint $c \in \C$ when the constraint holds
with every variable $v \in \V$ being replaced by it's assigned value $\sigma(v)$
or more formally:

Equality can be simulated by two constraints. 

and we say a constraint is satisfiable if there exists a variable assignment
that satisfies the constraint. 

\begin{equation*}
    e_1 = e_2 \equiv e_1 \leq e_2 \Land e_1 \geq e_2
\end{equation*}

For a set of constraints $C \subset \C$ we say that it is satisfied by the
assignment, if and only if the assignmnet satisfies every constraint contained
in the set. 

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

\todo{existentially quantify variables}

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.

- struktur = universum + signatur + interpretation der signatur
in unserem fall:
  - universum = integer
  - signatur = (+, *, 0, 1, <)
  - interpretation wie erwartet

% Solutions
The we define $\llbracket c \rrbracket$ as the set of all satisfying assignments
of the constraint $c$ and $\llbracket C \rrbracket$ as the set of all satisfying
assignments for $C$. The following holds:

wir arbeiten auf quantoren freie 
wir definieren constraints 
wir erlauben ausschließlich FO(\tau) formeln der form von constraints

\begin{equation*}
    \llbracket C \rrbracket = \Intersect_{c_i \in C} \llbracket c_i \rrbracket
\end{equation*}

- $FO(\tau)$ formeln
- Atom $
- constraints als quantoren freie Formeln auffassen.
- existentieller abschluss: existentielle quantifizierung aller Variablesn
Notation: $\models$

% Entailment
\begin{definition}[Entailment]
    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$.
\end{definition}
Example: $X < 0 \Land Y \leq X$ entails $Y \leq 1$.

Finding a variable assignment

\begin{definition}[Projection]
    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 \}$.
\end{definition}

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. 

\newacronym{pip}{PIP}{Probabilistic Integer Program}