Z3 Python 中以函数为属性的数据类型答案

【问题标题】：Datatypes with functions as attributes in Z3 PythonZ3 Python 中以函数为属性的数据类型
【发布时间】：2016-02-29 19:44:48
【问题描述】：

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

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

这是尝试创建具有属性my_function 的数据类型Foo，我可以在其中调用my_function x（如果x 是Foo 类型的变量）以获取一些从整数到布尔的函数。

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

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

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

或者这是不允许的事情？ function declaration in z3 的帖子向我建议 Z3 中不允许使用高阶函数，因此可能不允许向数据类型添加函数，以防止使用这些数据类型创建高阶函数。

【问题讨论】：

【解决方案1】：

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

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

【讨论】：