Z3Python: example of array?

Question

i am looking for some code examples using theory of array in Z3 python, but cannot find any.

please could somebody provide some code examples?

thanks!

Answer 1

Here is an example showing array declarations and accessing items by indices http://rise4fun.com/Z3Py/7jAj:

x = Int('x')
a = Array('a', IntSort(), BoolSort())
b = Array('b', IntSort(), BoolSort())
c = Array('c', BoolSort(), BoolSort())

e = ForAll(x, Or(Not(a[x]), c[b[x]]))
print e

solver = Solver()
solver.add(e)
c = solver.check()
print c

Here is another example using Select and Store on array theory http://rise4fun.com/Z3Py/2CAn:

x = Int('x')
y = Int('y')
a = Array('a', IntSort(), IntSort())

s = Solver()
s.add(Select(a, x) == x, Store(a, x, y) == a)
print s.check()
print s.model()

That said, there are a few array examples floating around StackOverflow. You can try to search on the site using "z3py array" keyword for more information.