2

我正在寻找一些在 Z3 python 中使用数组理论的代码示例,但找不到任何代码示例。

请问有人可以提供一些代码示例吗?

谢谢!

4

1 回答 1

3

这是一个显示数组声明和通过索引访问项目的示例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

这是另一个使用数组理论Select的示例http://rise4fun.com/Z3Py/2CAnStore

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

也就是说,StackOverflow 周围有一些数组示例。您可以尝试使用“z3py array”关键字在网站上搜索以获取更多信息。

于 2013-01-09T08:54:22.093 回答