是否可以在z3中爲關聯數組建模？

Question

我想知道z3是否支持關聯數組（又名地圖）？如果不是，有沒有簡單的方法來使用當前版本的z3建模這種數據結構？

Answer 1

Z3支持SMT-Lib定義的數組，它也支持數據類型，它們都可以讓你模擬地圖。在這個問題的答案中可以找到使用數據類型的詳細示例：a datatype contains a set in Z3。 Z3 Guide還包含有關如何使用數組以及數據類型的章節。