How to use z3 BitVec or Int as an array index?

Question

I want to use a Int vector as an array index.

python.

array = [12,45,66,34]
s= Solver()
x = Int('x')
s.add(array[x] == 66)

so the x should be 2..

how can i do it?

Schopenhauerism

Answer 1

Here's one way to do it:

from z3 import *

s = Solver ()

array = [12, 45, 66, 34]

A = Array ('A', IntSort(), IntSort())
i = 0
for elem in array:
  A = Store(A, i, elem)
  i = i + 1

x = Int ('x')
s.add(x >= 0)
s.add(x < len(array))
s.add(Select(A, x) == 66)

if s.check() == sat:
  print s.model()
else:
  print "Not found!"

This prints:

$ python a.py
[x = 2]

Griffis

Why did you add the x >= 0 and x < len(array) constraints. I thought Select only chooses from that range anyway? – Kingsize

@Kingsize That is not true. Select will operate over the entire domain, i.e., all integer values. Z3 arrays have no notion of lower/upper bounds. You can easily see that by removing those constraints and observing what Z3 does. – Griffis

Answer 2

It is not possible to access integer array element with Z3 ArithRef variables. I suppose, the specified problem is looking for an element in an integer array (index) through Z3 solver.

Another possible way of doing it might be:

array = [12, 45, 66, 34]
x = Int('x')

s= Solver()

for i in range(len(array)):
    s.add(Implies(array[i] == 66, x == i)) 

if s.check() == sat:
    print(s.model())

Nothingness