CODEWITHSUNDEEP
z3z3py
Rohac
Rohac

Reputation: 31

How to declare/use Arrays and Quantifiers in Z3Py?

I'm new to Z3py and I found an exercise where it would ask to check if some verification conditions were true. Up to this moment, the exercises I've done were basically to transform simple propositional formulas into z3py clauses, something like:

Propositional Formula would be:

(n>=4) -> (x = y +2)

Which would become in Z3Py:

n, x, y = Ints('n x y')

s.add(Implies(n>=5, x == y+3))

The conditions I'm presented now, introduce Arrays and Quantifiers and after spending hours trying to figure it out on the documentation around, I'm still not able to get it properly done.

For example, how would I do the same process above but with the following conditions:

n ≥ 1 ∧ i = 1 ∧ m = A[0]
i <= n ∧ ∀j. 0 ≤ j < i → m ≥ A[j]

A little snippet of what I think that is correctly done:

i, n = Ints('i n')

s.add(And(n>=1, i == 1, ???)
s.add(And(i<=n,Implies(???))

How should I replace the ??? so that the conditions would be correctly transformed into Z3Py?

Solution:

- The constraint

n ≥ 1 ∧ i = 1 ∧ m = A[0]

would become in Z3Py:

A = Array('A', IntSort(), IntSort()) //Array declaration
i, n, m, j = Ints('i n m j') //Ints declaration for both constraints

And(n>=1, i==1, m==A[0])

- The constraint

i <= n ∧ ∀j. 0 ≤ j < i → m ≥ A[j]

would become:

And(i<=n,ForAll(j,Implies(And(j>=0,j<i),m>=A[j])))

Upvotes: 0

Views: 91

Answers (1)

alias
alias

Reputation: 30428

Your questions is quite ambiguous. Note that you've the constraints:

n ≥ 1 ∧ i = 1

and then

i <= n

but that consequent is already implied by the first, and hence is redundant. Meaning, if you add them both to the solver like you did with your s.add lines, then it won't really mean much of anything at all.

I'm guessing these two lines actually arise in different "subparts" of the problem, i.e., they aren't used together for the same verification goal. And, making an educated guess, you're trying to say something about the maximum element of an array; where i is some sort of a loop-counter. The first line is what happens before the loop starts, and the second is the invariant the loop-body ensures. If this is the case, you should be explicit about that.

Assuming this is the case, then these sorts of problems are usually modeled on the "body" of that loop, i.e., you need to show us exactly what sort of a "program" you're dealing with. That is, these constraints will only make sense in the presence of some sort of a transformation of your program variables.

Upvotes: 0

Related Questions