z3 - 如何使用 z3 BitVec 或 Int 作为数组索引？

Question

我想使用 Int 向量作为数组索引。

Python。

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

所以 x 应该是 2..

我该怎么做？

Answer 1

这是一种方法:

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!"

这打印:

$ python a.py
[x = 2]