如何使用循环或其他方法自动调用 z3py 中的 Or() 之类的函数？

Question

我想使用 z3py 来实现一个访问策略分析器，就像 AWS Zelkova 一样。我需要做的第一步是将策略语言编码为逻辑表达式。比如一个控制策略

effect:Allow
principal:students
action: getObject
resource: cs240/Example.pdf,cs240/Answer.pdf

应该转换成

p = students ∧ a = getObject ∧ (r = cs240/Example.pdf ∨ r = cs240/Answer.pdf)

并使用 z3py 我可以将其表示为

s.add(x1 == And(a == StringVal("GetObject"),p == StringVal("tas"),Or(r == StringVal("cs240/Exam.pdf"),r == StringVal("cs240/Answer.pdf"))))

问题来了。当输入一个策略时，解析策略后，我可能会得到一个关于一个键的值数组，我需要使用循环调用 Or() 以获得结果 Or(r[0],r[1] ，...）。我怎样才能做到这一点？我已经尝试过类似的方法，但显然它不起作用。

from z3 import *
Action = ["getObject"]
Principal = ["tas"]
Resource = ["cs240/Exam.pdf","cs240/Answer.pdf"]
a,p,r,x = Bools('a p r x')
a_t,p_t,r_t = Strings('a_t p_t r_t')
s = Solver()
for act in Action:
    a = Or(a,a_t == StringVal(act))
for principal in Principal:
    p = Or(p,p_t == StringVal(principal))
for resource in Resource:
    r = Or(r,r_t == StringVal(resource))
s.add(And(a,p,r))
print(s.check())
print(s.model())

这是我程序的结果：

sat
[a_t = "", p = True, r_t = "", a = True, p_t = "", r = True]

Answer 1

您应该一次构建一个表达式，然后将它们全部添加在一起。伪代码：

foo = False

for i in items:
   foo = Or(foo, i == ...whatever it should equal...)

s.add(foo)

构建表达式时，确保变量从 False 开始。类似于：

from z3 import *
Action = ["getObject"]
Principal = ["tas"]
Resource = ["cs240/Exam.pdf","cs240/Answer.pdf"]
a = False
p = False
r = False
a_t,p_t,r_t = Strings('a_t p_t r_t')
s = Solver()
for act in Action:
    a = Or(a,a_t == StringVal(act))
for principal in Principal:
    p = Or(p,p_t == StringVal(principal))
for resource in Resource:
    r = Or(r,r_t == StringVal(resource))
s.add(And(a,p,r))
print(s.check())
print(s.model())

这会打印：

sat
[r_t = "cs240/Exam.pdf", p_t = "tas", a_t = "getObject"]

我无法判断这是否是正确答案，因为我还没有真正研究过你的约束，但模型似乎与问题更相关。

如何使用循环或其他方法自动调用 z3py 中的 Or() 之类的函数？

How to automatically call a function like Or() in z3py using a loop or other methods?

z3

z3py