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

问题描述

我想使用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,r))
print(s.check())
print(s.model())

那是我程序的结果：

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

解决方法

您应该一次构建一个表达式并将其全部添加在一起。伪代码：

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"]

由于我尚未真正研究您的约束条件，因此我无法确定这是否是正确的答案，但是该模型似乎与问题更相关。

z3 z3py