在Z3 Python中以函数作为属性的数据类型

Question

我正在为Z3使用Python绑定，并试图创建属性为函数的Z3数据类型。例如，我可能执行以下操作：

Foo = Datatype('Foo')
Foo.declare('foo', [('my_function', Function('f', IntSort(), BoolSort()))])
Foo.create()

这是一种创建带有属性Foo的数据类型my_function的尝试，在这里，我可以调用my_function x (如果x是一个Foo类型的变量)，以便将某些函数从ints输出到bools。

但是，我在第二行遇到了以下错误：

z3types.Z3Exception: Valid list of accessors expected. An accessor is a pair of the form (String, Datatype|Sort)

是否可以将带有函数的Z3数据类型声明为属性，也许可以使用不同的语法？

还是说是不允许的？post function declaration in z3向我建议，在Z3中不允许使用高阶函数，因此可能不允许向数据类型中添加函数，以防止使用这些数据类型创建高阶函数。

Answer 1

可以使用Array类型对函数空间进行编码。

Foo = Datatype('Foo')
Foo.declare('foo', ('my_function', ArraySort(IntSort(), BoolSort())))
print Foo.create()