% \documentclass{beamer}
% \setbeamertemplate{navigation symbols}{}
% \usepackage[utf8]{inputenc}
% \usepackage{amsthm}
% \usepackage{amssymb}

% \usepackage{listings}
% \input{../common/scalalistings}

% \input{../common/mysymbols}
% \input{../common/mywords-en}
% \input{../common/constructors}

% \title{Lecture 1 \\ Synthesis, Analysis, and Verification}
% \author{Viktor Kuncak}
% \date{}

% \begin{document}

% \maketitle
% %\tableofcontents

% %\renewcommand{\pause}{}

% \begin{frame}
% \frametitle{Today}

% See web site \url{http://lara.epfl.ch/w/sav} for logistics

% What
% \begin{itemize}
% \item verification
% \item analysis
% \item synthesis
% \end{itemize}

% Demo of \url{http://leon.epfl.ch}

% Verification industry ((r)/TM/(c))
% \begin{itemize}
% \item Coverity (press release)
% \item AbsInt and ASTREE
% \item Jasper
% \item Monoidics
% \end{itemize}
% \end{frame}

% \begin{frame}
% \frametitle{Countdown Program}

% \lstinputlisting{ex0.scala}

% \end{frame}

\newcommand{\w}[1]{\,\mbox{#1}} % word
\newcommand{\boolTrue}{\w{true}}
\newcommand{\boolFalse}{\w{false}}

\begin{frame}
\frametitle{Formal Verification Methodology}

We can view formal verification of program as a three-step approach:
\begin{enumerate}
\item Express properties in logic or code \\
  (assertions, preconditions, post-conditions, invariants, run-time error conditions)
\item Compile program meaning to \textbf{logical formulas} \\
  (verification-condition generator, symbolic execution)
\item Develop and use an automated theorem prover for generated conditions \\
  (SAT and SMT solving, resolution-based theorem proving, proof assistants)
\end{enumerate}

Which logic to use? Today: integer linear arithmetic (Presburger arithmetic)

\

\scalebox{0.8}{
\begin{minipage}{\textwidth}
References:
\begin{itemize}
\item Haase, Christoph. A survival guide to presburger arithmetic.
  ACM SIGLOG News. \url{https://dl.acm.org/doi/10.1145/3242953.3242964}.
\item \url{https://en.wikipedia.org/wiki/Presburger_arithmetic}
\item The Calculus of Computation (Bradley, Manna, Springer-Verlag 2007), Section 7.2
\end{itemize}
\end{minipage}}
\end{frame}

\begin{frame}
\frametitle{Presburger arithmetic}

Integer arithmetic with logical operations
(and, or, not), quantifiers, only addition as an arithmetic operation, and $<$ and $=$ as a relation.

\begin{itemize}
\item minimalistically one can define a variant of it over non-negative natural numbers as having $\land, \lnot, \forall,+,=$ as the only symbols
\end{itemize}

One of the earliest theories shown decidable.
Moj\.{z}esz Presburger gave an algorithm for quantifier elimination in 1929.
\begin{itemize}
\item a student of an influential logician and model theorist Alfred Tarski
\item Tarski assigned this question to Moj\.{z}esz for his MSc thesis and he solved it
\end{itemize} 

The result at this time was of interest to foundations of mathematics
(giving algorithmic meaning to quantifiers).

Subsequently, it found applications in automated reasoning, including
building first program verifiers
(Cooper 1972, Derek C. Oppen - STOC 1973).
\end{frame}

\nobox
\begin{frame}
\frametitle{Presburger Arithmetic for Verification}
\lstinputlisting{ex1.scala}

Verification condition (VC) for preservation of loop invariant:
\[
   \big[ I(res,i) \land i' = i - 1 \land res' = res + 2 \land 0 < i \big] 
   \rightarrow I(res',i')
\]
To prove that this VC is valid, we check whether its \emph{negation}
\[
   I(res,i) \land i' = i - 1 \land res' = res + 2 \land 0 < i \land \lnot I(res',i')
\]
is \emph{satisfiable}, i.e.\ whether this PA formula is true:
\[
   \exists x,res,i,res',i'.
\begin{array}[t]{l}
   \big[ res + 2i = 2x \ \land\ 0 \le i \ \land \  0 < i \ \land \\ 
   i' = i - 1 \ \land\ res' = res + 2 \ \land \ 
   \lnot (res' + 2i' = 2x\ \land\ 0 \le i') \big]
\end{array}
\]
\end{frame}

\begin{frame}
\frametitle{Introducing: One-Point Rule}
If $\bar y$ is a tuple of variables not containing $x$, then
\[
   \exists x. (x = t(\bar y) \land F(x,\bar y))  \  \iff \  F(t(\bar y),\bar y)
\]
Proof:
\begin{itemize}
\item[$\rightarrow$]: Consider the values of $\bar y$ such that there exists $x$, say 
$x_1$, for which $x_1 = t(\bar y) \land F(x_1,\bar y)$. Because $F(x_1,\bar y)$ evaluates
to true and the values of $x_1$
and $t(\bar y)$ are the same, $F(t,\bar y)$ also evaluates to true.
\item[$\leftarrow$]: Let $\bar y$ be such that $F(t,\bar y)$ holds. Let $x$ be the value
of $t(\bar y)$. Then of course $x = t(\bar y)$ evaluates to true and so does
$F(x,\bar y)$.  So there exists $x$
for which $x = t(\bar y) \land F(x,\bar y)$ holds.
\end{itemize}

\emph{One point rule}:\\ 
\ \ replaces left side (LHS) of equivalence by the right side (RHS). 

\emph{Flattening}, used when $t$ is complex, replaces RHS by LHS.
\end{frame}

\begin{frame}
\frametitle{Dual One-Point Rule for $\forall$}
\[
   \forall x. (x = t(\bar y) \rightarrow F(x,\bar y))  \  \iff \  F(t(\bar y),\bar y)
\]
To prove it, negate both sides:
\[
   \exists x. (x = t(\bar y) \land \lnot F(x,\bar y))  \  \iff \  \lnot F(t(\bar y),\bar y)
\]
so it reduces to the rule for $\exists$.
\end{frame}

\begin{frame}
\frametitle{Using One-Point Rule on Negated Verification Condition}
\[
   \exists x,res,i,res',\underline{\textbf{i'}}.
\begin{array}[t]{l}
   \big[ res + 2i = 2x \ \land\ 0 \le i \ \land \  0 < i \ \land \\ 
   \underline{\textbf{i' = i - 1}} \ \land\ res' = res + 2 \ \land \ \\ 
   \lnot (res' + 2i' = 2x\ \land\ 0 \le i') \big]
\end{array}
\]
\pause
\[
   \exists x,res,i,\underline{\textbf{res'}}.
\begin{array}[t]{l}
   \big[ res + 2i = 2x \ \land\ 0 \le i \ \land \  0 < i \ \land \\ 
     \underline{\textbf{res' = res + 2}} \ \land \ \\ 
   \lnot (res' + 2(i-1) = 2x\ \land\ 0 \le i-1) \big]
\end{array}
\]
\pause
\[
   \exists x,res,i.
\begin{array}[t]{l}
   \big[ \underline{res + 2i = 2x} \ \land\ 0 \le i \ \land \ 0 < i \ \land \\ 
   \lnot (res + 2 + 2(i-1) = 2x\ \land\ 0 \le i-1) \big]
\end{array}
\]
\pause
\[
   \exists x,\underline{\textbf{res}},i.
\begin{array}[t]{l}
   \big[ \underline{\textbf{res = 2x - 2i}} \ \land\ 0 \le i \ \land \ 0 < i \ \land \\ 
   \lnot (res + 2 + 2(i-1) = 2x\ \land\ 0 \le i-1) \big]
\end{array}
\]
\pause
\[
   \exists x,i.
\begin{array}[t]{l}
   \big[ 0 \le i \ \land \ 0 < i \ \land \\ 
   \lnot (2x - 2i + 2 + 2(i-1) = 2x\ \land\ 0 \le i-1) \big]
\end{array}
\]
Simplifies to $\exists x,i.\ 0 < i \land \lnot (0 \le i-1)$ and then to $\boolFalse$.
\end{frame}

\begin{frame}
\frametitle{But there is more}

One-point rule is one of the many steps used in \\
\textbf{quantifier elimination} procedures.
\end{frame}

%% \begin{frame}
%% \frametitle{Example 2: Lower Bounds}
%% \end{frame}
%% \begin{frame}
%% \frametitle{Example 3: Divisibility}
%% \end{frame}
%% \begin{frame}
%% \frametitle{Example 4: Disjunctions}
%% \end{frame}

\begin{frame}
\frametitle{Quantifier Elimination (QE)}

\centerline{
\scalebox{5}{
\huge$\ooalign{\raisebox{0.25ex}{\normalsize\hspace{0.28em}$\forall$\tiny $\exists$}\cr$\varnothing$}$
}}
%% \def\qeq{\mathrel{%
%%     \mathchoice{\QEQ}{\QEQ}{\scriptsize\QEQ}{\tiny\QEQ}%
%% }}
%% \def\QEQ{{%
%%     \setbox0\hbox{=}%
%%     \rlap{\hbox to \wd0{\hss?\hss}}\box0
%% }}

\ \\

Given a formula $F(\bar y)$ containing quantifiers find a 
formula $G(\bar y)$ 
\begin{itemize}
\item \textbf{equivalent} to $F(\bar y)$
\item that has \textbf{no quantifiers}
\item and has a \textbf{subset (or equal set) of free variables} of $F$
\end{itemize}
Note
\begin{itemize}
\item Equivalence: For all $\bar y$, $F(\bar y)$ and $G(\bar y)$ have same truth value \\
  $\leadsto$ we can use $G(\bar y)$ instead of $F(\bar y)$
\item No quantifiers: easier to check satisfiability of $G(\bar y)$
\end{itemize}

{\small $\bar y$ is a possibly empty tuple of variables}


\end{frame}

\begin{frame}
\frametitle{We are lucky when a theory has (``admits'') QE}

Suppose $F$ has no free variables (all variables are quantified).

What is the result of applying QE to $F$? 

\pause
Are there any variables in the resulting formula?
\pause
\begin{itemize}
\item No free variables: they are a subset of the original, empty set
\item No quantified variables: because it has no quantifiers \smiley
\end{itemize}
Formula without any variables! Example:
\[
    (2 + 4 = 7) \lor (1 + 1 = 2)
\]
We check the truth value of such formula by simply evaluating it!
\end{frame}

\begin{frame}
\frametitle{Using QE for Deciding Satisfiability/Validity}

\begin{itemize}
\item To check satisfiability of $H(\bar y)$: eliminate the quantifiers from
$\exists \bar y. H(\bar y)$ and evaluate.
\item Validity: eliminate quantifiers from $\forall \bar y. H(\bar y)$ and evaluate
\end{itemize}

We can even check formulas like this:
\[
    \forall x,y,r.\ \exists z.\ (5 \le r \land x + r \leq y) \rightarrow 
      (x < z \land z < y \land 3|z) 
\]
Here $3|z$ denotes that $z$ is divisible by 3.

\end{frame}

\begin{frame}
\frametitle{Does Presburger Arithmetic admit QE?}

\pause
Depends on the particular set of symbols!

(Recall objective: given $F(\bar y)$ containing quantifiers find a 
formula $G(\bar y)$ 
\begin{itemize}
\item \textbf{equivalent} to $F(\bar y)$
\item that has \textbf{no quantifiers}
\item and has a \textbf{subset (or equal set) of free variables} of $F$)
\end{itemize}

If we lack some operations that can be expressed using quantifiers, 
there may be no equivalent formula without quantifiers.
\begin{itemize}
\item $\exists y. x = y + y + y$, so we better have divisibility
\end{itemize}
Quantifier elimination says: if you can define some relationship between
variables using an arbitrary, possibly quantified, formula $F$,
\[
    r \mathop{=}\limits^{def} \{ (x,y) \mid F(x,y) \}
\]
then you can also define same $r$ using another quantifier-free formula $G$.

\end{frame}

\begin{frame}
\frametitle{Presburger Arithmetic (PA)}
We look at the theory of integers with addition.
\begin{itemize}
\item  introduce constant for each integer constant
\item to be able to restrict values to natural numbers when needed, and to compare them, we introduce $<$
\item introduce not only addition but also subtraction 
\item to conveniently express certain expressions, introduce function $m_K$ for each $K \in \mathcal{Z}$, to be interpreted as multiplication by a constant, $m_K(x)= K \cdot x$.  We write $m_K$ as $K \cdot x$. \\
 Note: there is \emph{no multiplication between variables} in PA
 \item to enable quantifier elimination from $\exists x. y= K \cdot x$ introduce for each $K$ predicate $K|y$ (divisibility,  $y \% K = 0$)
\end{itemize}
The resulting language has these function and relation symbols: \\
$\{ +, -, =, < \} \cup \{ K \mid K \in \mathbb{Z}\} \cup \{ (K \cdot \_) \mid K \in \mathbb{Z} \} \cup \{ (K|\_) \mid K \in \mathbb{Z} \}$
We also have, as usual:\ $\land,\lor,\lnot,\rightarrow$ \ and also:\ $\exists,\forall$
\end{frame}

\begin{frame}
\frametitle{Example}
\textbf{Eliminate $y$ from this formula:}
\[
    \exists y.\ \  3 y - 2 w + 1 > - w  \land  2y - 6 < z \land 4 \mid 5y + 1
\]
What should we do first?
\pause

Simplify/normalize what we can using properties of integer operations:
\[
    \exists y.\ \  0 <  -w + 3 y + 1 \ \ \land \ \  
                   0 < - 2y + z + 6 \ \land \ 4 \mid 5y + 1
\]
\pause
First we will consider only eliminating existential from a \textbf{conjunction of literals}.
\end{frame}

\begin{frame}
\frametitle{Conjunctions of Literals}

\textbf{Atomic formula}: a relation applied to argument. 

Here, relations are: $=$, $<$, $K|\_$. So, atomic formulas are: \\
\ \ $t_1 = t_2$, \ \ $t_1 < t_2$, \ \ $K \mid t$ \\

\pause

\textbf{Literal:} Atomic formula or its negation. Example: $\lnot (x = y+1)$

Conjunction of literals: $L_1 \land \ldots \land L_n$

\begin{itemize}
\item no disjunctions, no implications
\item negation only applies to atomic formulas
\end{itemize}

We first consider the quantifier elimination problem of the form:
\[
\exists y.\ L_1 \land \ldots \land L_n
\]
This will prove to be sufficient to eliminate all quantifiers!
\end{frame}

\begin{frame}
\frametitle{Eliminating $\exists$ from conjunction of literals suffices}

Can we eliminate $\exists$ from any \textbf{quantifier-free formula}?
\[
  \exists x. F(x,\bar y)
\]
where $F$ is quantifier-free?

\pause
Formula without quantifiers has $\land$,$\lor$,$\lnot$ applied to atomic formulas.

\pause
Convert $F$ to \textbf{disjunctive normal form}:
\[
    F   \iff   \bigvee_{i=1}^m C_i
\]
each $C_i$ is a \textbf{conjunction of literals}.

\pause
\[
    \big[ \exists x. \bigvee_{i=1}^m C_i \big]  \iff 
    \bigvee_{i=1}^m (\exists x. C_i)
\]

\end{frame}

\begin{frame}
\frametitle{How does disjunctive normal form (DNF) transformation work?}

Which steps should we use?

\pause
\textbf{Negation propagation:}
\[
   \lnot (p \land q) \ \leadsto\ (\lnot p) \lor (\lnot q)
\]
\[
   \lnot (p \lor q) \ \leadsto\ (\lnot p) \land (\lnot q)
\]
\[
   \lnot\lnot p \ \leadsto \ p
\]
Result is \textbf{negation-normal form}, NNF

NNF transformation is polynomial (exercise!)

\pause
\textbf{Distributivity}
\[
   a \land (b_1 \lor b_2) \ \leadsto \ (a \land b_1) \lor (a \land b_2)
\]
This can lead to exponential explosion.

Can we obtain \emph{equivalent} DNF formula without explosion?

\pause
No! We can prove this (no equivalent DNF formula exists), unrelated to NP vs P
\end{frame}

\begin{frame}
\frametitle{Eliminating from quantifier free formulas}

\[
    \exists x. F \iff
    \big[ \exists x. \bigvee_{i=1}^m C_i \big] \iff
    \bigvee_{i=1}^m (\exists x. C_i)
\]

\end{frame}

\begin{frame}
\frametitle{Nested Existential Quantifiers}
\[
  \exists x_1. \exists x_2. \underline{\mathbf{\exists x_3}}. F_0(x_1,x_2,x_3,\bar y)
\]
\pause
\[
  \exists x_1. \underline{\mathbf{\exists x_2}}. F_1(x_1,x_2,\bar y)
\]
\pause
\[
  \underline{\mathbf{\exists x_1}}. F_2(x_1,\bar y)
\]
\pause
\[
   F_3(\bar y)
\]
%\pause
%\centerline{\smiley}

\end{frame}

\begin{frame}
\frametitle{Universal Quantifiers}

If $F_0(x,\bar y)$ is quantifier-free, how to eliminate
\[
    \forall x. F_0(x,\bar y)
\]
\pause
Note this equivalence ($F_0$ universally holds if there is no counterexample):
\[
    \forall x. F_0(x,\bar y) \iff \lnot \big[ \exists x.  \lnot F_0(x,\bar y) \big]
\]
It thus suffices to handle:
\[
    \lnot \big[ \exists x.  \lnot F_0(x,\bar y) \big]
\]
Note that $\lnot F_0(x,\bar y)$ is quantifier-free, so we know how to eliminate $\exists x. \lnot F_0(x,\bar y)$:
\[
   \hspace*{2.5cm}
   \exists x. \lnot F_0(x,\bar y) \ \ \leadsto \ \ F_1(\bar y)
\]
Then the result of the elimination is the quantifier-free formula:
\[
    \lnot F_1(\bar y)
\]
\end{frame}

\begin{frame}
\frametitle{Removing any \textbf{alternation} of quantifiers: illustration}

Alternation: switch between existentials and universals
\[
  \exists x_1. \forall x_2. \forall x_3. \exists x_4. F_0(x_1,x_2,x_3,x_4,\bar y)
\]
\[
  \exists x_1. \lnot \exists x_2. \exists x_3. \lnot \underline{\exists x_4. 
     F_0(x_1,x_2,x_3,x_4,\bar y)}
\]
\[
  \exists x_1. \lnot \exists x_2. \underline{\exists x_3. \lnot 
     F_1(x_1,x_2,x_3,\bar y)}
\]
\[
  \exists x_1. \lnot \underline{\exists x_2. 
     F_2(x_1,x_2,\bar y)}
\]
\[
  \exists x_1. \lnot 
     F_3(x_1,\bar y)
\]
\[
    F_4(\bar y)
\]

Each quantifier alternation involves a disjunctive normal form transformation.

In practice, we do not have many alternations.

\end{frame}

\begin{frame}
\frametitle{Back to Presburger Arithmetic}
Consider the quantifier elimination problem of the form:
\[
\exists y.\ L_1 \land \ldots \land L_n
\]
where $L_i$ are literals from PA.

Note that, for integers:
\begin{itemize}
\item $\lnot (x < y) \iff y \le x$
\item $x < y \iff x + 1 \le y$
\item $x \le y \iff x < y + 1$
\end{itemize}
We use these observations below. 

Instead of $\le$ we choose to use $<$ only.

We do not write $x > y$ but only $y < x$.

\end{frame}

\begin{frame}
\frametitle{Normalizing Literals for PA}

\textbf{Normal Form of Terms:}
All \emph{terms} are built from $K,+,-,K\cdot\_$, so using standard transformations they can be represented as: $K_0 + \sum_{i=1}^n K_i x_i$
We call such term a linear term.

\textbf{Normal Form for Literals in PA:}
\begin{align*}
\lnot (t_1 < t_2) &\text{ becomes } t_2 < t_1 + 1\\
\lnot (t_1 = t_2) &\text{ becomes } t_1 < t_2 \lor t_2 < t_1\\
t_1 = t_2 &\text{ becomes } t_1 < t_2 + 1 \land t_2 < t_1 + 1 \ \ (*)\\
\lnot (K \mid t) &\text{ becomes } \displaystyle\bigvee_{i=1}^{K-1} K \mid t+i\\
t_1 < t_2 &\text{ becomes  } 0 < t_2 - t_1
\end{align*}
To remove disjunctions we generated, compute DNF again.

$(*)$
We transformed equalities just for simplicity. Usually we handle them directly.
\end{frame}


\begin{frame}
\frametitle{Why one-point rule will not be enough}

Note that we must handle inequalities, not merely equalities

\ \\

If we have integers, we cannot always divide perfectly.

Variable to eliminate can occur not as $y$ but as, e.g.\ $3y$

\end{frame}

\begin{frame}
\frametitle{Exposing the Variable to Eliminate: Example}
\[
    \exists y.\ \  0 <  -w + \bunder{3y} + 1 \ \ \land \ \  
                   0 < - \bunder{2y} + z + 6 \ \land \ 4 \mid \bunder{5y} + 1
\]
Least common multiple of coefficients next to $y$, $M = lcm(3, 2, 5) = 30$

Make all occurrences of $y$ in the body have this coefficient:
\[
\exists y. \ \ 0 < - 10w + \bunder{30y} + 10 \land 
               0 < - \bunder{30y} + 15 z + 90 \land 
               24 \mid \bunder{30y} + 6
\]
Now we are quantifying over $y$ and using $30y$ everywhere. 

Let $x$ denote $30y$.

It is \textbf{not an arbitrary} $x$. It is divisible by $30$.
\[
\exists x. \ \
0 < - 10w + x + 10 \land\ 0 < - x + 15 z + 90 \ \land\ 24 \mid x + 6\ \land\ 
30 \mid x
\]
\end{frame}

\begin{frame}
\frametitle{Exposing the Variable to Eliminate in General}

Eliminating $y$ from conjunction $F(y)$ of literals:
\begin{itemize}
\item $0 < t$ 
\item $K \mid t$ 
\end{itemize}
where $t$ is a linear term.  
To eliminate $\exists y$ from such conjunction, we wish to ensure that the coefficient next to $y$ is one or minus one. 

Observation: 
\begin{itemize}
\item $0 < t$ is equivalent to $0 < c\, t$
\item $K \mid t$ is equivalent to $c\, K \mid c\, t$ 
\end{itemize}
for $c$ a positive integer. 

Let $K_1,\ldots,K_n$ be all coefficients next to $y$ in the formula.

Let $M$ be a positive integer such that $K_i \mid M$ for all $i$, $1 \le i \le n$
\begin{itemize}
\item for example, let $M$ be the \textbf{least common multiple}
\[
    M = lcm(K_1,\ldots,K_n)
\]
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Ensuring Coefficient One}

Multiply each literal where $y$ occurs in subterm $K_i y$ by constant $M/|K_i|$
\begin{itemize}
\item the point is, $M$ is divisible by $|K_i|$ by construction
\end{itemize}

What is the coefficient next to $y$ in the resulting formula? 

\pause
\centerline{$M$ or $-M$}

\ \\

\pause
We obtain a formula of the form $\exists y. F(M \cdot y)$.  

Letting $x=My$, we conclude the formula is equivalent to 
\[
   \exists x.\ F(x) \land (M \mid x)
\]

What is the coefficient next to $y$ in the resulting formula? 

\pause
\centerline{$1$ or $-1$}
\end{frame}

% ======== from qe2

\begin{frame}
\frametitle{Exposing the Variable to Eliminate: Example}
\[
    \exists y.\ \  0 <  -w + \bunder{3y} + 1 \ \ \land \ \  
                   0 < - \bunder{2y} + z + 6 \ \land \ 4 \mid \bunder{5y} + 1
\]
Least common multiple of coefficients next to $y$, $M = lcm(3, 2, 5) = 30$

Make all occurrences of $y$ in the body have this coefficient:
\[
\exists y. \ \ 0 < - 10w + \bunder{30y} + 10 \land 
               0 < - \bunder{30y} + 15 z + 90 \land 
               24 \mid \bunder{30y} + 6
\]
Now we are quantifying over $y$ and using $30y$ everywhere. 

Let $x$ denote $30y$.

It is \textbf{not an arbitrary} $x$. It is divisible by $30$.
\[
\exists x. \ \
0 < - 10w + x + 10 \land\ 0 < - x + 15 z + 90 \ \land\ 24 \mid x + 6\ \land\ 
30 \mid x
\]
\end{frame}

\begin{frame}
\frametitle{ Lower and upper bounds:}
Consider the coefficient next to $x$ in $0 < t$.  If it is $-1$, move the term to left side. If it is $1$, move the remaining terms to the left side.  We obtain formula $F_1(x)$ of the form
$$
   \bigwedge_{i=1}^L a_i <  x \land
   \bigwedge_{j=1}^U x < b_j \land
   \bigwedge_{i=1}^D K_i \mid (x + t_i)
   $$

   \pause
If there are no divisibility constraints ($D=0$), what is the formula equivalent to?

\pause
$$
    \max_i a_i + 1 \le \min_j b_j - 1 \text{  which is equivalent to  }    \bigwedge_{ij} a_i + 1 < b_j
$$
\end{frame}

\begin{frame}
\frametitle{Replacing variable by test terms}
There is a an alternative way to express the above condition by replacing $F_1(x)$ with $\bigvee_k F_1(t_k)$ where $t_k$ do not contain $x$.  This is a common technique in quantifier elimination. Note that if $F_1(t_k)$ holds then certainly $\exists x. F_1(x)$.

What are example terms $t_i$ when $D=0$ and $L > 0$?  Hint: ensure that at least one of them evaluates to $\max a_i + 1$.

$$
   \bigvee_{k=1}^L F_1(a_k + 1)
$$

What if $D > 0$ i.e. we have additional divisibility constraints?
$$
   \bigvee_{k=1}^L \bigvee_{i=1}^N F_1(a_k + i)
$$

What is $N$? \pause least common multiple of $K_1,\ldots,K_D$

\pause
Correctness: note that if $F_1(u)$ holds then also $F_1(u-N)$ holds. 
\end{frame}

\begin{frame}
\frametitle{Back to Example}

\[
\exists x.\  -10 + 10w < x\ \land\ x < 90 + 15 z\ \land\ 24 \mid x + 6\ \land\ 30 \mid x
\]
%\[
% \bigvee_{i=1}^{120} 10w - 10  + i < 90 + 15 z \land 10w - 10 < 10w - 10 + i \land 24 %\mid 10w - 10 + i + 6 \land 30 | 10w - 10  + i
%\]

\

\

\pause
\[
 \bigvee_{i=1}^{120}\ 10w + i < 100 + 15 z\ \land\ 24 \mid 10w - 4 + i\ \land\ 30 \mid 10w - 10 + i
\]
\end{frame}

\begin{frame}
\frametitle{No lower bounds}
Now consider the case $L=0$. We cannot try all lower bounds, as there are none:
$$
   \bigwedge_{j=1}^U x < b_j \land
   \bigwedge_{i=1}^D K_i \mid (x + t_i)
   $$

\pause
We first drop all constraints except divisibility, obtaining $F_2(x)$:
$$
   \bigwedge_{i=1}^D K_i \mid (x + t_i)
$$
and then eliminate quantifier as
$$
   \bigvee_{i=1}^N F_2(i)
   $$

Exercise: prove equivalence of this result with $\exists x. F_1(x)$ in this case.
\end{frame}

\begin{frame}
\frametitle{An Example with No Lower Bounds}

Eliminate quantifier from this formula:
\[
\exists x.\  x < 5 + 7 z\ \land\ 2 \mid x\ \land\ 3 \mid x{+}2 
\]
\vspace*{5cm}
\end{frame}

%% \begin{frame}
%% \frametitle{Another Example with No Lower Bounds}

%% Eliminate quantifier from this formula:
%% \[
%% \exists x.\  x < 5 + 7 z\ \land\ 2 \mid x\ \land\ 3 \mid x{+}2\ \land\ 6 \mid x{+}1
%% \]
%% \vspace*{5cm}
%% \end{frame}

\begin{frame}
\frametitle{Wrap Up}

This completes the description of a quantifier elimination algorithm for 
Presburger Arithmetic (PA).

\pause

This algorithm and its correctness prove that:
\begin{itemize}
\item PA admits quantifier elimination
\item Satisfiability, validity, entailment, equivalence of PA formulas is decidable \\
We can use the algorithm to prove verification conditions. \\
Even if not the most efficient way, it gives us insights on which we
can later build to come up with better algorithms.
\item Quantified and quantifier-free formulas have the same expressive power
\end{itemize}
%Also implies that Presburger arithmetic has quantifier-free interpolants.

\end{frame}

%% \begin{frame}
%% \frametitle{Eliminate Quantifiers: Example}

%% \[
%%      \exists y. \exists x.\ \ x < -2 \wedge 1 - 5y < x \wedge 1 + y < 13x
%% \]
%% \vspace*{7cm}

%% \end{frame}


%% \begin{frame}
%% \frametitle{Check whether the formula is satisfiable}
%% \[
%%      x < y + 2\ \land\ y < x + 1 \land x = 3k \land (y = 6p+1 \lor y = 6p-1)
%% \]
%% \vspace*{7cm}
%% \end{frame}

%% \begin{frame}
%% \frametitle{Apply quantifier elimination}

%% \[
%%   \exists x.\ \ (3x + 1 < 10 \lor 7x - 6 < 7)\ \land\ 2 \mid x
%% \]
%% \vspace*{7cm}

%% \end{frame}

\begin{frame}
\frametitle{Approaches to Making QE for PA More Efficient in Practice}

Avoid transforming to conjunctions of literals: work directly on negation-normal form. The technique is similar to what we described for conjunctive normal form.
\begin{itemize}
\item[+] no need for DNF
\item[-] we may end up trying irrelevant bounds
\end{itemize}
This is the Cooper's algorithm:
 \begin{itemize}
\item  Reddy, Loveland: Presburger Arithmetic with Bounded Quantifier Alternation. (Gives a slight improvement of the original Cooper's algorithm.)
  \item Section 7.2 of the Calculus of Computation Textbook
\end{itemize}

An alternative direction for improvement: handle a system of
equalities more efficiently, without introducing
inequalities and divisibility constraints too eagerly, using
Euclid's GCD algorithm for solving linear Diophantine
equations. \\
(Hermite normal form of a matrix.)

Weak quantifier elimination: only eliminate alternations of quantifiers.
 
\end{frame}

%% \begin{frame}
%% \frametitle{}


%% \ \\

%% Hermite normal form of an integer matrix.
%% \end{frame}

%% \begin{frame}
%% \frametitle{Eliminate variables x and y}
%% \[
%%     5x + 7y = a \land x \le y \land 0 \le x
%% \]
%% \vspace*{7cm}
%% \end{frame}

 \begin{frame}
   \frametitle{Complexity of Deciding Quantified PA Formulas}

   Regardless how we proceed, we cannot escape inherent computational complexity
   of deciding if quantified Presburger arithmetic formula is true, which has been characterized
   using alternating complexity classes by Berman.

   \

   \pause
   A set $A$ is in $STA(s(n),t(n),a(n))$ iff there exists a single-tape \emph{alternating} Turing machine $M_i$
   (making $\land$ as well as $\lor$ choices)
   that accepts $A$ and runs within space $s(n)$, time $t(n)$ and performs at most $a(n)$ alternations between
   $\land$ and $\lor$ choices.

   \

   Deciding of a PA formula of size $n$ with $m$ quantifiers is in
   \[ 
       STA(*,2^{n^{O(m)}},m)
   \]
   Complexity is particularly sensitive to $m$.
 \end{frame}
