Show description

Replacing the previous conjunction by its image by Δ yields a schema that is actually identical to the first one. Hence the procedure stops (no further schema is generated) and we get Eρ∗ ◦unfold (φ) = {φ}. By Theorem 2, the T -satisfiability of φ is thus equivalent to the one of φ{n ← 0} which can be easily tested by any SMT-solver. Example 6. Consider the algorithm below, counting the number of occurrences o of an element e in an array t. We want to check that if the final value of o is 1 then the formula ∀i, j, ai ≈ e ∧ aj ≈ e ⇒ i ≈ j holds.

If u and v occur in θ(a), then the considered schema will possibly contain a conjunction of the form an+2 ≈ u∧an+2 ≈ v. 2, the symbol an+2 will have to be eliminated (since it is non-n-elementary) by applying an appropriate function Δ. But to this purpose, one necessarily has to ensure that the equation u ≈ v holds. The existence of the function τ guarantees that this property can be expressed as an n-elementary schema. 3. Schemata of SMT-Problems 39 Definition 9. Let L be the set of literals λ satisfying one of the following conditions: - λ is of the form u v 5 , where each of the u, v is either a non-indexed term or of the form aα where a ∈ C and α ∈ {n, n + 1, n + 2, i, i + 1}.

A ∧ a ≈ a ∧ · · · ∧ a i i i i ≈ ai+1 i+1 i=0 - Additional parameters. Inequalities of the form i ≤ m where m is an additional parameter interpreted as an element of [0, n] can be encoded by atoms n ≤m ≤m ≤m ≤m p≤m i defined by the following axioms: ¬pn+1 ∧ p0 ∧ i=0 (pi+1 ⇒ pi ). Then n ≤m ≤m i ≈ m can be defined using i=0 (p=m i ⇔ pi ∧ ¬pi+1 ) and a disequality m ≈ k n =k can be tested by the schema: i=0 (¬p=m i ∨ ¬pi ). - Using the parameter in iteration bodies. A term of the form an can be replaced by a fresh non-indexed constant b, with the axiom: b ≈ an .