是否可以在 z3 中对关联数组进行建模？

Question

我想知道 z3 是否支持关联数组（又名地图）？如果没有，是否有一种简单的方法可以使用当前版本的 z3 对此类数据结构进行建模？

Answer 1

Z3 支持SMT-Lib 定义的数组，它还支持数据类型，它们中的任何一个都应该允许您对地图进行建模。在这个问题的答案中可以找到使用数据类型的详细示例：a datatype contains a set in Z3。 Z3 Guide 还包含有关如何使用数组和数据类型的部分。