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

Answer 2

I concur to Leonardo's answer, especially that Arrays are designed to model LARGE input ranges. There is not really a way to define fixed size Arrays (unless you use a finite input sort such as BitVecSort(3)).

Since the Z3Py (Python) example was taken down i wanted to add my own solution. This function specifies a range of array entries, beginning at a starting address. (Assertions are stored in a Solver object.)

def assert_array(solver, array, start_index, data):
    for offset in range(len(data)):
        solver.add(array[start_index + offset] == data[offset])

Note that array[idx] is the Z3Py equivalent of (select array idx) in SMT 2.0. The array in the question could be modeled like this:

s = Solver()
a = Array('a', IntSort(), IntSort())
data = [10, 23, 27, 12, 19, 31, 41, 7]
assert_array(s, a, 0, data)

print s
#[a[0] == 10,
# a[1] == 23,
# a[2] == 27,
# a[3] == 12,
# a[4] == 19,
# a[5] == 31,
# a[6] == 41,
# a[7] == 7]