z3 - Create an array with fixed size and initialize it

Question

I'm going to create an array with fixed size and initialize it with some values.

For example, the following C++ code:

a[0] = 10;
a[1] = 23;
a[2] = 27;
a[3] = 12;
a[4] = 19;
a[5] = 31;
a[6] = 41;
a[7] = 7;

Are there some utilities in Z3 to model it?

Answer 1

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