Retrieving array from model in Z3Py

Question

I am aware that there is a similar question for Z3 C++ API, but I couldn't find corresponding information for Z3Py. I'm trying to retrieve arrays from models found by Z3, so that I can access the array's values using indexes. For instance, if I had

>>> b = Array('b', IntSort(), BitVecSort(8))
>>> s = Solver()
>>> s.add(b[0] == 0)
>>> s.check()
sat

then I'd like to do something like

>>> s.model()[b][0]
0

but I currently get :

>>> s.model()[b][0]
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
TypeError: 'FuncInterp' object does not support indexing

Judging from the C++ answer, it seems like I'd have to declare a new function using some values I got from the model, but I don't understand it well enough to adapt it to Z3Py myself.

Answer 1

You can ask the model to evaluate (eval(...)) the array at a particular point by constructing a call to the associated array model function. Here's an example:

b = Array('b', IntSort(), BitVecSort(8))
s = Solver()
s.add(b[0] == 21)
s.add(b[1] == 47)
s.check()

m = s.model()
print(m[b])

print(m.eval(b[0]))
print(m.eval(b[1]))

which produces

[1 -> 47, 0 -> 21, else -> 47]
21
47