如何使用循环或其他方法自动调用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"]

我不知道这是否是一个正确的答案，因为我还没有真正研究过你的约束，但这个模型似乎与这个问题更相关。