Z3Py 中的量词错误

Question

我希望 Z3 检查它是否存在满足我的公式的整数t。我收到以下错误：

Traceback (most recent call last):
  File "D:/z3-4.6.0-x64-win/bin/python/Expl20180725.py", line 18, in <module>
    g = ForAll(t, f1(t) == And(t>=0, t<10, user[t].rights == ["read"] ))
TypeError: list indices must be integers or slices, not ArithRef

代码：

from z3 import *
import random
from random import randrange
class Struct:
def __init__(self, **entries): self.__dict__.update(entries)

user = [Struct() for i in range(10)]
for i in range(10):
    user[i].uid = i
    user[i].rights = random.choice(["create","execute","read"]) 

s=Solver()

f1 = Function('f1', IntSort(), BoolSort())
t = Int('t')
f2 = Exists(t, f1(t))
g = ForAll(t, f1(t) == And(t>=0, t<10, user[t].rights == ["read"] ))
s.add(g)
s.add(f2)
print(s.check())
print(s.model())

Answer 1

您正在混合和匹配 Python 和 Z3 表达式，虽然这是 Z3py 的重点，但这绝对不意味着您可以任意混合/匹配它们。一般来说，您应该将所有“具体”部分保留在 Python 中，并将符号部分归入“z3”；仔细协调两者之间的相互作用。在您的特定情况下，您正在使用符号 z3 整数 (t) 访问 Python 列表 (您的 user)，这当然是不允许的。您必须使用 Z3 符号 Array 才能使用符号索引进行访问。

另一个问题是使用字符串（"create"/"read" 等）并期望它们在符号世界中具有意义。这也不是 z3py 的用途。如果您希望它们在符号世界中具有某种意义，则必须明确地对它们进行建模。

我强烈建议您阅读http://ericpony.github.io/z3py-tutorial/guide-examples.htm，这是对 z3py 的精彩介绍，包括许多高级功能。

说了这么多，我倾向于将您的示例编码如下：

from z3 import *
import random

Right, (create, execute, read) = EnumSort('Right', ('create', 'execute', 'read'))

users = Array('Users', IntSort(), Right)

for i in range(10):
    users = Store(users, i, random.choice([create, execute, read]))

s = Solver()
t = Int('t')
s.add(t >= 0)
s.add(t < 10)
s.add(users[t] == read)

r = s.check()
if r == sat:
   print s.model()[t]
else:
   print r

注意符号域中的枚举类型Right 是如何用于模拟您的“权限”的。

当我多次运行这个程序时，我得到：

$ python a.py
5
$ python a.py
9
$ python a.py
unsat
$ python a.py
6

注意unsat 是如何产生的，如果碰巧“随机”初始化没有让任何用户拥有read 权限。