2

我对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 这些都不起作用。

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

你能帮助我吗?

提前感谢您的回答。

一切顺利,马克西

4

1 回答 1

1

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

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

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

于 2011-09-19T14:22:53.910 回答