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
与恶龙缠斗过久,自身亦成为恶龙;凝视深渊过久,深渊将回以凝视…