在Z3 Python中以函数作为属性的数据类型
提问于 2016-02-29 11:44:48
我正在为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中不允许使用高阶函数，因此可能不允许向数据类型中添加函数，以防止使用这些数据类型创建高阶函数。
回答 1
Stack Overflow用户
回答已采纳
发布于 2016-02-29 12:36:13
可以使用Array类型对函数空间进行编码。
Foo = Datatype('Foo')
Foo.declare('foo', ('my_function', ArraySort(IntSort(), BoolSort())))
print Foo.create()页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/35708244
复制相关文章
腾讯云开发者
