Create an array with fixed size and initialize it

z3

Solution

Z3 supports the array theory, but is usually used to encode unbounded arrays, or arrays that are very big. By big, I mean the number of array accesses (i.e., selects) in your formula is much smaller than the actual size of the array. We should ask ourselves : "do we really need arrays for modeling/solving problem X?". For fixed size arrays like in your example, we can use a different variable for every array position. Example: `a0` for `a[0]`, `a1` for `a[1]`, etc. Of course, if we do not use theories, then encoding an array access such as `a[i]` must be encoded as a big if-then-else term such as

`(ite (= i 0) a0 (ite (= i 1) a1 ...))`

If the array size is known and small, then this is usually the most efficient approach for encoding a problem.

On the other hand, if you decide to use the array theory, you can encode the initialization in your question as:

(declare-const a (Array Int Int))
(assert (= (select a 0) 10))
...
(assert (= (select a 7) 7))

Here is the whole example encoded in SMT 2.0 format:

http://rise4fun.com/Z3/iwo

Note that to encode an update on this array. For example, the C statement `a[3] = 5`, we must create a new array variable representing the array after this assignment. The most compact way uses the `store` expression:

(declare-const a1 (Array Int Int))
(assert (= a1 (store a 3 5)))

Here is the full example with the update.

http://rise4fun.com/Z3/Kpln

You may also consider the Python/C++/.Net APIs. They allow us to encode examples like yours in a much more compact way. The idea is to implement functions that encode commonly used patterns such as array initialization. Here is your array initialization example in Python:

http://rise4fun.com/Z3Py/AAD

Problem

Original source