具有工作流可满足性的 z3答案

【问题标题】：z3 with workflow satisfiability具有工作流可满足性的 z3
【发布时间】：2014-06-11 18:50:55
【问题描述】：

我是使用 Z3 的新手，经过大量教程阅读了几乎所有相关问题后，我仍然对如何“编码”Z3 的问题有些疑问。有人可以帮帮我吗？.. 我想做的是用 Z3 对可满足性问题进行编码。我有两个表示角色（角色-任务关系）和特权（用户-角色关系）的数组。我还有一个数据类型，它是一个用户角色对，表示任务的“属性”。

(declare-datatypes (User Role) ((Pair (mk-pair (first User) (second Role)))))
(declare-const Privs (Array User Role))
(declare-const Roles (Array Role (Pair User Role)))

然后我试图断言，对于任何任务（对于所有），在 Privs 中都有一个元素包含用户角色关系，并且在 Roles 和元素中包含角色-“任务”（用户角色对），例如这个。

(assert (forall ((l (Pair User Role)))
        (and (= (select Privs (first oneTask)) (second oneTask))  
        (= (select Roles (second oneTask)) oneTask))))

直到那里我得到一个星期六的答案和一个模型（因为我使用的是未解释的排序，所以没有解释）。

但这是我的怀疑开始的地方......

1) 下一步是询问当有两个带有任务列表（用户角色对）的工作流时，我是否可以为列表中的所有任务声明相同的内容。我尝试创建一个新的 const，它是这样的任务列表：

(declare-const Workflow (List (Pair User Role)))

在 Z3 中是否有任何方法可以对列表的所有元素（在我的情况下为工作流程）指定断言？？

2) 一个人如何指定限制，例如对用户或分配的集合，以及如何在执行时间上表达限制，例如.. 一组任务的执行不能超过 n 秒？ ..

3) 有什么方法可以在使用解释型任务时获得解释型模型，让我们说类似...当 PRIVS = (U1, R1) , (U2,R2) and Role= (R1,T1) and wf =T1(U1,R1)

有人可以帮我从Z3的角度解决问题吗？？？？？请！！

【问题讨论】：

我只需要一个关于如何映射问题并表达它的想法。也许类似的东西和例子会对我有很大帮助。！

标签： z3

【解决方案1】：

Z3 支持标准的一阶量化。如果您想量化容器对象（列表）的元素数量，您将不得不编码访问容器对象。因此，对于您的列表示例，在对所有元素强制执行属性时，您需要定义访问列表元素的辅助关系。例如，您可以定义一个在 Nil 上为真的递归关系，如果感兴趣的谓词在列表的头部保持并且关系递归地在列表的尾部保持，则对于非空列表成立。当然，问题是这样的编码很快会导致 Z3 出现分歧的问题，主要是在可满足的情况下。数组当然是不同的：您可以通过对域进行量化并选择数组中的每个索引来直接访问数组范围内的每个元素。
我不明白您所说的“用户分配”是什么意思。您可以通过设置选项来指定时间限制：“(set-option :timeout 1000)”设置一秒超时。
我不明白你的最后一个问题。抱歉。

【讨论】：