是否可以在z3中为关联数组建模？

Question

我想知道z3是否支持关联数组（又名地图）？如果不是，有没有简单的方法来使用当前版本的z3建模这种数据结构？

Answer 1

Z3支持SMT-Lib定义的数组，它也支持数据类型，它们都可以让你模拟地图。在这个问题的答案中可以找到使用数据类型的详细示例：a datatype contains a set in Z3。 Z3 Guide还包含有关如何使用数组以及数据类型的章节。