z3 - 如何声明一条记录，使其其中一个字段是函数

Question

我对Z3很陌生，很抱歉问了一些愚蠢的问题。

我正在尝试定义一条记录，使其某些字段是函数。我试过这个：

(declare-datatypes (DOM RAN) ((PFun (mk-pfun (dom (DOM) Bool) (law (DOM) RAN)))))

意图是 dom 和 ran 是两个类型为函数的字段（dom 是从 DOM 到 Bool 的函数，而 law 是从 DOM 到 RAN 的函数）。我还尝试将函数类型括在括号中：

(declare-datatypes (DOM RAN) ((PFun (mk-pfun (dom ((DOM) Bool)) (law ((DOM) RAN))))))

bun 这些都不起作用。

我搜索了教程，但没有这方面的例子。

你能帮助我吗？

提前感谢您的回答。

一切顺利，马克西

Answer 1

Z3 基于一阶逻辑。因此，函数不能是数据类型构造函数或其他函数的参数。话虽如此，您可以使用数组“模拟”高阶特征。您可以将数据类型写为

  (declare-datatypes (DOM RAN) ((PFun (mk-pfun (dom (Array DOM Bool)) 
                                               (law (Array DOM RAN))))))

让p是PFun和d一个 排序 的 常数DOM, 然后 你 写(select (dom p) d)获得dom(p)(d), 和(select (law p) d)获得law(p)(d).