Definition von Array-Formeln

(nach Kroening/Strichman Kap. 7.3)

wir betrachten boolesche Kombinationen in negationstechnischer Normalform (NNF)

von Formeln der Gestalt ∀i₁,…, i_k : (I⇒V), mathend000# wobei

• I mathend000# (index guard): boolesche Kombination von linearen Gln. und Ungln. über i₁,…, i_k mathend000#,
• V mathend000# (value constraint): boolesche Komb. von Gleichheitsconstraints für Array-Elemente.

  Index-Ausdrücke in select und store ∈{i₁,…, i_k} mathend000# .

NNF: ∧/∨ mathend000# beliebig, ¬ mathend000# nur ganz unten, keine anderen Operatoren.