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

【问题标题】：How to use z3 BitVec or Int as an array index?如何使用 z3 BitVec 或 Int 作为数组索引？
【发布时间】：2018-03-25 09:21:22
【问题描述】：

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

蟒蛇。

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

所以 x 应该是 2..

我该怎么做？

【问题讨论】：

标签： z3 symbolic-math z3py

【解决方案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]

【讨论】：

为什么要添加x >= 0 和x < len(array) 约束。我以为Select 无论如何只能从那个范围中选择？
@stklik 这不是真的。 Select 将在整个域上运行，即所有整数值。 Z3 数组没有下限/上限的概念。通过消除这些限制并观察 Z3 的作用，您可以很容易地看到这一点。

【解决方案2】：

无法使用 Z3 ArithRef 变量访问整数数组元素。我想，指定的问题是通过 Z3 求解器在整数数组（索引）中查找元素。

另一种可能的方式可能是：

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())

【讨论】：