z3 - 最佳数组操作 API

Question

SMT-LIB 2.0 数组初始化和操作有点麻烦。如以下代码所示，http://rise4fun.com/Z3/kxmrd。

是否有任何优雅的方式来初始化或操作数组，使用 Python/C/C++/.Net API 而不是 SMT-LIB 2.0？

Answer 1

您可以使用常规的 Python 构造for i in range(n)来实现您想要的：

s = Solver()
a = Array('a', IntSort(), IntSort())
xs = [20, 23, 27, 12, 19, 31, 41, 7]

for i in range(len(xs)):
  s.add(Select(a, i) == xs[i])

a1 = Array('a1', IntSort(), IntSort())

s.add(a1 == Store(a, 3,9 ))

print s.check()

m = s.model()
for d in m.decls():
  print "%s = %s" % (d.name(), m[d])

在这里在线运行。

如果你能写类似s.add(a == xs)or的东西就好了s.add(a.startsWith(xs))，但我不知道这是否可能。