在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類型的變量），以從int到bools獲得一些功能。

不過，我在第二行運行到以下錯誤：

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

是否可以使用函數聲明Z3數據類型的屬性，可能使用不同的語法？

或者它是不允許的東西？後function declaration in z3暗示Z3中不允許使用高階函數，因此可能向數據類型添加函數是不允許的，以防止使用這些數據類型創建高階函數。

Answer 1

您可以使用數組類型來對函數空間進行編碼。

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