====== Deciding Boolean Algebra with Presburger Arithmetic ======

===== Motivation =====

{{sav08:bapa-example.png|BAPA Program Example}}

{{sav08:bapa-htriple.png|BAPA Hoare Triple}}

{{sav08:bapa-vc.png|BAPA Verification Condition}}

===== Definition of BAPA =====

See [[http://lara.epfl.ch/~kuncak/papers/KuncakETAL06DecidingBooleanAlgebraPresburgerArithmetic.pdf|Figure 3 on page 5 of the paper]] and compare to its special cases: BA and PA.

\begin{equation*}
\begin{array}{rcl}
      F & ::= & A \mid F_1 \land F_2 \mid F_1 \lor F_2 \mid \lnot F \mid 
                \exists x.F \mid \forall x.F \mid
                \exists k.F \mid \forall k.F \\
      A & ::= & B_1 = B_2 \mid B_1 \subseteq B_2 \mid 
               T_1 = T_2 \mid T_1 < T_2 \mid (K{|}T) \\
      B & ::= & x \mid \mathbf{0} \mid \mathbf{1}
                \mid B_1 \cup B_2 \mid B_1 \cap B_2 \mid B^{c} \\
      T & ::= & k \mid K \mid maxc \mid T_1 + T_2 \mid K \cdot T \mid \ \q{|} B \q{|} \\
      K & ::= & \ldots {-2} \mid -1 \mid 0 \mid 1 \mid 2 \ldots
    \end{array}
\end{equation*}

Semantics: we consider the theory of models where integers are interpreted as integers and sets are interpreted as subsets of some finite set.  For each finite set we have one interpretation.  (If we prove a valid formula, it will hold for arbitrarily large finite universes.)  $\mathbf{0},\mathbf{1}$ are empty and universal set.  We interpret constant $maxc$ as $|\mathbf{1}|$.













===== Example =====

Eliminate the quantifier $X$ from the following formula:
\begin{equation*}
\exists X. A \subseteq X \land X \cup B = B \land |X \cap A| = 2 |A| + 1
\end{equation*}

++++ |
\begin{equation*}
A \subseteq X \Rightarrow |A \cap X^c| = 0
\end{equation*}
\begin{equation*}
X \cup B = B \Rightarrow |(X \cup B) \cap B^c| = 0 \land |B \cap (X \cup B)^c| = 0
\end{equation*}
The starting point after transformation to cardinality constraints is: \\
<latex>
k_1 = |A| \land \\
k_2 = |X \cap A| \land \\
k_3 = |A \cap X^c| \land \\
k_4 = |(X \cup B) \cap B^c| \land \\
k_5 = |B \cap (X \cup B)^c| \land \\
k_2 = 2 k_1 + 1 \land 
k_3 = 0 \land 
k_4 = 0 \land 
k_5 = 0
</latex>

++++

===== Simplifying Atomic Formulas =====

For sets $x,y$:

$x = y$ becomes $x \subseteq y\ \land\ y \subseteq x$

$x \subseteq y$ becomes $|x \cap y^c|=0$

Result: all set variables and operators occur within $|b|$ formula where $b$ is expression built from set variables, $\mathbf{0},\mathbf{1},\cap,\cup,\_^c$.

Transform $b$ into union of disjoint Venn regions.  Let $s_1,\ldots,s_m$ be all set variables.  Venn regions are connected regions in the Venn diagram, and are analogous to conjunctive normal form:
\begin{equation*}
    \bigcup_{i=1}^m x_i^{\alpha_i}
\end{equation*}
where $x^\alpha$ is either $x$ or $x^c$ (complement of $x$).

Now observe that each set expression $b$ is a disjoint union of certain Venn regions.  It is union of precisely those regions that belong to disjunctive normal form of the corresponding propositional formula.

Then use
\begin{equation*}
   |b| = |s_{i_1}| + \ldots + |s_{i_k}|
\end{equation*}
We therefore assume that the only occurence of sets and set operators is within $|s|$ where $s$ is a Venn region.


===== Separating BA and PA Part =====

Transform formula to prenex form
\begin{equation*}
   Q_p v_p. \dots Q_1 v_1. G_1(|s_1|,\ldots,|s_n|)
\end{equation*}
where $F$ is quantifier-free.

For each expression $|s_i|$ in $G_1(|s_1|,\ldots,|s_n|)$ introduce a fresh variable $l_i$ that denotes the value $|s_i|$.  We obtain
\begin{equation*}
      Q_p v_p. \dots Q_1 v_1. \exists^+ l_1.\ldots \exists l_q. \left(\bigwedge_{i=1}^q |s_i|=l_i \right)\ \land\ G_1(l_1,\ldots,l_q)
\end{equation*}
Note that $G_1(l_1,\ldots,l_q)$ is a quantifier-free PA formula.  

Here $\exists^+ l.F$ denotes $\exists l. 0 \le l \land F$.

We will eliminate integer and set quantifiers from the entire subformula $Q_p v_p. \dots Q_1 v_1$
\begin{equation*}
\exists^+ l_1.\ldots \exists l_q. \left(\bigwedge_{i=1}^q |s_i|=l_i \right)\ \land\ G_1(l_1,\ldots,l_q)
\end{equation*}
Indeed, we can always transform this formula to a quantifier-free formula by substituting $|s_i|$ back into $G_1$.

In which parts of this formula do we find variables $v_p,\ldots,v_1$ that we wish to eliminate
  * integer variables? ++ | in $G_1(l_1,\ldots,l_q)$ ++
  * set variables? ++ | in $\displaystyle\bigwedge_{i=1}^q |s_i|=l_i$ ++

===== Eliminating Quantifiers =====

==== Eliminating Integer Existential ====


==== Eliminating Set Existential ====

**Lemma:**
Let $B_1, B_2$ be two finite disjoint sets and $L_1,L_2,K_1,K_2$ non-negative integers.  Then the following two conditions are equivalent:
  * there exists a finite set $A$ such that: $|B_1 \cap A|=L_1$, $|B_1 \setminus A|=K_1$, $|B_2 \cap A|=L_2$, and $|B_2 \setminus A|=K_2$;
  * $|B_1|=L_1+K_1$ and $|B_2|=L_2+K_2$.

==== Eliminating Universals ====

Express them using negation and existentials.