0

我创建了 4 种（任务、角色、用户和运行），最后一个接收 2 个参数，然后我为它们中的每一个声明一个乐趣，包括一个用于 Run ，调用 P 接收 2 个参数以创建 Run 的“实例” . 然后我创建了两个数组，一个包含用户角色“关系”（Privs），另一个包含角色任务“关系”（角色）。我使用这两个数组来断言当查看用户 u 时，它是否在 Privs 中具有角色 r，如果在查看角色 r 中的角色时，它是否具有任务 t。到目前为止，我设法在单独的行中做到这一点，如下所示：

(declare-sort Task)
(declare-sort Role)
(declare-sort User)
(declare-sort Run 2)
(define-sort P (User Role) (Run User Role))
(declare-fun t () Task)
(declare-fun r () Role)
(declare-fun u () User)
(declare-const Privs (Array User Role))
(declare-const Roles (Array Role Task))


(assert (= (select Privs u) r))
(assert (= (select Roles r) t))

但是现在我试图取笑它接收一个 Run (User,Role 对) 并且在函数内部断言相同但对于 P 中的所有用户及其所有角色。这可以通过将运行排序变量传递给函数来完成吗？？用于访问其内部的元素（用户、角色）？

4

1 回答 1

0

您对参数类型的使用似乎过分了：您只使用“运行”和实例化为“用户”和“角色”的排序。那么为什么你必须使“运行”参数化。http://smtlib.org详细描述了参数排序和用例的定义，Z3 实现了这种通用格式，因此 Z3 对您的问题没有什么特别之处。

于 2014-06-12T09:34:43.807 回答