z3 - 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是 type 的变量Foo）以获取从整数到布尔值的某些函数。

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

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

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

或者这是不允许的事情？z3 中的 post函数声明向我表明 Z3 中不允许使用高阶函数，因此可能不允许向数据类型添加函数，以防止使用这些数据类型创建高阶函数。

score 2 · Accepted Answer

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

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

1 回答 1