Skip to content

Partial Quantifier Elimination for the Theory of Arrays

Jump to bottom
Matthias Heizmann edited this page Jan 8, 2019 · 44 revisions

Introduction to the Topic

1. Getting familiar with SMT-LIB

Ex 1.1: Download and run an SMT solver, e.g., Z3 https://github.com/Z3Prover/z3

In principle you could also use the web interface of Z3, but I presume it is more convenient to have something that runs on your machine.

Ex 1.2 Write a bunch of SMT scripts that contain the check-sat command. Writing SMT scripts is not easy. Start with the scripts from the Z3 web interface and modify them. Use some formulas from you logics lecture. Use the get-model or the get-value command to get a satisfying assignment. Note that you will not get a response if your formulas become difficult. Formulas with quantifiers are typically difficult.

2. Getting familiar with the theory of arrays

Ex 2.1 Write a bunch of SMT scripts that use the theory of arrays. This means the scripts should contain "select" or "store" function symbols.

Ex 2.2 I think the following two facts are confusing.

  • Arrays are often infinite. As soon as the Sort of the index is infinite the array has an infinite number of entries.
  • Arrays are immutable. A "store" does not modify an array, it returns a new array. In fact, I think it is questionable if "array" is the best name for this theory. Alternatively, one could have called it the theory of maps. Use a quantifier to define an array that represents the function a_1(x)=x+1. Use a quantifier to define an array that represents the function a_2(x)=2*x. Define constant c and assert the formula a_1(c)=a_2(c). Is the SMT solver able to find a satisfying assignment for c?

3. Quantifier elimination

Quantifier elimination is the task of finding a quantifier-free formula that is logically equivalent to a given formula.

Ex 3.1 Find quantifier-free formulas that are equivalent to the following formulas. For simplicity let us interpret them over the theory of reals.

  1. ∃x. y = x /\ x = 7
  2. ∀x. y != x \/ x != 7
  3. ∃x. y <= x /\ x <= 42 /\ 3 <= x /\ x <= z
  4. ∀x. y > x \/ x > 42 \/ 3 > x \/ x > z
  5. ∃x. x >= y /\ x >= 42
  6. ∀x. x < y /\ x < 42

Ex 3.2 Use an SMT solver to check if your results from the preceding exercise are correct. Let f be the input from the preceding exercise and let f_r be your result. State a formula that is unsatisfiable iff your result f_r is equivalent to f. Try to check the results using the SMT solver. Note that the SMT solver may sometimes return unknown because the formulas are too difficult.

Ex 3.3 How did you eliminate the quantifiers? Try to find some rule for elimination.

4. Predicate transformers

In this section we consider the main applications of quantifier elimination in Ultimate: the strongest post predicate transformer sp (or sometimes written post) and the weakest precondition predicate transformer wp

Ex 4.0 Get familiar with these predicate transformers.

Literature

Ex 4.1 Apply sp and wp iteratively to the each of the following sequences of statements. For sp: start with the predicate true and apply sp from the beginning of the sequence to the end. For wp: start with the predicate false and apply wp from the end of the sequence to the beginning of the sequence. Try to elimination quantifiers in predicates.

Sequence 4.1A z:= 1; assume x>=7; x := x+1; assume y >= x; havoc x; assume (y < 8 || z >= 5);

Sequence 4.1B a[z]:= 1; assume a[x]>=7; a[x] := a[x] + 1; assume a[y] >= a[x]; assume (a[y] < 8 || a[z] >= 5);

(x, y, z are integers, a is an array)

5. Formulas that define relations

Internally Ultimate does not use program statements (like assignment, assume, havoc..) instead we translate all statements into relations that are represented by SMT formulas over primed and unprimed variables.

(TODO find literature - maybe could be understood without)

Example: Assume a program has variables x, y, z, then x := x + 1 would be translated into the formula x'=x+1 /\ y'=y /\ z'=z

Ex 5.1 Translate some of the statements from Sequence 4.1A to formulas.

