-
Notifications
You must be signed in to change notification settings - Fork 41
Partial Quantifier Elimination for the Theory of Arrays
Ex 1.1: Download and run an SMT solver, e.g., Z3 https://github.com/Z3Prover/z3
In principle you could also use the webinterface of the Z3 SMT solver, 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.
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?
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.
∃x. y = x /\ x = 7∀x. y != x \/ x != 7∃x. y <= x /\ x <= 42 /\ 3 <= x /\ x <= z∀x. y > x \/ x > 42 \/ 3 > x \/ x > z∃x. x >= y /\ x >= 42∀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.
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
- Wikipedia:Predicate transformer semantics
- 2017FSE - Dietsch,Heizmann,Musa,Nutz,Podelski - Craig vs. Newton in Software Model Checking sp is defined on p. 489 left, wp is defined on p. 490 right, in the figures you can find some examples
- Cheat sheet of program semantics TODO
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)
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.
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.)
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.
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
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 quantifiers
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.
Sol 7.5 ∀x. (x≠i ⇒ a1[x]=a2[x]) ∧ a1[i]=v)
Note that this transformation is simple but this transformation also introduces major problems.
The variable x is universally quantified, but the resulting formula does not allow us to apply DER.
In one of the next steps, we will eliminate the select terms and hence introduce a ∀∃ quantifier alternation.
The quantified index itself is typically not amenable to the "index equality optimization" and the quantifier alternation will increase the costs for index comparisons. If we fail to eliminate the inner quantifier we will most likely also fail to eliminate the outer quantifier. If the inner formula contains more array variables that have to be eliminated, we will probably introduce more quantifier eliminations in further steps.
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.
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.
Ex 8.1 Which of the following equivalences are correct?
-
∃x. (φ1(x) ∨ φ2(x)) =(∃x. φ1(x)) ∨ (∃x. φ2(x))` -
∃x. (φ1(x) ∧ φ2(x)) =(∃x. φ1(x)) ∧ (∃x. φ2(x))` -
∀x. (φ1(x) ∨ φ2(x)) =(∀x. φ1(x)) ∨ (∀x. φ2(x))` -
∀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.
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.
In Ultimate, we often have to deal with multi-dimensional arrays because we model the memory that can be accessed by a computer program as a 2-dimensional array.
SMT-LIB does not support multi-dimensional arrays directly, however multi-dimensional arrays can be represented by nested arrays via currying.
E.g., an 2-dimensional array whose indices both have type int are represented by an array whose sort is (Array Int (Array Int Int)).
An example of a read operation from a 2-dimensional array is: (select (select a) 7) 10)
An example of a write operation to a 2-dimensional array is: (store a (store (select a) 8 23)))
Difficulties for quantifier elimination: While applying the rule for eliminating all select terms, we introduce quantified variables whose sort is the same sort as the range sort of the array. Hence, while eliminating one array that has dimension n+1 we typically introduce many quantified arrays of dimension n that also have to be eliminated.
Ex 9.1 Apply your elimination procedure to the example Congo which is listed below.
∃a0. a0[7]=42 ∧ a0[k]=23 ∧ a=store(a0,2,1337)
where a and a0 have sort (Array Int Int) and k has sort Int
∃a0. a0[k]=42 ∧ a0[i]=23
where k and i have sort Int and a0 has sort (Array Int Int)
∃â. a1=store(â,k,v) ∧ a2=store(â,k,v) ∧ a1≠a2
where a1 and a2 have sort (Array Int Int) and k has sort Int
∃â. a1=store(â,k,v) ∧ a2=store(â,i,v) ∧ a1≠a2
∃â. (and (= (select (select â 5) 7) 10) (= a (store â 7 (store (select â 7) 8 23))))
where a and the existentially quantified â both have sort (Array Int (Array Int Int))
- Home
- Ultimate Development
- Ultimate Build System
- Documentation
- Project Topics