如何在z3py中使用Z3-LIB中的（_ map op）

Question

Z3-LIB支持擴展陣列理論的運算符，如（_ map op）。但是，我們如何在Z3py中使用這個運算符？

Answer 1

您可以使用

b = Map(f, a1, a2) 

與A1，A2和B數組變量。第一個參數f必須是一個函數聲明，所以使用例如z3.And不適用於我。相反，我引入了自定義函數f和另一個公理，使其等價於And。但是，也許你不需要預定義的。