0

My first question is whether I can express the following formula in Z3Py:

Exists i::Integer s.t. (0<=i<|arr|) & (avg(arr)+t<arr[i])

This means: whether there is a position i::0<i<|arr| in the array whose value a[i] is greater than the average of the array avg(arr) plus a given threshold t.

I know this kind of expressions can be queried in Dafny and (since Dafny uses Z3 below) I guess this can be done in Z3Py.

My second question is: how expressive is the decidable fragment involving arrays in Z3? I read this paper on how the full theory of arrays is not decidable (http://theory.stanford.edu/~arbrad/papers/arrays.pdf), but only a concrete fragment, the array property fragment.

Is there any interesting paper/tutorial on what can and cannot be done with arrays+quantifiers+functions in Z3?

Theo Deep
  • 666
  • 4
  • 15

1 Answers1

1

You found the best paper to read regarding reasoning with Array's, so I doubt there's a better resource or a tutorial out there for you.

I think the sequence logic (not yet officially supported by SMTLib, but z3 supports it), is the right logic to use for reasoning about these sorts of problems, see: https://microsoft.github.io/z3guide/docs/theories/Sequences/

Having said that, most properties about arrays/sequences of "arbitrary size" require inductive proofs. This is because most interesting functions on them are essentially recursive (or iterative), and induction is the only way to prove properties for such programs. While SMT solvers improved significantly regarding support for recursive definitions and induction, they still don't perform anywhere near well compared to a traditional theorem prover. (This is, of course, to be expected.)

I'd recommend looking at the sequence logic, and playing around with recursive definitions. You might get some mileage out of that, though don't expect proofs for anything that require induction, especially if the inductive-hypothesis needs some clever invariant to be specified.

Note that if you know the length of your array concretely (i.e., 10, 15, or some other hopefully not too large a number), then it's best to allocate the elements symbolically yourself, and not use arrays/sequences at all. (And you can repeat your proof for lenghts 0, 1, 2, .. upto some fixed number.) But if you want proofs that work for arbitrary lengths, your best bet is to use sequences in z3, not arrays; with all the caveats I mentioned above.

alias
  • 28,120
  • 2
  • 23
  • 40
  • Thanks a lot! Yes, I am referring to "arbitrary size: the whole time, sorry. I still have a doubt: which is the difference between sequence and array? More concretely: how do results of the paper of Manna/Pnueli affect reasoning of sequences? Is the decidable fragment of sequences "wider" than the one in arrays? In that case, I really should understand their differences :) Also, I do not fully understand about proofs: is the proof of the example too difficult for a solver to give us a model? – Theo Deep Sep 20 '22 at 15:47
  • 1
    An array is indexed by its entire domain. i.e., if you have an array in SMTLib that is indexed by integers, then every integer (including negative ones!) can be used to index it. A sequence, however, is like an array in a regular programming language. It's always indexed by numbers, starting from 0 to some fixed (but arbitrary) length. The length itself can, of course, be constrained by asserting properties on it. (Like you can say "odd length," "length at most 20," or "length exactly 10." Of course, in the last case, it's better to use symbolic elements directly instead of a sequence.) – alias Sep 20 '22 at 15:59
  • Thanks again: I understand arrays are kind of really "free" functions, where sequences are made with the idea to be similar to "classic programming arrays". Anyway, I think I still miss some points, so made a new question (as you once suggested) at: https://stackoverflow.com/questions/73789804/theory-of-arrays-in-z3-1-model-is-difficult-to-understand-2-do-not-know-ho – Theo Deep Sep 20 '22 at 16:24