sorting - 在 Z3 中使用排序

Question

有人可以帮助了解如何在 Z3 中正确使用“for all”吗？我一直在查看文档，但找不到信息。我想做的是

在“foo”中，我需要在 Z3 中说一些相当于

“让（u，r）在{（断言（（u，r）在用户中）（断言（r，t）在角色中）}中可运行（t）”

我不知道如何将 runnable 中的第一个元素断言在用户中，然后将第二个元素断言在角色中。

---

(declare-sort Task) (declare-sort Role) (declare-sort User) (declare-fun runnable (Task) (User Role)) (declare-fun perm (Role Task) Bool) (declare-fun users (User Role) ) 布尔)

(assert (forall (t Task)) (foo))

(check-sat) (get-model)

---

Answer 1

这个例子不是格式良好的 SMT2，函数不能返回多个对象。Z3 指南中有关如何使用数据类型和量词的示例。