\begin{slide}{Definition von Array-Formeln}

(nach Kroening/Strichman Kap. 7.3)

wir betrachten boolesche Kombinationen
in negationstechnischer Normalform (NNF)

von Formeln der Gestalt
\( \forall i_1, \ldots, i_k: (I \Rightarrow V), \)
wobei 
\begin{itemize}
\item $I$ (index guard): boolesche Kombination
  von linearen Gln. und Ungln. über $i_1,\ldots,i_k$,
\item $V$ (value constraint): boolesche Komb.
  von Gleichheitsconstraints für Array-Elemente.

  Index-Ausdrücke in select und store 
  $\in\{i_1,\ldots,i_k\}$ .
\end{itemize}
NNF: $\wedge/\vee$ beliebig, $\neg$ nur ganz unten,
keine anderen Operatoren.


\end{slide}

\begin{slide}{Vereinfachung von Array-Formeln:}

  \begin{itemize} \itemsep 0pt \parskip 2pt
  \item $\store$ entfernen:

ersetze  $\store(a,i,e)$ durch $a'$ und füge Constraints hinzu:

$\select(a',i)=e \wedge 
(\forall j: j\neq i \rightarrow
\select(a',j)=\select(a',j))$.

\item ersetze $\neg\forall j:P(j)$ 
durch $\neg P(z)$ mit neuer Variablen $z$

\item ersetze $\forall j: P(j)$ 
durch  $\bigwedge_{j \in J} P(j)$

mit $J=$ alle vorkommenden Index-Ausdrücke
(ohne die quantifizierten Variablen)
\item $\select$ entfernen: 
ersetze $\select(a,i)$ durch $f_a(i)$

  \end{itemize}




Für Startformel $F$ der Array-Logik in NNF:

Verfahren erzeugt
erfüllbarkeitsäquivalente Formel $F'$ 

mit Index-Prädikaten und uninterpretierten Funktionen.

$\Rightarrow$ Betrachtung von Theorie-Kombinationen
\end{slide}