Ex 5.2 We can use relations/formulas to represent sequences of statements. Let us assume that formula φ1(x,x') represents statement st1 and that formula φ2(x,x') represents statement st2. How can we combine both formulas in order to obtain a formula that represents the sequence st1;st2. (Hint: quantifier and substitution)

Ex 5.2 Find a formula over primed and unprimed variables that does not represent any single statement but only a sequence of statements.

Ex 5.3 Define sp and wp for relations/formulas. Note that there is one single definition for each predicate transformer, we do not have to distinguish between different kinds of statements.

Ex 5.4 Translate some of the statements from Sequence 4.1B to formulas.

6. Quantifier elimination for arrays

Ex 6.1 How did you eliminate the quantifiers above if the quantified variable had an array type? Try to find some rule for elimination. (very difficult)

Ex 6.2 Assume we have a formula of the form ∃a. φ(a), where a is an array. Let us assume furthermore that a occurs in φ only two times. On occurrence is in a subformula (select a k1) the other occurrence is in a subformula (select a k2). Find a rule for eliminating the quantifier in this special case.

(This will become our main elimination rule. All other rules will only be extensions of this rule and/or combinations with the preprocessing steps discussed in the following section.)

7. Elimination of array operations

Elimination of array equalities and array disequalities.

Ex 7.1 Consider the formula (= a1 a2), where a1 and a2 are arrays whose indices are integers. Find a logically equivalent formula in which no equality of arrays occurs.

Hint: use quantifiers and introduce a new variable.

Ex 7.2 Consider the formula (not (= a1 a2)), where a1 and a2 are arrays whose indices are integers. Find a logically equivalent formula in which no equality of arrays occurs.

Elimination of select-over-store

Ex 7.3 Consider the formula φ(t) where t is (select (store a i1 v) i2). Find a formula that is equivalent to φ(t) but does not contain t.

Hint: not directly related to quantifirs

Elimination of store-over-store

Ex 7.4 Consider the formula φ(t) where t is (store (store a i1 v1) i2 v2). Find a formula that is equivalent to φ(t) but does not contain t.

Hint: not directly related to quantifirs

Elimination of store subformulas

Ex 7.5 Consider the formula (= a1 (store a2 i v)). Find a logically equivalent formula in which no store term occurs. Hint: use quantifiers and introduce a new variable.

Ex 7.6 Consider the formula φ(t) where t is (store a i v). Let us assume that φ does contain neither equalities of arrays nor store terms other than t. Find a formula that is equivalent to φ but neither contains store terms nor array equalities.

8. Distributivity

So far, we eliminated existential quantifiers only from conjunctions of atoms and we eliminated universal quantifiers only from disjunctions of atoms. In practice we will have to apply the elimination to arbitrary formulas.

Distributivity of ∃ and ∀ over ∧ and ∨

Ex 8.1 Which of the following equivalences are correct?

  1. ∃x. (φ1(x) ∨ φ2(x)) = (∃x. φ1(x)) ∨ (∃x. φ2(x))`
  2. ∃x. (φ1(x) ∧ φ2(x)) = (∃x. φ1(x)) ∧ (∃x. φ2(x))`
  3. ∀x. (φ1(x) ∨ φ2(x)) = (∀x. φ1(x)) ∨ (∀x. φ2(x))`
  4. ∀x. (φ1(x) ∧ φ2(x)) = (∀x. φ1(x)) ∧ (∀x. φ2(x))`

Give a counterexample for each equivalence that is not correct. For each equivalence that is correct: state an example of a quantified formula where could only apply DER after using this equivalence.

Distributivity of ∧ and ∨

Ex 8.2 We cannot directly apply the DER elimination rule to the following formula. ∃x. (φ(x) ∧ (x=1 ∨ x=2)) Use distributivity of ∧ and ∨ and apply DER afterwards.

99. Examples

Argentina

∃a0. a0[7]=42 ∧ a0[k]=23 ∧ a=store(a0,2,1337)

Finland

∃a0. a0[k]=42 ∧ a0[i]=23

Clone this wiki locally