在Z3中使用排序

Question

有人可以幫助知道如何在Z3中正確使用「for all」，我一直在尋找文檔，但我無法找到信息。我所試圖做的是

「FOO」 我需要在Z3的東西說的

相當於內「讓{（斷言（（U，R（U，R）是可運行（T） ）在用戶中）（assert（r，t）在角色中））}「

我不知道的是如何獲取runnable中的第一個元素來斷言是在用戶中，然後是第二個元素斷言這是角色。

---

（聲明排序任務） （聲明-樣的角色） （聲明排序用戶） （聲明樂趣可運行（任務）（用戶角色）） （聲明樂趣燙髮（角色任務）布爾） （聲明樂趣的用戶（用戶角色）布爾）

（斷言（FORALL（T任務））（富））

（檢查-SAT） （獲取模型）

---

Answer 1

這個例子不是良構的SMT2，函數不能返回多個對象。有關如何使用數據類型以及量詞的示例，請參見Z3 Guide。