0

我想知道是否可以在 Z3Py 中创建依赖于另一种代数数据类型的代数数据类型。

例如，假设我定义了自己的 Bool 数据类型，并且我想自己定义一个 Bool 列表：

from z3 import *
Bool = Datatype('Bool')
Bool.declare('TRUE')
Bool.declare('FALSE')
Bool = Bool.create()
TRUE = Bool.TRUE
FALSE = Bool.FALSE

这工作正常，然后：

BoolList = Datatype('BoolList')
BoolList.declare('bNIL')
BoolList.declare('bCONS', ('hd', Bool()), ('tail', BoolList))
BoolList = BoolList.create()

这失败并显示以下消息：

>>> BoolList.declare('bCONS', ('hd', Bool()), ('tail', BoolList))
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
AttributeError: DatatypeSortRef instance has no __call__ method

原因是使用 Bool() 作为对早期定义的数据类型的引用。使用 Z3 布尔排序就像一个魅力：

BoolList = Datatype('BoolList')
BoolList.declare('bNIL')
BoolList.declare('bCONS', ('hd', BoolSort()), ('tail', BoolList))

依赖于另一个代数数据类型的代数数据类型的定义是不可能的，还是我需要通过 s.th。除了 Bool() 吗？

提前致谢！卡斯滕

4

1 回答 1

1

好吧，事实证明我在不应该使用括号的地方使用了括号 - 对自定义数据类型“Bool”的引用不需要调用：

BoolList.declare('bCONS', ('hd', Bool), ('tail', BoolList))

工作得很好:)

于 2014-05-12T11:57:46.733 回答