我对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 这些都不起作用。
我搜索了教程,但没有这方面的例子。
你能帮助我吗?
提前感谢您的回答。
一切顺利,马克西