Z3 可以处理包含由声明排序/定义排序引入的排序的数据类型吗？
我试图定义一个包含由声明排序或定义排序引入的排序的数据类型。 但以下尝试会导致错误。
(declare-sort A)
(define-sort B () Int)
(declare-datatypes ((listA (nilA) (consA (hdA A) (tlA listA))))) ;=> unknown sort 'A'
(declare-datatypes ((listB (nilB) (consB (hdB B) (tlB listB))))) ;=> unknown sort 'B'
有办法做到这一点吗？
提前致谢。
I'm trying to define a datatype that contains sorts introduced by declare-sort or define-sort.
But the following attempt results in errors.
(declare-sort A)
(define-sort B () Int)
(declare-datatypes ((listA (nilA) (consA (hdA A) (tlA listA))))) ;=> unknown sort 'A'
(declare-datatypes ((listB (nilB) (consB (hdB B) (tlB listB))))) ;=> unknown sort 'B'
Is there a way to do that?
Thanks in advance.
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
是的，可以。顺便说一句，您似乎使用的是旧版本的 Z3。
您应该尝试最新版本。
Z3 3.x 支持参数类型。因此，声明数据类型的语法发生了一些变化。
现在，您必须编写：
在新语法中，您可以指定类型参数。由于 listA 不是参数化的，因此您只需提供类型参数的空列表
()。有关 Z3 中数据类型的更多信息，请参阅 Z3 指南。
使用参数类型，您还可以将
listA和listB编码为：Yes, it can. BTW, it seems you are using an old version of Z3.
You should try the latest version.
Z3 3.x supports parametric types. So, the syntax for declaring datatypes changed a little bit.
Now, you have to write:
In the new syntax, you can specify type parameters. Since listA is not parametric, you just provided the empty list
()of type parameters.For more information about datatypes in Z3, consult the Z3 guide.
Using parametric types, you can also encode
listAandlistBas: